The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

It seems to me that the variant of Madhukars solution in attachment has 
less syntactic overhead: in the chain of functors, we only handle 
functors of one argument.

Hope this helps,

Regards,

Sylvain.



Le 05/11/2021 à 10:01, Chris Dams a écrit :
> Dear all,
>
> In case anyone is interested in what I did after asking my question about
> modules in this mailing list, I will describe the final solution that
> I arrived at.
> I tried both the solutions by Guillaume and by Madhukar and they both work
> but also have some disadvantages. In the end I ended up going with my
> own solution (Example-2 in the original post) but basically turning the chain
> of modules that import each other into an implementation detail. I renamed
> some of the files involved adding '_internal' to their name in order to 
> indicate
> that they are not meant to be used separately and added a facade file
> that is just importing the whole chain but with a generic name suggesting
> that it is the file that one is supposed to import as opposed to the other
> internal ones. In future I could imagine putting the 'internal' files in a
> subdirectory to further indicate their internal nature. Now my whole project
> is compiling again, so I am happy :-).
>
> The problem with Guillaumes  solution is that while it works I really have to
> pull out a lot of definitions out of my modules. It is not one
> inductive definition
> that needs to be pulled out of Module1 as in my example. It is 9 of them.
> And then more inductive definitions from the other modules. Also, the 
> inductive
> definitions in subsequent modules do not just refer to inductive definitions 
> in
> the previous modules but also to ordinary definitions, which, as a result 
> would
> also have to be pulled out of the module. At this point it gets quite
> impractical.
> Also, some of these inductive definitions are Records and then I have to not
> just import the name of the Record but also the name of its constructor and
> the names of its fields into the module and give all of these different names.
> I prefixed the 'global' ones with a 'g' which is not very nice either.
>
> The problem with Madhukars solution is that while it also works it has quite
> a bit of syntactic overhead that is quite tricky that is not just in
> the internal
> files but also in the code that uses it. Because of this I decided in the end 
> to
> put the modules behind the facade that I described above so code using this
> can just Import one module and be done with it.
>
> After looking into all of this I cannot really help feeling that the issue 
> that
> importing a module with an inductive definition copies the inductive 
> definition
> such there there are then two incompatible inductive types really should
> be considered a bug in coq. I understand that the current way is the easiest
> way to implement modules and I really do not know whether improving the
> situation is possible but it just seems strange and highly impractical....
>
> Kind Regards,
> Chris
Module Type Thing.
Parameter S: Set.
End Thing.

Module Type Module1.
Declare Module T: Thing.
Export T.
Inductive flups: Set := flups1 | flups2.
End Module1.

Module Type Module2.
Declare Module M1: Module1.
Export M1.
End Module2.


Module SpecificModule1 (ST: Thing) <: Module1 with Module T:=ST.
Include Module1 with Module T:=ST.
End SpecificModule1.

Module SpecificModule2 (SM1: Module1) <: Module2 with Module M1:=SM1.
Include Module2 with Module M1:=SM1.
End SpecificModule2.


Module SpecificThing <: Thing.
Definition S: Set := nat.
End SpecificThing.

Module Import SM1 := SpecificModule1 SpecificThing.
Module Import SM2 := SpecificModule2 SM1.

Print SpecificModule2.

Check SM1.flups.
Check SM2.M1.flups.

Parameter p: SM1.flups.
Goal SM2.M1.flups.
exact p.
Qed.