mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
Regenerate Syntax.tex from Syntax.md.
This commit is contained in:
parent
bf2a235c1c
commit
c62a88a8ec
@ -2,7 +2,8 @@
|
||||
% markdown in ../../Syntax.md. If you make changes, please make them
|
||||
% there and then regenerate the .tex file using the Makefile.
|
||||
|
||||
\section{Layout}\label{layout}
|
||||
\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
|
||||
@ -32,7 +33,8 @@ 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}
|
||||
\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
|
||||
@ -47,7 +49,8 @@ Examples:
|
||||
/* This is a /* Nested */ block comment */
|
||||
\end{verbatim}
|
||||
|
||||
\section{Identifiers}\label{identifiers}
|
||||
\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{\_}).
|
||||
@ -64,8 +67,9 @@ 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}}
|
||||
\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:
|
||||
@ -116,8 +120,9 @@ left\tabularnewline
|
||||
\bottomrule
|
||||
\end{longtable}
|
||||
|
||||
\hypertarget{built-in-type-level-operators}{%
|
||||
\section{Built-in Type-level
|
||||
Operators}\label{built-in-type-level-operators}
|
||||
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.
|
||||
@ -149,7 +154,8 @@ up)\tabularnewline
|
||||
\bottomrule
|
||||
\end{longtable}
|
||||
|
||||
\section{Numeric Literals}\label{numeric-literals}
|
||||
\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:
|
||||
@ -182,7 +188,84 @@ is inferred from context in which the literal is used. Examples:
|
||||
// a = Integer or [n] where n >= width 10
|
||||
\end{verbatim}
|
||||
|
||||
\section{Bits}\label{bits}
|
||||
\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`
|
||||
\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
|
||||
@ -213,7 +296,8 @@ Operator & Associativity & Description\tabularnewline
|
||||
\bottomrule
|
||||
\end{longtable}
|
||||
|
||||
\section{Multi-way Conditionals}\label{multi-way-conditionals}
|
||||
\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:
|
||||
@ -227,7 +311,8 @@ x = if y % 2 == 0 then 1
|
||||
else 7
|
||||
\end{verbatim}
|
||||
|
||||
\section{Tuples and Records}\label{tuples-and-records}
|
||||
\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
|
||||
@ -255,7 +340,8 @@ of record components is not important. Examples:
|
||||
{ x = 1, y = 2 } == { y = 2, x = 1 } // True
|
||||
\end{verbatim}
|
||||
|
||||
\subsection{Accessing Fields}\label{accessing-fields}
|
||||
\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
|
||||
@ -299,7 +385,8 @@ f p = x + y where
|
||||
(x, y) = p
|
||||
\end{verbatim}
|
||||
|
||||
\subsection{Updating Fields}\label{updating-fields}
|
||||
\hypertarget{updating-fields}{%
|
||||
\subsection{Updating Fields}\label{updating-fields}}
|
||||
|
||||
The components of a record or a tuple may be updated using the following
|
||||
notation:
|
||||
@ -322,7 +409,8 @@ n = { pt = r, size = 100 } // nested record
|
||||
{ n | pt.x -> x + 10 } == { pt = { x = 25, y = 20 }, size = 100 }
|
||||
\end{verbatim}
|
||||
|
||||
\section{Sequences}\label{sequences}
|
||||
\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
|
||||
@ -333,15 +421,19 @@ 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
|
||||
[e1,e2,e3] // A sequence with three elements
|
||||
|
||||
[t1 .. t3 ] // Sequence enumerations
|
||||
[t1, t2 .. t3 ] // Step by t2 - t1
|
||||
[e1 ... ] // Infinite sequence starting at e1
|
||||
[e1, e2 ... ] // Infinite sequence stepping by e2-e1
|
||||
[t1 .. t3 ] // Sequence enumerations
|
||||
[t1, t2 .. t3 ] // 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
|
||||
[ 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
|
||||
@ -383,14 +475,16 @@ There are also lifted pointwise operations.
|
||||
p1 # p2 // Split sequence pattern
|
||||
\end{verbatim}
|
||||
|
||||
\section{Functions}\label{functions}
|
||||
\hypertarget{functions}{%
|
||||
\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}
|
||||
\hypertarget{local-declarations}{%
|
||||
\section{Local Declarations}\label{local-declarations}}
|
||||
|
||||
\begin{verbatim}
|
||||
e where ds
|
||||
@ -400,7 +494,9 @@ 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}
|
||||
\hypertarget{explicit-type-instantiation}{%
|
||||
\section{Explicit Type
|
||||
Instantiation}\label{explicit-type-instantiation}}
|
||||
|
||||
If \texttt{f} is a polymorphic value with type:
|
||||
|
||||
@ -415,8 +511,9 @@ you can evaluate \texttt{f}, passing it a type parameter:
|
||||
f `{ tyParam = 13 }
|
||||
\end{verbatim}
|
||||
|
||||
\hypertarget{demoting-numeric-types-to-values}{%
|
||||
\section{Demoting Numeric Types to
|
||||
Values}\label{demoting-numeric-types-to-values}
|
||||
Values}\label{demoting-numeric-types-to-values}}
|
||||
|
||||
The value corresponding to a numeric type may be accessed using the
|
||||
following notation:
|
||||
@ -433,7 +530,8 @@ accommodate the value of the type:
|
||||
`t : {n} (fin n, n >= width t) => [n]
|
||||
\end{verbatim}
|
||||
|
||||
\section{Explicit Type Annotations}\label{explicit-type-annotations}
|
||||
\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.
|
||||
@ -446,19 +544,22 @@ p : t
|
||||
f (x : t) = ...
|
||||
\end{verbatim}
|
||||
|
||||
\section{Type Signatures}\label{type-signatures}
|
||||
\hypertarget{type-signatures}{%
|
||||
\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}
|
||||
\hypertarget{type-synonym-declarations}{%
|
||||
\section{Type Synonym Declarations}\label{type-synonym-declarations}}
|
||||
|
||||
\begin{verbatim}
|
||||
type T a b = [a] b
|
||||
\end{verbatim}
|
||||
|
||||
\section{Modules}\label{modules}
|
||||
\hypertarget{modules}{%
|
||||
\section{Modules}\label{modules}}
|
||||
|
||||
A \textbf{\emph{module}} is used to group some related definitions.
|
||||
|
||||
@ -471,7 +572,8 @@ f : [8]
|
||||
f = 10
|
||||
\end{verbatim}
|
||||
|
||||
\section{Hierarchical Module Names}\label{hierarchical-module-names}
|
||||
\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
|
||||
@ -490,7 +592,8 @@ 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}.
|
||||
|
||||
\section{Module Imports}\label{module-imports}
|
||||
\hypertarget{module-imports}{%
|
||||
\section{Module Imports}\label{module-imports}}
|
||||
|
||||
To use the definitions from one module in another module, we use
|
||||
\texttt{import} declarations:
|
||||
@ -511,7 +614,8 @@ import M // import all definitions from `M`
|
||||
g = f // `f` was imported from `M`
|
||||
\end{verbatim}
|
||||
|
||||
\section{Import Lists}\label{import-lists}
|
||||
\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
|
||||
@ -535,7 +639,8 @@ 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.
|
||||
|
||||
\section{Hiding Imports}\label{hiding-imports}
|
||||
\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
|
||||
@ -558,7 +663,8 @@ import M hiding (h) // Import everything but `h`
|
||||
x = f + g
|
||||
\end{verbatim}
|
||||
|
||||
\section{Qualified Module Imports}\label{qualified-module-imports}
|
||||
\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.
|
||||
@ -601,7 +707,8 @@ 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:::}.
|
||||
|
||||
\section{Private Blocks}\label{private-blocks}
|
||||
\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
|
||||
@ -642,7 +749,8 @@ private
|
||||
helper2 = 3
|
||||
\end{verbatim}
|
||||
|
||||
\section{Parameterized Modules}\label{parameterized-modules}
|
||||
\hypertarget{parameterized-modules}{%
|
||||
\section{Parameterized Modules}\label{parameterized-modules}}
|
||||
|
||||
\begin{verbatim}
|
||||
module M where
|
||||
@ -660,7 +768,9 @@ f : [n]
|
||||
f = 1 + x
|
||||
\end{verbatim}
|
||||
|
||||
\section{Named Module Instantiations}\label{named-module-instantiations}
|
||||
\hypertarget{named-module-instantiations}{%
|
||||
\section{Named Module
|
||||
Instantiations}\label{named-module-instantiations}}
|
||||
|
||||
One way to use a parameterized module is through a named instantiation:
|
||||
|
||||
@ -697,8 +807,9 @@ 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}
|
||||
Instantiations}\label{parameterized-instantiations}}
|
||||
|
||||
It is possible for a module instantiations to be itself parameterized.
|
||||
This could be useful if we need to define some of a module's parameters
|
||||
@ -733,8 +844,9 @@ 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}
|
||||
Modules}\label{importing-parameterized-modules}}
|
||||
|
||||
It is also possible to import a parameterized module without using a
|
||||
module instantiation:
|
||||
|
Loading…
Reference in New Issue
Block a user