.. _Modules:

************************************************************
Modules
************************************************************


Top Level Modules
==================================================

A module is a compilation unit. It is part of a package. It contains an
implementation file ``<name>.al`` and an interface file ``<name>.ali``.

A module consist of a use block and a series of declarations.



Use Block
--------------------------------------------------

The use block indicates which other modules are used by the current module.
::

    use
        <mod₁>                  -- modules of the same package
        <mod₂>
        alba
            standard            -- some modules of package 'alba.standard' used
                natural         -- used modules of the package 'alba.standard'
                list
                array
                ...
            browser
                virtual-dom
                ...
            ...
        ...

The order of the used modules is not relevant. If a used module already uses
some other modules publicly (i.e. uses it in its interface file), then the other
modules are used implicitly by the current module. This avoids cluttering up the
use block.




.. _Declarations:

Declarations
--------------------------------------------------

A declaration block consists of zero or more declarations.  A declaration is one
of:

- :ref:`Inductive Type <Inductive Types>`
- :ref:`Function Declaration <Functions>` (or constants)
- :ref:`Section <Sections>`
- :ref:`Inner Module <Inner Modules>`
- :ref:`Mutually Inductive Types <Mutually Inductive>`
- :ref:`Mutually Recursive Functions <Mutually Recursive>`


In a module interface functions and constants can be declared without
definition. In that case the definition (or implementation) of a function /
constant is not visible to the clients.

Inductive data types and their constructors can be declared in a module
interface as constants without definition as well. In that case the user of the
module does not know, that the type is an inductive type and cannot pattern
match on objects of that type.



Interface and Implementation File
--------------------------------------------------

The implementation file of a module must implement all types, constants and
functions declared in its interface file. If the interface file defines
everything completely, then the implementation file is not necessary.




.. _Inner Modules:

Inner Modules
==================================================


An inner module is a module within a module. It has no use bock. Only
implementation files can have inner modules.

Syntax::

    module
        <declaration₁>          -- publicly visible declarations
        <declaration₂>
        ...
    :=
        <declaration₁>          -- private definitions and implementations
        <declaration₂>          -- for the public declarations
        ...