[Why3-club] constant in code

Andrei Paskevich andrei.paskevich at lri.fr
Tue Mar 26 11:19:23 CET 2019


On Mon, 25 Mar 2019 at 19:15, Jean-Jacques Levy <jean-jacques.levy at inria.fr>
wrote:

> Dear Andrei,
>
> many thanks for your quick answer. I finally succeeded in modifying my
> files to release 1.2.0 … BUT I now have:
>
> - many xxx.contents in my text to translate an xxx Appset into a xxx Set
> :-(
> - to define a virtual ‘selements’ function to have a code version of the
> ‘elements’ function of the library :-(
> _ qualifying the Appmap and Appset modules to avoid clashes with the
> .contents qualifier, the choose, remove functions on sets
>
> There must be ways for simplifications, but I have to understand what are
> the actual meanings of:
>
> - use
>

Include the "used" module into the logical context of your development. A
rough equivalent of "Require" in Coq. Two consecutive "use A" are the same
as a single "use A". Additional qualifiers "import", "export" and "as
<Name>" change the handling of namespaces.


> - clone
>

Instantiate the "cloned" module (each name declared/defined in the module
is either instantiated explicitly by the user or given a fresh name) and
add it to the logical context. A rough equivalent of applying a functor.
Two consecutive "clone A" would add two disctinct renamed copies of A
(actually the second clone will fail because of name conflicts). Additional
qualifiers "import", "export" and "as <Name>" change the handling of
namespaces.


> - clone import
>

"import" means that the names in the cloned module can be used in the
current scope without an explicit qualifier. After "clone import A", both
"A.x" and "x" can be used. In the latest versions of Why3, "import" is used
by default, so you rarely need to write it explicitly.


> Is ‘export' still used ?
>

Yes, "export" means that a new scope (namespace) is not created: all names
are added directly to the current namespace. After "clone export A", you
cannot write "A.x", because "x" is put in the current namespace.

Best,
Andrei
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190326/a843eb26/attachment-0001.html>


More information about the Why3-club mailing list