cryptol/docs/ProgrammingCryptol/appendices/Syntax.tex
Rob Dockins d740442035 Update documenetation with new enumeration forms,
and update the reference semantics.
Other minor documentation fixes and updates.
2021-07-20 17:01:50 -07:00

1006 lines
29 KiB
TeX

% IMPORTANT: The file Syntax.tex is generated automatically from the
% markdown in ../../Syntax.md. If you make changes, please make them
% there and then regenerate the .tex file using the Makefile.
\hypertarget{layout}{%
\section{Layout}\label{layout}}
Groups of declarations are organized based on indentation. Declarations
with the same indentation belong to the same group. Lines of text that
are indented more than the beginning of a declaration belong to that
declaration, while lines of text that are indented less terminate a
group of declarations. Groups of declarations appear at the top level of
a Cryptol file, and inside \texttt{where} blocks in expressions. For
example, consider the following declaration group:
\begin{verbatim}
f x = x + y + z
where
y = x * x
z = x + y
g y = y
\end{verbatim}
This group has two declarations, one for \texttt{f} and one for
\texttt{g}. All the lines between \texttt{f} and \texttt{g} that are
indented more than \texttt{f} belong to \texttt{f}.
This example also illustrates how groups of declarations may be nested
within each other. For example, the \texttt{where} expression in the
definition of \texttt{f} starts another group of declarations,
containing \texttt{y} and \texttt{z}. This group ends just before
\texttt{g}, because \texttt{g} is indented less than \texttt{y} and
\texttt{z}.
\hypertarget{comments}{%
\section{Comments}\label{comments}}
Cryptol supports block comments, which start with \texttt{/*} and end
with \texttt{*/}, and line comments, which start with \texttt{//} and
terminate at the end of the line. Block comments may be nested
arbitrarily.
Examples:
\begin{verbatim}
/* This is a block comment */
// This is a line comment
/* This is a /* Nested */ block comment */
\end{verbatim}
\hypertarget{identifiers}{%
\section{Identifiers}\label{identifiers}}
Cryptol identifiers consist of one or more characters. The first
character must be either an English letter or underscore (\texttt{\_}).
The following characters may be an English letter, a decimal digit,
underscore (\texttt{\_}), or a prime (\texttt{\textquotesingle{}}). Some
identifiers have special meaning in the language, so they may not be
used in programmer-defined names (see
\protect\hyperlink{keywords-and-built-in-operators}{Keywords}).
Examples:
\begin{verbatim}
name name1 name' longer_name
Name Name2 Name'' longerName
\end{verbatim}
\hypertarget{keywords-and-built-in-operators}{%
\section{Keywords and Built-in
Operators}\label{keywords-and-built-in-operators}}
The following identifiers have special meanings in Cryptol, and may not
be used for programmer defined names:
\begin{verbatim}
else include property let infixl parameter
extern module then import infixr constraint
if newtype type as infix by
private pragma where hiding primitive down
\end{verbatim}
The following table contains Cryptol's operators and their associativity
with lowest precedence operators first, and highest precedence last.
\begin{longtable}[]{@{}ll@{}}
\caption{Operator precedences.}\tabularnewline
\toprule
Operator & Associativity \\
\midrule
\endfirsthead
\toprule
Operator & Associativity \\
\midrule
\endhead
\texttt{==\textgreater{}} & right \\
\texttt{\textbackslash{}/} & right \\
\texttt{/\textbackslash{}} & right \\
\texttt{==} \texttt{!=} \texttt{===} \texttt{!==} & not associative \\
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
\texttt{\textgreater{}=} \texttt{\textless{}\$}
\texttt{\textgreater{}\$} \texttt{\textless{}=\$}
\texttt{\textgreater{}=\$} & not associative \\
\texttt{\textbar{}\textbar{}} & right \\
\texttt{\^{}} & left \\
\texttt{\&\&} & right \\
\texttt{\#} & right \\
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}}
\texttt{\textgreater{}\textgreater{}\textgreater{}}
\texttt{\textless{}\textless{}\textless{}}
\texttt{\textgreater{}\textgreater{}\$} & left \\
\texttt{+} \texttt{-} & left \\
\texttt{*} \texttt{/} \texttt{\%} \texttt{/\$} \texttt{\%\$} & left \\
\texttt{\^{}\^{}} & right \\
\texttt{@} \texttt{@@} \texttt{!} \texttt{!!} & left \\
(unary) \texttt{-} \texttt{\textasciitilde{}} & right \\
\bottomrule
\end{longtable}
\hypertarget{built-in-type-level-operators}{%
\section{Built-in Type-level
Operators}\label{built-in-type-level-operators}}
Cryptol includes a variety of operators that allow computations on the
numeric types used to specify the sizes of sequences.
\begin{longtable}[]{@{}ll@{}}
\caption{Type-level operators}\tabularnewline
\toprule
Operator & Meaning \\
\midrule
\endfirsthead
\toprule
Operator & Meaning \\
\midrule
\endhead
\texttt{+} & Addition \\
\texttt{-} & Subtraction \\
\texttt{*} & Multiplication \\
\texttt{/} & Division \\
\texttt{/\^{}} & Ceiling division (\texttt{/} rounded up) \\
\texttt{\%} & Modulus \\
\texttt{\%\^{}} & Ceiling modulus (compute padding) \\
\texttt{\^{}\^{}} & Exponentiation \\
\texttt{lg2} & Ceiling logarithm (base 2) \\
\texttt{width} & Bit width (equal to \texttt{lg2(n+1)}) \\
\texttt{max} & Maximum \\
\texttt{min} & Minimum \\
\bottomrule
\end{longtable}
\hypertarget{numeric-literals}{%
\section{Numeric Literals}\label{numeric-literals}}
Numeric literals may be written in binary, octal, decimal, or
hexadecimal notation. The base of a literal is determined by its prefix:
\texttt{0b} for binary, \texttt{0o} for octal, no special prefix for
decimal, and \texttt{0x} for hexadecimal.
Examples:
\begin{verbatim}
254 // Decimal literal
0254 // Decimal literal
0b11111110 // Binary literal
0o376 // Octal literal
0xFE // Hexadecimal literal
0xfe // Hexadecimal literal
\end{verbatim}
Numeric literals in binary, octal, or hexadecimal notation result in bit
sequences of a fixed length (i.e., they have type \texttt{{[}n{]}} for
some \texttt{n}). The length is determined by the base and the number of
digits in the literal. Decimal literals are overloaded, and so the type
is inferred from context in which the literal is used. Examples:
\begin{verbatim}
0b1010 // : [4], 1 * number of digits
0o1234 // : [12], 3 * number of digits
0x1234 // : [16], 4 * number of digits
10 // : {a}. (Literal 10 a) => a
// a = Integer or [n] where n >= width 10
\end{verbatim}
Numeric literals may also be written as polynomials by writing a
polynomial expression in terms of \texttt{x} between an opening
\texttt{\textless{}\textbar{}} and a closing
\texttt{\textbar{}\textgreater{}}. Numeric literals in polynomial
notation result in bit sequences of length one more than the degree of
the polynomial. Examples:
\begin{verbatim}
<| x^^6 + x^^4 + x^^2 + x^^1 + 1 |> // : [7], equal to 0b1010111
<| x^^4 + x^^3 + x |> // : [5], equal to 0b11010
\end{verbatim}
Cryptol also supports fractional literals using binary (prefix
\texttt{0b}), octal (prefix \texttt{0o}), decimal (no prefix), and
hexadecimal (prefix \texttt{ox}) digits. A fractional literal must
contain a \texttt{.} and may optionally have an exponent. The base of
the exponent for binary, octal, and hexadecimal literals is 2 and the
exponent is marked using the symbol \texttt{p}. Decimal fractional
literals use exponent base 10, and the symbol \texttt{e}. Examples:
\begin{verbatim}
10.2
10.2e3 // 10.2 * 10^3
0x30.1 // 3 * 64 + 1/16
0x30.1p4 // (3 * 64 + 1/16) * 2^4
\end{verbatim}
All fractional literals are overloaded and may be used with types that
support fractional numbers (e.g., \texttt{Rational}, and the
\texttt{Float} family of types).
Some types (e.g.~the \texttt{Float} family) cannot represent all
fractional literals precisely. Such literals are rejected statically
when using binary, octal, or hexadecimal notation. When using decimal
notation, the literal is rounded to the closest representable even
number.
All numeric literals may also include \texttt{\_}, which has no effect
on the literal value but may be used to improve readability. Here are
some examples:
\begin{verbatim}
0b_0000_0010
0x_FFFF_FFEA
\end{verbatim}
\hypertarget{expressions}{%
\section{Expressions}\label{expressions}}
This section provides an overview of the Cryptol's expression syntax.
\textbf{Calling Functions}
\begin{verbatim}
f 2 // call `f` with parameter `2`
g x y // call `g` with two parameters: `x` and `y`
h (x,y) // call `h` with one parameter, the pair `(x,y)`
\end{verbatim}
\textbf{Prefix Operators}
\begin{verbatim}
-2 // call unary `-` with parameter `2`
- 2 // call unary `-` with parameter `2`
f (-2) // call `f` with one argument: `-2`, parens are important
-f 2 // call unary `-` with parameter `f 2`
- f 2 // call unary `-` with parameter `f 2`
\end{verbatim}
\textbf{Infix Functions}
\begin{verbatim}
2 + 3 // call `+` with two parameters: `2` and `3`
2 + 3 * 5 // call `+` with two parameters: `2` and `3 * 5`
(+) 2 3 // call `+` with two parameters: `2` and `3`
f 2 + g 3 // call `+` with two parameters: `f 2` and `g 3`
- 2 + - 3 // call `+` with two parameters: `-2` and `-3`
- f 2 + - g 3
\end{verbatim}
\textbf{Type Annotations}
\begin{verbatim}
x : Bit // specify that `x` has type `Bit`
f x : Bit // specify that `f x` has type `Bit`
- f x : [8] // specify that `- f x` has type `[8]`
2 + 3 : [8] // specify that `2 + 3` has type `[8]`
\x -> x : [8] // type annotation is on `x`, not the function
if x
then y
else z : Bit // the type annotation is on `z`, not the whole `if`
[1..9 : [8]] // specify that elements in `[1..9]` have type `[8]`
\end{verbatim}
\textbf{Local Declarations}
Local declarations have the weakest precedence of all expressions.
\begin{verbatim}
2 + x : [T]
where
type T = 8
x = 2 // `T` and `x` are in scope of `2 + x : `[T]`
if x then 1 else 2
where x = 2 // `x` is in scope in the whole `if`
\y -> x + y
where x = 2 // `y` is not in scope in the defintion of `x`
\end{verbatim}
\textbf{Block Arguments}
When used as the last argument to a function call, \texttt{if} and
lambda expressions do not need parens:
\begin{verbatim}
f \x -> x // call `f` with one argument `x -> x`
2 + if x
then y
else z // call `+` with two arguments: `2` and `if ...`
\end{verbatim}
\hypertarget{bits}{%
\section{Bits}\label{bits}}
The type \texttt{Bit} has two inhabitants: \texttt{True} and
\texttt{False}. These values may be combined using various logical
operators, or constructed as results of comparisons.
\begin{longtable}[]{@{}lll@{}}
\caption{Bit operations.}\tabularnewline
\toprule
Operator & Associativity & Description \\
\midrule
\endfirsthead
\toprule
Operator & Associativity & Description \\
\midrule
\endhead
\texttt{==\textgreater{}} & right & Short-cut implication \\
\texttt{\textbackslash{}/} & right & Short-cut or \\
\texttt{/\textbackslash{}} & right & Short-cut and \\
\texttt{!=} \texttt{==} & none & Not equals, equals \\
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
\texttt{\textgreater{}=} \texttt{\textless{}\$}
\texttt{\textgreater{}\$} \texttt{\textless{}=\$}
\texttt{\textgreater{}=\$} & none & Comparisons \\
\texttt{\textbar{}\textbar{}} & right & Logical or \\
\texttt{\^{}} & left & Exclusive-or \\
\texttt{\&\&} & right & Logical and \\
\texttt{\textasciitilde{}} & right & Logical negation \\
\bottomrule
\end{longtable}
\hypertarget{multi-way-conditionals}{%
\section{Multi-way Conditionals}\label{multi-way-conditionals}}
The \texttt{if\ ...\ then\ ...\ else} construct can be used with
multiple branches. For example:
\begin{verbatim}
x = if y % 2 == 0 then 22 else 33
x = if y % 2 == 0 then 1
| y % 3 == 0 then 2
| y % 5 == 0 then 3
else 7
\end{verbatim}
\hypertarget{tuples-and-records}{%
\section{Tuples and Records}\label{tuples-and-records}}
Tuples and records are used for packaging multiple values together.
Tuples are enclosed in parentheses, while records are enclosed in curly
braces. The components of both tuples and records are separated by
commas. The components of tuples are expressions, while the components
of records are a label and a value separated by an equal sign. Examples:
\begin{verbatim}
(1,2,3) // A tuple with 3 component
() // A tuple with no components
{ x = 1, y = 2 } // A record with two fields, `x` and `y`
{} // A record with no fields
\end{verbatim}
The components of tuples are identified by position, while the
components of records are identified by their label, and so the ordering
of record components is not important for most purposes. Examples:
\begin{verbatim}
(1,2) == (1,2) // True
(1,2) == (2,1) // False
{ x = 1, y = 2 } == { x = 1, y = 2 } // True
{ x = 1, y = 2 } == { y = 2, x = 1 } // True
\end{verbatim}
Ordering on tuples and records is defined lexicographically. Tuple
components are compared in the order they appear, whereas record fields
are compared in alphabetical order of field names.
\hypertarget{accessing-fields}{%
\subsection{Accessing Fields}\label{accessing-fields}}
The components of a record or a tuple may be accessed in two ways: via
pattern matching or by using explicit component selectors. Explicit
component selectors are written as follows:
\begin{verbatim}
(15, 20).0 == 15
(15, 20).1 == 20
{ x = 15, y = 20 }.x == 15
\end{verbatim}
Explicit record selectors may be used only if the program contains
sufficient type information to determine the shape of the tuple or
record. For example:
\begin{verbatim}
type T = { sign : Bit, number : [15] }
// Valid definition:
// the type of the record is known.
isPositive : T -> Bit
isPositive x = x.sign
// Invalid definition:
// insufficient type information.
badDef x = x.f
\end{verbatim}
The components of a tuple or a record may also be accessed using pattern
matching. Patterns for tuples and records mirror the syntax for
constructing values: tuple patterns use parentheses, while record
patterns use braces. Examples:
\begin{verbatim}
getFst (x,_) = x
distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
f p = x + y where
(x, y) = p
\end{verbatim}
Selectors are also lifted through sequence and function types,
point-wise, so that the following equations should hold:
\begin{verbatim}
xs.l == [ x.l | x <- xs ] // sequences
f.l == \x -> (f x).l // functions
\end{verbatim}
Thus, if we have a sequence of tuples, \texttt{xs}, then we can quickly
obtain a sequence with only the tuples' first components by writing
\texttt{xs.0}.
Similarly, if we have a function, \texttt{f}, that computes a tuple of
results, then we can write \texttt{f.0} to get a function that computes
only the first entry in the tuple.
This behavior is quite handy when examining complex data at the REPL.
\hypertarget{updating-fields}{%
\subsection{Updating Fields}\label{updating-fields}}
The components of a record or a tuple may be updated using the following
notation:
\begin{verbatim}
// Example values
r = { x = 15, y = 20 } // a record
t = (True,True) // a tuple
n = { pt = r, size = 100 } // nested record
// Setting fields
{ r | x = 30 } == { x = 30, y = 20 }
{ t | 0 = False } == (False,True)
// Update relative to the old value
{ r | x -> x + 5 } == { x = 20, y = 20 }
// Update a nested field
{ n | pt.x = 10 } == { pt = { x = 10, y = 20 }, size = 100 }
{ n | pt.x -> x + 10 } == { pt = { x = 25, y = 20 }, size = 100 }
\end{verbatim}
\hypertarget{sequences}{%
\section{Sequences}\label{sequences}}
A sequence is a fixed-length collection of elements of the same type.
The type of a finite sequence of length \texttt{n}, with elements of
type \texttt{a} is \texttt{{[}n{]}\ a}. Often, a finite sequence of
bits, \texttt{{[}n{]}\ Bit}, is called a \emph{word}. We may abbreviate
the type \texttt{{[}n{]}\ Bit} as \texttt{{[}n{]}}. An infinite sequence
with elements of type \texttt{a} has type \texttt{{[}inf{]}\ a}, and
\texttt{{[}inf{]}} is an infinite stream of bits.
\begin{verbatim}
[e1,e2,e3] // A sequence with three elements
[t1 .. t2] // Enumeration
[t1 .. <t2] // Enumeration (exclusive bound)
[t1 .. t2 by n] // Enumeration (stride)
[t1 .. <t2 by n] // Enumeration (stride, ex. bound)
[t1 .. t2 down by n] // Enumeration (downward stride)
[t1 .. >t2 down by n] // Enumeration (downward stride, ex. bound)
[t1, t2 .. t3] // Enumeration (step by t2 - t1)
[e1 ...] // Infinite sequence starting at e1
[e1, e2 ...] // Infinite sequence stepping by e2-e1
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
| p21 <- e21, p22 <- e22 ]
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
\end{verbatim}
Note: the bounds in finite sequences (those with \texttt{..}) are type
expressions, while the bounds in infinite sequences are value
expressions.
\begin{longtable}[]{@{}ll@{}}
\caption{Sequence operations.}\tabularnewline
\toprule
Operator & Description \\
\midrule
\endfirsthead
\toprule
Operator & Description \\
\midrule
\endhead
\texttt{\#} & Sequence concatenation \\
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} &
Shift (right, left) \\
\texttt{\textgreater{}\textgreater{}\textgreater{}}
\texttt{\textless{}\textless{}\textless{}} & Rotate (right, left) \\
\texttt{\textgreater{}\textgreater{}\$} & Arithmetic right shift (on
bitvectors only) \\
\texttt{@} \texttt{!} & Access elements (front, back) \\
\texttt{@@} \texttt{!!} & Access sub-sequence (front, back) \\
\texttt{update} \texttt{updateEnd} & Update the value of a sequence at a
location (front, back) \\
\texttt{updates} \texttt{updatesEnd} & Update multiple values of a
sequence (front, back) \\
\bottomrule
\end{longtable}
There are also lifted pointwise operations.
\begin{verbatim}
[p1, p2, p3, p4] // Sequence pattern
p1 # p2 // Split sequence pattern
\end{verbatim}
\hypertarget{functions}{%
\section{Functions}\label{functions}}
\begin{verbatim}
\p1 p2 -> e // Lambda expression
f p1 p2 = e // Function definition
\end{verbatim}
\hypertarget{local-declarations}{%
\section{Local Declarations}\label{local-declarations}}
\begin{verbatim}
e where ds
\end{verbatim}
Note that by default, any local declarations without type signatures are
monomorphized. If you need a local declaration to be polymorphic, use an
explicit type signature.
\hypertarget{explicit-type-instantiation}{%
\section{Explicit Type
Instantiation}\label{explicit-type-instantiation}}
If \texttt{f} is a polymorphic value with type:
\begin{verbatim}
f : { tyParam } tyParam
f = zero
\end{verbatim}
you can evaluate \texttt{f}, passing it a type parameter:
\begin{verbatim}
f `{ tyParam = 13 }
\end{verbatim}
\hypertarget{demoting-numeric-types-to-values}{%
\section{Demoting Numeric Types to
Values}\label{demoting-numeric-types-to-values}}
The value corresponding to a numeric type may be accessed using the
following notation:
\begin{verbatim}
`t
\end{verbatim}
Here \texttt{t} should be a finite type expression with numeric kind.
The resulting expression will be of a numeric base type, which is
sufficiently large to accommodate the value of the type:
\begin{verbatim}
`t : {a} (Literal t a) => a
\end{verbatim}
This backtick notation is syntax sugar for an application of the
\texttt{number} primtive, so the above may be written as:
\begin{verbatim}
number`{t} : {a} (Literal t a) => a
\end{verbatim}
If a type cannot be inferred from context, a suitable type will be
automatically chosen if possible, usually \texttt{Integer}.
\hypertarget{explicit-type-annotations}{%
\section{Explicit Type Annotations}\label{explicit-type-annotations}}
Explicit type annotations may be added on expressions, patterns, and in
argument definitions.
\begin{verbatim}
e : t
p : t
f (x : t) = ...
\end{verbatim}
\hypertarget{type-signatures}{%
\section{Type Signatures}\label{type-signatures}}
\begin{verbatim}
f,g : {a,b} (fin a) => [a] b
\end{verbatim}
\hypertarget{type-synonyms-and-newtypes}{%
\section{Type Synonyms and Newtypes}\label{type-synonyms-and-newtypes}}
\hypertarget{type-synonyms}{%
\subsection{Type synonyms}\label{type-synonyms}}
\begin{verbatim}
type T a b = [a] b
\end{verbatim}
A \texttt{type} declaration creates a synonym for a pre-existing type
expression, which may optionally have arguments. A type synonym is
transparently unfolded at use sites and is treated as though the user
had instead written the body of the type synonym in line. Type synonyms
may mention other synonyms, but it is not allowed to create a recursive
collection of type synonyms.
\hypertarget{newtypes}{%
\subsection{Newtypes}\label{newtypes}}
\begin{verbatim}
newtype NewT a b = { seq : [a]b }
\end{verbatim}
A \texttt{newtype} declaration declares a new named type which is
defined by a record body. Unlike type synonyms, each named
\texttt{newtype} is treated as a distinct type by the type checker, even
if they have the same bodies. Moreover, types created by a
\texttt{newtype} declaration will not be members of any typeclasses,
even if the record defining their body would be. For the purposes of
typechecking, two newtypes are considered equal only if all their
arguments are equal, even if the arguments do not appear in the body of
the newtype, or are otherwise irrelevant. Just like type synonyms,
newtypes are not allowed to form recursive groups.
Every \texttt{newtype} declaration brings into scope a new function with
the same name as the type which can be used to create values of the
newtype.
\begin{verbatim}
x : NewT 3 Integer
x = NewT { seq = [1,2,3] }
\end{verbatim}
Just as with records, field projections can be used directly on values
of newtypes to extract the values in the body of the type.
\begin{verbatim}
> sum x.seq
6
\end{verbatim}
\hypertarget{modules}{%
\section{Modules}\label{modules}}
A \textbf{\emph{module}} is used to group some related definitions. Each
file may contain at most one module.
\begin{verbatim}
module M where
type T = [8]
f : [8]
f = 10
\end{verbatim}
\hypertarget{hierarchical-module-names}{%
\section{Hierarchical Module Names}\label{hierarchical-module-names}}
Module may have either simple or \textbf{\emph{hierarchical}} names.
Hierarchical names are constructed by gluing together ordinary
identifiers using the symbol \texttt{::}.
\begin{verbatim}
module Hash::SHA256 where
sha256 = ...
\end{verbatim}
The structure in the name may be used to group together related modules.
Also, the Cryptol implementation uses the structure of the name to
locate the file containing the definition of the module. For example,
when searching for module \texttt{Hash::SHA256}, Cryptol will look for a
file named \texttt{SHA256.cry} in a directory called \texttt{Hash},
contained in one of the directories specified by \texttt{CRYPTOLPATH}.
\hypertarget{module-imports}{%
\section{Module Imports}\label{module-imports}}
To use the definitions from one module in another module, we use
\texttt{import} declarations:
\begin{verbatim}
// Provide some definitions
module M where
f : [8]
f = 2
// Uses definitions from `M`
module N where
import M // import all definitions from `M`
g = f // `f` was imported from `M`
\end{verbatim}
\hypertarget{import-lists}{%
\section{Import Lists}\label{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
\textbf{\emph{import list}}.
\begin{verbatim}
module M where
f = 0x02
g = 0x03
h = 0x04
module N where
import M(f,g) // Imports only `f` and `g`, but not `h`
x = f + g
\end{verbatim}
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.
\hypertarget{hiding-imports}{%
\section{Hiding Imports}\label{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
\textbf{\emph{hiding}} import:
module M where
\begin{verbatim}
f = 0x02
g = 0x03
h = 0x04
module N where
import M hiding (h) // Import everything but `h`
x = f + g
\end{verbatim}
\hypertarget{qualified-module-imports}{%
\section{Qualified Module Imports}\label{qualified-module-imports}}
Another way to avoid name collisions is by using a
\textbf{\emph{qualified}} import.
\begin{verbatim}
module M where
f : [8]
f = 2
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`
\end{verbatim}
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:
\begin{verbatim}
import A as B (f) // introduces B::f
import X as Y hiding (f) // introduces everything but `f` from X
// using the prefix `X`
\end{verbatim}
It is also possible to use the same qualifier prefix for imports from
different modules. For example:
\begin{verbatim}
import A as B
import X as B
\end{verbatim}
Such declarations will introduces all definitions from \texttt{A} and
\texttt{X} but to use them, you would have to qualify using the prefix
\texttt{B:::}.
\hypertarget{private-blocks}{%
\section{Private Blocks}\label{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 \textbf{\emph{private blocks}}:
\begin{verbatim}
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
helper2 : [8]
helper2 = 3
\end{verbatim}
The keyword \texttt{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:
\begin{verbatim}
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
private
helper2 : [8]
helper2 = 3
\end{verbatim}
\hypertarget{parameterized-modules}{%
\section{Parameterized Modules}\label{parameterized-modules}}
\begin{verbatim}
module M where
parameter
type n : # // `n` is a numeric type parameter
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
\end{verbatim}
\hypertarget{named-module-instantiations}{%
\section{Named Module
Instantiations}\label{named-module-instantiations}}
One way to use a parameterized module is through a named instantiation:
\begin{verbatim}
// 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
\end{verbatim}
The second module, \texttt{N}, is computed by instantiating the
parameterized module \texttt{M}. Module \texttt{N} will provide the
exact same definitions as \texttt{M}, except that the parameters will be
replaced by the values in the body of \texttt{N}. In this example,
\texttt{N} provides just a single definition, \texttt{f}.
Note that the only purpose of the body of \texttt{N} (the declarations
after the \texttt{where} keyword) is to define the parameters for
\texttt{M}.
\hypertarget{parameterized-instantiations}{%
\section{Parameterized
Instantiations}\label{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.
\begin{verbatim}
// 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
\end{verbatim}
In this case \texttt{N} has a single parameter \texttt{x}. The result of
instantiating \texttt{N} would result in instantiating \texttt{M} using
the value of \texttt{x} and \texttt{12} for the value of \texttt{y}.
\hypertarget{importing-parameterized-modules}{%
\section{Importing Parameterized
Modules}\label{importing-parameterized-modules}}
It is also possible to import a parameterized module without using a
module instantiation:
\begin{verbatim}
module M where
parameter
x : [8]
y : [8]
f : [8]
f = x + y
module N where
import `M
g = f { x = 2, y = 3 }
\end{verbatim}
A \textbf{\emph{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 \texttt{f} is applied to a record of values,
even though its definition in \texttt{M} does not look like a function.