The Coq mailing list

[Jacek Chrzaszcz <chrzaszc AT mimuw.edu.pl>]

On Wed, Feb 04, 2004 at 10:52:33AM +0100, Thery Laurent wrote:
> 
> Hi,
> 
> 
> I'm trying to use the module system to see how I could simplify some of my
> developments. 
> 
> The typical case I encounter is a hierarchy of files that share common
> parameters (or at least a common subset).
> 
> Here is a toy example.
> 
(...)
> =================
> 
> I thought I could use functor to get rid of these locals.
> 
> So my first attempt was to functorize everything, starting
> with a type for my parameters:
> 
> Module Type PARAM.
> 
> Parameter param: int
> 
> End PARAM.
> 
> ======================
> 
> File A:
>     Module FA (X: PARAM).
>     Export A.

What do you export here? The whole module-file A? It is impossible since its
existence starts when you finish the file. Or you mean Export X?

>     Theorem A1: ... param ...
>     End FA.
> 
> File B:
>     Require A.
>     Module FB (X: PARAM).
>     Module F1 := (FA X).
>     Export F1.
>     Theorem B1: ... param ...
>     End FB.
> 
> File C:
> 
>     Require A.
>     Module FC (X: PARAM).
>     Module F1 := (FA X).
>     Export F1.
>     Theorem C1: ... param ...
>     End FC.
> 
> 
> File D:
>     Require B C.
>     Module FC (X: PARAM).
>     Module F1 := (FB X).
>     Export F1.
>     Module F2 := (FC X).
>     Export F2.
>     Theorem D1: ... param ...
>     End FC.
> 
> 
> =================
> 
> But this does not work because F1 and F2 contains two different 
> versions of A. 

No! They do not "contain" A at all! Well, not more then B or C. If there is
something wrong, it is probably a bug.

> So my current solution is to linearize my hierarchy:
> 
> ======================
> 
> File A:
>     Module FA (X: PARAM).
>     Export A.
>     Theorem A1: ... param ...
>     End FA.
> 
> File B:
>     Require A.
>     Module FB (X: PARAM).
>     Module F1 := (FA X).
>     Export F1.
>     Theorem B1: ... param ...
>     End FB.
> 
> File C:
> 
>     Require B.
>     Module FC (X: PARAM).
>     Module F1 := (FB X).
>     Export F1.
>     Theorem C1: ... param ...
>     End FC.
> 
> 
> File D:
>     Require C.
>     Module FC (X: PARAM).
>     Module F1 := (FC X).
>     Export F1.
>     Theorem D1: ... param ...
>     End FC.
> 
> 
> =================
> 
> This works quite nicely, there are only two small problems:
> 
>  first there is this module F1 that is  hanging around. The more files
>   I add the deeper A1 (F1.F1.F1.....A1) is. What I would like in fact
>   is to avoid creating the module and just write  Export (FC X).
> 
This would require serious modifications of Coq... introduction of global
names of the form (FC X).A1, completely different approach to implicits,
morphisms, hints etc allowing for module-level patterns, like (FC ?).A1.hint
for example...

>  second I've lost my hierarchical structure.
> 
> 
> Is there a better way to use module to do what I want?
> 

Your first approach is definitely better :)

Jacek

> --
> Laurent Thery
> 
> 
> 
> 
> 
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--