Expressions
===========
This section provides an overview of the Cryptol's expression syntax.
Calling Functions
-----------------
.. code-block:: cryptol
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)`
Prefix Operators
-----------------
.. code-block:: cryptol
-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`
Infix Functions
-----------------
.. code-block:: cryptol
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
Type Annotations
-----------------
Explicit type annotations may be added on expressions, patterns, and
in argument definitions.
.. code-block:: cryptol
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]`
f (x : [8]) = x + 1 // type annotation on patterns
.. todo::
Patterns with type variables
Explicit Type Instantiation
----------------------------
If ``f`` is a polymorphic value with type:
.. code-block:: cryptol
f : { tyParam } tyParam
f = zero
you can evaluate ``f``, passing it a type parameter:
.. code-block:: cryptol
f `{ tyParam = 13 }
Local Declarations
------------------
Local declarations have the weakest precedence of all expressions.
.. code-block:: cryptol
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`
Block Arguments
---------------
When used as the last argument to a function call,
``if`` and lambda expressions do not need parens:
.. code-block:: cryptol
f \x -> x // call `f` with one argument `x -> x`
2 + if x
then y
else z // call `+` with two arguments: `2` and `if ...`
Conditionals
------------
The ``if ... then ... else`` construct can be used with
multiple branches. For example:
.. code-block:: cryptol
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
Demoting Numeric Types to Values
--------------------------------
The value corresponding to a numeric type may be accessed using the
following notation:
.. code-block:: cryptol
`t
Here `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:
.. code-block:: cryptol
`t : {a} (Literal t a) => a
This backtick notation is syntax sugar for an application of the
`number` primtive, so the above may be written as:
.. code-block:: cryptol
number`{t} : {a} (Literal t a) => a
If a type cannot be inferred from context, a suitable type will be
automatically chosen if possible, usually `Integer`.