mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-24 08:24:19 +03:00
284338c938
When `:set mono-binds=on`, any local definitions lacking type signatures will not be generalized (i.e., will be monomorphic). This reduces what is in most cases unnecessary polymorphism that can give rise to constraints that are difficult to solve. This also improves the performance of the Cryptol interpreter by lifting many polymorphic type applications out of the inner loops that are commonly defined as bindings in `where` clauses. The flag is on by default in the Cryptol REPL, and in most cases makes it possible to leave out more type signatures in `where` clauses than before. However, some programs really do rely on inferring polymorphic types for local variables; in this case adding an explicit polymorphic type signature to the local binding in question will make the program typecheck.
392 lines
12 KiB
TeX
392 lines
12 KiB
TeX
\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 declaration. 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 declaration, one for \texttt{f} and one for
|
|
\texttt{g}. All the lines between \texttt{f} and \texttt{g} that are
|
|
indented more then \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}.
|
|
|
|
\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}
|
|
|
|
\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{'}). Some identifiers have
|
|
special meaning in the language, so they may not be used in
|
|
programmer-defined names (see
|
|
\hyperref[keywords-and-built-in-operators]{Keywords}).
|
|
|
|
Examples:
|
|
|
|
\begin{verbatim}
|
|
name name1 name' longer_name
|
|
Name Name2 Name'' longerName
|
|
\end{verbatim}
|
|
|
|
\hyperdef{}{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}
|
|
Arith Inf extern inf module then
|
|
Bit True fin lg2 newtype type
|
|
Cmp else if max pragma where
|
|
False export import min property width
|
|
\end{verbatim}
|
|
|
|
The following table contains Cryptol's operators and their associativity
|
|
with lowest precedence operators first, and highest precedence last.
|
|
|
|
\begin{longtable}[c]{@{}ll@{}}
|
|
\toprule\addlinespace
|
|
Operator & Associativity
|
|
\\\addlinespace
|
|
\midrule\endhead
|
|
\texttt{\textbar{}\textbar{}} & left
|
|
\\\addlinespace
|
|
\texttt{\^{}} & left
|
|
\\\addlinespace
|
|
\texttt{\&\&} & left
|
|
\\\addlinespace
|
|
\texttt{-\textgreater{}} (types) & right
|
|
\\\addlinespace
|
|
\texttt{!=} \texttt{==} & not associative
|
|
\\\addlinespace
|
|
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
|
|
\texttt{\textgreater{}=} & not associative
|
|
\\\addlinespace
|
|
\texttt{\#} & right
|
|
\\\addlinespace
|
|
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}}
|
|
\texttt{\textgreater{}\textgreater{}\textgreater{}}
|
|
\texttt{\textless{}\textless{}\textless{}} & left
|
|
\\\addlinespace
|
|
\texttt{+} \texttt{-} & left
|
|
\\\addlinespace
|
|
\texttt{*} \texttt{/} \texttt{\%} & left
|
|
\\\addlinespace
|
|
\texttt{\^{}\^{}} & right
|
|
\\\addlinespace
|
|
\texttt{!} \texttt{!!} \texttt{@} \texttt{@@} & left
|
|
\\\addlinespace
|
|
(unary) \texttt{-} \texttt{\textasciitilde{}} & right
|
|
\\\addlinespace
|
|
\bottomrule
|
|
\addlinespace
|
|
\caption{Operator precedences.}
|
|
\end{longtable}
|
|
|
|
\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 represent finite bit sequences (i.e., they have type
|
|
\texttt{{[}n{]}}). Using binary, octal, and hexadecimal notation results
|
|
in bit sequences of a fixed length, depending on the number of digits in
|
|
the literal. Decimal literals are overloaded, and so the length of the
|
|
sequence 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 // : {n}. (fin n, n >= 4) => [n]
|
|
// (need at least 4 bits)
|
|
|
|
0 // : {n}. (fin n) => [n]
|
|
\end{verbatim}
|
|
|
|
\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}[c]{@{}lll@{}}
|
|
\toprule\addlinespace
|
|
Operator & Associativity & Description
|
|
\\\addlinespace
|
|
\midrule\endhead
|
|
\texttt{\textbar{}\textbar{}} & left & Logical or
|
|
\\\addlinespace
|
|
\texttt{\^{}} & left & Exclusive-or
|
|
\\\addlinespace
|
|
\texttt{\&\&} & left & Logical and
|
|
\\\addlinespace
|
|
\texttt{!=} \texttt{==} & none & Not equals, equals
|
|
\\\addlinespace
|
|
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
|
|
\texttt{\textgreater{}=} & none & Comparisons
|
|
\\\addlinespace
|
|
\texttt{\textasciitilde{}} & right & Logical negation
|
|
\\\addlinespace
|
|
\bottomrule
|
|
\addlinespace
|
|
\caption{Bit operations.}
|
|
\end{longtable}
|
|
|
|
\section{If Then Else with Multiway}\label{if-then-else-with-multiway}
|
|
|
|
\texttt{If then else} has been extended to support multi-way
|
|
conditionals. Examples:
|
|
|
|
\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}
|
|
|
|
\section{Tuples and Records}\label{tuples-and-records}
|
|
|
|
Tuples and records are used for packaging multiples values together.
|
|
Tuples are enclosed in parenthesis, while records are enclosed in
|
|
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 fileds
|
|
\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. 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}
|
|
|
|
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 defintion:
|
|
// the type of the record is known.
|
|
isPositive : T -> Bit
|
|
isPositive x = x.sign
|
|
|
|
// Invalid defintion:
|
|
// insufficient type information.
|
|
badDef x = x.f
|
|
\end{verbatim}
|
|
|
|
The components of a tuple or a record may also be access by using
|
|
pattern matching. Patterns for tuples and records mirror the syntax for
|
|
constructing values: tuple patterns use parenthesis, while record
|
|
patterns use braces. Examples:
|
|
|
|
\begin{verbatim}
|
|
getFst (x,_) = x
|
|
|
|
distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
|
|
|
|
f x = fst + snd where
|
|
\end{verbatim}
|
|
|
|
\section{Sequences}\label{sequences}
|
|
|
|
A sequence is a fixed-length collection of element 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
|
|
|
|
[t .. ] // Sequence enumerations
|
|
[t1, t2 .. ] // Step by t2 - t1
|
|
[t1 .. t3 ]
|
|
[t1, t2 .. t3 ]
|
|
[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 ]
|
|
\end{verbatim}
|
|
|
|
Note: the bounds in finite unbounded (those with ..) sequences are type
|
|
expressions, while the bounds in bounded-finite and infinite sequences
|
|
are value expressions.
|
|
|
|
\begin{longtable}[c]{@{}ll@{}}
|
|
\toprule\addlinespace
|
|
Operator & Description
|
|
\\\addlinespace
|
|
\midrule\endhead
|
|
\texttt{\#} & Sequence concatenation
|
|
\\\addlinespace
|
|
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} &
|
|
Shift (right,left)
|
|
\\\addlinespace
|
|
\texttt{\textgreater{}\textgreater{}\textgreater{}}
|
|
\texttt{\textless{}\textless{}\textless{}} & Rotate (right,left)
|
|
\\\addlinespace
|
|
\texttt{@} \texttt{!} & Access elements (front,back)
|
|
\\\addlinespace
|
|
\texttt{@@} \texttt{!!} & Access sub-sequence (front,back)
|
|
\\\addlinespace
|
|
\bottomrule
|
|
\addlinespace
|
|
\caption{Sequence operations.}
|
|
\end{longtable}
|
|
|
|
There are also lifted point-wise operations.
|
|
|
|
\begin{verbatim}
|
|
[p1, p2, p3, p4] // Sequence pattern
|
|
p1 # p2 // Split sequence pattern
|
|
\end{verbatim}
|
|
|
|
\section{Functions}\label{functions}
|
|
|
|
\begin{verbatim}
|
|
\p1 p2 -> e // Lambda expression
|
|
f p1 p2 = e // Function definition
|
|
\end{verbatim}
|
|
|
|
\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.
|
|
|
|
\section{Explicit Type Instantiation}\label{explicit-type-instantiation}
|
|
|
|
If \texttt{f} is a polymorphic value with type:
|
|
|
|
\begin{verbatim}
|
|
f : { tyParam }
|
|
|
|
f `{ tyParam = t }
|
|
\end{verbatim}
|
|
|
|
\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 type expression with numeric kind. The
|
|
resulting expression is a finite word, which is sufficiently large to
|
|
accomodate the value of the type:
|
|
|
|
\begin{verbatim}
|
|
`{t} :: {w >= width t}. [w]
|
|
\end{verbatim}
|
|
|
|
\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}
|
|
|
|
\section{Type Signatures}\label{type-signatures}
|
|
|
|
\begin{verbatim}
|
|
f,g : {a,b} (fin a) => [a] b
|
|
\end{verbatim}
|
|
|
|
\section{Type Synonym Declarations}\label{type-synonym-declarations}
|
|
|
|
\begin{verbatim}
|
|
type T a b = [a] b
|
|
\end{verbatim}
|