coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thery Laurent <thery AT ns.di.univaq.it>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] A little question about modules
- Date: Wed, 4 Feb 2004 10:52:33 +0100 (CET)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] A little question about modules, Thery Laurent
- [Coq-Club] Announce: Cyp tool, Thery Laurent
- Re: [Coq-Club] A little question about modules,
Jacek Chrzaszcz
- Re: [Coq-Club] A little question about modules, Thery Laurent
Archive powered by MhonArc 2.6.16.