cryptol/docs/ProgrammingCryptol/appendices/Syntax.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 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}.

\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{\textquotesingle{}}). 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:

\todo[inline]{ The table below can be generated by running
  \texttt{chop.hs} on this list: else extern if private include module newtype pragma property then type where let import as hiding newtype  infixl infixr infix primitive parameter constraint }

\begin{verbatim}
else       include    property    let       newtype    primitive
extern     module     then        import    infixl     parameter
if         newtype    type        as        infixr     constraint
private    pragma     where       hiding    infix
\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@{}}
\caption{Operator precedences.}\tabularnewline
\toprule
Operator & Associativity\tabularnewline
\midrule
\endfirsthead
\toprule
Operator & Associativity\tabularnewline
\midrule
\endhead
\texttt{-\textgreater{}} (types) & right\tabularnewline
\texttt{==\textgreater{}} & right\tabularnewline
\texttt{\textbackslash{}/} & right\tabularnewline
\texttt{/\textbackslash{}} & right\tabularnewline
\texttt{==} \texttt{!=} \texttt{===} \texttt{!===} & not associative\tabularnewline
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=} \texttt{\textgreater{}=}
\texttt{\textgreater{}\$} \texttt{\textless{}\$} \texttt{\textless{}=\$} \texttt{\textgreater{}=\$}
& not associative\tabularnewline
\texttt{\textbar{}\textbar{}} & right\tabularnewline
\texttt{\^{}} & left\tabularnewline
\texttt{\&\&} & right\tabularnewline
\texttt{\#} & right\tabularnewline
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}}
\texttt{\textgreater{}\textgreater{}\textgreater{}}
\texttt{\textless{}\textless{}\textless{}}
\texttt{\textgreater{}\textgreater{}\$} & left\tabularnewline
\texttt{+} \texttt{-} & left\tabularnewline
\texttt{*} \texttt{/} \texttt{\%} & left\tabularnewline
\texttt{\^{}\^{}} & right\tabularnewline
\texttt{@} \texttt{@@} \texttt{!} \texttt{!!} & left\tabularnewline
(unary) \texttt{-} \texttt{\textasciitilde{}} & right\tabularnewline
\bottomrule
\end{longtable}

\hyperdef{}{built-in-type-operators}{\section{Built-in Type-level
Operators}\label{built-in-type-operators}}

Cryptol includes a variety of operators that allow computations on
the numeric types used to specify the sizes of sequences.

\begin{longtable}[c]{@{}ll@{}}
\caption{Type-level operators}\tabularnewline
\toprule
Operator & Meaning\tabularnewline
\midrule
\endfirsthead
\toprule
Operator & Meaning\tabularnewline
\midrule
\endhead
\texttt{+} & Size addition\tabularnewline
\texttt{-} & Size subtraction\tabularnewline
\texttt{*} & Size multiplication\tabularnewline
\texttt{/} & Size division\tabularnewline
\verb+/^+ & Size ceiling division (\texttt{/} rounded up)\tabularnewline
\verb+%+ & Size modulus\tabularnewline
\verb+%^+ & Size ceiling modulus (\verb+%+ rounded up)\tabularnewline
\verb+^^+ & Size exponentiation\tabularnewline
\texttt{lg2} & Size logarithm (base-2)\tabularnewline
\texttt{width} & Size width (\texttt{lg2} rounded up)\tabularnewline
\texttt{max} & Size maximum\tabularnewline
\texttt{min} & Size minimum\tabularnewline
\bottomrule
\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 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}

\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@{}}
\caption{Bit operations.}\tabularnewline
\toprule
Operator & Associativity & Description\tabularnewline
\midrule
\endfirsthead
\toprule
Operator & Associativity & Description\tabularnewline
\midrule
\endhead
\texttt{\textbar{}\textbar{}} & right & Logical or\tabularnewline
\texttt{\&\&} & right & Logical and\tabularnewline
\texttt{!=} \texttt{==} & none & Not equals, equals\tabularnewline
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
\texttt{\textgreater{}=} & none & Comparisons\tabularnewline
\texttt{\^{}} & left & Exclusive-or\tabularnewline
\texttt{\textasciitilde{}} & right & Logical negation\tabularnewline
\bottomrule
\end{longtable}

\section{Multi-way Conditionals}\label{multiway-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}

\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. 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 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}

\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

[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@{}}
\caption{Sequence operations.}\tabularnewline
\toprule
Operator & Description\tabularnewline
\midrule
\endfirsthead
\toprule
Operator & Description\tabularnewline
\midrule
\endhead
\texttt{\#} & Sequence concatenation\tabularnewline
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} &
Shift (right, left)\tabularnewline
\texttt{\textgreater{}\textgreater{}\textgreater{}}
\texttt{\textless{}\textless{}\textless{}} & Rotate
(right, left)\tabularnewline
\texttt{@} \texttt{!} & Access elements (front, back)\tabularnewline
\texttt{@@} \texttt{!!} & Access sub-sequence
(front, back)\tabularnewline
\texttt{update} \texttt{updateEnd} & Update the value of a sequence at a location (front, back)\tabularnewline
\texttt{updates} \texttt{updatesEnd} & Update multiple values of a sequence (front, back)\tabularnewline
\bottomrule
\end{longtable}

There are also lifted pointwise 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 } tyParam
f = zero
\end{verbatim}

you can evaluate \texttt{f}, passing it a type parameter:

\begin{verbatim}
f `{ tyParam = 13 }
\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
accommodate the value of the type:

\begin{verbatim}
`t : {a} (fin a, a >= width t} => [a]
\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}

\section{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}

\section{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 \textit{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.


\section{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 \textit{hiding} import:


\begin{verbatim}
   module M where

    f = 0x02
    g = 0x03
    h = 0x04



    module N where

    import M hiding (h) // Import everything but `h`

    x = f + g
\end{verbatim}



\section{Qualified Module Imports}

Another way to avoid name collisions is by using a
\textit{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 qualified `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 the 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:::}.


\section{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 \textit{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} introduce 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}


\section{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}


\section{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}.


\section{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
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}.


\section{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 \textit{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.