The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

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.

======================

File A:
    Section A.
    Variable param: int.
    Theorem A1: ... param ...
    End A.

File B:
    Require A.
    Section B
    Variable param: int.
    Local A1 := (A1 param).
    Theorem B1: ... param ...
    End B.

File C:

    Require A.
    Section C.
    Variable param: int.
    Local A1 := (A1 param).
    Theorem C1: ... param ...
    End C.

File D:
    Require A B C.
    Section D.
    Variable param: int.
    Local A1 := (A1 param).
    Local C1 := (B1 param).
    Local B1 := (C1 param).
    Local C1 := (D1 param).
    Theorem D1: ... param ...
    End D.

=================

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.
    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. 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).

 second I've lost my hierarchical structure.


Is there a better way to use module to do what I want?

--
Laurent Thery