Modules
=======

A *module* is used to group related definitions.  Each file may
contain at most one top-level module.

.. code-block:: cryptol

  module M where

  type T = [8]

  f : [8]
  f = 10


Hierarchical Module Names
-------------------------

Modules may have either simple or *hierarchical* names.
Hierarchical names are constructed by gluing together ordinary
identifiers using the symbol ``::``.

.. code-block:: cryptol

  module Hash::SHA256 where

  sha256 = ...

The structure in the name may be used to group together related
modules. The Cryptol implementation uses the structure of the
name to locate the file containing the module definition.
For example, when searching for module ``Hash::SHA256``, Cryptol
will look for a file named ``SHA256.cry`` in a directory called
``Hash``, contained in one of the directories specified by ``CRYPTOLPATH``.


Module Imports
--------------

To use the definitions from one module in another module, we use
``import`` declarations:


.. code-block:: cryptol
  :caption: module M

  // Provide some definitions
  module M where

  f : [8]
  f = 2


.. code-block:: cryptol
  :caption: module N

  // Uses definitions from `M`
  module N where

  import M  // import all definitions from `M`

  g = f   // `f` was imported from `M`


Import Lists
~~~~~~~~~~~~

Sometimes, we may want to import only some of the definitions
from a module.  To do so, we use an import declaration with
an *import list*.

.. code-block:: cryptol

  module M where

  f = 0x02
  g = 0x03
  h = 0x04

.. code-block:: cryptol

  module N where

  import M(f,g)  // Imports only `f` and `g`, but not `h`

  x = f + g

Using explicit import lists helps reduce name collisions.
It also tends to make code easier to understand,  because
it makes it easy to see the source of definitions.


Hiding Imports
~~~~~~~~~~~~~~

Sometimes a module may provide many definitions, and we want to use
most of them but with a few exceptions (e.g., because those would
result to a name clash).   In such situations it is convenient
to use a *hiding* import:

.. code-block:: cryptol
  :caption: module M

  module M where

  f = 0x02
  g = 0x03
  h = 0x04


.. code-block:: cryptol
  :caption: module N

  module N where

  import M hiding (h) // Import everything but `h`

  x = f + g



Qualified Module Imports
~~~~~~~~~~~~~~~~~~~~~~~~

Another way to avoid name collisions is by using a
*qualified* import.

.. code-block:: cryptol
  :caption: module M

  module M where

  f : [8]
  f = 2


.. code-block:: cryptol
  :caption: module N

  module N where

  import M as P

  g = P::f
  // `f` was imported from `M`
  // but when used it needs to be prefixed by the qualifier `P`

Qualified imports make it possible to work with definitions
that happen to have the same name but are defined in different modules.

Qualified imports may be combined with import lists or hiding clauses:

.. code-block:: cryptol
  :caption: Example

  import A as B (f)         // introduces B::f
  import X as Y hiding (f)  // introduces everything but `f` from X
                            // using the prefix `X`

It is also possible to use the same qualifier prefix for imports
from different modules.  For example:

.. code-block:: cryptol
  :caption: Example

  import A as B
  import X as B

Such declarations will introduces all definitions from ``A`` and ``X``
but to use them, you would have to qualify using the prefix ``B::``.


Private Blocks
--------------

In some cases, definitions in a module might use helper
functions that are not intended to be used outside the module.
It is good practice to place such declarations in *private blocks*:

.. code-block:: cryptol
  :caption: Private blocks

  module M where

  f : [8]
  f = 0x01 + helper1 + helper2

  private

    helper1 : [8]
    helper1 = 2

    helper2 : [8]
    helper2 = 3

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
extend to the end of the module.

.. code-block:: cryptol
  :caption: Private blocks

  module M where

  f : [8]
  f = 0x01 + helper1 + helper2

  private

  helper1 : [8]
  helper1 = 2

  helper2 : [8]
  helper2 = 3


The keyword ``private`` introduces a new layout scope, and all declarations
in the block are considered to be private to the module.  A single module
may contain multiple private blocks.  For example, the following module
is equivalent to the previous one:

.. code-block:: cryptol
  :caption: Private blocks

  module M where

  f : [8]
  f = 0x01 + helper1 + helper2

  private
    helper1 : [8]
    helper1 = 2

  private
    helper2 : [8]
    helper2 = 3


Nested Modules
--------------

Module may be declared within 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 submodule 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 submodule 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 be declared in the public or private sections of their
containing module, and must 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
---------------------

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, interface modules may be nested in
other modules:

.. code-block:: cryptol
  :caption: A nested interface module

  module M where

    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

Interface modules may contain ``type`` or ``type constraint`` synonyms:

.. code-block:: cryptol
  :caption: A nested interface module

  interface module I where

    type n : #      // `n` is a numeric type

    type W = [n]    // A type synonym, available when the interface is imported

    type constraint (fin n, n >= 1)
                    // Assumptions about the declared numeric type

    x : W           // A declarations of a constant;  uses type synonym.




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)
    x : [n]


  // This module is parameterized
  module F where
    import interface I

    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

A parameterized module is also called a *functor*, in the tradition
of module parameterization in languages like Standard ML and OCaml.


    
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.

