Stream: Coq users

Topic: directory structure for a PL project


view this post on Zulip Cong Ma (Feb 09 2023 at 20:20):

I'm trying to figure out the best way to organize my Coq project, which formalizes a source to IR translation. Currently, the directories look like this

/Source
   Syntax.v
   Typing.v
/IR
   Syntax.v
   Typing.v
source2IR.v

In source2IR.v, I combine the files into modules SC and IR so that they are in different namespaces, like below

Require Import Source.Syntax Source.Typing IR.Syntax IR.Typing.

Module SC := Source.Syntax <+ Source.Typing.
Module IR := IR.Syntax <+ IR.Typing.

Definition translation: SC.term -> IR.term -> Prop.

Am I doing it right?

Edit:
The problem with my approach is that when I do induction on the proposition from the newly created module, Coq introduces variables whose types are from the original file, but I don't want that. For example, I did a induction H0between the two images. Notice that Coq introduces τ0: Syntax.ty which replaces τ: SC.ty, but I want to keep τ: SC.ty.

FYI the constructor for SC.ok_term is below

| ok_term_val : forall E H v τ,
  ok_val E H v τ ->
  ok_term E H (trm_val v) (τ, nil)

image.png
image.png

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 20:59):

That's a bug with Include (and the <+ syntax), and that's unlikely to be fixed soon. Sometimes it works to turn the Module you're including into a Module Type, but that's probably a hassle here. I'd rather recommend a different namespacing tech; coq-elpi + NES is a promising option, and I use it a lot

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 21:04):

However, NES does something else. It does not create an alias with a different type; it rather lets you put the original definitions in the SC and IR "namespaces" directly.

view this post on Zulip Gaëtan Gilbert (Feb 09 2023 at 21:06):

how is it a bug?

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 21:06):

Inside Source and IR, you can respectively use Import SC (or rather, NES.Open SC) and ditto with IR.

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 21:08):

Gaetan: let me change that to "infelicity"; I'm not interested in arguing the difference.

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 21:11):

More precisely: let's pretend Include implements the spec correctly (which it doesn't, as PMP points out). It's still unclear whether that spec is useful to accomplish some actual goal.

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 21:14):

I usually run into slightly different problems, but "avoid Including concrete modules, and avoid Include here at all" remains IMHO the simplest advice.

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 21:15):

("Follow Coq's numeric hierarchy" aka "only use Include on Module Type" seems the second-best option to use Include, and I've done it and can explain it, but it's far from a clear win).

view this post on Zulip Cong Ma (Feb 09 2023 at 21:51):

Thanks Paolo. I'd like to learn about using Module Type to achieve my goal. If I simply replace the keyword Module with Module Type, I can't refer to anything inside.

Can you give a short example?

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 21:54):

I can try later, but the solution involves learning more about the Coq module system and writing ML-style functors

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 21:57):

for instance:

Module Type SC_Syntax.
(* current contents of Source/Syntax.v *)
End Syntax.

Module Type SC_Typing (Import S : SC_Syntax).
(* current contents of Source/Typing.v *)
End Typing (S : Syntax).

Module SC.
  Include SC_Syntax <+ SC_Typing.
End SC.

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 21:58):

here, SC is usable normally, but anybody wanting to use SC_Syntax must be written like SC_Typing.

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 22:00):

It can get worse if your hierarchy grows:

Module Type SC_Typing_Correctness (Import S : SC_Syntax) (Import T : SC_Typing S).
...
End SC_Typing_Correctness.

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 22:01):

if I added enough examples, the Module Type SC_Foo ... line would have a quadratic size. There are variants with subtle tradeoffs.

view this post on Zulip Paolo Giarrusso (Feb 09 2023 at 22:04):

I wouldn't recommend such a setup to most people, and it's definitely overkill for the original question. That's why I recommend https://github.com/LPCIC/coq-elpi/blob/master/apps/NES/examples/usage_NES.v instead...

view this post on Zulip Cong Ma (Feb 09 2023 at 22:35):

Thanks. NES looks very promising. Let me try it out.


Last updated: Jun 20 2024 at 13:02 UTC