mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-08-16 09:20:24 +03:00
Add some documentation about the module system
This commit is contained in:
Iavor Diatchki
parent
87e51efbe6
commit
9f8d711638
@ -94,6 +94,8 @@ not be used for programmer defined names:
|
||||
private
|
||||
include
|
||||
module
|
||||
submodule
|
||||
interface
|
||||
newtype
|
||||
pragma
|
||||
property
|
||||
@ -117,11 +119,10 @@ not be used for programmer defined names:
|
||||
.. code-block:: none
|
||||
:caption: Keywords
|
||||
|
||||
else include property let infixl parameter
|
||||
extern module then import infixr constraint
|
||||
if newtype type as infix down
|
||||
private pragma where hiding primitive by
|
||||
|
||||
as extern include interface parameter property where
|
||||
by hiding infix let pragma submodule else
|
||||
constraint if infixl module primitive then
|
||||
down import infixr newtype private type
|
||||
|
||||
The following table contains Cryptol's operators and their
|
||||
associativity with lowest precedence operators first, and highest
|
||||
|
||||
@ -196,7 +196,7 @@ It is good practice to place such declarations in *private blocks*:
|
||||
|
||||
The private block only needs to be indented if it might be followed by
|
||||
additional public declarations. If all remaining declarations are to be
|
||||
private then no additional indentation is needed as the `private` block will
|
||||
private then no additional indentation is needed as the ``private`` block will
|
||||
extend to the end of the module.
|
||||
|
||||
.. code-block:: cryptol
|
||||
@ -238,139 +238,373 @@ is equivalent to the previous one:
|
||||
helper2 = 3
|
||||
|
||||
|
||||
Nested Modules
|
||||
--------------
|
||||
|
||||
Module may be declared withing other modules, using the ``submodule`` keword.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Declaring a nested module called N
|
||||
|
||||
module M where
|
||||
|
||||
x = 0x02
|
||||
|
||||
submodule N where
|
||||
y = x + 2
|
||||
|
||||
Submodules may refer to names in their enclosing scope.
|
||||
Declarations in a sub-module will shadow names in the outer scope.
|
||||
|
||||
Declarations in a submdule may be imported with ``import submodule``,
|
||||
which works just like an ordinary import except that ``X`` refers
|
||||
to the name of a submodule.
|
||||
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Using declarations from a submodule.
|
||||
|
||||
module M where
|
||||
|
||||
x = 0x02
|
||||
|
||||
submodule N where
|
||||
y = x + 2
|
||||
|
||||
import submodule N as P
|
||||
|
||||
z = 2 * P::y
|
||||
|
||||
Note that recursive definitions across modules are not allowed.
|
||||
So, in the previous example, it would be an error if ``y`` was
|
||||
to try to use ``z`` in its definition.
|
||||
|
||||
|
||||
|
||||
Implicit Imports
|
||||
~~~~~~~~~~~~~~~~
|
||||
|
||||
For convenience, we add an implicit qualified submodule import for
|
||||
each locally defined submodules.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Making use of the implicit import for a submodule.
|
||||
|
||||
module M where
|
||||
|
||||
x = 0x02
|
||||
|
||||
submodule N where
|
||||
y = x + 2
|
||||
|
||||
z = 2 * N::y
|
||||
|
||||
``N::y`` works in the previous example because Cryptol added
|
||||
an implicit import ``import submoulde N as N``.
|
||||
|
||||
|
||||
Managing Module Names
|
||||
~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
The names of nested modules are managed by the module system just
|
||||
like the name of any other declaration in Cryptol. Thus, nested
|
||||
modules may declared in the public or private sections of their
|
||||
containing module, and need to be imported before they can be used.
|
||||
Thus, to use a submodule defined in top-level module ``A`` into
|
||||
another top-level module ``B`` requires two steps:
|
||||
|
||||
1. First we need to import ``A`` to bring the name of the submodule in scope
|
||||
2. Then we need to import the submodule to bring the names defined in it in scope.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Using a nested module from a different top-level module.
|
||||
|
||||
module A where
|
||||
|
||||
x = 0x02
|
||||
|
||||
submodule N where
|
||||
y = x + 2
|
||||
|
||||
module B where
|
||||
import A // Brings `N` in scope
|
||||
import submodule N // Brings `y` in scope
|
||||
z = 2 * y
|
||||
|
||||
|
||||
Parameterized Modules
|
||||
---------------------
|
||||
|
||||
.. warning::
|
||||
This section documents the current design, but we are in the process of
|
||||
redesigning some aspects of the parameterized modules mechanism.
|
||||
|
||||
Interface Modules
|
||||
~~~~~~~~~~~~~~~~~
|
||||
|
||||
An *interface module* describes the content of a module
|
||||
without providing a concrete implementation.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: An interface module.
|
||||
|
||||
interface module I where
|
||||
|
||||
type n : # // `n` is a numeric type
|
||||
|
||||
type constraint (fin n, n >= 1)
|
||||
// Assumptions about the declared numeric type
|
||||
|
||||
x : [n] // A declarations of a constant
|
||||
|
||||
Like other modules, interfaces modules may be nested in
|
||||
other modules:
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: A nested interface module
|
||||
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : # // `n` is a numeric type parameter
|
||||
interface submodule I where
|
||||
|
||||
type n : # // `n` is a numeric type
|
||||
|
||||
type constraint (fin n, n >= 1)
|
||||
// Assumptions about the declared numeric type
|
||||
|
||||
x : [n] // A declarations of a constant
|
||||
|
||||
|
||||
Importing an Interface Module
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
A module may be parameterized by importing an interface,
|
||||
instead of a concrete module
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: A parameterized module
|
||||
|
||||
// The interface desribes the parmaeters
|
||||
interface module I where
|
||||
type n : #
|
||||
type constraint (fin n, n >= 1)
|
||||
// Assumptions about the parameter
|
||||
|
||||
x : [n] // A value parameter
|
||||
|
||||
// This definition uses the parameters.
|
||||
f : [n]
|
||||
f = 1 + x
|
||||
x : [n]
|
||||
|
||||
|
||||
Named Module Instantiations
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
// This module is parameterized
|
||||
module F where
|
||||
import interface I
|
||||
|
||||
One way to use a parameterized module is through a named instantiation:
|
||||
y : [n]
|
||||
y = x + 1
|
||||
|
||||
To import a nested interface use ``import interface sumbodule I``
|
||||
and make sure that ``I`` is in scope.
|
||||
|
||||
It is also possible to import multiple interface modules,
|
||||
or the same interface module more than once. Each import
|
||||
of an interface module maybe be linked to a different concrete
|
||||
module, as described in :ref:`instantiating_modules`.
|
||||
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Multiple interface parameters
|
||||
|
||||
interface module I where
|
||||
type n : #
|
||||
type constraint (fin n, n >= 1)
|
||||
x : [n]
|
||||
|
||||
|
||||
module F where
|
||||
import interface I as I
|
||||
import interface I as J
|
||||
|
||||
y : [I::n]
|
||||
y = I::x + 1
|
||||
|
||||
z : [J::n]
|
||||
z = J::x + 1
|
||||
|
||||
|
||||
Interface Constraints
|
||||
~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
When working with multiple interfaces, it is to useful
|
||||
to be able to impose additional constraints on the
|
||||
types imported from the interface.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Adding constraints to interface parameters
|
||||
|
||||
interface module I where
|
||||
type n : #
|
||||
type constraint (fin n, n >= 1)
|
||||
x : [n]
|
||||
|
||||
|
||||
module F where
|
||||
import interface I as I
|
||||
import interface I as J
|
||||
|
||||
interface constraint (I::n == J::n)
|
||||
|
||||
y : [I::n]
|
||||
y = I::x + J::x
|
||||
|
||||
In this example we impose the constraint that ``n``
|
||||
(the width of ``x``) in both interfaces must be the
|
||||
same. Note that, of course, the two instantiations
|
||||
may provide different values for ``x``.
|
||||
|
||||
|
||||
.. _instantiating_modules:
|
||||
|
||||
|
||||
Instantiating a Parameterized Module
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
To use a parameterized module we need to provide concrete
|
||||
implementations for the interfaces that it uses, and provide
|
||||
a name for the resulting module. This is done as follows:
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Instantiating a parameterized module using a single interface.
|
||||
|
||||
interface module I where
|
||||
type n : #
|
||||
type constraint (fin n, n >= 1)
|
||||
x : [n]
|
||||
|
||||
module F where
|
||||
import interface I
|
||||
|
||||
y : [n]
|
||||
y = x + 1
|
||||
|
||||
module Impl where
|
||||
type n = 8
|
||||
x = 26
|
||||
|
||||
module MyF = F { Impl }
|
||||
|
||||
Here we defined a new module called ``MyF`` which is
|
||||
obtained by filling in module ``Impl`` for the interface
|
||||
used by ``F``.
|
||||
|
||||
If a module is parameterized my multiple interfaces
|
||||
we need to provide an implementation module for each
|
||||
interface, using a slight variation on the previous notation.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Instantiating a parameterized module by name.
|
||||
|
||||
// I is defined as above
|
||||
|
||||
module F where
|
||||
import interface I as I
|
||||
import interface I as J
|
||||
|
||||
interface constraint (I::n == J::n)
|
||||
|
||||
y : [I::n]
|
||||
y = I::x + J::x
|
||||
|
||||
module Impl1 where
|
||||
type n = 8
|
||||
x = 26
|
||||
|
||||
module Impl2 where
|
||||
type n = 8
|
||||
x = 30
|
||||
|
||||
module MyF = F { I = Impl1, J = Impl 2 }
|
||||
|
||||
Each interface import is identified by its name,
|
||||
which is derived from the ``as`` clause on the
|
||||
interface import. If there is no ``as`` clause,
|
||||
then the name of the parameter is derived from
|
||||
the name of the interface itself.
|
||||
|
||||
Since interfaces are identified by name, the
|
||||
order in which they are provided is not important.
|
||||
|
||||
Modules defined by instantiation may be nested,
|
||||
just like any other module:
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Nested module instantiation.
|
||||
|
||||
module M where
|
||||
|
||||
import Somewhere // defines G
|
||||
|
||||
submodule F = submodule G { I }
|
||||
|
||||
In this example, ``submodule F`` is defined
|
||||
by instantiating some other parameterized
|
||||
module ``G``, presumably imported from ``Somewhere``.
|
||||
Note that in this case the argument to the instantiation
|
||||
``I`` is a top-level module, because it is not
|
||||
preceded by the ``submodule`` keyword.
|
||||
|
||||
|
||||
Anonymous Interface Modules
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
If we need to just parameterize a module by a couple of types/values,
|
||||
it is quite cumbersome to have to define a whole separate interface module.
|
||||
To make this more convenient we provide the following notation for defining
|
||||
an anonymous interface and using it straight away:
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Simple parameterized module.
|
||||
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : #
|
||||
type constraint (fin n, n >= 1)
|
||||
x : [n]
|
||||
|
||||
f : [n]
|
||||
f = 1 + x
|
||||
|
||||
The ``parameter`` block defines an interface module and uses it.
|
||||
Note that the parameters may not use things defined in ``M`` as
|
||||
the interface is declared outside of ``M``.
|
||||
|
||||
|
||||
Anonymous Instantiation Arguments
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
Sometimes it is also a bit cumbersome to have to define a whole
|
||||
separate module just to pass it as an argument to some parameterized
|
||||
module. To make this more convenient we support the following notion
|
||||
for instantiation a module:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
// A parameterized module
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : #
|
||||
x : [n]
|
||||
y : [n]
|
||||
parameter
|
||||
type n : #
|
||||
x : [n]
|
||||
y : [n]
|
||||
|
||||
f : [n]
|
||||
f = x + y
|
||||
f : [n]
|
||||
f = x + y
|
||||
|
||||
|
||||
// A module instantiation
|
||||
module N = M where
|
||||
module N = M
|
||||
where
|
||||
type n = 32
|
||||
x = 11
|
||||
y = helper
|
||||
|
||||
type n = 32
|
||||
x = 11
|
||||
y = helper
|
||||
|
||||
helper = 12
|
||||
|
||||
The second module, ``N``, is computed by instantiating the parameterized
|
||||
module ``M``. Module ``N`` will provide the exact same definitions as ``M``,
|
||||
except that the parameters will be replaced by the values in the body
|
||||
of ``N``. In this example, ``N`` provides just a single definition, ``f``.
|
||||
|
||||
Note that the only purpose of the body of ``N`` (the declarations
|
||||
after the ``where`` keyword) is to define the parameters for ``M``.
|
||||
|
||||
|
||||
Parameterized Instantiations
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
It is possible for a module instantiation to be itself parameterized.
|
||||
This could be useful if we need to define some of a module's parameters
|
||||
but not others.
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
// A parameterized module
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : #
|
||||
x : [n]
|
||||
y : [n]
|
||||
|
||||
f : [n]
|
||||
f = x + y
|
||||
|
||||
|
||||
// A parameterized instantiation
|
||||
module N = M where
|
||||
|
||||
parameter
|
||||
x : [32]
|
||||
|
||||
type n = 32
|
||||
y = helper
|
||||
|
||||
helper = 12
|
||||
|
||||
In this case ``N`` has a single parameter ``x``. The result of instantiating
|
||||
``N`` would result in instantiating ``M`` using the value of ``x`` and ``12``
|
||||
for the value of ``y``.
|
||||
|
||||
|
||||
Importing Parameterized Modules
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
It is also possible to import a parameterized module without using
|
||||
a module instantiation:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
module M where
|
||||
|
||||
parameter
|
||||
x : [8]
|
||||
y : [8]
|
||||
|
||||
f : [8]
|
||||
f = x + y
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
module N where
|
||||
|
||||
import `M
|
||||
|
||||
g = f { x = 2, y = 3 }
|
||||
|
||||
A *backtick* at the start of the name of an imported module indicates
|
||||
that we are importing a parameterized module. In this case, Cryptol
|
||||
will import all definitions from the module as usual, however every
|
||||
definition will have some additional parameters corresponding to
|
||||
the parameters of a module. All value parameters are grouped in a record.
|
||||
|
||||
This is why in the example ``f`` is applied to a record of values,
|
||||
even though its definition in ``M`` does not look like a function.
|
||||
helper = 12
|
||||
|
||||
The declarations in the ``where`` block are treated as the
|
||||
definition of an anonymous module which is passed as the argument
|
||||
to parameterized module ``M``.
|
||||
|
||||
|
||||
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
@ -152,10 +152,10 @@ names (see <a class="reference internal" href="#keywords-and-built-in-operators"
|
||||
not be used for programmer defined names:</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id3">
|
||||
<span id="keywords"></span><div class="code-block-caption"><span class="caption-text">Keywords</span><a class="headerlink" href="#id3" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-none notranslate"><div class="highlight"><pre><span></span>else include property let infixl parameter
|
||||
extern module then import infixr constraint
|
||||
if newtype type as infix down
|
||||
private pragma where hiding primitive by
|
||||
<div class="highlight-none notranslate"><div class="highlight"><pre><span></span>as extern include interface parameter property where
|
||||
by hiding infix let pragma submodule else
|
||||
constraint if infixl module primitive then
|
||||
down import infixr newtype private type
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
|
||||
@ -51,10 +51,18 @@
|
||||
</ul>
|
||||
</li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#private-blocks">Private Blocks</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#nested-modules">Nested Modules</a><ul>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#implicit-imports">Implicit Imports</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#managing-module-names">Managing Module Names</a></li>
|
||||
</ul>
|
||||
</li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#parameterized-modules">Parameterized Modules</a><ul>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#named-module-instantiations">Named Module Instantiations</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#parameterized-instantiations">Parameterized Instantiations</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#importing-parameterized-modules">Importing Parameterized Modules</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#interface-modules">Interface Modules</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#importing-an-interface-module">Importing an Interface Module</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#interface-constraints">Interface Constraints</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#instantiating-a-parameterized-module">Instantiating a Parameterized Module</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#anonymous-interface-modules">Anonymous Interface Modules</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#anonymous-instantiation-arguments">Anonymous Instantiation Arguments</a></li>
|
||||
</ul>
|
||||
</li>
|
||||
</ul>
|
||||
@ -262,7 +270,7 @@ It is good practice to place such declarations in <em>private blocks</em>:</p>
|
||||
</div>
|
||||
<p>The private block only needs to be indented if it might be followed by
|
||||
additional public declarations. If all remaining declarations are to be
|
||||
private then no additional indentation is needed as the <cite>private</cite> block will
|
||||
private then no additional indentation is needed as the <code class="docutils literal notranslate"><span class="pre">private</span></code> block will
|
||||
extend to the end of the module.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id10">
|
||||
<div class="code-block-caption"><span class="caption-text">Private blocks</span><a class="headerlink" href="#id10" title="Permalink to this code"></a></div>
|
||||
@ -303,121 +311,348 @@ is equivalent to the previous one:</p>
|
||||
</div>
|
||||
</div>
|
||||
</div>
|
||||
<div class="section" id="parameterized-modules">
|
||||
<h2>Parameterized Modules<a class="headerlink" href="#parameterized-modules" title="Permalink to this headline"></a></h2>
|
||||
<div class="admonition warning">
|
||||
<p class="admonition-title">Warning</p>
|
||||
<p>This section documents the current design, but we are in the process of
|
||||
redesigning some aspects of the parameterized modules mechanism.</p>
|
||||
</div>
|
||||
<div class="section" id="nested-modules">
|
||||
<h2>Nested Modules<a class="headerlink" href="#nested-modules" title="Permalink to this headline"></a></h2>
|
||||
<p>Module may be declared withing other modules, using the <code class="docutils literal notranslate"><span class="pre">submodule</span></code> keword.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id12">
|
||||
<div class="code-block-caption"><span class="caption-text">Declaring a nested module called N</span><a class="headerlink" href="#id12" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
|
||||
|
||||
<span class="nf">parameter</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span> <span class="c1">// `n` is a numeric type parameter</span>
|
||||
<span class="n">x</span> <span class="ow">=</span> <span class="mh">0x02</span>
|
||||
|
||||
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">>=</span> <span class="mi">1</span><span class="p">)</span>
|
||||
<span class="c1">// Assumptions about the parameter</span>
|
||||
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span> <span class="c1">// A value parameter</span>
|
||||
|
||||
<span class="c1">// This definition uses the parameters.</span>
|
||||
<span class="nf">f</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="nf">f</span> <span class="ow">=</span> <span class="mi">1</span> <span class="o">+</span> <span class="n">x</span>
|
||||
<span class="n">submodule</span> <span class="kt">N</span> <span class="kr">where</span>
|
||||
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<div class="section" id="named-module-instantiations">
|
||||
<h3>Named Module Instantiations<a class="headerlink" href="#named-module-instantiations" title="Permalink to this headline"></a></h3>
|
||||
<p>One way to use a parameterized module is through a named instantiation:</p>
|
||||
</div>
|
||||
<p>Submodules may refer to names in their enclosing scope.
|
||||
Declarations in a sub-module will shadow names in the outer scope.</p>
|
||||
<p>Declarations in a submdule may be imported with <code class="docutils literal notranslate"><span class="pre">import</span> <span class="pre">submodule</span></code>,
|
||||
which works just like an ordinary import except that <code class="docutils literal notranslate"><span class="pre">X</span></code> refers
|
||||
to the name of a submodule.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id13">
|
||||
<div class="code-block-caption"><span class="caption-text">Using declarations from a submodule.</span><a class="headerlink" href="#id13" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
|
||||
|
||||
<span class="n">x</span> <span class="ow">=</span> <span class="mh">0x02</span>
|
||||
|
||||
<span class="n">submodule</span> <span class="kt">N</span> <span class="kr">where</span>
|
||||
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span>
|
||||
|
||||
<span class="kr">import</span> <span class="nn">submodule</span> <span class="kt">N</span> <span class="n">as</span> <span class="kt">P</span>
|
||||
|
||||
<span class="n">z</span> <span class="ow">=</span> <span class="mi">2</span> <span class="o">*</span> <span class="kt">P</span><span class="ow">::</span><span class="n">y</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
<p>Note that recursive definitions across modules are not allowed.
|
||||
So, in the previous example, it would be an error if <code class="docutils literal notranslate"><span class="pre">y</span></code> was
|
||||
to try to use <code class="docutils literal notranslate"><span class="pre">z</span></code> in its definition.</p>
|
||||
<div class="section" id="implicit-imports">
|
||||
<h3>Implicit Imports<a class="headerlink" href="#implicit-imports" title="Permalink to this headline"></a></h3>
|
||||
<p>For convenience, we add an implicit qualified submodule import for
|
||||
each locally defined submodules.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id14">
|
||||
<div class="code-block-caption"><span class="caption-text">Making use of the implicit import for a submodule.</span><a class="headerlink" href="#id14" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
|
||||
|
||||
<span class="n">x</span> <span class="ow">=</span> <span class="mh">0x02</span>
|
||||
|
||||
<span class="n">submodule</span> <span class="kt">N</span> <span class="kr">where</span>
|
||||
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span>
|
||||
|
||||
<span class="n">z</span> <span class="ow">=</span> <span class="mi">2</span> <span class="o">*</span> <span class="kt">N</span><span class="ow">::</span><span class="n">y</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
<p><code class="docutils literal notranslate"><span class="pre">N::y</span></code> works in the previous example because Cryptol added
|
||||
an implicit import <code class="docutils literal notranslate"><span class="pre">import</span> <span class="pre">submoulde</span> <span class="pre">N</span> <span class="pre">as</span> <span class="pre">N</span></code>.</p>
|
||||
</div>
|
||||
<div class="section" id="managing-module-names">
|
||||
<h3>Managing Module Names<a class="headerlink" href="#managing-module-names" title="Permalink to this headline"></a></h3>
|
||||
<p>The names of nested modules are managed by the module system just
|
||||
like the name of any other declaration in Cryptol. Thus, nested
|
||||
modules may declared in the public or private sections of their
|
||||
containing module, and need to be imported before they can be used.
|
||||
Thus, to use a submodule defined in top-level module <code class="docutils literal notranslate"><span class="pre">A</span></code> into
|
||||
another top-level module <code class="docutils literal notranslate"><span class="pre">B</span></code> requires two steps:</p>
|
||||
<blockquote>
|
||||
<div><ol class="arabic simple">
|
||||
<li><p>First we need to import <code class="docutils literal notranslate"><span class="pre">A</span></code> to bring the name of the submodule in scope</p></li>
|
||||
<li><p>Then we need to import the submodule to bring the names defined in it in scope.</p></li>
|
||||
</ol>
|
||||
</div></blockquote>
|
||||
<div class="literal-block-wrapper docutils container" id="id15">
|
||||
<div class="code-block-caption"><span class="caption-text">Using a nested module from a different top-level module.</span><a class="headerlink" href="#id15" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">A</span> <span class="kr">where</span>
|
||||
|
||||
<span class="n">x</span> <span class="ow">=</span> <span class="mh">0x02</span>
|
||||
|
||||
<span class="n">submodule</span> <span class="kt">N</span> <span class="kr">where</span>
|
||||
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span>
|
||||
|
||||
<span class="kr">module</span> <span class="nn">B</span> <span class="kr">where</span>
|
||||
<span class="kr">import</span> <span class="nn">A</span> <span class="c1">// Brings `N` in scope</span>
|
||||
<span class="kr">import</span> <span class="nn">submodule</span> <span class="kt">N</span> <span class="c1">// Brings `y` in scope</span>
|
||||
<span class="n">z</span> <span class="ow">=</span> <span class="mi">2</span> <span class="o">*</span> <span class="n">y</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
</div>
|
||||
</div>
|
||||
<div class="section" id="parameterized-modules">
|
||||
<h2>Parameterized Modules<a class="headerlink" href="#parameterized-modules" title="Permalink to this headline"></a></h2>
|
||||
<div class="section" id="interface-modules">
|
||||
<h3>Interface Modules<a class="headerlink" href="#interface-modules" title="Permalink to this headline"></a></h3>
|
||||
<p>An <em>interface module</em> describes the content of a module
|
||||
without providing a concrete implementation.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id16">
|
||||
<div class="code-block-caption"><span class="caption-text">An interface module.</span><a class="headerlink" href="#id16" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">interface</span> <span class="kr">module</span> <span class="nn">I</span> <span class="kr">where</span>
|
||||
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span> <span class="c1">// `n` is a numeric type</span>
|
||||
|
||||
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">>=</span> <span class="mi">1</span><span class="p">)</span>
|
||||
<span class="c1">// Assumptions about the declared numeric type</span>
|
||||
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span> <span class="c1">// A declarations of a constant</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
<p>Like other modules, interfaces modules may be nested in
|
||||
other modules:</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id17">
|
||||
<div class="code-block-caption"><span class="caption-text">A nested interface module</span><a class="headerlink" href="#id17" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
|
||||
|
||||
<span class="n">interface</span> <span class="n">submodule</span> <span class="kt">I</span> <span class="kr">where</span>
|
||||
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span> <span class="c1">// `n` is a numeric type</span>
|
||||
|
||||
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">>=</span> <span class="mi">1</span><span class="p">)</span>
|
||||
<span class="c1">// Assumptions about the declared numeric type</span>
|
||||
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span> <span class="c1">// A declarations of a constant</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
</div>
|
||||
<div class="section" id="importing-an-interface-module">
|
||||
<h3>Importing an Interface Module<a class="headerlink" href="#importing-an-interface-module" title="Permalink to this headline"></a></h3>
|
||||
<p>A module may be parameterized by importing an interface,
|
||||
instead of a concrete module</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id18">
|
||||
<div class="code-block-caption"><span class="caption-text">A parameterized module</span><a class="headerlink" href="#id18" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// The interface desribes the parmaeters</span>
|
||||
<span class="nf">interface</span> <span class="kr">module</span> <span class="nn">I</span> <span class="kr">where</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
|
||||
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">>=</span> <span class="mi">1</span><span class="p">)</span>
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
|
||||
|
||||
<span class="c1">// This module is parameterized</span>
|
||||
<span class="kr">module</span> <span class="nn">F</span> <span class="kr">where</span>
|
||||
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span>
|
||||
|
||||
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
<p>To import a nested interface use <code class="docutils literal notranslate"><span class="pre">import</span> <span class="pre">interface</span> <span class="pre">sumbodule</span> <span class="pre">I</span></code>
|
||||
and make sure that <code class="docutils literal notranslate"><span class="pre">I</span></code> is in scope.</p>
|
||||
<p>It is also possible to import multiple interface modules,
|
||||
or the same interface module more than once. Each import
|
||||
of an interface module maybe be linked to a different concrete
|
||||
module, as described in <a class="reference internal" href="#instantiating-modules"><span class="std std-ref">Instantiating a Parameterized Module</span></a>.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id19">
|
||||
<div class="code-block-caption"><span class="caption-text">Multiple interface parameters</span><a class="headerlink" href="#id19" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">interface</span> <span class="kr">module</span> <span class="nn">I</span> <span class="kr">where</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
|
||||
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">>=</span> <span class="mi">1</span><span class="p">)</span>
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
|
||||
|
||||
<span class="kr">module</span> <span class="nn">F</span> <span class="kr">where</span>
|
||||
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">I</span>
|
||||
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">J</span>
|
||||
|
||||
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="kt">I</span><span class="ow">::</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">y</span> <span class="ow">=</span> <span class="kt">I</span><span class="ow">::</span><span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
|
||||
|
||||
<span class="n">z</span> <span class="kt">:</span> <span class="p">[</span><span class="kt">J</span><span class="ow">::</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">z</span> <span class="ow">=</span> <span class="kt">J</span><span class="ow">::</span><span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
</div>
|
||||
<div class="section" id="interface-constraints">
|
||||
<h3>Interface Constraints<a class="headerlink" href="#interface-constraints" title="Permalink to this headline"></a></h3>
|
||||
<p>When working with multiple interfaces, it is to useful
|
||||
to be able to impose additional constraints on the
|
||||
types imported from the interface.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id20">
|
||||
<div class="code-block-caption"><span class="caption-text">Adding constraints to interface parameters</span><a class="headerlink" href="#id20" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">interface</span> <span class="kr">module</span> <span class="nn">I</span> <span class="kr">where</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
|
||||
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">>=</span> <span class="mi">1</span><span class="p">)</span>
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
|
||||
|
||||
<span class="kr">module</span> <span class="nn">F</span> <span class="kr">where</span>
|
||||
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">I</span>
|
||||
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">J</span>
|
||||
|
||||
<span class="n">interface</span> <span class="n">constraint</span> <span class="p">(</span><span class="kt">I</span><span class="ow">::</span><span class="n">n</span> <span class="o">==</span> <span class="kt">J</span><span class="ow">::</span><span class="n">n</span><span class="p">)</span>
|
||||
|
||||
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="kt">I</span><span class="ow">::</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">y</span> <span class="ow">=</span> <span class="kt">I</span><span class="ow">::</span><span class="n">x</span> <span class="o">+</span> <span class="kt">J</span><span class="ow">::</span><span class="n">x</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
<p>In this example we impose the constraint that <code class="docutils literal notranslate"><span class="pre">n</span></code>
|
||||
(the width of <code class="docutils literal notranslate"><span class="pre">x</span></code>) in both interfaces must be the
|
||||
same. Note that, of course, the two instantiations
|
||||
may provide different values for <code class="docutils literal notranslate"><span class="pre">x</span></code>.</p>
|
||||
</div>
|
||||
<div class="section" id="instantiating-a-parameterized-module">
|
||||
<span id="instantiating-modules"></span><h3>Instantiating a Parameterized Module<a class="headerlink" href="#instantiating-a-parameterized-module" title="Permalink to this headline"></a></h3>
|
||||
<p>To use a parameterized module we need to provide concrete
|
||||
implementations for the interfaces that it uses, and provide
|
||||
a name for the resulting module. This is done as follows:</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id21">
|
||||
<div class="code-block-caption"><span class="caption-text">Instantiating a parameterized module using a single interface.</span><a class="headerlink" href="#id21" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">interface</span> <span class="kr">module</span> <span class="nn">I</span> <span class="kr">where</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
|
||||
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">>=</span> <span class="mi">1</span><span class="p">)</span>
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
|
||||
<span class="kr">module</span> <span class="nn">F</span> <span class="kr">where</span>
|
||||
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span>
|
||||
|
||||
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
|
||||
|
||||
<span class="kr">module</span> <span class="nn">Impl</span> <span class="kr">where</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="ow">=</span> <span class="mi">8</span>
|
||||
<span class="n">x</span> <span class="ow">=</span> <span class="mi">26</span>
|
||||
|
||||
<span class="kr">module</span> <span class="nn">MyF</span> <span class="ow">=</span> <span class="kt">F</span> <span class="p">{</span> <span class="kt">Impl</span> <span class="p">}</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
<p>Here we defined a new module called <code class="docutils literal notranslate"><span class="pre">MyF</span></code> which is
|
||||
obtained by filling in module <code class="docutils literal notranslate"><span class="pre">Impl</span></code> for the interface
|
||||
used by <code class="docutils literal notranslate"><span class="pre">F</span></code>.</p>
|
||||
<p>If a module is parameterized my multiple interfaces
|
||||
we need to provide an implementation module for each
|
||||
interface, using a slight variation on the previous notation.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id22">
|
||||
<div class="code-block-caption"><span class="caption-text">Instantiating a parameterized module by name.</span><a class="headerlink" href="#id22" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// I is defined as above</span>
|
||||
|
||||
<span class="kr">module</span> <span class="nn">F</span> <span class="kr">where</span>
|
||||
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">I</span>
|
||||
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">J</span>
|
||||
|
||||
<span class="n">interface</span> <span class="n">constraint</span> <span class="p">(</span><span class="kt">I</span><span class="ow">::</span><span class="n">n</span> <span class="o">==</span> <span class="kt">J</span><span class="ow">::</span><span class="n">n</span><span class="p">)</span>
|
||||
|
||||
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="kt">I</span><span class="ow">::</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">y</span> <span class="ow">=</span> <span class="kt">I</span><span class="ow">::</span><span class="n">x</span> <span class="o">+</span> <span class="kt">J</span><span class="ow">::</span><span class="n">x</span>
|
||||
|
||||
<span class="kr">module</span> <span class="nn">Impl1</span> <span class="kr">where</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="ow">=</span> <span class="mi">8</span>
|
||||
<span class="n">x</span> <span class="ow">=</span> <span class="mi">26</span>
|
||||
|
||||
<span class="kr">module</span> <span class="nn">Impl2</span> <span class="kr">where</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="ow">=</span> <span class="mi">8</span>
|
||||
<span class="n">x</span> <span class="ow">=</span> <span class="mi">30</span>
|
||||
|
||||
<span class="kr">module</span> <span class="nn">MyF</span> <span class="ow">=</span> <span class="kt">F</span> <span class="p">{</span> <span class="kt">I</span> <span class="ow">=</span> <span class="kt">Impl1</span><span class="p">,</span> <span class="kt">J</span> <span class="ow">=</span> <span class="kt">Impl</span> <span class="mi">2</span> <span class="p">}</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
<p>Each interface import is identified by its name,
|
||||
which is derived from the <code class="docutils literal notranslate"><span class="pre">as</span></code> clause on the
|
||||
interface import. If there is no <code class="docutils literal notranslate"><span class="pre">as</span></code> clause,
|
||||
then the name of the parameter is derived from
|
||||
the name of the interface itself.</p>
|
||||
<p>Since interfaces are identified by name, the
|
||||
order in which they are provided is not important.</p>
|
||||
<p>Modules defined by instantiation may be nested,
|
||||
just like any other module:</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id23">
|
||||
<div class="code-block-caption"><span class="caption-text">Nested module instantiation.</span><a class="headerlink" href="#id23" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
|
||||
|
||||
<span class="kr">import</span> <span class="nn">Somewhere</span> <span class="c1">// defines G</span>
|
||||
|
||||
<span class="n">submodule</span> <span class="kt">F</span> <span class="ow">=</span> <span class="n">submodule</span> <span class="kt">G</span> <span class="p">{</span> <span class="kt">I</span> <span class="p">}</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
<p>In this example, <code class="docutils literal notranslate"><span class="pre">submodule</span> <span class="pre">F</span></code> is defined
|
||||
by instantiating some other parameterized
|
||||
module <code class="docutils literal notranslate"><span class="pre">G</span></code>, presumably imported from <code class="docutils literal notranslate"><span class="pre">Somewhere</span></code>.
|
||||
Note that in this case the argument to the instantiation
|
||||
<code class="docutils literal notranslate"><span class="pre">I</span></code> is a top-level module, because it is not
|
||||
preceded by the <code class="docutils literal notranslate"><span class="pre">submodule</span></code> keyword.</p>
|
||||
</div>
|
||||
<div class="section" id="anonymous-interface-modules">
|
||||
<h3>Anonymous Interface Modules<a class="headerlink" href="#anonymous-interface-modules" title="Permalink to this headline"></a></h3>
|
||||
<p>If we need to just parameterize a module by a couple of types/values,
|
||||
it is quite cumbersome to have to define a whole separate interface module.
|
||||
To make this more convenient we provide the following notation for defining
|
||||
an anonymous interface and using it straight away:</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id24">
|
||||
<div class="code-block-caption"><span class="caption-text">Simple parameterized module.</span><a class="headerlink" href="#id24" title="Permalink to this code"></a></div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
|
||||
|
||||
<span class="n">parameter</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
|
||||
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">>=</span> <span class="mi">1</span><span class="p">)</span>
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
|
||||
<span class="n">f</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">f</span> <span class="ow">=</span> <span class="mi">1</span> <span class="o">+</span> <span class="n">x</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</div>
|
||||
<p>The <code class="docutils literal notranslate"><span class="pre">parameter</span></code> block defines an interface module and uses it.
|
||||
Note that the parameters may not use things defined in <code class="docutils literal notranslate"><span class="pre">M</span></code> as
|
||||
the interface is declared outside of <code class="docutils literal notranslate"><span class="pre">M</span></code>.</p>
|
||||
</div>
|
||||
<div class="section" id="anonymous-instantiation-arguments">
|
||||
<h3>Anonymous Instantiation Arguments<a class="headerlink" href="#anonymous-instantiation-arguments" title="Permalink to this headline"></a></h3>
|
||||
<p>Sometimes it is also a bit cumbersome to have to define a whole
|
||||
separate module just to pass it as an argument to some parameterized
|
||||
module. To make this more convenient we support the following notion
|
||||
for instantiation a module:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// A parameterized module</span>
|
||||
<span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
|
||||
|
||||
<span class="nf">parameter</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">parameter</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
|
||||
<span class="nf">f</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="nf">f</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span>
|
||||
<span class="n">f</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">f</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span>
|
||||
|
||||
|
||||
<span class="c1">// A module instantiation</span>
|
||||
<span class="kr">module</span> <span class="nn">N</span> <span class="ow">=</span> <span class="kt">M</span> <span class="kr">where</span>
|
||||
<span class="kr">module</span> <span class="nn">N</span> <span class="ow">=</span> <span class="kt">M</span>
|
||||
<span class="kr">where</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="ow">=</span> <span class="mi">32</span>
|
||||
<span class="n">x</span> <span class="ow">=</span> <span class="mi">11</span>
|
||||
<span class="n">y</span> <span class="ow">=</span> <span class="n">helper</span>
|
||||
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="ow">=</span> <span class="mi">32</span>
|
||||
<span class="nf">x</span> <span class="ow">=</span> <span class="mi">11</span>
|
||||
<span class="nf">y</span> <span class="ow">=</span> <span class="n">helper</span>
|
||||
|
||||
<span class="nf">helper</span> <span class="ow">=</span> <span class="mi">12</span>
|
||||
<span class="n">helper</span> <span class="ow">=</span> <span class="mi">12</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>The second module, <code class="docutils literal notranslate"><span class="pre">N</span></code>, is computed by instantiating the parameterized
|
||||
module <code class="docutils literal notranslate"><span class="pre">M</span></code>. Module <code class="docutils literal notranslate"><span class="pre">N</span></code> will provide the exact same definitions as <code class="docutils literal notranslate"><span class="pre">M</span></code>,
|
||||
except that the parameters will be replaced by the values in the body
|
||||
of <code class="docutils literal notranslate"><span class="pre">N</span></code>. In this example, <code class="docutils literal notranslate"><span class="pre">N</span></code> provides just a single definition, <code class="docutils literal notranslate"><span class="pre">f</span></code>.</p>
|
||||
<p>Note that the only purpose of the body of <code class="docutils literal notranslate"><span class="pre">N</span></code> (the declarations
|
||||
after the <code class="docutils literal notranslate"><span class="pre">where</span></code> keyword) is to define the parameters for <code class="docutils literal notranslate"><span class="pre">M</span></code>.</p>
|
||||
</div>
|
||||
<div class="section" id="parameterized-instantiations">
|
||||
<h3>Parameterized Instantiations<a class="headerlink" href="#parameterized-instantiations" title="Permalink to this headline"></a></h3>
|
||||
<p>It is possible for a module instantiation to be itself parameterized.
|
||||
This could be useful if we need to define some of a module’s parameters
|
||||
but not others.</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// A parameterized module</span>
|
||||
<span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
|
||||
|
||||
<span class="nf">parameter</span>
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
|
||||
<span class="nf">f</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
|
||||
<span class="nf">f</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span>
|
||||
|
||||
|
||||
<span class="c1">// A parameterized instantiation</span>
|
||||
<span class="kr">module</span> <span class="nn">N</span> <span class="ow">=</span> <span class="kt">M</span> <span class="kr">where</span>
|
||||
|
||||
<span class="nf">parameter</span>
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">32</span><span class="p">]</span>
|
||||
|
||||
<span class="kr">type</span> <span class="n">n</span> <span class="ow">=</span> <span class="mi">32</span>
|
||||
<span class="nf">y</span> <span class="ow">=</span> <span class="n">helper</span>
|
||||
|
||||
<span class="nf">helper</span> <span class="ow">=</span> <span class="mi">12</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>In this case <code class="docutils literal notranslate"><span class="pre">N</span></code> has a single parameter <code class="docutils literal notranslate"><span class="pre">x</span></code>. The result of instantiating
|
||||
<code class="docutils literal notranslate"><span class="pre">N</span></code> would result in instantiating <code class="docutils literal notranslate"><span class="pre">M</span></code> using the value of <code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">12</span></code>
|
||||
for the value of <code class="docutils literal notranslate"><span class="pre">y</span></code>.</p>
|
||||
</div>
|
||||
<div class="section" id="importing-parameterized-modules">
|
||||
<h3>Importing Parameterized Modules<a class="headerlink" href="#importing-parameterized-modules" title="Permalink to this headline"></a></h3>
|
||||
<p>It is also possible to import a parameterized module without using
|
||||
a module instantiation:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
|
||||
|
||||
<span class="nf">parameter</span>
|
||||
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
|
||||
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
|
||||
|
||||
<span class="nf">f</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
|
||||
<span class="nf">f</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span>module N where
|
||||
|
||||
import `M
|
||||
|
||||
g = f { x = 2, y = 3 }
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>A <em>backtick</em> at the start of the name of an imported module indicates
|
||||
that we are importing a parameterized module. In this case, Cryptol
|
||||
will import all definitions from the module as usual, however every
|
||||
definition will have some additional parameters corresponding to
|
||||
the parameters of a module. All value parameters are grouped in a record.</p>
|
||||
<p>This is why in the example <code class="docutils literal notranslate"><span class="pre">f</span></code> is applied to a record of values,
|
||||
even though its definition in <code class="docutils literal notranslate"><span class="pre">M</span></code> does not look like a function.</p>
|
||||
<p>The declarations in the <code class="docutils literal notranslate"><span class="pre">where</span></code> block are treated as the
|
||||
definition of an anonymous module which is passed as the argument
|
||||
to parameterized module <code class="docutils literal notranslate"><span class="pre">M</span></code>.</p>
|
||||
</div>
|
||||
</div>
|
||||
</div>
|
||||
|
||||
@ -133,10 +133,18 @@
|
||||
</ul>
|
||||
</li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="Modules.html#private-blocks">Private Blocks</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="Modules.html#nested-modules">Nested Modules</a><ul>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#implicit-imports">Implicit Imports</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#managing-module-names">Managing Module Names</a></li>
|
||||
</ul>
|
||||
</li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="Modules.html#parameterized-modules">Parameterized Modules</a><ul>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#named-module-instantiations">Named Module Instantiations</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#parameterized-instantiations">Parameterized Instantiations</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#importing-parameterized-modules">Importing Parameterized Modules</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#interface-modules">Interface Modules</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#importing-an-interface-module">Importing an Interface Module</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#interface-constraints">Interface Constraints</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#instantiating-a-parameterized-module">Instantiating a Parameterized Module</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#anonymous-interface-modules">Anonymous Interface Modules</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="Modules.html#anonymous-instantiation-arguments">Anonymous Instantiation Arguments</a></li>
|
||||
</ul>
|
||||
</li>
|
||||
</ul>
|
||||
|
||||
@ -94,6 +94,8 @@ not be used for programmer defined names:
|
||||
private
|
||||
include
|
||||
module
|
||||
submodule
|
||||
interface
|
||||
newtype
|
||||
pragma
|
||||
property
|
||||
@ -117,11 +119,10 @@ not be used for programmer defined names:
|
||||
.. code-block:: none
|
||||
:caption: Keywords
|
||||
|
||||
else include property let infixl parameter
|
||||
extern module then import infixr constraint
|
||||
if newtype type as infix down
|
||||
private pragma where hiding primitive by
|
||||
|
||||
as extern include interface parameter property where
|
||||
by hiding infix let pragma submodule else
|
||||
constraint if infixl module primitive then
|
||||
down import infixr newtype private type
|
||||
|
||||
The following table contains Cryptol's operators and their
|
||||
associativity with lowest precedence operators first, and highest
|
||||
|
||||
@ -196,7 +196,7 @@ It is good practice to place such declarations in *private blocks*:
|
||||
|
||||
The private block only needs to be indented if it might be followed by
|
||||
additional public declarations. If all remaining declarations are to be
|
||||
private then no additional indentation is needed as the `private` block will
|
||||
private then no additional indentation is needed as the ``private`` block will
|
||||
extend to the end of the module.
|
||||
|
||||
.. code-block:: cryptol
|
||||
@ -238,139 +238,373 @@ is equivalent to the previous one:
|
||||
helper2 = 3
|
||||
|
||||
|
||||
Nested Modules
|
||||
--------------
|
||||
|
||||
Module may be declared withing other modules, using the ``submodule`` keword.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Declaring a nested module called N
|
||||
|
||||
module M where
|
||||
|
||||
x = 0x02
|
||||
|
||||
submodule N where
|
||||
y = x + 2
|
||||
|
||||
Submodules may refer to names in their enclosing scope.
|
||||
Declarations in a sub-module will shadow names in the outer scope.
|
||||
|
||||
Declarations in a submdule may be imported with ``import submodule``,
|
||||
which works just like an ordinary import except that ``X`` refers
|
||||
to the name of a submodule.
|
||||
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Using declarations from a submodule.
|
||||
|
||||
module M where
|
||||
|
||||
x = 0x02
|
||||
|
||||
submodule N where
|
||||
y = x + 2
|
||||
|
||||
import submodule N as P
|
||||
|
||||
z = 2 * P::y
|
||||
|
||||
Note that recursive definitions across modules are not allowed.
|
||||
So, in the previous example, it would be an error if ``y`` was
|
||||
to try to use ``z`` in its definition.
|
||||
|
||||
|
||||
|
||||
Implicit Imports
|
||||
~~~~~~~~~~~~~~~~
|
||||
|
||||
For convenience, we add an implicit qualified submodule import for
|
||||
each locally defined submodules.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Making use of the implicit import for a submodule.
|
||||
|
||||
module M where
|
||||
|
||||
x = 0x02
|
||||
|
||||
submodule N where
|
||||
y = x + 2
|
||||
|
||||
z = 2 * N::y
|
||||
|
||||
``N::y`` works in the previous example because Cryptol added
|
||||
an implicit import ``import submoulde N as N``.
|
||||
|
||||
|
||||
Managing Module Names
|
||||
~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
The names of nested modules are managed by the module system just
|
||||
like the name of any other declaration in Cryptol. Thus, nested
|
||||
modules may declared in the public or private sections of their
|
||||
containing module, and need to be imported before they can be used.
|
||||
Thus, to use a submodule defined in top-level module ``A`` into
|
||||
another top-level module ``B`` requires two steps:
|
||||
|
||||
1. First we need to import ``A`` to bring the name of the submodule in scope
|
||||
2. Then we need to import the submodule to bring the names defined in it in scope.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Using a nested module from a different top-level module.
|
||||
|
||||
module A where
|
||||
|
||||
x = 0x02
|
||||
|
||||
submodule N where
|
||||
y = x + 2
|
||||
|
||||
module B where
|
||||
import A // Brings `N` in scope
|
||||
import submodule N // Brings `y` in scope
|
||||
z = 2 * y
|
||||
|
||||
|
||||
Parameterized Modules
|
||||
---------------------
|
||||
|
||||
.. warning::
|
||||
This section documents the current design, but we are in the process of
|
||||
redesigning some aspects of the parameterized modules mechanism.
|
||||
|
||||
Interface Modules
|
||||
~~~~~~~~~~~~~~~~~
|
||||
|
||||
An *interface module* describes the content of a module
|
||||
without providing a concrete implementation.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: An interface module.
|
||||
|
||||
interface module I where
|
||||
|
||||
type n : # // `n` is a numeric type
|
||||
|
||||
type constraint (fin n, n >= 1)
|
||||
// Assumptions about the declared numeric type
|
||||
|
||||
x : [n] // A declarations of a constant
|
||||
|
||||
Like other modules, interfaces modules may be nested in
|
||||
other modules:
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: A nested interface module
|
||||
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : # // `n` is a numeric type parameter
|
||||
interface submodule I where
|
||||
|
||||
type n : # // `n` is a numeric type
|
||||
|
||||
type constraint (fin n, n >= 1)
|
||||
// Assumptions about the declared numeric type
|
||||
|
||||
x : [n] // A declarations of a constant
|
||||
|
||||
|
||||
Importing an Interface Module
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
A module may be parameterized by importing an interface,
|
||||
instead of a concrete module
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: A parameterized module
|
||||
|
||||
// The interface desribes the parmaeters
|
||||
interface module I where
|
||||
type n : #
|
||||
type constraint (fin n, n >= 1)
|
||||
// Assumptions about the parameter
|
||||
|
||||
x : [n] // A value parameter
|
||||
|
||||
// This definition uses the parameters.
|
||||
f : [n]
|
||||
f = 1 + x
|
||||
x : [n]
|
||||
|
||||
|
||||
Named Module Instantiations
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
// This module is parameterized
|
||||
module F where
|
||||
import interface I
|
||||
|
||||
One way to use a parameterized module is through a named instantiation:
|
||||
y : [n]
|
||||
y = x + 1
|
||||
|
||||
To import a nested interface use ``import interface sumbodule I``
|
||||
and make sure that ``I`` is in scope.
|
||||
|
||||
It is also possible to import multiple interface modules,
|
||||
or the same interface module more than once. Each import
|
||||
of an interface module maybe be linked to a different concrete
|
||||
module, as described in :ref:`instantiating_modules`.
|
||||
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Multiple interface parameters
|
||||
|
||||
interface module I where
|
||||
type n : #
|
||||
type constraint (fin n, n >= 1)
|
||||
x : [n]
|
||||
|
||||
|
||||
module F where
|
||||
import interface I as I
|
||||
import interface I as J
|
||||
|
||||
y : [I::n]
|
||||
y = I::x + 1
|
||||
|
||||
z : [J::n]
|
||||
z = J::x + 1
|
||||
|
||||
|
||||
Interface Constraints
|
||||
~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
When working with multiple interfaces, it is to useful
|
||||
to be able to impose additional constraints on the
|
||||
types imported from the interface.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Adding constraints to interface parameters
|
||||
|
||||
interface module I where
|
||||
type n : #
|
||||
type constraint (fin n, n >= 1)
|
||||
x : [n]
|
||||
|
||||
|
||||
module F where
|
||||
import interface I as I
|
||||
import interface I as J
|
||||
|
||||
interface constraint (I::n == J::n)
|
||||
|
||||
y : [I::n]
|
||||
y = I::x + J::x
|
||||
|
||||
In this example we impose the constraint that ``n``
|
||||
(the width of ``x``) in both interfaces must be the
|
||||
same. Note that, of course, the two instantiations
|
||||
may provide different values for ``x``.
|
||||
|
||||
|
||||
.. _instantiating_modules:
|
||||
|
||||
|
||||
Instantiating a Parameterized Module
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
To use a parameterized module we need to provide concrete
|
||||
implementations for the interfaces that it uses, and provide
|
||||
a name for the resulting module. This is done as follows:
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Instantiating a parameterized module using a single interface.
|
||||
|
||||
interface module I where
|
||||
type n : #
|
||||
type constraint (fin n, n >= 1)
|
||||
x : [n]
|
||||
|
||||
module F where
|
||||
import interface I
|
||||
|
||||
y : [n]
|
||||
y = x + 1
|
||||
|
||||
module Impl where
|
||||
type n = 8
|
||||
x = 26
|
||||
|
||||
module MyF = F { Impl }
|
||||
|
||||
Here we defined a new module called ``MyF`` which is
|
||||
obtained by filling in module ``Impl`` for the interface
|
||||
used by ``F``.
|
||||
|
||||
If a module is parameterized my multiple interfaces
|
||||
we need to provide an implementation module for each
|
||||
interface, using a slight variation on the previous notation.
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Instantiating a parameterized module by name.
|
||||
|
||||
// I is defined as above
|
||||
|
||||
module F where
|
||||
import interface I as I
|
||||
import interface I as J
|
||||
|
||||
interface constraint (I::n == J::n)
|
||||
|
||||
y : [I::n]
|
||||
y = I::x + J::x
|
||||
|
||||
module Impl1 where
|
||||
type n = 8
|
||||
x = 26
|
||||
|
||||
module Impl2 where
|
||||
type n = 8
|
||||
x = 30
|
||||
|
||||
module MyF = F { I = Impl1, J = Impl 2 }
|
||||
|
||||
Each interface import is identified by its name,
|
||||
which is derived from the ``as`` clause on the
|
||||
interface import. If there is no ``as`` clause,
|
||||
then the name of the parameter is derived from
|
||||
the name of the interface itself.
|
||||
|
||||
Since interfaces are identified by name, the
|
||||
order in which they are provided is not important.
|
||||
|
||||
Modules defined by instantiation may be nested,
|
||||
just like any other module:
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Nested module instantiation.
|
||||
|
||||
module M where
|
||||
|
||||
import Somewhere // defines G
|
||||
|
||||
submodule F = submodule G { I }
|
||||
|
||||
In this example, ``submodule F`` is defined
|
||||
by instantiating some other parameterized
|
||||
module ``G``, presumably imported from ``Somewhere``.
|
||||
Note that in this case the argument to the instantiation
|
||||
``I`` is a top-level module, because it is not
|
||||
preceded by the ``submodule`` keyword.
|
||||
|
||||
|
||||
Anonymous Interface Modules
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
If we need to just parameterize a module by a couple of types/values,
|
||||
it is quite cumbersome to have to define a whole separate interface module.
|
||||
To make this more convenient we provide the following notation for defining
|
||||
an anonymous interface and using it straight away:
|
||||
|
||||
.. code-block:: cryptol
|
||||
:caption: Simple parameterized module.
|
||||
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : #
|
||||
type constraint (fin n, n >= 1)
|
||||
x : [n]
|
||||
|
||||
f : [n]
|
||||
f = 1 + x
|
||||
|
||||
The ``parameter`` block defines an interface module and uses it.
|
||||
Note that the parameters may not use things defined in ``M`` as
|
||||
the interface is declared outside of ``M``.
|
||||
|
||||
|
||||
Anonymous Instantiation Arguments
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
Sometimes it is also a bit cumbersome to have to define a whole
|
||||
separate module just to pass it as an argument to some parameterized
|
||||
module. To make this more convenient we support the following notion
|
||||
for instantiation a module:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
// A parameterized module
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : #
|
||||
x : [n]
|
||||
y : [n]
|
||||
parameter
|
||||
type n : #
|
||||
x : [n]
|
||||
y : [n]
|
||||
|
||||
f : [n]
|
||||
f = x + y
|
||||
f : [n]
|
||||
f = x + y
|
||||
|
||||
|
||||
// A module instantiation
|
||||
module N = M where
|
||||
module N = M
|
||||
where
|
||||
type n = 32
|
||||
x = 11
|
||||
y = helper
|
||||
|
||||
type n = 32
|
||||
x = 11
|
||||
y = helper
|
||||
|
||||
helper = 12
|
||||
|
||||
The second module, ``N``, is computed by instantiating the parameterized
|
||||
module ``M``. Module ``N`` will provide the exact same definitions as ``M``,
|
||||
except that the parameters will be replaced by the values in the body
|
||||
of ``N``. In this example, ``N`` provides just a single definition, ``f``.
|
||||
|
||||
Note that the only purpose of the body of ``N`` (the declarations
|
||||
after the ``where`` keyword) is to define the parameters for ``M``.
|
||||
|
||||
|
||||
Parameterized Instantiations
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
It is possible for a module instantiation to be itself parameterized.
|
||||
This could be useful if we need to define some of a module's parameters
|
||||
but not others.
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
// A parameterized module
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : #
|
||||
x : [n]
|
||||
y : [n]
|
||||
|
||||
f : [n]
|
||||
f = x + y
|
||||
|
||||
|
||||
// A parameterized instantiation
|
||||
module N = M where
|
||||
|
||||
parameter
|
||||
x : [32]
|
||||
|
||||
type n = 32
|
||||
y = helper
|
||||
|
||||
helper = 12
|
||||
|
||||
In this case ``N`` has a single parameter ``x``. The result of instantiating
|
||||
``N`` would result in instantiating ``M`` using the value of ``x`` and ``12``
|
||||
for the value of ``y``.
|
||||
|
||||
|
||||
Importing Parameterized Modules
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
It is also possible to import a parameterized module without using
|
||||
a module instantiation:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
module M where
|
||||
|
||||
parameter
|
||||
x : [8]
|
||||
y : [8]
|
||||
|
||||
f : [8]
|
||||
f = x + y
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
module N where
|
||||
|
||||
import `M
|
||||
|
||||
g = f { x = 2, y = 3 }
|
||||
|
||||
A *backtick* at the start of the name of an imported module indicates
|
||||
that we are importing a parameterized module. In this case, Cryptol
|
||||
will import all definitions from the module as usual, however every
|
||||
definition will have some additional parameters corresponding to
|
||||
the parameters of a module. All value parameters are grouped in a record.
|
||||
|
||||
This is why in the example ``f`` is applied to a record of values,
|
||||
even though its definition in ``M`` does not look like a function.
|
||||
helper = 12
|
||||
|
||||
The declarations in the ``where`` block are treated as the
|
||||
definition of an anonymous module which is passed as the argument
|
||||
to parameterized module ``M``.
|
||||
|
||||
|
||||
|
||||
Binary file not shown.
File diff suppressed because one or more lines are too long
@ -9,12 +9,12 @@
|
||||
-- Portability : portable
|
||||
|
||||
{- A utility for spliting a long column of stuff into multiple columns. -}
|
||||
import Data.List(transpose)
|
||||
import Data.List(transpose,sort)
|
||||
|
||||
rs = 4 -- number of rows per column
|
||||
spacing = 4 -- blanks between columns
|
||||
|
||||
main = interact (unlines . map concat . transpose . map toCol . chop rs . lines)
|
||||
main = interact (unlines . map concat . transpose . map toCol . chop rs . sort . lines)
|
||||
|
||||
colWidth xs = spacing + maximum (0 : map length xs)
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user