To pass a nested module as the argument of a function,
use ``submodule I`` like this:

.. code-block:: cryptol
  :caption: Nested module instantiation.

  module M where

    import Somewhere // defines G and I

    submodule F = submodule G { submodule I }




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``.  The ``parameter``
may contain the same sort of declarations that may appear in interfaces.


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 notation
for instantiating a module:

.. code-block:: cryptol

  // A parameterized module
  module M where

    parameter
      type n : #
      x      : [n]
      y      : [n]

    f : [n]
    f = x + y


  // A module instantiation
  module N = M
    where
    type n = 32
    x      = 11
    y      = helper

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


Anonymous Import Instantiations
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

We provide syntactic sugar for importing and instantiating a functor
at the same time:

.. code-block:: cryptol

  submodule F where
    parameter
      x : [8]
    y = x + 1

  import submodule F where
    x = 2

The ``where`` block may is the same as the ``where`` block in
expressions:  you may define type synonyms and values, but nothing else
(e.g., no ``newtype``).

It is also possible to import and instantiate a functor with an existing module
like this:

.. code-block:: cryptol

  submodule F where
    parameter
      x : [8]
    y = x + 1

  submodule G where
    x = 7

  import submodule F { submodule G }


Semantically, instantiating imports declare a local nested module and
import it.  For example, the ``where`` import above is equivalent
to the following declarations:

.. code-block:: cryptol

  submodule F where

    parameter
      x : [8]

    y = x + 1


  submodule M where
    x = 2


  submodule N = submodule F { submodule M }


  import submodule N


Passing Through Module Parameters
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Occasionally it is useful to define a functor that instantiates *another*
functor using the same parameters as the functor being defined
(i.e., a functor parameter is passed on to another functor).  This can
be done by using the keyword ``interface`` followed by the name of a parameter
in an instantiation.  Here is an example:

.. code-block:: cryptol

  interface submodule S where
    x : [8]

  // A functor, parameterized on S
  submodule G where
    import interface submodule S
    y = x + 1

  // Another functor, also parameterize on S
  submodule F where
    import interface submodule S as A

    // Instantiate `G` using parameter `A` of `F`
    import submodule G { interface A }    // Brings `y` in scope

    z = A::x + y

  // Brings `z` into scope: z = A::x + y
  //                          = 5    + (5 + 1)
  //                          = 11
  import submodule F where
    x = 5


Instantiation by Parametrizing Declarations
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

It is also possible to instantiate a functor parameter *without* providing
an implementation module.  Instead, the declarations in the instantiated
module all get additional parameters corresponding to the functor's parameters.
This is done by providing ``_`` as the parameter to a functor:

.. code-block:: cryptol
  :caption: Instantiation by Parametrizing Declarations

  submodule F where
    parameter
      type n : #
      x : [n]

    f : (fin n) => [n] -> [n]
    f v = v + x

  submodule M = submodule F { _ }
  import submodule M as M

This example defines module ``M`` by instantiating ``F`` without
a parameter.  Here is the resulting type of ``f``:

.. code-block::

  Main> :t M::f
  M::f : {n} (fin n) => {x : [n]} -> [n] -> [n]

Note that ``f`` has a new type parameter ``n``, and a new value parameter
of a record type.  The type parameter ``n`` corresponds to the functor's
type parameter while the record parameter has one field for each value
parameter of the functor.

.. warning::

  The order in which type parameters are added to a declaration is not
  specified, so you'd have to use a *named* type application to apply
  a type explicitly.

Functors with multiple parameters may use ``_`` as argument for more
than one parameter, and may also provide implementations for some of
the parameters and use ``_`` for others.

**[Parameter Names]** The names of the parameters in the declarations
are the same as the names that are in scope, unless a parameter came
in through a qualified interface import (i.e., the interface import
uses the ``as`` clause).  In the case the name of the parameter is
computed by replacing the ``::`` with ``'`` because ``::`` may not appear
in type parameters or record fields.  For example, if a module had
a parameter ``I::x``, then its ``_`` instantiation will use a
record with a field named ``I'x``.

**[Restrictions]** There are some restrictions on functor parameters
that can be defined with ``_``:

  * The functor should not contain other functors nested in it.
    This is because it is unclear how to parameterize the parameters of
    nested functors.

  * All values coming through ``_`` parameters should have simple
    (i.e., non-polymorphic) types.  This is because Cryptol does not
    support records with polymorphic fields.

  * All types and values coming through ``_`` parameters should have
    distinct names.  This is because the fields in the record and
    type names use labels derived. Generally this should not be a
    problem unless a functor defined some parameters that have
    ``'`` in the middle.


**[Backtick Imports]** For backward compatibility, we also provide
syntactic sugar for importing a functor with a single interface parameter
and instantiating it:

.. code-block:: cryptol
  :caption: Backtick Import

  submodule F where
    parameter
      type n : #
      x : [n]

    f : (fin n) => [n] -> [n]
    f v = v + x

  import submodule `F

This is equivalent to writing:

.. code-block:: cryptol

  import submodule F { _ }

This, in turn, is syntactic sugar for creating an anonymous module:

.. code-block:: cryptol

  submodule M = F { _ }
  import submodule M