mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
1006 lines
29 KiB
TeX
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.
|