The Coq mailing list

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

Hi Milad,

Le 06/06/2018 à 07:50, Milad Ketabii a écrit :
> Hi there!
>
> I have a problem, for which a solution already is there. However, I am 
> looking for a better way of accomplishing the task.
>
> Here, I will first explain the problem itself, as much simply as 
> possible. Then I mention the crazy solution which I have. But I hope 
> someone would kindly hint at a superior approach.
>
> *The problem and a crazy solution:*
>
> I have a formalisation which I intend to break into a base file and some 
> modules, each of which calls this base in.
>
> The base formalisation has variables. These variables are used inside 
> each module as well. We finally would extract executable program into 
> Haskell.
>
> The base is constituted of some sections. To make the variables in the 
> base file available to the modules (without instantiating them), I have 
> made the out-most part of the base file as a module, rather than a 
> section. This prevents errors that I would get by trying to compile the 
> modules.

I do not fully understand your current solution: is this "out-most" part 
a module in parameter of each module ? (Now, are your modules actually 
functors ?)

> However, the hassle is that I need to put the name of the base module in 
> front of every variable, definition, and function which are celled in 
> the modules.

Whatever module "Base" is: a parameter or an actual implementation, you 
only need to write "Import Base." in each module that uses "Base" in 
order to solve your problem.

Regards,

Sylvain.