CryptolModuleSystem

Cryptol's Module System

Cryptol has a simple module system, used to organize code, manage names, and avoid name conflicts.

Module Declarations

A module is a collection of declarations. Some of the declarations may be public, which means that they are available for use in other modules. Other declarations may be private, which means that they are only available to be used by other declarations in the module. A module declarations has the following structure:

module ModuleName where

ImportDelcarations

Declarations

For example, here is what a typical module might look like:

module MyModule where
     
import ThatOneModule
import TheOtherModule

myFun x      = x + 0x10
myOtherFun y = y + myFun y

Public and Private Declarations

By default, all declarations in a module are public, which means that they may be used in other modules. Sometimes, it is convenient to define declarations that are not visible in other modules, for example, to avoid name clashes, or to make it explicit that some declarations are not part of the module's interface. This is done using the keyword ''private'':

module A where

x = y + z

private
  y = 0x10
  z = 0x20

In this example, the module A contains one public name, x, and two private ones: y, and z. Multiple private declarations may be written either in the same block, or in multiple blocks, for example, like this:

module A where

x = y + z

private
  y = 0x10

private
  z = 0x20

Import Declarations

An import declaration is used to specify that one module uses some of the declarations in another module. Import declarations are written at the top of a module, right after the where following the module's name. In general, an import declaration has the following structure:

import ModuleName OptionalQualifier OptionalImportList

Simple Imports

The simplest form of an import is as follows:

import ModuleName

This means that all public names defined in module ModuleName are now in scope in the current module. Here is an example:

module A where
  x = 0x10
  y = 0x20

module B where
  import A
  z = x + y

If a name used in the program may be resolved via an import from two different modules, then the program is ambiguous and should be rejected. However, declarations in the current module will "shadow" imported names so, effectively, they take precedence. For example, consider the following two modules:

module A where
  x = 0x10
  y = 0x20

module B where
  import A
  x = 0x00
  z = x + y

These two modules are well formed, and the value of z defined in module B will evaluate to 0x20, because x will refer to the locally defined x, and y will be imported from A.