GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-17 09:50:35 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into ffi

Browse Source
This commit is contained in:
Bretton 2022-08-05 14:36:59 -07:00
commit 5c2a409b36
51 changed files with 18708 additions and 16263 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
.github/workflows/ci.yml vendored
View File

@ -9,7 +9,7 @@ on:
workflow_dispatch:
env:
SOLVER_PKG_VERSION: "snapshot-20220114"
SOLVER_PKG_VERSION: "snapshot-20220721"
# The CACHE_VERSION can be updated to force the use of a new cache if
# the current cache contents become corrupted/invalid. This can
# sometimes happen when (for example) the OS version is changed but
@ -58,7 +58,7 @@ jobs:
strategy:
fail-fast: false
matrix:
os: [ubuntu-20.04, macos-10.15, windows-2019]
os: [ubuntu-20.04, macos-12, windows-2019]
ghc-version: ["8.8.4", "8.10.7", "9.0.2", "9.2.2"]
exclude:
# https://gitlab.haskell.org/ghc/ghc/-/issues/18550
@ -196,14 +196,14 @@ jobs:
- uses: actions/upload-artifact@v2
with:
name: ${{ env.NAME }}
name: ${{ env.NAME }} (GHC ${{ matrix.ghc-version }})
path: "${{ env.NAME }}.tar.gz*"
if-no-files-found: error
retention-days: ${{ needs.config.outputs.retention-days }}
- uses: actions/upload-artifact@v2
with:
name: ${{ env.NAME }}-with-solvers
name: ${{ env.NAME }}-with-solvers (GHC ${{ matrix.ghc-version }})
path: "${{ env.NAME }}-with-solvers.tar.gz*"
if-no-files-found: error
retention-days: ${{ needs.config.outputs.retention-days }}
@ -223,7 +223,7 @@ jobs:
- uses: actions/upload-artifact@v2
if: runner.os == 'Windows'
with:
name: ${{ env.NAME }}
name: ${{ env.NAME }} (GHC ${{ matrix.ghc-version }})
path: "cryptol.msi*"
if-no-files-found: error
retention-days: ${{ needs.config.outputs.retention-days }}
@ -236,7 +236,7 @@ jobs:
matrix:
suite: [test-lib]
target: ${{ fromJson(needs.build.outputs.test-lib-json) }}
os: [ubuntu-20.04, macos-10.15, windows-2019]
os: [ubuntu-20.04, macos-12, windows-2019]
continue-on-error: [false]
include:
- suite: rpc
@ -245,7 +245,7 @@ jobs:
continue-on-error: false
#- suite: rpc
# target: ''
# os: macos-10.05
# os: macos-12
# continue-on-error: false
#- suite: rpc
# target: ''

4
README.md
View File

@ -46,7 +46,7 @@ Cryptol currently uses Microsoft Research's [Z3 SMT
solver](https://github.com/Z3Prover/z3) by default to solve constraints
during type checking, and as the default solver for the `:sat` and
`:prove` commands. Cryptol generally requires the most recent version
of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20220114).
of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20220721).
You can download Z3 binaries for a variety of platforms from their
[releases page](https://github.com/Z3Prover/z3/releases). If you
@ -74,7 +74,7 @@ on [GitHub](https://github.com/GaloisInc/cryptol).
Cryptol builds and runs on various flavors of Linux, Mac OS X, and
Windows. We regularly build and test it in the following environments:
- macOS 10.15, 64-bit
- macOS 12, 64-bit
- Ubuntu 18.04, 64-bit
- Ubuntu 20.04, 64-bit
- Windows Server 2019, 64-bit

2
cryptol-remote-api/src/CryptolServer/Sat.hs
View File

@ -67,7 +67,7 @@ proveSat (ProveSatParams queryType (ProverName proverName) jsonExpr hConsing) =
ProverCommand
{ pcQueryType = queryType
, pcProverName = proverName
, pcVerbose = True
, pcVerbose = False
, pcProverStats = timing
, pcExtraDecls = decls
, pcSmtFile = Nothing

283
docs/RefMan/BasicSyntax.rst Normal file
View File

@ -0,0 +1,283 @@
Basic Syntax
============
Declarations
------------
.. code-block:: cryptol
f x = x + y + z
Type Signatures
---------------
.. code-block:: cryptol
f,g : {a,b} (fin a) => [a] b
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. Consider, for example,
the following Cryptol declarations:
.. code-block:: cryptol
f x = x + y + z
where
y = x * x
z = x + y
g y = y
This group has two declarations, one for `f` and one for `g`. All the
lines between `f` and `g` that are indented more than `f` belong to
`f`. The same principle applies to the declarations in the ``where`` block
of `f`, which defines two more local names, `y` and `z`.
Comments
--------
Cryptol supports block comments, which start with ``/*`` and end with
``*/``, and line comments, which start with ``//`` and terminate at the
end of the line. Block comments may be nested arbitrarily.
.. code-block:: cryptol
/* This is a block comment */
// This is a line comment
/* This is a /* Nested */ block comment */
.. todo::
Document ``/** */``
Identifiers
-----------
Cryptol identifiers consist of one or more characters. The first
character must be either an English letter or underscore (``_``). The
following characters may be an English letter, a decimal digit,
underscore (``_``), or a prime (``'``). Some identifiers have special
meaning in the language, so they may not be used in programmer-defined
names (see `Keywords and Built-in Operators`_).
.. code-block:: cryptol
:caption: Examples of identifiers
name name1 name' longer_name
Name Name2 Name'' longerName
Keywords and Built-in Operators
-------------------------------
The following identifiers have special meanings in Cryptol, and may
not be used for programmer defined names:
.. The table below can be generated by running `chop.hs` on this list:
else
extern
if
private
include
module
submodule
interface
newtype
pragma
property
then
type
where
let
import
as
hiding
infixl
infixr
infix
primitive
parameter
constraint
down
by
.. _Keywords:
.. code-block:: none
:caption: Keywords
as extern include interface parameter property where
by hiding infix let pragma submodule else
constraint if infixl module primitive then
down import infixr newtype private type
The following table contains Cryptol's operators and their
associativity with lowest precedence operators first, and highest
precedence last.
.. table:: Operator precedences
+-----------------------------------------+-----------------+
| Operator | Associativity |
+=========================================+=================+
| ``==>`` | right |
+-----------------------------------------+-----------------+
| ``\/`` | right |
+-----------------------------------------+-----------------+
| ``/\`` | right |
+-----------------------------------------+-----------------+
| ``==`` ``!=`` ``===`` ``!==`` | not associative |
+-----------------------------------------+-----------------+
| ``>`` ``<`` ``<=`` ``>=`` | not associative |
| ``<$`` ``>$`` ``<=$`` ``>=$`` | |
+-----------------------------------------+-----------------+
| ``||`` | right |
+-----------------------------------------+-----------------+
| ``^`` | left |
+-----------------------------------------+-----------------+
| ``&&`` | right |
+-----------------------------------------+-----------------+
| ``#`` | right |
+-----------------------------------------+-----------------+
| ``>>`` ``<<`` ``>>>`` ``<<<`` ``>>$`` | left |
+-----------------------------------------+-----------------+
| ``+`` ``-`` | left |
+-----------------------------------------+-----------------+
| ``*`` ``/`` ``%`` ``/$`` ``%$`` | left |
+-----------------------------------------+-----------------+
| ``^^`` | right |
+-----------------------------------------+-----------------+
| ``@`` ``@@`` ``!`` ``!!`` | left |
+-----------------------------------------+-----------------+
| (unary) ``-`` ``~`` | right |
+-----------------------------------------+-----------------+
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.
.. table:: Type-level operators
+------------+----------------------------------------+
| Operator | Meaning |
+============+========================================+
| ``+`` | Addition |
+------------+----------------------------------------+
| ``-`` | Subtraction |
+------------+----------------------------------------+
| ``*`` | Multiplication |
+------------+----------------------------------------+
| ``/`` | Division |
+------------+----------------------------------------+
| ``/^`` | Ceiling division (``/`` rounded up) |
+------------+----------------------------------------+
| ``%`` | Modulus |
+------------+----------------------------------------+
| ``%^`` | Ceiling modulus (compute padding) |
+------------+----------------------------------------+
| ``^^`` | Exponentiation |
+------------+----------------------------------------+
| ``lg2`` | Ceiling logarithm (base 2) |
+------------+----------------------------------------+
| ``width`` | Bit width (equal to ``lg2(n+1)``) |
+------------+----------------------------------------+
| ``max`` | Maximum |
+------------+----------------------------------------+
| ``min`` | Minimum |
+------------+----------------------------------------+
Numeric Literals
----------------
Numeric literals may be written in binary, octal, decimal, or
hexadecimal notation. The base of a literal is determined by its prefix:
``0b`` for binary, ``0o`` for octal, no special prefix for
decimal, and ``0x`` for hexadecimal.
.. code-block:: cryptol
:caption: Examples of literals
254 // Decimal literal
0254 // Decimal literal
0b11111110 // Binary literal
0o376 // Octal literal
0xFE // Hexadecimal literal
0xfe // Hexadecimal literal
Numeric literals in binary, octal, or hexadecimal notation result in
bit sequences of a fixed length (i.e., they have type ``[n]`` for
some `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:
.. code-block:: cryptol
:caption: Literals and their types
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
Numeric literals may also be written as polynomials by writing a polynomial
expression in terms of `x` between an opening ``<|`` and a closing ``|>``.
Numeric literals in polynomial notation result in bit sequences of length
one more than the degree of the polynomial. Examples:
.. code-block:: cryptol
:caption: Polynomial literals
<| x^^6 + x^^4 + x^^2 + x^^1 + 1 |> // : [7], equal to 0b1010111
<| x^^4 + x^^3 + x |> // : [5], equal to 0b11010
Cryptol also supports fractional literals using binary (prefix ``0b``),
octal (prefix ``0o``), decimal (no prefix), and hexadecimal (prefix ``ox``)
digits. A fractional literal must contain a ``.`` 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 ``p``.
Decimal fractional literals use exponent base 10, and the symbol ``e``.
Examples:
.. code-block:: cryptol
:caption: Fractional literals
10.2
10.2e3 // 10.2 * 10^3
0x30.1 // 3 * 64 + 1/16
0x30.1p4 // (3 * 64 + 1/16) * 2^4
All fractional literals are overloaded and may be used with types that support
fractional numbers (e.g., ``Rational``, and the ``Float`` family of types).
Some types (e.g. the ``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 ``_``, which has no effect on the
literal value but may be used to improve readability. Here are some examples:
.. code-block:: cryptol
:caption: Using _
0b_0000_0010
0x_FFFF_FFEA

211
docs/RefMan/BasicTypes.rst Normal file
View File

@ -0,0 +1,211 @@
Basic Types
===========
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:
.. code-block:: cryptol
(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
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:
.. code-block:: cryptol
(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
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.
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:
.. code-block:: cryptol
(15, 20).0 == 15
(15, 20).1 == 20
{ x = 15, y = 20 }.x == 15
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:
.. code-block:: cryptol
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
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:
.. code-block:: cryptol
getFst (x,_) = x
distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
f p = x + y where
(x, y) = p
Selectors are also lifted through sequence and function types, point-wise,
so that the following equations should hold:
.. code-block:: cryptol
xs.l == [ x.l | x <- xs ] // sequences
f.l == \x -> (f x).l // functions
Thus, if we have a sequence of tuples, ``xs``, then we can quickly obtain a
sequence with only the tuples' first components by writing ``xs.0``.
Similarly, if we have a function, ``f``, that computes a tuple of results,
then we can write ``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.
Updating Fields
~~~~~~~~~~~~~~~
The components of a record or a tuple may be updated using the following
notation:
.. code-block:: cryptol
// 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 }
Sequences
---------
A sequence is a fixed-length collection of elements of the same type.
The type of a finite sequence of length `n`, with elements of type `a`
is ``[n] a``. Often, a finite sequence of bits, ``[n] Bit``, is called a
*word*. We may abbreviate the type ``[n] Bit`` as ``[n]``. An infinite
sequence with elements of type `a` has type ``[inf] a``, and ``[inf]`` is
an infinite stream of bits.
.. code-block:: cryptol
[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
Note: the bounds in finite sequences (those with `..`) are type
expressions, while the bounds in infinite sequences are value
expressions.
.. table:: Sequence operations.
+------------------------------+---------------------------------------------+
| Operator | Description |
+==============================+=============================================+
| ``#`` | Sequence concatenation |
+------------------------------+---------------------------------------------+
| ``>>`` ``<<`` | Shift (right, left) |
+------------------------------+---------------------------------------------+
| ``>>>`` ``<<<`` | Rotate (right, left) |
+------------------------------+---------------------------------------------+
| ``>>$`` | Arithmetic right shift (on bitvectors only) |
+------------------------------+---------------------------------------------+
| ``@`` ``!`` | Access elements (front, back) |
+------------------------------+---------------------------------------------+
| ``@@`` ``!!`` | Access sub-sequence (front, back) |
+------------------------------+---------------------------------------------+
| ``update`` ``updateEnd`` | Update the value of a sequence at |
| | a location |
| | (front, back) |
+------------------------------+---------------------------------------------+
| ``updates`` ``updatesEnd`` | Update multiple values of a sequence |
| | (front, back) |
+------------------------------+---------------------------------------------+
There are also lifted pointwise operations.
.. code-block:: cryptol
[p1, p2, p3, p4] // Sequence pattern
p1 # p2 // Split sequence pattern
Functions
---------
.. code-block:: cryptol
\p1 p2 -> e // Lambda expression
f p1 p2 = e // Function definition

162
docs/RefMan/Expressions.rst Normal file
View File

@ -0,0 +1,162 @@
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`.

730
docs/RefMan/Modules.rst Normal file
View File

@ -0,0 +1,730 @@
Modules
=======
A *module* is used to group some related definitions. Each file may
contain at most one top-level module.
.. code-block:: cryptol
module M where
type T = [8]
f : [8]
f = 10
Hierarchical Module Names
-------------------------
Module may have either simple or *hierarchical* names.
Hierarchical names are constructed by gluing together ordinary
identifiers using the symbol ``::``.
.. code-block:: cryptol
module Hash::SHA256 where
sha256 = ...
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 ``Hash::SHA256``, Cryptol
will look for a file named ``SHA256.cry`` in a directory called
``Hash``, contained in one of the directories specified by ``CRYPTOLPATH``.
Module Imports
--------------
To use the definitions from one module in another module, we use
``import`` declarations:
.. code-block:: cryptol
:caption: module M
// Provide some definitions
module M where
f : [8]
f = 2
.. code-block:: cryptol
:caption: module N
// Uses definitions from `M`
module N where
import M // import all definitions from `M`
g = f // `f` was imported from `M`
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 *import list*.
.. code-block:: cryptol
module M where
f = 0x02
g = 0x03
h = 0x04
.. code-block:: cryptol
module N where
import M(f,g) // Imports only `f` and `g`, but not `h`
x = f + g
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.
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 *hiding* import:
.. code-block:: cryptol
:caption: module M
module M where
f = 0x02
g = 0x03
h = 0x04
.. code-block:: cryptol
:caption: module N
module N where
import M hiding (h) // Import everything but `h`
x = f + g
Qualified Module Imports
~~~~~~~~~~~~~~~~~~~~~~~~
Another way to avoid name collisions is by using a
*qualified* import.
.. code-block:: cryptol
:caption: module M
module M where
f : [8]
f = 2
.. code-block:: cryptol
:caption: module N
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`
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:
.. code-block:: cryptol
:caption: Example
import A as B (f) // introduces B::f
import X as Y hiding (f) // introduces everything but `f` from X
// using the prefix `X`
It is also possible to use the same qualifier prefix for imports
from different modules. For example:
.. code-block:: cryptol
:caption: Example
import A as B
import X as B
Such declarations will introduces all definitions from ``A`` and ``X``
but to use them, you would have to qualify using the prefix ``B::``.
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 *private blocks*:
.. code-block:: cryptol
:caption: Private blocks
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
helper2 : [8]
helper2 = 3
The private block only needs to be indented if it might be followed by
additional public declarations. If all remaining declarations are to be
private then no additional indentation is needed as the ``private`` block will
extend to the end of the module.
.. code-block:: cryptol
:caption: Private blocks
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
helper2 : [8]
helper2 = 3
The keyword ``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:
.. code-block:: cryptol
:caption: Private blocks
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
private
helper2 : [8]
helper2 = 3
Nested Modules
--------------
Module may be declared withing other modules, using the ``submodule`` keword.
.. code-block:: cryptol
:caption: Declaring a nested module called N
module M where
x = 0x02
submodule N where
y = x + 2
Submodules may refer to names in their enclosing scope.
Declarations in a sub-module will shadow names in the outer scope.
Declarations in a submdule may be imported with ``import submodule``,
which works just like an ordinary import except that ``X`` refers
to the name of a submodule.
.. code-block:: cryptol
:caption: Using declarations from a submodule.
module M where
x = 0x02
submodule N where
y = x + 2
import submodule N as P
z = 2 * P::y
Note that recursive definitions across modules are not allowed.
So, in the previous example, it would be an error if ``y`` was
to try to use ``z`` in its definition.
Implicit Imports
~~~~~~~~~~~~~~~~
For convenience, we add an implicit qualified submodule import for
each locally defined submodules.
.. code-block:: cryptol
:caption: Making use of the implicit import for a submodule.
module M where
x = 0x02
submodule N where
y = x + 2
z = 2 * N::y
``N::y`` works in the previous example because Cryptol added
an implicit import ``import submoulde N as N``.
Managing Module Names
~~~~~~~~~~~~~~~~~~~~~
The names of nested modules are managed by the module system just
like the name of any other declaration in Cryptol. Thus, nested
modules may declared in the public or private sections of their
containing module, and need to be imported before they can be used.
Thus, to use a submodule defined in top-level module ``A`` into
another top-level module ``B`` requires two steps:
1. First we need to import ``A`` to bring the name of the submodule in scope
2. Then we need to import the submodule to bring the names defined in it in scope.
.. code-block:: cryptol
:caption: Using a nested module from a different top-level module.
module A where
x = 0x02
submodule N where
y = x + 2
module B where
import A // Brings `N` in scope
import submodule N // Brings `y` in scope
z = 2 * y
Parameterized Modules
---------------------
.. warning::
The documentation in this section is for the upcoming variant of
the feature, which is not yet part of main line Cryptol.
Interface Modules
~~~~~~~~~~~~~~~~~
An *interface module* describes the content of a module
without providing a concrete implementation.
.. code-block:: cryptol
:caption: An interface module.
interface module I where
type n : # // `n` is a numeric type
type constraint (fin n, n >= 1)
// Assumptions about the declared numeric type
x : [n] // A declarations of a constant
Like other modules, interfaces modules may be nested in
other modules:
.. code-block:: cryptol
:caption: A nested interface module
module M where
interface submodule I where
type n : # // `n` is a numeric type
type constraint (fin n, n >= 1)
// Assumptions about the declared numeric type
x : [n] // A declarations of a constant
Importing an Interface Module
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A module may be parameterized by importing an interface,
instead of a concrete module
.. code-block:: cryptol
:caption: A parameterized module
// The interface desribes the parmaeters
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
// This module is parameterized
module F where
import interface I
y : [n]
y = x + 1
To import a nested interface use ``import interface sumbodule I``
and make sure that ``I`` is in scope.
It is also possible to import multiple interface modules,
or the same interface module more than once. Each import
of an interface module maybe be linked to a different concrete
module, as described in :ref:`instantiating_modules`.
.. code-block:: cryptol
:caption: Multiple interface parameters
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
module F where
import interface I as I
import interface I as J
y : [I::n]
y = I::x + 1
z : [J::n]
z = J::x + 1
Interface Constraints
~~~~~~~~~~~~~~~~~~~~~
When working with multiple interfaces, it is to useful
to be able to impose additional constraints on the
types imported from the interface.
.. code-block:: cryptol
:caption: Adding constraints to interface parameters
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
module F where
import interface I as I
import interface I as J
interface constraint (I::n == J::n)
y : [I::n]
y = I::x + J::x
In this example we impose the constraint that ``n``
(the width of ``x``) in both interfaces must be the
same. Note that, of course, the two instantiations
may provide different values for ``x``.
.. _instantiating_modules:
Instantiating a Parameterized Module
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To use a parameterized module we need to provide concrete
implementations for the interfaces that it uses, and provide
a name for the resulting module. This is done as follows:
.. code-block:: cryptol
:caption: Instantiating a parameterized module using a single interface.
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
module F where
import interface I
y : [n]
y = x + 1
module Impl where
type n = 8
x = 26
module MyF = F { Impl }
Here we defined a new module called ``MyF`` which is
obtained by filling in module ``Impl`` for the interface
used by ``F``.
If a module is parameterized my multiple interfaces
we need to provide an implementation module for each
interface, using a slight variation on the previous notation.
.. code-block:: cryptol
:caption: Instantiating a parameterized module by name.
// I is defined as above
module F where
import interface I as I
import interface I as J
interface constraint (I::n == J::n)
y : [I::n]
y = I::x + J::x
module Impl1 where
type n = 8
x = 26
module Impl2 where
type n = 8
x = 30
module MyF = F { I = Impl1, J = Impl 2 }
Each interface import is identified by its name,
which is derived from the ``as`` clause on the
interface import. If there is no ``as`` clause,
then the name of the parameter is derived from
the name of the interface itself.
Since interfaces are identified by name, the
order in which they are provided is not important.
Modules defined by instantiation may be nested,
just like any other module:
.. code-block:: cryptol
:caption: Nested module instantiation.
module M where
import Somewhere // defines G
submodule F = submodule G { I }
In this example, ``submodule F`` is defined
by instantiating some other parameterized
module ``G``, presumably imported from ``Somewhere``.
Note that in this case the argument to the instantiation
``I`` is a top-level module, because it is not
preceded by the ``submodule`` keyword.
To pass a nested module as the argument of a function,
use ``submodule I`` like this:
.. code-block:: cryptol
:caption: Nested module instantiation.
module M where
import Somewhere // defines G and I
submodule F = submodule G { submodule I }
Anonymous Interface Modules
~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we need to just parameterize a module by a couple of types/values,
it is quite cumbersome to have to define a whole separate interface module.
To make this more convenient we provide the following notation for defining
an anonymous interface and using it straight away:
.. code-block:: cryptol
:caption: Simple parameterized module.
module M where
parameter
type n : #
type constraint (fin n, n >= 1)
x : [n]
f : [n]
f = 1 + x
The ``parameter`` block defines an interface module and uses it.
Note that the parameters may not use things defined in ``M`` as
the interface is declared outside of ``M``.
Anonymous Instantiation Arguments
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Sometimes it is also a bit cumbersome to have to define a whole
separate module just to pass it as an argument to some parameterized
module. To make this more convenient we support the following notion
for instantiation a module:
.. code-block:: cryptol
// 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
The declarations in the ``where`` block are treated as the
definition of an anonymous module which is passed as the argument
to parameterized module ``M``.
Anonymous Import Instantiations
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We provide syntactic sugar for importing and instantiating a functor
at the same time:
.. code-block:: cryptol
submodule F where
parameter
x : [8]
y = x + 1
import submodule F where
x = 2
The ``where`` block may is the same as the ``where`` block in
expressions: you may define type synonyms and values, but nothing else
(e.g., no ``newtype``).
It is also possible to import and instantiate using an existing module
like this:
.. code-block:: cryptol
submodule F where
parameter
x : [8]
y = x + 1
submodule G where
x = 7
import submodule F { submodule G }
Semantically, instantiating imports declare a local nested module and
import it. For example, the ``where`` import from above is equivalent
to the following declarations:
.. code-block:: cryptol
submodule F where
parameter
x : [8]
y = x + 1
submodule M where
x = 2
submodule N = submodule F { submodule M }
import submodule N
Passing Through Module Parameters
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Occasionally it is useful to define a functor that instantiates *another*
functor using the same parameters as the functor being defined
(i.e., a functor parameter is passed on to another functor). This can
be done by using the keyword ``interface`` followed by the name of a parameter
in an instantiation. Here is an example:
.. code-block:: cryptol
interface submodule S where
x : [8]
// A functor, parameterized on S
submodule G where
import interface submodule S
y = x + 1
// Another functor, also parameterize on S
submodule F where
import interface submodule S as A
// Instantiate `G` using parameter `A` of `F`
import submodule G { interface A } // Brings `y` in scope
z = A::x + y
// Brings `z` into scope: z = A::x + y
// = 5 + (5 + 1)
// = 11
import submodule F where
x = 5

107
docs/RefMan/OverloadedOperations.rst Normal file
View File

@ -0,0 +1,107 @@
Overloaded Operations
=====================
Equality
--------
.. code-block:: cryptol
Eq
(==) : {a} (Eq a) => a -> a -> Bit
(!=) : {a} (Eq a) => a -> a -> Bit
(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
Comparisons
-----------
.. code-block:: cryptol
Cmp
(<) : {a} (Cmp a) => a -> a -> Bit
(>) : {a} (Cmp a) => a -> a -> Bit
(<=) : {a} (Cmp a) => a -> a -> Bit
(>=) : {a} (Cmp a) => a -> a -> Bit
min : {a} (Cmp a) => a -> a -> a
max : {a} (Cmp a) => a -> a -> a
abs : {a} (Cmp a, Ring a) => a -> a
Signed Comparisons
------------------
.. code-block:: cryptol
SignedCmp
(<$) : {a} (SignedCmp a) => a -> a -> Bit
(>$) : {a} (SignedCmp a) => a -> a -> Bit
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
Zero
----
.. code-block:: cryptol
Zero
zero : {a} (Zero a) => a
Logical Operations
------------------
.. code-block:: cryptol
Logic
(&&) : {a} (Logic a) => a -> a -> a
(||) : {a} (Logic a) => a -> a -> a
(^) : {a} (Logic a) => a -> a -> a
complement : {a} (Logic a) => a -> a
Basic Arithmetic
----------------
.. code-block:: cryptol
Ring
fromInteger : {a} (Ring a) => Integer -> a
(+) : {a} (Ring a) => a -> a -> a
(-) : {a} (Ring a) => a -> a -> a
(*) : {a} (Ring a) => a -> a -> a
negate : {a} (Ring a) => a -> a
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
Integral Operations
-------------------
.. code-block:: cryptol
Integral
(/) : {a} (Integral a) => a -> a -> a
(%) : {a} (Integral a) => a -> a -> a
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
toInteger : {a} (Integral a) => a -> Integer
infFrom : {a} (Integral a) => a -> [inf]a
infFromThen : {a} (Integral a) => a -> a -> [inf]a
Division
--------
.. code-block:: cryptol
Field
recip : {a} (Field a) => a -> a
(/.) : {a} (Field a) => a -> a -> a
Rounding
--------
.. code-block:: cryptol
Round
ceiling : {a} (Round a) => a -> Integer
floor : {a} (Round a) => a -> Integer
trunc : {a} (Round a) => a -> Integer
roundAway : {a} (Round a) => a -> Integer
roundToEven : {a} (Round a) => a -> Integer

1255
docs/RefMan/RefMan.rst
View File

File diff suppressed because it is too large Load Diff

53
docs/RefMan/TypeDeclarations.rst Normal file
View File

@ -0,0 +1,53 @@
Type Declarations
=================
Type Synonyms
-------------
.. code-block:: cryptol
type T a b = [a] b
A ``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.
Newtypes
--------
.. code-block:: cryptol
newtype NewT a b = { seq : [a]b }
A ``newtype`` declaration declares a new named type which is defined by
a record body. Unlike type synonyms, each named ``newtype`` is treated
as a distinct type by the type checker, even if they have the same
bodies. Moreover, types created by a ``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 ``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.
.. code-block:: cryptol
x : NewT 3 Integer
x = NewT { seq = [1,2,3] }
Just as with records, field projections can be used directly on values
of newtypes to extract the values in the body of the type.
.. code-block:: none
> sum x.seq
6

BIN
docs/RefMan/_build/doctrees/BasicSyntax.doctree Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/doctrees/BasicTypes.doctree Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/doctrees/Expressions.doctree Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/doctrees/Modules.doctree Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/doctrees/OverloadedOperations.doctree Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/doctrees/RefMan.doctree
View File

Binary file not shown.

BIN
docs/RefMan/_build/doctrees/TypeDeclarations.doctree Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/doctrees/environment.pickle
View File

Binary file not shown.

2
docs/RefMan/_build/html/.buildinfo
View File

@ -1,4 +1,4 @@
# Sphinx build info version 1
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
config: 3f9a4daf23c759ed9c684b18b96cc6ff
config: a4ccf7f1b3589b784c5cab7c48946aab
tags: 645f666f9bcd5a90fca523b33c5a78b7

390
docs/RefMan/_build/html/BasicSyntax.html Normal file
View File

@ -0,0 +1,390 @@
<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Basic Syntax &mdash; Cryptol 2.11.0 documentation</title>
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<!--[if lt IE 9]>
<script src="_static/js/html5shiv.min.js"></script>
<![endif]-->
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="next" title="Expressions" href="Expressions.html" />
<link rel="prev" title="Cryptol Reference Manual" href="RefMan.html" />
</head>
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="RefMan.html" class="icon icon-home"> Cryptol
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
<ul class="current">
<li class="toctree-l1 current"><a class="current reference internal" href="#">Basic Syntax</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#declarations">Declarations</a></li>
<li class="toctree-l2"><a class="reference internal" href="#type-signatures">Type Signatures</a></li>
<li class="toctree-l2"><a class="reference internal" href="#layout">Layout</a></li>
<li class="toctree-l2"><a class="reference internal" href="#comments">Comments</a></li>
<li class="toctree-l2"><a class="reference internal" href="#identifiers">Identifiers</a></li>
<li class="toctree-l2"><a class="reference internal" href="#keywords-and-built-in-operators">Keywords and Built-in Operators</a></li>
<li class="toctree-l2"><a class="reference internal" href="#built-in-type-level-operators">Built-in Type-level Operators</a></li>
<li class="toctree-l2"><a class="reference internal" href="#numeric-literals">Numeric Literals</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="Expressions.html">Expressions</a></li>
<li class="toctree-l1"><a class="reference internal" href="BasicTypes.html">Basic Types</a></li>
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
</ul>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="RefMan.html">Cryptol</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="RefMan.html" class="icon icon-home"></a> &raquo;</li>
<li>Basic Syntax</li>
<li class="wy-breadcrumbs-aside">
<a href="_sources/BasicSyntax.rst.txt" rel="nofollow"> View page source</a>
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<div class="section" id="basic-syntax">
<h1>Basic Syntax<a class="headerlink" href="#basic-syntax" title="Permalink to this headline"></a></h1>
<div class="section" id="declarations">
<h2>Declarations<a class="headerlink" href="#declarations" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span> <span class="n">x</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="o">+</span> <span class="n">z</span>
</pre></div>
</div>
</div>
<div class="section" id="type-signatures">
<h2>Type Signatures<a class="headerlink" href="#type-signatures" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="p">,</span><span class="n">g</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">,</span><span class="n">b</span><span class="p">}</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="p">[</span><span class="n">a</span><span class="p">]</span> <span class="n">b</span>
</pre></div>
</div>
</div>
<div class="section" id="layout">
<h2>Layout<a class="headerlink" href="#layout" title="Permalink to this headline"></a></h2>
<p>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. Consider, for example,
the following Cryptol declarations:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span> <span class="n">x</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="o">+</span> <span class="n">z</span>
<span class="kr">where</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">*</span> <span class="n">x</span>
<span class="n">z</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span>
<span class="nf">g</span> <span class="n">y</span> <span class="ow">=</span> <span class="n">y</span>
</pre></div>
</div>
<p>This group has two declarations, one for <cite>f</cite> and one for <cite>g</cite>. All the
lines between <cite>f</cite> and <cite>g</cite> that are indented more than <cite>f</cite> belong to
<cite>f</cite>. The same principle applies to the declarations in the <code class="docutils literal notranslate"><span class="pre">where</span></code> block
of <cite>f</cite>, which defines two more local names, <cite>y</cite> and <cite>z</cite>.</p>
</div>
<div class="section" id="comments">
<h2>Comments<a class="headerlink" href="#comments" title="Permalink to this headline"></a></h2>
<p>Cryptol supports block comments, which start with <code class="docutils literal notranslate"><span class="pre">/*</span></code> and end with
<code class="docutils literal notranslate"><span class="pre">*/</span></code>, and line comments, which start with <code class="docutils literal notranslate"><span class="pre">//</span></code> and terminate at the
end of the line. Block comments may be nested arbitrarily.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="cm">/* This is a block comment */</span>
<span class="c1">// This is a line comment</span>
<span class="cm">/* This is a /* Nested */ block comment */</span>
</pre></div>
</div>
<div class="admonition-todo admonition" id="id1">
<p class="admonition-title">Todo</p>
<p>Document <code class="docutils literal notranslate"><span class="pre">/**</span> <span class="pre">*/</span></code></p>
</div>
</div>
<div class="section" id="identifiers">
<h2>Identifiers<a class="headerlink" href="#identifiers" title="Permalink to this headline"></a></h2>
<p>Cryptol identifiers consist of one or more characters. The first
character must be either an English letter or underscore (<code class="docutils literal notranslate"><span class="pre">_</span></code>). The
following characters may be an English letter, a decimal digit,
underscore (<code class="docutils literal notranslate"><span class="pre">_</span></code>), or a prime (<code class="docutils literal notranslate"><span class="pre">'</span></code>). Some identifiers have special
meaning in the language, so they may not be used in programmer-defined
names (see <a class="reference internal" href="#keywords-and-built-in-operators">Keywords and Built-in Operators</a>).</p>
<div class="literal-block-wrapper docutils container" id="id2">
<div class="code-block-caption"><span class="caption-text">Examples of identifiers</span><a class="headerlink" href="#id2" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">name</span> <span class="n">name1</span> <span class="n">name&#39;</span> <span class="n">longer_name</span>
<span class="kt">Name</span> <span class="kt">Name2</span> <span class="kt">Name&#39;&#39;</span> <span class="n">longerName</span>
</pre></div>
</div>
</div>
</div>
<div class="section" id="keywords-and-built-in-operators">
<h2>Keywords and Built-in Operators<a class="headerlink" href="#keywords-and-built-in-operators" title="Permalink to this headline"></a></h2>
<p>The following identifiers have special meanings in Cryptol, and may
not be used for programmer defined names:</p>
<div class="literal-block-wrapper docutils container" id="id3">
<span id="keywords"></span><div class="code-block-caption"><span class="caption-text">Keywords</span><a class="headerlink" href="#id3" title="Permalink to this code"></a></div>
<div class="highlight-none notranslate"><div class="highlight"><pre><span></span>as extern include interface parameter property where
by hiding infix let pragma submodule else
constraint if infixl module primitive then
down import infixr newtype private type
</pre></div>
</div>
</div>
<p>The following table contains Cryptol’s operators and their
associativity with lowest precedence operators first, and highest
precedence last.</p>
<table class="docutils align-default" id="id4">
<caption><span class="caption-text">Operator precedences</span><a class="headerlink" href="#id4" title="Permalink to this table"></a></caption>
<colgroup>
<col style="width: 71%" />
<col style="width: 29%" />
</colgroup>
<thead>
<tr class="row-odd"><th class="head"><p>Operator</p></th>
<th class="head"><p>Associativity</p></th>
</tr>
</thead>
<tbody>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">==&gt;</span></code></p></td>
<td><p>right</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">\/</span></code></p></td>
<td><p>right</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">/\</span></code></p></td>
<td><p>right</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">==</span></code> <code class="docutils literal notranslate"><span class="pre">!=</span></code> <code class="docutils literal notranslate"><span class="pre">===</span></code> <code class="docutils literal notranslate"><span class="pre">!==</span></code></p></td>
<td><p>not associative</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">&gt;</span></code> <code class="docutils literal notranslate"><span class="pre">&lt;</span></code> <code class="docutils literal notranslate"><span class="pre">&lt;=</span></code> <code class="docutils literal notranslate"><span class="pre">&gt;=</span></code>
<code class="docutils literal notranslate"><span class="pre">&lt;$</span></code> <code class="docutils literal notranslate"><span class="pre">&gt;$</span></code> <code class="docutils literal notranslate"><span class="pre">&lt;=$</span></code> <code class="docutils literal notranslate"><span class="pre">&gt;=$</span></code></p></td>
<td><p>not associative</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">||</span></code></p></td>
<td><p>right</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">^</span></code></p></td>
<td><p>left</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">&amp;&amp;</span></code></p></td>
<td><p>right</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">#</span></code></p></td>
<td><p>right</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">&gt;&gt;</span></code> <code class="docutils literal notranslate"><span class="pre">&lt;&lt;</span></code> <code class="docutils literal notranslate"><span class="pre">&gt;&gt;&gt;</span></code> <code class="docutils literal notranslate"><span class="pre">&lt;&lt;&lt;</span></code> <code class="docutils literal notranslate"><span class="pre">&gt;&gt;$</span></code></p></td>
<td><p>left</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">+</span></code> <code class="docutils literal notranslate"><span class="pre">-</span></code></p></td>
<td><p>left</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">*</span></code> <code class="docutils literal notranslate"><span class="pre">/</span></code> <code class="docutils literal notranslate"><span class="pre">%</span></code> <code class="docutils literal notranslate"><span class="pre">/$</span></code> <code class="docutils literal notranslate"><span class="pre">%$</span></code></p></td>
<td><p>left</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">^^</span></code></p></td>
<td><p>right</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">&#64;</span></code> <code class="docutils literal notranslate"><span class="pre">&#64;&#64;</span></code> <code class="docutils literal notranslate"><span class="pre">!</span></code> <code class="docutils literal notranslate"><span class="pre">!!</span></code></p></td>
<td><p>left</p></td>
</tr>
<tr class="row-even"><td><p>(unary) <code class="docutils literal notranslate"><span class="pre">-</span></code> <code class="docutils literal notranslate"><span class="pre">~</span></code></p></td>
<td><p>right</p></td>
</tr>
</tbody>
</table>
</div>
<div class="section" id="built-in-type-level-operators">
<h2>Built-in Type-level Operators<a class="headerlink" href="#built-in-type-level-operators" title="Permalink to this headline"></a></h2>
<p>Cryptol includes a variety of operators that allow computations on
the numeric types used to specify the sizes of sequences.</p>
<table class="docutils align-default" id="id5">
<caption><span class="caption-text">Type-level operators</span><a class="headerlink" href="#id5" title="Permalink to this table"></a></caption>
<colgroup>
<col style="width: 23%" />
<col style="width: 77%" />
</colgroup>
<thead>
<tr class="row-odd"><th class="head"><p>Operator</p></th>
<th class="head"><p>Meaning</p></th>
</tr>
</thead>
<tbody>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">+</span></code></p></td>
<td><p>Addition</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">-</span></code></p></td>
<td><p>Subtraction</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">*</span></code></p></td>
<td><p>Multiplication</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">/</span></code></p></td>
<td><p>Division</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">/^</span></code></p></td>
<td><p>Ceiling division (<code class="docutils literal notranslate"><span class="pre">/</span></code> rounded up)</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">%</span></code></p></td>
<td><p>Modulus</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">%^</span></code></p></td>
<td><p>Ceiling modulus (compute padding)</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">^^</span></code></p></td>
<td><p>Exponentiation</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">lg2</span></code></p></td>
<td><p>Ceiling logarithm (base 2)</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">width</span></code></p></td>
<td><p>Bit width (equal to <code class="docutils literal notranslate"><span class="pre">lg2(n+1)</span></code>)</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">max</span></code></p></td>
<td><p>Maximum</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">min</span></code></p></td>
<td><p>Minimum</p></td>
</tr>
</tbody>
</table>
</div>
<div class="section" id="numeric-literals">
<h2>Numeric Literals<a class="headerlink" href="#numeric-literals" title="Permalink to this headline"></a></h2>
<p>Numeric literals may be written in binary, octal, decimal, or
hexadecimal notation. The base of a literal is determined by its prefix:
<code class="docutils literal notranslate"><span class="pre">0b</span></code> for binary, <code class="docutils literal notranslate"><span class="pre">0o</span></code> for octal, no special prefix for
decimal, and <code class="docutils literal notranslate"><span class="pre">0x</span></code> for hexadecimal.</p>
<div class="literal-block-wrapper docutils container" id="id6">
<div class="code-block-caption"><span class="caption-text">Examples of literals</span><a class="headerlink" href="#id6" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="mi">254</span> <span class="c1">// Decimal literal</span>
<span class="mi">0254</span> <span class="c1">// Decimal literal</span>
<span class="mi">0</span><span class="n">b11111110</span> <span class="c1">// Binary literal</span>
<span class="mo">0o376</span> <span class="c1">// Octal literal</span>
<span class="mh">0xFE</span> <span class="c1">// Hexadecimal literal</span>
<span class="mh">0xfe</span> <span class="c1">// Hexadecimal literal</span>
</pre></div>
</div>
</div>
<p>Numeric literals in binary, octal, or hexadecimal notation result in
bit sequences of a fixed length (i.e., they have type <code class="docutils literal notranslate"><span class="pre">[n]</span></code> for
some <cite>n</cite>). 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:</p>
<div class="literal-block-wrapper docutils container" id="id7">
<div class="code-block-caption"><span class="caption-text">Literals and their types</span><a class="headerlink" href="#id7" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="mi">0</span><span class="n">b1010</span> <span class="c1">// : [4], 1 * number of digits</span>
<span class="mo">0o1234</span> <span class="c1">// : [12], 3 * number of digits</span>
<span class="mh">0x1234</span> <span class="c1">// : [16], 4 * number of digits</span>
<span class="mi">10</span> <span class="c1">// : {a}. (Literal 10 a) =&gt; a</span>
<span class="c1">// a = Integer or [n] where n &gt;= width 10</span>
</pre></div>
</div>
</div>
<p>Numeric literals may also be written as polynomials by writing a polynomial
expression in terms of <cite>x</cite> between an opening <code class="docutils literal notranslate"><span class="pre">&lt;|</span></code> and a closing <code class="docutils literal notranslate"><span class="pre">|&gt;</span></code>.
Numeric literals in polynomial notation result in bit sequences of length
one more than the degree of the polynomial. Examples:</p>
<div class="literal-block-wrapper docutils container" id="id8">
<div class="code-block-caption"><span class="caption-text">Polynomial literals</span><a class="headerlink" href="#id8" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="o">&lt;|</span> <span class="n">x</span><span class="o">^^</span><span class="mi">6</span> <span class="o">+</span> <span class="n">x</span><span class="o">^^</span><span class="mi">4</span> <span class="o">+</span> <span class="n">x</span><span class="o">^^</span><span class="mi">2</span> <span class="o">+</span> <span class="n">x</span><span class="o">^^</span><span class="mi">1</span> <span class="o">+</span> <span class="mi">1</span> <span class="o">|&gt;</span> <span class="c1">// : [7], equal to 0b1010111</span>
<span class="o">&lt;|</span> <span class="n">x</span><span class="o">^^</span><span class="mi">4</span> <span class="o">+</span> <span class="n">x</span><span class="o">^^</span><span class="mi">3</span> <span class="o">+</span> <span class="n">x</span> <span class="o">|&gt;</span> <span class="c1">// : [5], equal to 0b11010</span>
</pre></div>
</div>
</div>
<p>Cryptol also supports fractional literals using binary (prefix <code class="docutils literal notranslate"><span class="pre">0b</span></code>),
octal (prefix <code class="docutils literal notranslate"><span class="pre">0o</span></code>), decimal (no prefix), and hexadecimal (prefix <code class="docutils literal notranslate"><span class="pre">ox</span></code>)
digits. A fractional literal must contain a <code class="docutils literal notranslate"><span class="pre">.</span></code> 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 <code class="docutils literal notranslate"><span class="pre">p</span></code>.
Decimal fractional literals use exponent base 10, and the symbol <code class="docutils literal notranslate"><span class="pre">e</span></code>.
Examples:</p>
<div class="literal-block-wrapper docutils container" id="id9">
<div class="code-block-caption"><span class="caption-text">Fractional literals</span><a class="headerlink" href="#id9" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="mf">10.2</span>
<span class="mf">10.2e3</span> <span class="c1">// 10.2 * 10^3</span>
<span class="mh">0x30</span><span class="o">.</span><span class="mi">1</span> <span class="c1">// 3 * 64 + 1/16</span>
<span class="mh">0x30</span><span class="o">.</span><span class="mi">1</span><span class="n">p4</span> <span class="c1">// (3 * 64 + 1/16) * 2^4</span>
</pre></div>
</div>
</div>
<p>All fractional literals are overloaded and may be used with types that support
fractional numbers (e.g., <code class="docutils literal notranslate"><span class="pre">Rational</span></code>, and the <code class="docutils literal notranslate"><span class="pre">Float</span></code> family of types).</p>
<p>Some types (e.g. the <code class="docutils literal notranslate"><span class="pre">Float</span></code> 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.</p>
<p>All numeric literals may also include <code class="docutils literal notranslate"><span class="pre">_</span></code>, which has no effect on the
literal value but may be used to improve readability. Here are some examples:</p>
<div class="literal-block-wrapper docutils container" id="id10">
<div class="code-block-caption"><span class="caption-text">Using _</span><a class="headerlink" href="#id10" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="mi">0</span><span class="n">b_0000_0010</span>
<span class="mi">0</span><span class="n">x_FFFF_FFEA</span>
</pre></div>
</div>
</div>
</div>
</div>
</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="RefMan.html" class="btn btn-neutral float-left" title="Cryptol Reference Manual" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="Expressions.html" class="btn btn-neutral float-right" title="Expressions" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>
<hr/>
<div role="contentinfo">
<p>&#169; Copyright 2021, The Cryptol Team.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</body>
</html>

306
docs/RefMan/_build/html/BasicTypes.html Normal file
View File

@ -0,0 +1,306 @@
<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Basic Types &mdash; Cryptol 2.11.0 documentation</title>
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<!--[if lt IE 9]>
<script src="_static/js/html5shiv.min.js"></script>
<![endif]-->
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="next" title="Overloaded Operations" href="OverloadedOperations.html" />
<link rel="prev" title="Expressions" href="Expressions.html" />
</head>
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="RefMan.html" class="icon icon-home"> Cryptol
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a></li>
<li class="toctree-l1"><a class="reference internal" href="Expressions.html">Expressions</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">Basic Types</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#tuples-and-records">Tuples and Records</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#accessing-fields">Accessing Fields</a></li>
<li class="toctree-l3"><a class="reference internal" href="#updating-fields">Updating Fields</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#sequences">Sequences</a></li>
<li class="toctree-l2"><a class="reference internal" href="#functions">Functions</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
</ul>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="RefMan.html">Cryptol</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="RefMan.html" class="icon icon-home"></a> &raquo;</li>
<li>Basic Types</li>
<li class="wy-breadcrumbs-aside">
<a href="_sources/BasicTypes.rst.txt" rel="nofollow"> View page source</a>
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<div class="section" id="basic-types">
<h1>Basic Types<a class="headerlink" href="#basic-types" title="Permalink to this headline"></a></h1>
<div class="section" id="tuples-and-records">
<h2>Tuples and Records<a class="headerlink" href="#tuples-and-records" title="Permalink to this headline"></a></h2>
<p>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:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="mi">2</span><span class="p">,</span><span class="mi">3</span><span class="p">)</span> <span class="c1">// A tuple with 3 component</span>
<span class="nb">()</span> <span class="c1">// A tuple with no components</span>
<span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">1</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">2</span> <span class="p">}</span> <span class="c1">// A record with two fields, `x` and `y`</span>
<span class="p">{}</span> <span class="c1">// A record with no fields</span>
</pre></div>
</div>
<p>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:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span> <span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="mi">2</span><span class="p">)</span> <span class="o">==</span> <span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="mi">2</span><span class="p">)</span> <span class="c1">// True</span>
<span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="mi">2</span><span class="p">)</span> <span class="o">==</span> <span class="p">(</span><span class="mi">2</span><span class="p">,</span><span class="mi">1</span><span class="p">)</span> <span class="c1">// False</span>
<span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">1</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">2</span> <span class="p">}</span> <span class="o">==</span> <span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">1</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">2</span> <span class="p">}</span> <span class="c1">// True</span>
<span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">1</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">2</span> <span class="p">}</span> <span class="o">==</span> <span class="p">{</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">2</span><span class="p">,</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">1</span> <span class="p">}</span> <span class="c1">// True</span>
</pre></div>
</div>
<p>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.</p>
<div class="section" id="accessing-fields">
<h3>Accessing Fields<a class="headerlink" href="#accessing-fields" title="Permalink to this headline"></a></h3>
<p>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:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="mi">15</span><span class="p">,</span> <span class="mi">20</span><span class="p">)</span><span class="o">.</span><span class="mi">0</span> <span class="o">==</span> <span class="mi">15</span>
<span class="p">(</span><span class="mi">15</span><span class="p">,</span> <span class="mi">20</span><span class="p">)</span><span class="o">.</span><span class="mi">1</span> <span class="o">==</span> <span class="mi">20</span>
<span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">15</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">20</span> <span class="p">}</span><span class="o">.</span><span class="n">x</span> <span class="o">==</span> <span class="mi">15</span>
</pre></div>
</div>
<p>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:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">type</span> <span class="kt">T</span> <span class="ow">=</span> <span class="p">{</span> <span class="n">sign</span> <span class="kt">:</span> <span class="kr">Bit</span><span class="p">,</span> <span class="n">number</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">15</span><span class="p">]</span> <span class="p">}</span>
<span class="c1">// Valid definition:</span>
<span class="c1">// the type of the record is known.</span>
<span class="nf">isPositive</span> <span class="kt">:</span> <span class="kt">T</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
<span class="nf">isPositive</span> <span class="n">x</span> <span class="ow">=</span> <span class="n">x</span><span class="o">.</span><span class="n">sign</span>
<span class="c1">// Invalid definition:</span>
<span class="c1">// insufficient type information.</span>
<span class="nf">badDef</span> <span class="n">x</span> <span class="ow">=</span> <span class="n">x</span><span class="o">.</span><span class="n">f</span>
</pre></div>
</div>
<p>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:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">getFst</span> <span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="n">_</span><span class="p">)</span> <span class="ow">=</span> <span class="n">x</span>
<span class="nf">distance2</span> <span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="n">xPos</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="n">yPos</span> <span class="p">}</span> <span class="ow">=</span> <span class="n">xPos</span> <span class="o">^^</span> <span class="mi">2</span> <span class="o">+</span> <span class="n">yPos</span> <span class="o">^^</span> <span class="mi">2</span>
<span class="nf">f</span> <span class="n">p</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="kr">where</span>
<span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">)</span> <span class="ow">=</span> <span class="n">p</span>
</pre></div>
</div>
<p>Selectors are also lifted through sequence and function types, point-wise,
so that the following equations should hold:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">xs</span><span class="o">.</span><span class="n">l</span> <span class="o">==</span> <span class="p">[</span> <span class="n">x</span><span class="o">.</span><span class="n">l</span> <span class="o">|</span> <span class="n">x</span> <span class="ow">&lt;-</span> <span class="n">xs</span> <span class="p">]</span> <span class="c1">// sequences</span>
<span class="nf">f</span><span class="o">.</span><span class="n">l</span> <span class="o">==</span> <span class="nf">\</span><span class="n">x</span> <span class="ow">-&gt;</span> <span class="p">(</span><span class="n">f</span> <span class="n">x</span><span class="p">)</span><span class="o">.</span><span class="n">l</span> <span class="c1">// functions</span>
</pre></div>
</div>
<p>Thus, if we have a sequence of tuples, <code class="docutils literal notranslate"><span class="pre">xs</span></code>, then we can quickly obtain a
sequence with only the tuples’ first components by writing <code class="docutils literal notranslate"><span class="pre">xs.0</span></code>.</p>
<p>Similarly, if we have a function, <code class="docutils literal notranslate"><span class="pre">f</span></code>, that computes a tuple of results,
then we can write <code class="docutils literal notranslate"><span class="pre">f.0</span></code> to get a function that computes only the first
entry in the tuple.</p>
<p>This behavior is quite handy when examining complex data at the REPL.</p>
</div>
<div class="section" id="updating-fields">
<h3>Updating Fields<a class="headerlink" href="#updating-fields" title="Permalink to this headline"></a></h3>
<p>The components of a record or a tuple may be updated using the following
notation:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// Example values</span>
<span class="nf">r</span> <span class="ow">=</span> <span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">15</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">20</span> <span class="p">}</span> <span class="c1">// a record</span>
<span class="nf">t</span> <span class="ow">=</span> <span class="p">(</span><span class="kr">True</span><span class="p">,</span><span class="kr">True</span><span class="p">)</span> <span class="c1">// a tuple</span>
<span class="nf">n</span> <span class="ow">=</span> <span class="p">{</span> <span class="n">pt</span> <span class="ow">=</span> <span class="n">r</span><span class="p">,</span> <span class="n">size</span> <span class="ow">=</span> <span class="mi">100</span> <span class="p">}</span> <span class="c1">// nested record</span>
<span class="c1">// Setting fields</span>
<span class="p">{</span> <span class="n">r</span> <span class="o">|</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">30</span> <span class="p">}</span> <span class="o">==</span> <span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">30</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">20</span> <span class="p">}</span>
<span class="p">{</span> <span class="n">t</span> <span class="o">|</span> <span class="mi">0</span> <span class="ow">=</span> <span class="kr">False</span> <span class="p">}</span> <span class="o">==</span> <span class="p">(</span><span class="kr">False</span><span class="p">,</span><span class="kr">True</span><span class="p">)</span>
<span class="c1">// Update relative to the old value</span>
<span class="p">{</span> <span class="n">r</span> <span class="o">|</span> <span class="n">x</span> <span class="ow">-&gt;</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">5</span> <span class="p">}</span> <span class="o">==</span> <span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">20</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">20</span> <span class="p">}</span>
<span class="c1">// Update a nested field</span>
<span class="p">{</span> <span class="n">n</span> <span class="o">|</span> <span class="n">pt</span><span class="o">.</span><span class="n">x</span> <span class="ow">=</span> <span class="mi">10</span> <span class="p">}</span> <span class="o">==</span> <span class="p">{</span> <span class="n">pt</span> <span class="ow">=</span> <span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">10</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">20</span> <span class="p">},</span> <span class="n">size</span> <span class="ow">=</span> <span class="mi">100</span> <span class="p">}</span>
<span class="p">{</span> <span class="n">n</span> <span class="o">|</span> <span class="n">pt</span><span class="o">.</span><span class="n">x</span> <span class="ow">-&gt;</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">10</span> <span class="p">}</span> <span class="o">==</span> <span class="p">{</span> <span class="n">pt</span> <span class="ow">=</span> <span class="p">{</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">25</span><span class="p">,</span> <span class="n">y</span> <span class="ow">=</span> <span class="mi">20</span> <span class="p">},</span> <span class="n">size</span> <span class="ow">=</span> <span class="mi">100</span> <span class="p">}</span>
</pre></div>
</div>
</div>
</div>
<div class="section" id="sequences">
<h2>Sequences<a class="headerlink" href="#sequences" title="Permalink to this headline"></a></h2>
<p>A sequence is a fixed-length collection of elements of the same type.
The type of a finite sequence of length <cite>n</cite>, with elements of type <cite>a</cite>
is <code class="docutils literal notranslate"><span class="pre">[n]</span> <span class="pre">a</span></code>. Often, a finite sequence of bits, <code class="docutils literal notranslate"><span class="pre">[n]</span> <span class="pre">Bit</span></code>, is called a
<em>word</em>. We may abbreviate the type <code class="docutils literal notranslate"><span class="pre">[n]</span> <span class="pre">Bit</span></code> as <code class="docutils literal notranslate"><span class="pre">[n]</span></code>. An infinite
sequence with elements of type <cite>a</cite> has type <code class="docutils literal notranslate"><span class="pre">[inf]</span> <span class="pre">a</span></code>, and <code class="docutils literal notranslate"><span class="pre">[inf]</span></code> is
an infinite stream of bits.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="p">[</span><span class="n">e1</span><span class="p">,</span><span class="n">e2</span><span class="p">,</span><span class="n">e3</span><span class="p">]</span> <span class="c1">// A sequence with three elements</span>
<span class="p">[</span><span class="n">t1</span> <span class="o">..</span> <span class="n">t2</span><span class="p">]</span> <span class="c1">// Enumeration</span>
<span class="p">[</span><span class="n">t1</span> <span class="o">..</span> <span class="o">&lt;</span><span class="n">t2</span><span class="p">]</span> <span class="c1">// Enumeration (exclusive bound)</span>
<span class="p">[</span><span class="n">t1</span> <span class="o">..</span> <span class="n">t2</span> <span class="n">by</span> <span class="n">n</span><span class="p">]</span> <span class="c1">// Enumeration (stride)</span>
<span class="p">[</span><span class="n">t1</span> <span class="o">..</span> <span class="o">&lt;</span><span class="n">t2</span> <span class="n">by</span> <span class="n">n</span><span class="p">]</span> <span class="c1">// Enumeration (stride, ex. bound)</span>
<span class="p">[</span><span class="n">t1</span> <span class="o">..</span> <span class="n">t2</span> <span class="n">down</span> <span class="n">by</span> <span class="n">n</span><span class="p">]</span> <span class="c1">// Enumeration (downward stride)</span>
<span class="p">[</span><span class="n">t1</span> <span class="o">..</span> <span class="o">&gt;</span><span class="n">t2</span> <span class="n">down</span> <span class="n">by</span> <span class="n">n</span><span class="p">]</span> <span class="c1">// Enumeration (downward stride, ex. bound)</span>
<span class="p">[</span><span class="n">t1</span><span class="p">,</span> <span class="n">t2</span> <span class="o">..</span> <span class="n">t3</span><span class="p">]</span> <span class="c1">// Enumeration (step by t2 - t1)</span>
<span class="p">[</span><span class="n">e1</span> <span class="o">...</span><span class="p">]</span> <span class="c1">// Infinite sequence starting at e1</span>
<span class="p">[</span><span class="n">e1</span><span class="p">,</span> <span class="n">e2</span> <span class="o">...</span><span class="p">]</span> <span class="c1">// Infinite sequence stepping by e2-e1</span>
<span class="p">[</span> <span class="n">e</span> <span class="o">|</span> <span class="n">p11</span> <span class="ow">&lt;-</span> <span class="n">e11</span><span class="p">,</span> <span class="n">p12</span> <span class="ow">&lt;-</span> <span class="n">e12</span> <span class="c1">// Sequence comprehensions</span>
<span class="o">|</span> <span class="n">p21</span> <span class="ow">&lt;-</span> <span class="n">e21</span><span class="p">,</span> <span class="n">p22</span> <span class="ow">&lt;-</span> <span class="n">e22</span> <span class="p">]</span>
<span class="nf">x</span> <span class="ow">=</span> <span class="n">generate</span> <span class="p">(</span><span class="nf">\</span><span class="n">i</span> <span class="ow">-&gt;</span> <span class="n">e</span><span class="p">)</span> <span class="c1">// Sequence from generating function</span>
<span class="nf">x</span> <span class="o">@</span> <span class="n">i</span> <span class="ow">=</span> <span class="n">e</span> <span class="c1">// Sequence with index binding</span>
<span class="nf">arr</span> <span class="o">@</span> <span class="n">i</span> <span class="o">@</span> <span class="n">j</span> <span class="ow">=</span> <span class="n">e</span> <span class="c1">// Two-dimensional sequence</span>
</pre></div>
</div>
<p>Note: the bounds in finite sequences (those with <cite>..</cite>) are type
expressions, while the bounds in infinite sequences are value
expressions.</p>
<table class="docutils align-default" id="id1">
<caption><span class="caption-text">Sequence operations.</span><a class="headerlink" href="#id1" title="Permalink to this table"></a></caption>
<colgroup>
<col style="width: 40%" />
<col style="width: 60%" />
</colgroup>
<thead>
<tr class="row-odd"><th class="head"><p>Operator</p></th>
<th class="head"><p>Description</p></th>
</tr>
</thead>
<tbody>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">#</span></code></p></td>
<td><p>Sequence concatenation</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">&gt;&gt;</span></code> <code class="docutils literal notranslate"><span class="pre">&lt;&lt;</span></code></p></td>
<td><p>Shift (right, left)</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">&gt;&gt;&gt;</span></code> <code class="docutils literal notranslate"><span class="pre">&lt;&lt;&lt;</span></code></p></td>
<td><p>Rotate (right, left)</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">&gt;&gt;$</span></code></p></td>
<td><p>Arithmetic right shift (on bitvectors only)</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">&#64;</span></code> <code class="docutils literal notranslate"><span class="pre">!</span></code></p></td>
<td><p>Access elements (front, back)</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">&#64;&#64;</span></code> <code class="docutils literal notranslate"><span class="pre">!!</span></code></p></td>
<td><p>Access sub-sequence (front, back)</p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">update</span></code> <code class="docutils literal notranslate"><span class="pre">updateEnd</span></code></p></td>
<td><p>Update the value of a sequence at
a location
(front, back)</p></td>
</tr>
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">updates</span></code> <code class="docutils literal notranslate"><span class="pre">updatesEnd</span></code></p></td>
<td><p>Update multiple values of a sequence
(front, back)</p></td>
</tr>
</tbody>
</table>
<p>There are also lifted pointwise operations.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="p">[</span><span class="n">p1</span><span class="p">,</span> <span class="n">p2</span><span class="p">,</span> <span class="n">p3</span><span class="p">,</span> <span class="n">p4</span><span class="p">]</span> <span class="c1">// Sequence pattern</span>
<span class="nf">p1</span> <span class="o">#</span> <span class="n">p2</span> <span class="c1">// Split sequence pattern</span>
</pre></div>
</div>
</div>
<div class="section" id="functions">
<h2>Functions<a class="headerlink" href="#functions" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">\</span><span class="n">p1</span> <span class="n">p2</span> <span class="ow">-&gt;</span> <span class="n">e</span> <span class="c1">// Lambda expression</span>
<span class="nf">f</span> <span class="n">p1</span> <span class="n">p2</span> <span class="ow">=</span> <span class="n">e</span> <span class="c1">// Function definition</span>
</pre></div>
</div>
</div>
</div>
</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="Expressions.html" class="btn btn-neutral float-left" title="Expressions" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="OverloadedOperations.html" class="btn btn-neutral float-right" title="Overloaded Operations" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>
<hr/>
<div role="contentinfo">
<p>&#169; Copyright 2021, The Cryptol Team.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</body>
</html>

244
docs/RefMan/_build/html/Expressions.html Normal file
View File

@ -0,0 +1,244 @@
<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Expressions &mdash; Cryptol 2.11.0 documentation</title>
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<!--[if lt IE 9]>
<script src="_static/js/html5shiv.min.js"></script>
<![endif]-->
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="next" title="Basic Types" href="BasicTypes.html" />
<link rel="prev" title="Basic Syntax" href="BasicSyntax.html" />
</head>
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="RefMan.html" class="icon icon-home"> Cryptol
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">Expressions</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#calling-functions">Calling Functions</a></li>
<li class="toctree-l2"><a class="reference internal" href="#prefix-operators">Prefix Operators</a></li>
<li class="toctree-l2"><a class="reference internal" href="#infix-functions">Infix Functions</a></li>
<li class="toctree-l2"><a class="reference internal" href="#type-annotations">Type Annotations</a></li>
<li class="toctree-l2"><a class="reference internal" href="#explicit-type-instantiation">Explicit Type Instantiation</a></li>
<li class="toctree-l2"><a class="reference internal" href="#local-declarations">Local Declarations</a></li>
<li class="toctree-l2"><a class="reference internal" href="#block-arguments">Block Arguments</a></li>
<li class="toctree-l2"><a class="reference internal" href="#conditionals">Conditionals</a></li>
<li class="toctree-l2"><a class="reference internal" href="#demoting-numeric-types-to-values">Demoting Numeric Types to Values</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="BasicTypes.html">Basic Types</a></li>
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
</ul>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="RefMan.html">Cryptol</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="RefMan.html" class="icon icon-home"></a> &raquo;</li>
<li>Expressions</li>
<li class="wy-breadcrumbs-aside">
<a href="_sources/Expressions.rst.txt" rel="nofollow"> View page source</a>
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<div class="section" id="expressions">
<h1>Expressions<a class="headerlink" href="#expressions" title="Permalink to this headline"></a></h1>
<p>This section provides an overview of the Cryptol’s expression syntax.</p>
<div class="section" id="calling-functions">
<h2>Calling Functions<a class="headerlink" href="#calling-functions" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span> <span class="mi">2</span> <span class="c1">// call `f` with parameter `2`</span>
<span class="nf">g</span> <span class="n">x</span> <span class="n">y</span> <span class="c1">// call `g` with two parameters: `x` and `y`</span>
<span class="nf">h</span> <span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="n">y</span><span class="p">)</span> <span class="c1">// call `h` with one parameter, the pair `(x,y)`</span>
</pre></div>
</div>
</div>
<div class="section" id="prefix-operators">
<h2>Prefix Operators<a class="headerlink" href="#prefix-operators" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="o">-</span><span class="mi">2</span> <span class="c1">// call unary `-` with parameter `2`</span>
<span class="o">-</span> <span class="mi">2</span> <span class="c1">// call unary `-` with parameter `2`</span>
<span class="nf">f</span> <span class="p">(</span><span class="o">-</span><span class="mi">2</span><span class="p">)</span> <span class="c1">// call `f` with one argument: `-2`, parens are important</span>
<span class="o">-</span><span class="n">f</span> <span class="mi">2</span> <span class="c1">// call unary `-` with parameter `f 2`</span>
<span class="o">-</span> <span class="n">f</span> <span class="mi">2</span> <span class="c1">// call unary `-` with parameter `f 2`</span>
</pre></div>
</div>
</div>
<div class="section" id="infix-functions">
<h2>Infix Functions<a class="headerlink" href="#infix-functions" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="mi">2</span> <span class="o">+</span> <span class="mi">3</span> <span class="c1">// call `+` with two parameters: `2` and `3`</span>
<span class="mi">2</span> <span class="o">+</span> <span class="mi">3</span> <span class="o">*</span> <span class="mi">5</span> <span class="c1">// call `+` with two parameters: `2` and `3 * 5`</span>
<span class="p">(</span><span class="o">+</span><span class="p">)</span> <span class="mi">2</span> <span class="mi">3</span> <span class="c1">// call `+` with two parameters: `2` and `3`</span>
<span class="nf">f</span> <span class="mi">2</span> <span class="o">+</span> <span class="n">g</span> <span class="mi">3</span> <span class="c1">// call `+` with two parameters: `f 2` and `g 3`</span>
<span class="o">-</span> <span class="mi">2</span> <span class="o">+</span> <span class="o">-</span> <span class="mi">3</span> <span class="c1">// call `+` with two parameters: `-2` and `-3`</span>
<span class="o">-</span> <span class="n">f</span> <span class="mi">2</span> <span class="o">+</span> <span class="o">-</span> <span class="n">g</span> <span class="mi">3</span>
</pre></div>
</div>
</div>
<div class="section" id="type-annotations">
<h2>Type Annotations<a class="headerlink" href="#type-annotations" title="Permalink to this headline"></a></h2>
<p>Explicit type annotations may be added on expressions, patterns, and
in argument definitions.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">x</span> <span class="kt">:</span> <span class="kr">Bit</span> <span class="c1">// specify that `x` has type `Bit`</span>
<span class="nf">f</span> <span class="n">x</span> <span class="kt">:</span> <span class="kr">Bit</span> <span class="c1">// specify that `f x` has type `Bit`</span>
<span class="o">-</span> <span class="n">f</span> <span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span> <span class="c1">// specify that `- f x` has type `[8]`</span>
<span class="mi">2</span> <span class="o">+</span> <span class="mi">3</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span> <span class="c1">// specify that `2 + 3` has type `[8]`</span>
<span class="nf">\</span><span class="n">x</span> <span class="ow">-&gt;</span> <span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span> <span class="c1">// type annotation is on `x`, not the function</span>
<span class="kr">if</span> <span class="n">x</span>
<span class="kr">then</span> <span class="n">y</span>
<span class="kr">else</span> <span class="n">z</span> <span class="kt">:</span> <span class="kr">Bit</span> <span class="c1">// the type annotation is on `z`, not the whole `if`</span>
<span class="p">[</span><span class="mi">1</span><span class="o">..</span><span class="mi">9</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]]</span> <span class="c1">// specify that elements in `[1..9]` have type `[8]`</span>
<span class="nf">f</span> <span class="p">(</span><span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">])</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span> <span class="c1">// type annotation on patterns</span>
</pre></div>
</div>
<div class="admonition-todo admonition" id="id1">
<p class="admonition-title">Todo</p>
<p>Patterns with type variables</p>
</div>
</div>
<div class="section" id="explicit-type-instantiation">
<h2>Explicit Type Instantiation<a class="headerlink" href="#explicit-type-instantiation" title="Permalink to this headline"></a></h2>
<p>If <code class="docutils literal notranslate"><span class="pre">f</span></code> is a polymorphic value with type:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span> <span class="kt">:</span> <span class="p">{</span> <span class="n">tyParam</span> <span class="p">}</span> <span class="n">tyParam</span>
<span class="nf">f</span> <span class="ow">=</span> <span class="n">zero</span>
</pre></div>
</div>
<p>you can evaluate <code class="docutils literal notranslate"><span class="pre">f</span></code>, passing it a type parameter:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span> <span class="p">`{</span> <span class="n">tyParam</span> <span class="ow">=</span> <span class="mi">13</span> <span class="p">}</span>
</pre></div>
</div>
</div>
<div class="section" id="local-declarations">
<h2>Local Declarations<a class="headerlink" href="#local-declarations" title="Permalink to this headline"></a></h2>
<p>Local declarations have the weakest precedence of all expressions.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="mi">2</span> <span class="o">+</span> <span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="kt">T</span><span class="p">]</span>
<span class="kr">where</span>
<span class="kr">type</span> <span class="kt">T</span> <span class="ow">=</span> <span class="mi">8</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mi">2</span> <span class="c1">// `T` and `x` are in scope of `2 + x : `[T]`</span>
<span class="kr">if</span> <span class="n">x</span> <span class="kr">then</span> <span class="mi">1</span> <span class="kr">else</span> <span class="mi">2</span>
<span class="kr">where</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">2</span> <span class="c1">// `x` is in scope in the whole `if`</span>
<span class="nf">\</span><span class="n">y</span> <span class="ow">-&gt;</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span>
<span class="kr">where</span> <span class="n">x</span> <span class="ow">=</span> <span class="mi">2</span> <span class="c1">// `y` is not in scope in the defintion of `x`</span>
</pre></div>
</div>
</div>
<div class="section" id="block-arguments">
<h2>Block Arguments<a class="headerlink" href="#block-arguments" title="Permalink to this headline"></a></h2>
<p>When used as the last argument to a function call,
<code class="docutils literal notranslate"><span class="pre">if</span></code> and lambda expressions do not need parens:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span> <span class="nf">\</span><span class="n">x</span> <span class="ow">-&gt;</span> <span class="n">x</span> <span class="c1">// call `f` with one argument `x -&gt; x`</span>
<span class="mi">2</span> <span class="o">+</span> <span class="kr">if</span> <span class="n">x</span>
<span class="kr">then</span> <span class="n">y</span>
<span class="kr">else</span> <span class="n">z</span> <span class="c1">// call `+` with two arguments: `2` and `if ...`</span>
</pre></div>
</div>
</div>
<div class="section" id="conditionals">
<h2>Conditionals<a class="headerlink" href="#conditionals" title="Permalink to this headline"></a></h2>
<p>The <code class="docutils literal notranslate"><span class="pre">if</span> <span class="pre">...</span> <span class="pre">then</span> <span class="pre">...</span> <span class="pre">else</span></code> construct can be used with
multiple branches. For example:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">x</span> <span class="ow">=</span> <span class="kr">if</span> <span class="n">y</span> <span class="o">%</span> <span class="mi">2</span> <span class="o">==</span> <span class="mi">0</span> <span class="kr">then</span> <span class="mi">22</span> <span class="kr">else</span> <span class="mi">33</span>
<span class="nf">x</span> <span class="ow">=</span> <span class="kr">if</span> <span class="n">y</span> <span class="o">%</span> <span class="mi">2</span> <span class="o">==</span> <span class="mi">0</span> <span class="kr">then</span> <span class="mi">1</span>
<span class="o">|</span> <span class="n">y</span> <span class="o">%</span> <span class="mi">3</span> <span class="o">==</span> <span class="mi">0</span> <span class="kr">then</span> <span class="mi">2</span>
<span class="o">|</span> <span class="n">y</span> <span class="o">%</span> <span class="mi">5</span> <span class="o">==</span> <span class="mi">0</span> <span class="kr">then</span> <span class="mi">3</span>
<span class="kr">else</span> <span class="mi">7</span>
</pre></div>
</div>
</div>
<div class="section" id="demoting-numeric-types-to-values">
<h2>Demoting Numeric Types to Values<a class="headerlink" href="#demoting-numeric-types-to-values" title="Permalink to this headline"></a></h2>
<p>The value corresponding to a numeric type may be accessed using the
following notation:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="p">`</span><span class="n">t</span>
</pre></div>
</div>
<p>Here <cite>t</cite> 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:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="p">`</span><span class="n">t</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Literal</span> <span class="n">t</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span>
</pre></div>
</div>
<p>This backtick notation is syntax sugar for an application of the
<cite>number</cite> primtive, so the above may be written as:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">number</span><span class="p">`{</span><span class="n">t</span><span class="p">}</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Literal</span> <span class="n">t</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span>
</pre></div>
</div>
<p>If a type cannot be inferred from context, a suitable type will be
automatically chosen if possible, usually <cite>Integer</cite>.</p>
</div>
</div>
</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="BasicSyntax.html" class="btn btn-neutral float-left" title="Basic Syntax" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="BasicTypes.html" class="btn btn-neutral float-right" title="Basic Types" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>
<hr/>
<div role="contentinfo">
<p>&#169; Copyright 2021, The Cryptol Team.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</body>
</html>

792
docs/RefMan/_build/html/Modules.html Normal file
View File

@ -0,0 +1,792 @@
<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Modules &mdash; Cryptol 2.11.0 documentation</title>
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<!--[if lt IE 9]>
<script src="_static/js/html5shiv.min.js"></script>
<![endif]-->
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="prev" title="Type Declarations" href="TypeDeclarations.html" />
</head>
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="RefMan.html" class="icon icon-home"> Cryptol
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a></li>
<li class="toctree-l1"><a class="reference internal" href="Expressions.html">Expressions</a></li>
<li class="toctree-l1"><a class="reference internal" href="BasicTypes.html">Basic Types</a></li>
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">Modules</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#hierarchical-module-names">Hierarchical Module Names</a></li>
<li class="toctree-l2"><a class="reference internal" href="#module-imports">Module Imports</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#import-lists">Import Lists</a></li>
<li class="toctree-l3"><a class="reference internal" href="#hiding-imports">Hiding Imports</a></li>
<li class="toctree-l3"><a class="reference internal" href="#qualified-module-imports">Qualified Module Imports</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#private-blocks">Private Blocks</a></li>
<li class="toctree-l2"><a class="reference internal" href="#nested-modules">Nested Modules</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#implicit-imports">Implicit Imports</a></li>
<li class="toctree-l3"><a class="reference internal" href="#managing-module-names">Managing Module Names</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#parameterized-modules">Parameterized Modules</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#interface-modules">Interface Modules</a></li>
<li class="toctree-l3"><a class="reference internal" href="#importing-an-interface-module">Importing an Interface Module</a></li>
<li class="toctree-l3"><a class="reference internal" href="#interface-constraints">Interface Constraints</a></li>
<li class="toctree-l3"><a class="reference internal" href="#instantiating-a-parameterized-module">Instantiating a Parameterized Module</a></li>
<li class="toctree-l3"><a class="reference internal" href="#anonymous-interface-modules">Anonymous Interface Modules</a></li>
<li class="toctree-l3"><a class="reference internal" href="#anonymous-instantiation-arguments">Anonymous Instantiation Arguments</a></li>
<li class="toctree-l3"><a class="reference internal" href="#anonymous-import-instantiations">Anonymous Import Instantiations</a></li>
<li class="toctree-l3"><a class="reference internal" href="#passing-through-module-parameters">Passing Through Module Parameters</a></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="RefMan.html">Cryptol</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="RefMan.html" class="icon icon-home"></a> &raquo;</li>
<li>Modules</li>
<li class="wy-breadcrumbs-aside">
<a href="_sources/Modules.rst.txt" rel="nofollow"> View page source</a>
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<div class="section" id="modules">
<h1>Modules<a class="headerlink" href="#modules" title="Permalink to this headline"></a></h1>
<p>A <em>module</em> is used to group some related definitions. Each file may
contain at most one top-level module.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="kr">type</span> <span class="kt">T</span> <span class="ow">=</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="nf">f</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="nf">f</span> <span class="ow">=</span> <span class="mi">10</span>
</pre></div>
</div>
<div class="section" id="hierarchical-module-names">
<h2>Hierarchical Module Names<a class="headerlink" href="#hierarchical-module-names" title="Permalink to this headline"></a></h2>
<p>Module may have either simple or <em>hierarchical</em> names.
Hierarchical names are constructed by gluing together ordinary
identifiers using the symbol <code class="docutils literal notranslate"><span class="pre">::</span></code>.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">Hash</span><span class="ow">::</span><span class="kt">SHA256</span> <span class="kr">where</span>
<span class="nf">sha256</span> <span class="ow">=</span> <span class="o">...</span>
</pre></div>
</div>
<p>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 <code class="docutils literal notranslate"><span class="pre">Hash::SHA256</span></code>, Cryptol
will look for a file named <code class="docutils literal notranslate"><span class="pre">SHA256.cry</span></code> in a directory called
<code class="docutils literal notranslate"><span class="pre">Hash</span></code>, contained in one of the directories specified by <code class="docutils literal notranslate"><span class="pre">CRYPTOLPATH</span></code>.</p>
</div>
<div class="section" id="module-imports">
<h2>Module Imports<a class="headerlink" href="#module-imports" title="Permalink to this headline"></a></h2>
<p>To use the definitions from one module in another module, we use
<code class="docutils literal notranslate"><span class="pre">import</span></code> declarations:</p>
<div class="literal-block-wrapper docutils container" id="id1">
<div class="code-block-caption"><span class="caption-text">module M</span><a class="headerlink" href="#id1" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// Provide some definitions</span>
<span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="nf">f</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="nf">f</span> <span class="ow">=</span> <span class="mi">2</span>
</pre></div>
</div>
</div>
<div class="literal-block-wrapper docutils container" id="id2">
<div class="code-block-caption"><span class="caption-text">module N</span><a class="headerlink" href="#id2" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// Uses definitions from `M`</span>
<span class="kr">module</span> <span class="nn">N</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">M</span> <span class="c1">// import all definitions from `M`</span>
<span class="nf">g</span> <span class="ow">=</span> <span class="n">f</span> <span class="c1">// `f` was imported from `M`</span>
</pre></div>
</div>
</div>
<div class="section" id="import-lists">
<h3>Import Lists<a class="headerlink" href="#import-lists" title="Permalink to this headline"></a></h3>
<p>Sometimes, we may want to import only some of the definitions
from a module. To do so, we use an import declaration with
an <em>import list</em>.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="nf">f</span> <span class="ow">=</span> <span class="mh">0x02</span>
<span class="nf">g</span> <span class="ow">=</span> <span class="mh">0x03</span>
<span class="nf">h</span> <span class="ow">=</span> <span class="mh">0x04</span>
</pre></div>
</div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">N</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">M</span><span class="p">(</span><span class="n">f</span><span class="p">,</span><span class="n">g</span><span class="p">)</span> <span class="c1">// Imports only `f` and `g`, but not `h`</span>
<span class="nf">x</span> <span class="ow">=</span> <span class="n">f</span> <span class="o">+</span> <span class="n">g</span>
</pre></div>
</div>
<p>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.</p>
</div>
<div class="section" id="hiding-imports">
<h3>Hiding Imports<a class="headerlink" href="#hiding-imports" title="Permalink to this headline"></a></h3>
<p>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 <em>hiding</em> import:</p>
<div class="literal-block-wrapper docutils container" id="id3">
<div class="code-block-caption"><span class="caption-text">module M</span><a class="headerlink" href="#id3" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="nf">f</span> <span class="ow">=</span> <span class="mh">0x02</span>
<span class="nf">g</span> <span class="ow">=</span> <span class="mh">0x03</span>
<span class="nf">h</span> <span class="ow">=</span> <span class="mh">0x04</span>
</pre></div>
</div>
</div>
<div class="literal-block-wrapper docutils container" id="id4">
<div class="code-block-caption"><span class="caption-text">module N</span><a class="headerlink" href="#id4" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">N</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">M</span> <span class="k">hiding</span> <span class="p">(</span><span class="nf">h</span><span class="p">)</span> <span class="c1">// Import everything but `h`</span>
<span class="nf">x</span> <span class="ow">=</span> <span class="n">f</span> <span class="o">+</span> <span class="n">g</span>
</pre></div>
</div>
</div>
</div>
<div class="section" id="qualified-module-imports">
<h3>Qualified Module Imports<a class="headerlink" href="#qualified-module-imports" title="Permalink to this headline"></a></h3>
<p>Another way to avoid name collisions is by using a
<em>qualified</em> import.</p>
<div class="literal-block-wrapper docutils container" id="id5">
<div class="code-block-caption"><span class="caption-text">module M</span><a class="headerlink" href="#id5" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="nf">f</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="nf">f</span> <span class="ow">=</span> <span class="mi">2</span>
</pre></div>
</div>
</div>
<div class="literal-block-wrapper docutils container" id="id6">
<div class="code-block-caption"><span class="caption-text">module N</span><a class="headerlink" href="#id6" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">N</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">M</span> <span class="k">as</span> <span class="n">P</span>
<span class="nf">g</span> <span class="ow">=</span> <span class="kt">P</span><span class="ow">::</span><span class="n">f</span>
<span class="c1">// `f` was imported from `M`</span>
<span class="c1">// but when used it needs to be prefixed by the qualifier `P`</span>
</pre></div>
</div>
</div>
<p>Qualified imports make it possible to work with definitions
that happen to have the same name but are defined in different modules.</p>
<p>Qualified imports may be combined with import lists or hiding clauses:</p>
<div class="literal-block-wrapper docutils container" id="id7">
<div class="code-block-caption"><span class="caption-text">Example</span><a class="headerlink" href="#id7" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">import</span> <span class="nn">A</span> <span class="k">as</span> <span class="n">B</span> <span class="p">(</span><span class="n">f</span><span class="p">)</span> <span class="c1">// introduces B::f</span>
<span class="kr">import</span> <span class="nn">X</span> <span class="k">as</span> <span class="n">Y</span> <span class="n">hiding</span> <span class="p">(</span><span class="n">f</span><span class="p">)</span> <span class="c1">// introduces everything but `f` from X</span>
<span class="c1">// using the prefix `X`</span>
</pre></div>
</div>
</div>
<p>It is also possible to use the same qualifier prefix for imports
from different modules. For example:</p>
<div class="literal-block-wrapper docutils container" id="id8">
<div class="code-block-caption"><span class="caption-text">Example</span><a class="headerlink" href="#id8" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">import</span> <span class="nn">A</span> <span class="k">as</span> <span class="n">B</span>
<span class="kr">import</span> <span class="nn">X</span> <span class="k">as</span> <span class="n">B</span>
</pre></div>
</div>
</div>
<p>Such declarations will introduces all definitions from <code class="docutils literal notranslate"><span class="pre">A</span></code> and <code class="docutils literal notranslate"><span class="pre">X</span></code>
but to use them, you would have to qualify using the prefix <code class="docutils literal notranslate"><span class="pre">B::</span></code>.</p>
</div>
</div>
<div class="section" id="private-blocks">
<h2>Private Blocks<a class="headerlink" href="#private-blocks" title="Permalink to this headline"></a></h2>
<p>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 <em>private blocks</em>:</p>
<div class="literal-block-wrapper docutils container" id="id9">
<div class="code-block-caption"><span class="caption-text">Private blocks</span><a class="headerlink" href="#id9" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="nf">f</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="nf">f</span> <span class="ow">=</span> <span class="mh">0x01</span> <span class="o">+</span> <span class="n">helper1</span> <span class="o">+</span> <span class="n">helper2</span>
<span class="nf">private</span>
<span class="n">helper1</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="n">helper1</span> <span class="ow">=</span> <span class="mi">2</span>
<span class="n">helper2</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="n">helper2</span> <span class="ow">=</span> <span class="mi">3</span>
</pre></div>
</div>
</div>
<p>The private block only needs to be indented if it might be followed by
additional public declarations. If all remaining declarations are to be
private then no additional indentation is needed as the <code class="docutils literal notranslate"><span class="pre">private</span></code> block will
extend to the end of the module.</p>
<div class="literal-block-wrapper docutils container" id="id10">
<div class="code-block-caption"><span class="caption-text">Private blocks</span><a class="headerlink" href="#id10" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="nf">f</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="nf">f</span> <span class="ow">=</span> <span class="mh">0x01</span> <span class="o">+</span> <span class="n">helper1</span> <span class="o">+</span> <span class="n">helper2</span>
<span class="nf">private</span>
<span class="nf">helper1</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="nf">helper1</span> <span class="ow">=</span> <span class="mi">2</span>
<span class="nf">helper2</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="nf">helper2</span> <span class="ow">=</span> <span class="mi">3</span>
</pre></div>
</div>
</div>
<p>The keyword <code class="docutils literal notranslate"><span class="pre">private</span></code> 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:</p>
<div class="literal-block-wrapper docutils container" id="id11">
<div class="code-block-caption"><span class="caption-text">Private blocks</span><a class="headerlink" href="#id11" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="nf">f</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="nf">f</span> <span class="ow">=</span> <span class="mh">0x01</span> <span class="o">+</span> <span class="n">helper1</span> <span class="o">+</span> <span class="n">helper2</span>
<span class="nf">private</span>
<span class="n">helper1</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="n">helper1</span> <span class="ow">=</span> <span class="mi">2</span>
<span class="nf">private</span>
<span class="n">helper2</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="n">helper2</span> <span class="ow">=</span> <span class="mi">3</span>
</pre></div>
</div>
</div>
</div>
<div class="section" id="nested-modules">
<h2>Nested Modules<a class="headerlink" href="#nested-modules" title="Permalink to this headline"></a></h2>
<p>Module may be declared withing other modules, using the <code class="docutils literal notranslate"><span class="pre">submodule</span></code> keword.</p>
<div class="literal-block-wrapper docutils container" id="id12">
<div class="code-block-caption"><span class="caption-text">Declaring a nested module called N</span><a class="headerlink" href="#id12" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mh">0x02</span>
<span class="n">submodule</span> <span class="kt">N</span> <span class="kr">where</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span>
</pre></div>
</div>
</div>
<p>Submodules may refer to names in their enclosing scope.
Declarations in a sub-module will shadow names in the outer scope.</p>
<p>Declarations in a submdule may be imported with <code class="docutils literal notranslate"><span class="pre">import</span> <span class="pre">submodule</span></code>,
which works just like an ordinary import except that <code class="docutils literal notranslate"><span class="pre">X</span></code> refers
to the name of a submodule.</p>
<div class="literal-block-wrapper docutils container" id="id13">
<div class="code-block-caption"><span class="caption-text">Using declarations from a submodule.</span><a class="headerlink" href="#id13" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mh">0x02</span>
<span class="n">submodule</span> <span class="kt">N</span> <span class="kr">where</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span>
<span class="kr">import</span> <span class="nn">submodule</span> <span class="kt">N</span> <span class="n">as</span> <span class="kt">P</span>
<span class="n">z</span> <span class="ow">=</span> <span class="mi">2</span> <span class="o">*</span> <span class="kt">P</span><span class="ow">::</span><span class="n">y</span>
</pre></div>
</div>
</div>
<p>Note that recursive definitions across modules are not allowed.
So, in the previous example, it would be an error if <code class="docutils literal notranslate"><span class="pre">y</span></code> was
to try to use <code class="docutils literal notranslate"><span class="pre">z</span></code> in its definition.</p>
<div class="section" id="implicit-imports">
<h3>Implicit Imports<a class="headerlink" href="#implicit-imports" title="Permalink to this headline"></a></h3>
<p>For convenience, we add an implicit qualified submodule import for
each locally defined submodules.</p>
<div class="literal-block-wrapper docutils container" id="id14">
<div class="code-block-caption"><span class="caption-text">Making use of the implicit import for a submodule.</span><a class="headerlink" href="#id14" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mh">0x02</span>
<span class="n">submodule</span> <span class="kt">N</span> <span class="kr">where</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span>
<span class="n">z</span> <span class="ow">=</span> <span class="mi">2</span> <span class="o">*</span> <span class="kt">N</span><span class="ow">::</span><span class="n">y</span>
</pre></div>
</div>
</div>
<p><code class="docutils literal notranslate"><span class="pre">N::y</span></code> works in the previous example because Cryptol added
an implicit import <code class="docutils literal notranslate"><span class="pre">import</span> <span class="pre">submoulde</span> <span class="pre">N</span> <span class="pre">as</span> <span class="pre">N</span></code>.</p>
</div>
<div class="section" id="managing-module-names">
<h3>Managing Module Names<a class="headerlink" href="#managing-module-names" title="Permalink to this headline"></a></h3>
<p>The names of nested modules are managed by the module system just
like the name of any other declaration in Cryptol. Thus, nested
modules may declared in the public or private sections of their
containing module, and need to be imported before they can be used.
Thus, to use a submodule defined in top-level module <code class="docutils literal notranslate"><span class="pre">A</span></code> into
another top-level module <code class="docutils literal notranslate"><span class="pre">B</span></code> requires two steps:</p>
<blockquote>
<div><ol class="arabic simple">
<li><p>First we need to import <code class="docutils literal notranslate"><span class="pre">A</span></code> to bring the name of the submodule in scope</p></li>
<li><p>Then we need to import the submodule to bring the names defined in it in scope.</p></li>
</ol>
</div></blockquote>
<div class="literal-block-wrapper docutils container" id="id15">
<div class="code-block-caption"><span class="caption-text">Using a nested module from a different top-level module.</span><a class="headerlink" href="#id15" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">A</span> <span class="kr">where</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mh">0x02</span>
<span class="n">submodule</span> <span class="kt">N</span> <span class="kr">where</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span>
<span class="kr">module</span> <span class="nn">B</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">A</span> <span class="c1">// Brings `N` in scope</span>
<span class="kr">import</span> <span class="nn">submodule</span> <span class="kt">N</span> <span class="c1">// Brings `y` in scope</span>
<span class="n">z</span> <span class="ow">=</span> <span class="mi">2</span> <span class="o">*</span> <span class="n">y</span>
</pre></div>
</div>
</div>
</div>
</div>
<div class="section" id="parameterized-modules">
<h2>Parameterized Modules<a class="headerlink" href="#parameterized-modules" title="Permalink to this headline"></a></h2>
<div class="admonition warning">
<p class="admonition-title">Warning</p>
<p>The documentation in this section is for the upcoming variant of
the feature, which is not yet part of main line Cryptol.</p>
</div>
<div class="section" id="interface-modules">
<h3>Interface Modules<a class="headerlink" href="#interface-modules" title="Permalink to this headline"></a></h3>
<p>An <em>interface module</em> describes the content of a module
without providing a concrete implementation.</p>
<div class="literal-block-wrapper docutils container" id="id16">
<div class="code-block-caption"><span class="caption-text">An interface module.</span><a class="headerlink" href="#id16" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">interface</span> <span class="kr">module</span> <span class="nn">I</span> <span class="kr">where</span>
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span> <span class="c1">// `n` is a numeric type</span>
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">&gt;=</span> <span class="mi">1</span><span class="p">)</span>
<span class="c1">// Assumptions about the declared numeric type</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span> <span class="c1">// A declarations of a constant</span>
</pre></div>
</div>
</div>
<p>Like other modules, interfaces modules may be nested in
other modules:</p>
<div class="literal-block-wrapper docutils container" id="id17">
<div class="code-block-caption"><span class="caption-text">A nested interface module</span><a class="headerlink" href="#id17" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="n">interface</span> <span class="n">submodule</span> <span class="kt">I</span> <span class="kr">where</span>
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span> <span class="c1">// `n` is a numeric type</span>
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">&gt;=</span> <span class="mi">1</span><span class="p">)</span>
<span class="c1">// Assumptions about the declared numeric type</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span> <span class="c1">// A declarations of a constant</span>
</pre></div>
</div>
</div>
</div>
<div class="section" id="importing-an-interface-module">
<h3>Importing an Interface Module<a class="headerlink" href="#importing-an-interface-module" title="Permalink to this headline"></a></h3>
<p>A module may be parameterized by importing an interface,
instead of a concrete module</p>
<div class="literal-block-wrapper docutils container" id="id18">
<div class="code-block-caption"><span class="caption-text">A parameterized module</span><a class="headerlink" href="#id18" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// The interface desribes the parmaeters</span>
<span class="nf">interface</span> <span class="kr">module</span> <span class="nn">I</span> <span class="kr">where</span>
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">&gt;=</span> <span class="mi">1</span><span class="p">)</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="c1">// This module is parameterized</span>
<span class="kr">module</span> <span class="nn">F</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span>
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
</pre></div>
</div>
</div>
<p>To import a nested interface use <code class="docutils literal notranslate"><span class="pre">import</span> <span class="pre">interface</span> <span class="pre">sumbodule</span> <span class="pre">I</span></code>
and make sure that <code class="docutils literal notranslate"><span class="pre">I</span></code> is in scope.</p>
<p>It is also possible to import multiple interface modules,
or the same interface module more than once. Each import
of an interface module maybe be linked to a different concrete
module, as described in <a class="reference internal" href="#instantiating-modules"><span class="std std-ref">Instantiating a Parameterized Module</span></a>.</p>
<div class="literal-block-wrapper docutils container" id="id19">
<div class="code-block-caption"><span class="caption-text">Multiple interface parameters</span><a class="headerlink" href="#id19" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">interface</span> <span class="kr">module</span> <span class="nn">I</span> <span class="kr">where</span>
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">&gt;=</span> <span class="mi">1</span><span class="p">)</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="kr">module</span> <span class="nn">F</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">I</span>
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">J</span>
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="kt">I</span><span class="ow">::</span><span class="n">n</span><span class="p">]</span>
<span class="n">y</span> <span class="ow">=</span> <span class="kt">I</span><span class="ow">::</span><span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
<span class="n">z</span> <span class="kt">:</span> <span class="p">[</span><span class="kt">J</span><span class="ow">::</span><span class="n">n</span><span class="p">]</span>
<span class="n">z</span> <span class="ow">=</span> <span class="kt">J</span><span class="ow">::</span><span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
</pre></div>
</div>
</div>
</div>
<div class="section" id="interface-constraints">
<h3>Interface Constraints<a class="headerlink" href="#interface-constraints" title="Permalink to this headline"></a></h3>
<p>When working with multiple interfaces, it is to useful
to be able to impose additional constraints on the
types imported from the interface.</p>
<div class="literal-block-wrapper docutils container" id="id20">
<div class="code-block-caption"><span class="caption-text">Adding constraints to interface parameters</span><a class="headerlink" href="#id20" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">interface</span> <span class="kr">module</span> <span class="nn">I</span> <span class="kr">where</span>
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">&gt;=</span> <span class="mi">1</span><span class="p">)</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="kr">module</span> <span class="nn">F</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">I</span>
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">J</span>
<span class="n">interface</span> <span class="n">constraint</span> <span class="p">(</span><span class="kt">I</span><span class="ow">::</span><span class="n">n</span> <span class="o">==</span> <span class="kt">J</span><span class="ow">::</span><span class="n">n</span><span class="p">)</span>
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="kt">I</span><span class="ow">::</span><span class="n">n</span><span class="p">]</span>
<span class="n">y</span> <span class="ow">=</span> <span class="kt">I</span><span class="ow">::</span><span class="n">x</span> <span class="o">+</span> <span class="kt">J</span><span class="ow">::</span><span class="n">x</span>
</pre></div>
</div>
</div>
<p>In this example we impose the constraint that <code class="docutils literal notranslate"><span class="pre">n</span></code>
(the width of <code class="docutils literal notranslate"><span class="pre">x</span></code>) in both interfaces must be the
same. Note that, of course, the two instantiations
may provide different values for <code class="docutils literal notranslate"><span class="pre">x</span></code>.</p>
</div>
<div class="section" id="instantiating-a-parameterized-module">
<span id="instantiating-modules"></span><h3>Instantiating a Parameterized Module<a class="headerlink" href="#instantiating-a-parameterized-module" title="Permalink to this headline"></a></h3>
<p>To use a parameterized module we need to provide concrete
implementations for the interfaces that it uses, and provide
a name for the resulting module. This is done as follows:</p>
<div class="literal-block-wrapper docutils container" id="id21">
<div class="code-block-caption"><span class="caption-text">Instantiating a parameterized module using a single interface.</span><a class="headerlink" href="#id21" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">interface</span> <span class="kr">module</span> <span class="nn">I</span> <span class="kr">where</span>
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">&gt;=</span> <span class="mi">1</span><span class="p">)</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="kr">module</span> <span class="nn">F</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span>
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
<span class="kr">module</span> <span class="nn">Impl</span> <span class="kr">where</span>
<span class="kr">type</span> <span class="n">n</span> <span class="ow">=</span> <span class="mi">8</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mi">26</span>
<span class="kr">module</span> <span class="nn">MyF</span> <span class="ow">=</span> <span class="kt">F</span> <span class="p">{</span> <span class="kt">Impl</span> <span class="p">}</span>
</pre></div>
</div>
</div>
<p>Here we defined a new module called <code class="docutils literal notranslate"><span class="pre">MyF</span></code> which is
obtained by filling in module <code class="docutils literal notranslate"><span class="pre">Impl</span></code> for the interface
used by <code class="docutils literal notranslate"><span class="pre">F</span></code>.</p>
<p>If a module is parameterized my multiple interfaces
we need to provide an implementation module for each
interface, using a slight variation on the previous notation.</p>
<div class="literal-block-wrapper docutils container" id="id22">
<div class="code-block-caption"><span class="caption-text">Instantiating a parameterized module by name.</span><a class="headerlink" href="#id22" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// I is defined as above</span>
<span class="kr">module</span> <span class="nn">F</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">I</span>
<span class="kr">import</span> <span class="nn">interface</span> <span class="kt">I</span> <span class="n">as</span> <span class="kt">J</span>
<span class="n">interface</span> <span class="n">constraint</span> <span class="p">(</span><span class="kt">I</span><span class="ow">::</span><span class="n">n</span> <span class="o">==</span> <span class="kt">J</span><span class="ow">::</span><span class="n">n</span><span class="p">)</span>
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="kt">I</span><span class="ow">::</span><span class="n">n</span><span class="p">]</span>
<span class="n">y</span> <span class="ow">=</span> <span class="kt">I</span><span class="ow">::</span><span class="n">x</span> <span class="o">+</span> <span class="kt">J</span><span class="ow">::</span><span class="n">x</span>
<span class="kr">module</span> <span class="nn">Impl1</span> <span class="kr">where</span>
<span class="kr">type</span> <span class="n">n</span> <span class="ow">=</span> <span class="mi">8</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mi">26</span>
<span class="kr">module</span> <span class="nn">Impl2</span> <span class="kr">where</span>
<span class="kr">type</span> <span class="n">n</span> <span class="ow">=</span> <span class="mi">8</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mi">30</span>
<span class="kr">module</span> <span class="nn">MyF</span> <span class="ow">=</span> <span class="kt">F</span> <span class="p">{</span> <span class="kt">I</span> <span class="ow">=</span> <span class="kt">Impl1</span><span class="p">,</span> <span class="kt">J</span> <span class="ow">=</span> <span class="kt">Impl</span> <span class="mi">2</span> <span class="p">}</span>
</pre></div>
</div>
</div>
<p>Each interface import is identified by its name,
which is derived from the <code class="docutils literal notranslate"><span class="pre">as</span></code> clause on the
interface import. If there is no <code class="docutils literal notranslate"><span class="pre">as</span></code> clause,
then the name of the parameter is derived from
the name of the interface itself.</p>
<p>Since interfaces are identified by name, the
order in which they are provided is not important.</p>
<p>Modules defined by instantiation may be nested,
just like any other module:</p>
<div class="literal-block-wrapper docutils container" id="id23">
<div class="code-block-caption"><span class="caption-text">Nested module instantiation.</span><a class="headerlink" href="#id23" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">Somewhere</span> <span class="c1">// defines G</span>
<span class="n">submodule</span> <span class="kt">F</span> <span class="ow">=</span> <span class="n">submodule</span> <span class="kt">G</span> <span class="p">{</span> <span class="kt">I</span> <span class="p">}</span>
</pre></div>
</div>
</div>
<p>In this example, <code class="docutils literal notranslate"><span class="pre">submodule</span> <span class="pre">F</span></code> is defined
by instantiating some other parameterized
module <code class="docutils literal notranslate"><span class="pre">G</span></code>, presumably imported from <code class="docutils literal notranslate"><span class="pre">Somewhere</span></code>.
Note that in this case the argument to the instantiation
<code class="docutils literal notranslate"><span class="pre">I</span></code> is a top-level module, because it is not
preceded by the <code class="docutils literal notranslate"><span class="pre">submodule</span></code> keyword.</p>
<p>To pass a nested module as the argument of a function,
use <code class="docutils literal notranslate"><span class="pre">submodule</span> <span class="pre">I</span></code> like this:</p>
<div class="literal-block-wrapper docutils container" id="id24">
<div class="code-block-caption"><span class="caption-text">Nested module instantiation.</span><a class="headerlink" href="#id24" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">Somewhere</span> <span class="c1">// defines G and I</span>
<span class="n">submodule</span> <span class="kt">F</span> <span class="ow">=</span> <span class="n">submodule</span> <span class="kt">G</span> <span class="p">{</span> <span class="n">submodule</span> <span class="kt">I</span> <span class="p">}</span>
</pre></div>
</div>
</div>
</div>
<div class="section" id="anonymous-interface-modules">
<h3>Anonymous Interface Modules<a class="headerlink" href="#anonymous-interface-modules" title="Permalink to this headline"></a></h3>
<p>If we need to just parameterize a module by a couple of types/values,
it is quite cumbersome to have to define a whole separate interface module.
To make this more convenient we provide the following notation for defining
an anonymous interface and using it straight away:</p>
<div class="literal-block-wrapper docutils container" id="id25">
<div class="code-block-caption"><span class="caption-text">Simple parameterized module.</span><a class="headerlink" href="#id25" title="Permalink to this code"></a></div>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="n">parameter</span>
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
<span class="kr">type</span> <span class="n">constraint</span> <span class="p">(</span><span class="kr">fin</span> <span class="n">n</span><span class="p">,</span> <span class="n">n</span> <span class="o">&gt;=</span> <span class="mi">1</span><span class="p">)</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="n">f</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="n">f</span> <span class="ow">=</span> <span class="mi">1</span> <span class="o">+</span> <span class="n">x</span>
</pre></div>
</div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">parameter</span></code> block defines an interface module and uses it.
Note that the parameters may not use things defined in <code class="docutils literal notranslate"><span class="pre">M</span></code> as
the interface is declared outside of <code class="docutils literal notranslate"><span class="pre">M</span></code>.</p>
</div>
<div class="section" id="anonymous-instantiation-arguments">
<h3>Anonymous Instantiation Arguments<a class="headerlink" href="#anonymous-instantiation-arguments" title="Permalink to this headline"></a></h3>
<p>Sometimes it is also a bit cumbersome to have to define a whole
separate module just to pass it as an argument to some parameterized
module. To make this more convenient we support the following notion
for instantiation a module:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// A parameterized module</span>
<span class="kr">module</span> <span class="nn">M</span> <span class="kr">where</span>
<span class="n">parameter</span>
<span class="kr">type</span> <span class="n">n</span> <span class="kt">:</span> <span class="o">#</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="n">y</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="n">f</span> <span class="kt">:</span> <span class="p">[</span><span class="n">n</span><span class="p">]</span>
<span class="n">f</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span>
<span class="c1">// A module instantiation</span>
<span class="kr">module</span> <span class="nn">N</span> <span class="ow">=</span> <span class="kt">M</span>
<span class="kr">where</span>
<span class="kr">type</span> <span class="n">n</span> <span class="ow">=</span> <span class="mi">32</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mi">11</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">helper</span>
<span class="n">helper</span> <span class="ow">=</span> <span class="mi">12</span>
</pre></div>
</div>
<p>The declarations in the <code class="docutils literal notranslate"><span class="pre">where</span></code> block are treated as the
definition of an anonymous module which is passed as the argument
to parameterized module <code class="docutils literal notranslate"><span class="pre">M</span></code>.</p>
</div>
<div class="section" id="anonymous-import-instantiations">
<h3>Anonymous Import Instantiations<a class="headerlink" href="#anonymous-import-instantiations" title="Permalink to this headline"></a></h3>
<p>We provide syntactic sugar for importing and instantiating a functor
at the same time:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">submodule</span> <span class="kt">F</span> <span class="kr">where</span>
<span class="n">parameter</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
<span class="kr">import</span> <span class="nn">submodule</span> <span class="kt">F</span> <span class="kr">where</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mi">2</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">where</span></code> block may is the same as the <code class="docutils literal notranslate"><span class="pre">where</span></code> block in
expressions: you may define type synonyms and values, but nothing else
(e.g., no <code class="docutils literal notranslate"><span class="pre">newtype</span></code>).</p>
<p>It is also possible to import and instantiate using an existing module
like this:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">submodule</span> <span class="kt">F</span> <span class="kr">where</span>
<span class="n">parameter</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
<span class="nf">submodule</span> <span class="kt">G</span> <span class="kr">where</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mi">7</span>
<span class="kr">import</span> <span class="nn">submodule</span> <span class="kt">F</span> <span class="p">{</span> <span class="n">submodule</span> <span class="kt">G</span> <span class="p">}</span>
</pre></div>
</div>
<p>Semantically, instantiating imports declare a local nested module and
import it. For example, the <code class="docutils literal notranslate"><span class="pre">where</span></code> import from above is equivalent
to the following declarations:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">submodule</span> <span class="kt">F</span> <span class="kr">where</span>
<span class="n">parameter</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
<span class="nf">submodule</span> <span class="kt">M</span> <span class="kr">where</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mi">2</span>
<span class="nf">submodule</span> <span class="kt">N</span> <span class="ow">=</span> <span class="n">submodule</span> <span class="kt">F</span> <span class="p">{</span> <span class="n">submodule</span> <span class="kt">M</span> <span class="p">}</span>
<span class="kr">import</span> <span class="nn">submodule</span> <span class="kt">N</span>
</pre></div>
</div>
</div>
<div class="section" id="passing-through-module-parameters">
<h3>Passing Through Module Parameters<a class="headerlink" href="#passing-through-module-parameters" title="Permalink to this headline"></a></h3>
<p>Occasionally it is useful to define a functor that instantiates <em>another</em>
functor using the same parameters as the functor being defined
(i.e., a functor parameter is passed on to another functor). This can
be done by using the keyword <code class="docutils literal notranslate"><span class="pre">interface</span></code> followed by the name of a parameter
in an instantiation. Here is an example:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">interface</span> <span class="n">submodule</span> <span class="kt">S</span> <span class="kr">where</span>
<span class="n">x</span> <span class="kt">:</span> <span class="p">[</span><span class="mi">8</span><span class="p">]</span>
<span class="c1">// A functor, parameterized on S</span>
<span class="nf">submodule</span> <span class="kt">G</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">interface</span> <span class="n">submodule</span> <span class="kt">S</span>
<span class="n">y</span> <span class="ow">=</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span>
<span class="c1">// Another functor, also parameterize on S</span>
<span class="nf">submodule</span> <span class="kt">F</span> <span class="kr">where</span>
<span class="kr">import</span> <span class="nn">interface</span> <span class="n">submodule</span> <span class="kt">S</span> <span class="n">as</span> <span class="kt">A</span>
<span class="c1">// Instantiate `G` using parameter `A` of `F`</span>
<span class="kr">import</span> <span class="nn">submodule</span> <span class="kt">G</span> <span class="p">{</span> <span class="n">interface</span> <span class="kt">A</span> <span class="p">}</span> <span class="c1">// Brings `y` in scope</span>
<span class="n">z</span> <span class="ow">=</span> <span class="kt">A</span><span class="ow">::</span><span class="n">x</span> <span class="o">+</span> <span class="n">y</span>
<span class="c1">// Brings `z` into scope: z = A::x + y</span>
<span class="c1">// = 5 + (5 + 1)</span>
<span class="c1">// = 11</span>
<span class="kr">import</span> <span class="nn">submodule</span> <span class="kt">F</span> <span class="kr">where</span>
<span class="n">x</span> <span class="ow">=</span> <span class="mi">5</span>
</pre></div>
</div>
</div>
</div>
</div>
</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="TypeDeclarations.html" class="btn btn-neutral float-left" title="Type Declarations" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
</div>
<hr/>
<div role="contentinfo">
<p>&#169; Copyright 2021, The Cryptol Team.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</body>
</html>

212
docs/RefMan/_build/html/OverloadedOperations.html Normal file
View File

@ -0,0 +1,212 @@
<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Overloaded Operations &mdash; Cryptol 2.11.0 documentation</title>
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<!--[if lt IE 9]>
<script src="_static/js/html5shiv.min.js"></script>
<![endif]-->
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="next" title="Type Declarations" href="TypeDeclarations.html" />
<link rel="prev" title="Basic Types" href="BasicTypes.html" />
</head>
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="RefMan.html" class="icon icon-home"> Cryptol
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a></li>
<li class="toctree-l1"><a class="reference internal" href="Expressions.html">Expressions</a></li>
<li class="toctree-l1"><a class="reference internal" href="BasicTypes.html">Basic Types</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">Overloaded Operations</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#equality">Equality</a></li>
<li class="toctree-l2"><a class="reference internal" href="#comparisons">Comparisons</a></li>
<li class="toctree-l2"><a class="reference internal" href="#signed-comparisons">Signed Comparisons</a></li>
<li class="toctree-l2"><a class="reference internal" href="#zero">Zero</a></li>
<li class="toctree-l2"><a class="reference internal" href="#logical-operations">Logical Operations</a></li>
<li class="toctree-l2"><a class="reference internal" href="#basic-arithmetic">Basic Arithmetic</a></li>
<li class="toctree-l2"><a class="reference internal" href="#integral-operations">Integral Operations</a></li>
<li class="toctree-l2"><a class="reference internal" href="#division">Division</a></li>
<li class="toctree-l2"><a class="reference internal" href="#rounding">Rounding</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
</ul>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="RefMan.html">Cryptol</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="RefMan.html" class="icon icon-home"></a> &raquo;</li>
<li>Overloaded Operations</li>
<li class="wy-breadcrumbs-aside">
<a href="_sources/OverloadedOperations.rst.txt" rel="nofollow"> View page source</a>
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<div class="section" id="overloaded-operations">
<h1>Overloaded Operations<a class="headerlink" href="#overloaded-operations" title="Permalink to this headline"></a></h1>
<div class="section" id="equality">
<h2>Equality<a class="headerlink" href="#equality" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Eq</span>
<span class="p">(</span><span class="o">==</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Eq</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
<span class="p">(</span><span class="o">!=</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Eq</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
<span class="p">(</span><span class="o">===</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">}</span> <span class="p">(</span><span class="kt">Eq</span> <span class="n">b</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="p">(</span><span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">b</span><span class="p">)</span> <span class="ow">-&gt;</span> <span class="p">(</span><span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">b</span><span class="p">)</span> <span class="ow">-&gt;</span> <span class="p">(</span><span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span><span class="p">)</span>
<span class="p">(</span><span class="o">!==</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">}</span> <span class="p">(</span><span class="kt">Eq</span> <span class="n">b</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="p">(</span><span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">b</span><span class="p">)</span> <span class="ow">-&gt;</span> <span class="p">(</span><span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">b</span><span class="p">)</span> <span class="ow">-&gt;</span> <span class="p">(</span><span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span><span class="p">)</span>
</pre></div>
</div>
</div>
<div class="section" id="comparisons">
<h2>Comparisons<a class="headerlink" href="#comparisons" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">Cmp</span>
<span class="p">(</span><span class="o">&lt;</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
<span class="p">(</span><span class="o">&gt;</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
<span class="p">(</span><span class="o">&lt;=</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
<span class="p">(</span><span class="o">&gt;=</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
<span class="kr">min</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="kr">max</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="n">abs</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">,</span> <span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
</pre></div>
</div>
</div>
<div class="section" id="signed-comparisons">
<h2>Signed Comparisons<a class="headerlink" href="#signed-comparisons" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">SignedCmp</span>
<span class="p">(</span><span class="o">&lt;$</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">SignedCmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
<span class="p">(</span><span class="o">&gt;$</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">SignedCmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
<span class="p">(</span><span class="o">&lt;=$</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">SignedCmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
<span class="p">(</span><span class="o">&gt;=$</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">SignedCmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kr">Bit</span>
</pre></div>
</div>
</div>
<div class="section" id="zero">
<h2>Zero<a class="headerlink" href="#zero" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Zero</span>
<span class="n">zero</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Zero</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span>
</pre></div>
</div>
</div>
<div class="section" id="logical-operations">
<h2>Logical Operations<a class="headerlink" href="#logical-operations" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Logic</span>
<span class="p">(</span><span class="o">&amp;&amp;</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Logic</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="p">(</span><span class="o">||</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Logic</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="p">(</span><span class="o">^</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Logic</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="n">complement</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Logic</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
</pre></div>
</div>
</div>
<div class="section" id="basic-arithmetic">
<h2>Basic Arithmetic<a class="headerlink" href="#basic-arithmetic" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Ring</span>
<span class="n">fromInteger</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="kt">Integer</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="p">(</span><span class="o">+</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="p">(</span><span class="o">-</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="p">(</span><span class="o">*</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="n">negate</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="p">(</span><span class="o">^^</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">,</span> <span class="n">e</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">,</span> <span class="kt">Integral</span> <span class="n">e</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">e</span> <span class="ow">-&gt;</span> <span class="n">a</span>
</pre></div>
</div>
</div>
<div class="section" id="integral-operations">
<h2>Integral Operations<a class="headerlink" href="#integral-operations" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Integral</span>
<span class="p">(</span><span class="o">/</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Integral</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="p">(</span><span class="o">%</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Integral</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="p">(</span><span class="o">^^</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">,</span> <span class="n">e</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">,</span> <span class="kt">Integral</span> <span class="n">e</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">e</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="n">toInteger</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Integral</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kt">Integer</span>
<span class="n">infFrom</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Integral</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="p">[</span><span class="kr">inf</span><span class="p">]</span><span class="n">a</span>
<span class="n">infFromThen</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Integral</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="p">[</span><span class="kr">inf</span><span class="p">]</span><span class="n">a</span>
</pre></div>
</div>
</div>
<div class="section" id="division">
<h2>Division<a class="headerlink" href="#division" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Field</span>
<span class="n">recip</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Field</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
<span class="p">(</span><span class="o">/.</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Field</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="n">a</span>
</pre></div>
</div>
</div>
<div class="section" id="rounding">
<h2>Rounding<a class="headerlink" href="#rounding" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Round</span>
<span class="n">ceiling</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Round</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kt">Integer</span>
<span class="n">floor</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Round</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kt">Integer</span>
<span class="n">trunc</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Round</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kt">Integer</span>
<span class="n">roundAway</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Round</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kt">Integer</span>
<span class="n">roundToEven</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Round</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="n">a</span> <span class="ow">-&gt;</span> <span class="kt">Integer</span>
</pre></div>
</div>
</div>
</div>
</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="BasicTypes.html" class="btn btn-neutral float-left" title="Basic Types" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="TypeDeclarations.html" class="btn btn-neutral float-right" title="Type Declarations" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>
<hr/>
<div role="contentinfo">
<p>&#169; Copyright 2021, The Cryptol Team.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</body>
</html>

1453
docs/RefMan/_build/html/RefMan.html
View File

File diff suppressed because it is too large Load Diff

154
docs/RefMan/_build/html/TypeDeclarations.html Normal file
View File

@ -0,0 +1,154 @@
<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Type Declarations &mdash; Cryptol 2.11.0 documentation</title>
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<!--[if lt IE 9]>
<script src="_static/js/html5shiv.min.js"></script>
<![endif]-->
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="next" title="Modules" href="Modules.html" />
<link rel="prev" title="Overloaded Operations" href="OverloadedOperations.html" />
</head>
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="RefMan.html" class="icon icon-home"> Cryptol
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a></li>
<li class="toctree-l1"><a class="reference internal" href="Expressions.html">Expressions</a></li>
<li class="toctree-l1"><a class="reference internal" href="BasicTypes.html">Basic Types</a></li>
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">Type Declarations</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#type-synonyms">Type Synonyms</a></li>
<li class="toctree-l2"><a class="reference internal" href="#newtypes">Newtypes</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
</ul>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="RefMan.html">Cryptol</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="RefMan.html" class="icon icon-home"></a> &raquo;</li>
<li>Type Declarations</li>
<li class="wy-breadcrumbs-aside">
<a href="_sources/TypeDeclarations.rst.txt" rel="nofollow"> View page source</a>
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<div class="section" id="type-declarations">
<h1>Type Declarations<a class="headerlink" href="#type-declarations" title="Permalink to this headline"></a></h1>
<div class="section" id="type-synonyms">
<h2>Type Synonyms<a class="headerlink" href="#type-synonyms" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">type</span> <span class="kt">T</span> <span class="n">a</span> <span class="n">b</span> <span class="ow">=</span> <span class="p">[</span><span class="n">a</span><span class="p">]</span> <span class="n">b</span>
</pre></div>
</div>
<p>A <code class="docutils literal notranslate"><span class="pre">type</span></code> 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.</p>
</div>
<div class="section" id="newtypes">
<h2>Newtypes<a class="headerlink" href="#newtypes" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">newtype</span> <span class="kt">NewT</span> <span class="n">a</span> <span class="n">b</span> <span class="ow">=</span> <span class="p">{</span> <span class="nb">seq</span> <span class="kt">:</span> <span class="p">[</span><span class="n">a</span><span class="p">]</span><span class="n">b</span> <span class="p">}</span>
</pre></div>
</div>
<p>A <code class="docutils literal notranslate"><span class="pre">newtype</span></code> declaration declares a new named type which is defined by
a record body. Unlike type synonyms, each named <code class="docutils literal notranslate"><span class="pre">newtype</span></code> is treated
as a distinct type by the type checker, even if they have the same
bodies. Moreover, types created by a <code class="docutils literal notranslate"><span class="pre">newtype</span></code> 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.</p>
<p>Every <code class="docutils literal notranslate"><span class="pre">newtype</span></code> declaration brings into scope a new function with the
same name as the type which can be used to create values of the
newtype.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">x</span> <span class="kt">:</span> <span class="kt">NewT</span> <span class="mi">3</span> <span class="kt">Integer</span>
<span class="nf">x</span> <span class="ow">=</span> <span class="kt">NewT</span> <span class="p">{</span> <span class="nb">seq</span> <span class="ow">=</span> <span class="p">[</span><span class="mi">1</span><span class="p">,</span><span class="mi">2</span><span class="p">,</span><span class="mi">3</span><span class="p">]</span> <span class="p">}</span>
</pre></div>
</div>
<p>Just as with records, field projections can be used directly on values
of newtypes to extract the values in the body of the type.</p>
<div class="highlight-none notranslate"><div class="highlight"><pre><span></span>&gt; sum x.seq
6
</pre></div>
</div>
</div>
</div>
</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="OverloadedOperations.html" class="btn btn-neutral float-left" title="Overloaded Operations" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="Modules.html" class="btn btn-neutral float-right" title="Modules" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>
<hr/>
<div role="contentinfo">
<p>&#169; Copyright 2021, The Cryptol Team.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</body>
</html>

283
docs/RefMan/_build/html/_sources/BasicSyntax.rst.txt Normal file
View File

@ -0,0 +1,283 @@
Basic Syntax
============
Declarations
------------
.. code-block:: cryptol
f x = x + y + z
Type Signatures
---------------
.. code-block:: cryptol
f,g : {a,b} (fin a) => [a] b
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. Consider, for example,
the following Cryptol declarations:
.. code-block:: cryptol
f x = x + y + z
where
y = x * x
z = x + y
g y = y
This group has two declarations, one for `f` and one for `g`. All the
lines between `f` and `g` that are indented more than `f` belong to
`f`. The same principle applies to the declarations in the ``where`` block
of `f`, which defines two more local names, `y` and `z`.
Comments
--------
Cryptol supports block comments, which start with ``/*`` and end with
``*/``, and line comments, which start with ``//`` and terminate at the
end of the line. Block comments may be nested arbitrarily.
.. code-block:: cryptol
/* This is a block comment */
// This is a line comment
/* This is a /* Nested */ block comment */
.. todo::
Document ``/** */``
Identifiers
-----------
Cryptol identifiers consist of one or more characters. The first
character must be either an English letter or underscore (``_``). The
following characters may be an English letter, a decimal digit,
underscore (``_``), or a prime (``'``). Some identifiers have special
meaning in the language, so they may not be used in programmer-defined
names (see `Keywords and Built-in Operators`_).
.. code-block:: cryptol
:caption: Examples of identifiers
name name1 name' longer_name
Name Name2 Name'' longerName
Keywords and Built-in Operators
-------------------------------
The following identifiers have special meanings in Cryptol, and may
not be used for programmer defined names:
.. The table below can be generated by running `chop.hs` on this list:
else
extern
if
private
include
module
submodule
interface
newtype
pragma
property
then
type
where
let
import
as
hiding
infixl
infixr
infix
primitive
parameter
constraint
down
by
.. _Keywords:
.. code-block:: none
:caption: Keywords
as extern include interface parameter property where
by hiding infix let pragma submodule else
constraint if infixl module primitive then
down import infixr newtype private type
The following table contains Cryptol's operators and their
associativity with lowest precedence operators first, and highest
precedence last.
.. table:: Operator precedences
+-----------------------------------------+-----------------+
| Operator | Associativity |
+=========================================+=================+
| ``==>`` | right |
+-----------------------------------------+-----------------+
| ``\/`` | right |
+-----------------------------------------+-----------------+
| ``/\`` | right |
+-----------------------------------------+-----------------+
| ``==`` ``!=`` ``===`` ``!==`` | not associative |
+-----------------------------------------+-----------------+
| ``>`` ``<`` ``<=`` ``>=`` | not associative |
| ``<$`` ``>$`` ``<=$`` ``>=$`` | |
+-----------------------------------------+-----------------+
| ``||`` | right |
+-----------------------------------------+-----------------+
| ``^`` | left |
+-----------------------------------------+-----------------+
| ``&&`` | right |
+-----------------------------------------+-----------------+
| ``#`` | right |
+-----------------------------------------+-----------------+
| ``>>`` ``<<`` ``>>>`` ``<<<`` ``>>$`` | left |
+-----------------------------------------+-----------------+
| ``+`` ``-`` | left |
+-----------------------------------------+-----------------+
| ``*`` ``/`` ``%`` ``/$`` ``%$`` | left |
+-----------------------------------------+-----------------+
| ``^^`` | right |
+-----------------------------------------+-----------------+
| ``@`` ``@@`` ``!`` ``!!`` | left |
+-----------------------------------------+-----------------+
| (unary) ``-`` ``~`` | right |
+-----------------------------------------+-----------------+
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.
.. table:: Type-level operators
+------------+----------------------------------------+
| Operator | Meaning |
+============+========================================+
| ``+`` | Addition |
+------------+----------------------------------------+
| ``-`` | Subtraction |
+------------+----------------------------------------+
| ``*`` | Multiplication |
+------------+----------------------------------------+
| ``/`` | Division |
+------------+----------------------------------------+
| ``/^`` | Ceiling division (``/`` rounded up) |
+------------+----------------------------------------+
| ``%`` | Modulus |
+------------+----------------------------------------+
| ``%^`` | Ceiling modulus (compute padding) |
+------------+----------------------------------------+
| ``^^`` | Exponentiation |
+------------+----------------------------------------+
| ``lg2`` | Ceiling logarithm (base 2) |
+------------+----------------------------------------+
| ``width`` | Bit width (equal to ``lg2(n+1)``) |
+------------+----------------------------------------+
| ``max`` | Maximum |
+------------+----------------------------------------+
| ``min`` | Minimum |
+------------+----------------------------------------+
Numeric Literals
----------------
Numeric literals may be written in binary, octal, decimal, or
hexadecimal notation. The base of a literal is determined by its prefix:
``0b`` for binary, ``0o`` for octal, no special prefix for
decimal, and ``0x`` for hexadecimal.
.. code-block:: cryptol
:caption: Examples of literals
254 // Decimal literal
0254 // Decimal literal
0b11111110 // Binary literal
0o376 // Octal literal
0xFE // Hexadecimal literal
0xfe // Hexadecimal literal
Numeric literals in binary, octal, or hexadecimal notation result in
bit sequences of a fixed length (i.e., they have type ``[n]`` for
some `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:
.. code-block:: cryptol
:caption: Literals and their types
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
Numeric literals may also be written as polynomials by writing a polynomial
expression in terms of `x` between an opening ``<|`` and a closing ``|>``.
Numeric literals in polynomial notation result in bit sequences of length
one more than the degree of the polynomial. Examples:
.. code-block:: cryptol
:caption: Polynomial literals
<| x^^6 + x^^4 + x^^2 + x^^1 + 1 |> // : [7], equal to 0b1010111
<| x^^4 + x^^3 + x |> // : [5], equal to 0b11010
Cryptol also supports fractional literals using binary (prefix ``0b``),
octal (prefix ``0o``), decimal (no prefix), and hexadecimal (prefix ``ox``)
digits. A fractional literal must contain a ``.`` 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 ``p``.
Decimal fractional literals use exponent base 10, and the symbol ``e``.
Examples:
.. code-block:: cryptol
:caption: Fractional literals
10.2
10.2e3 // 10.2 * 10^3
0x30.1 // 3 * 64 + 1/16
0x30.1p4 // (3 * 64 + 1/16) * 2^4
All fractional literals are overloaded and may be used with types that support
fractional numbers (e.g., ``Rational``, and the ``Float`` family of types).
Some types (e.g. the ``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 ``_``, which has no effect on the
literal value but may be used to improve readability. Here are some examples:
.. code-block:: cryptol
:caption: Using _
0b_0000_0010
0x_FFFF_FFEA

211
docs/RefMan/_build/html/_sources/BasicTypes.rst.txt Normal file
View File

@ -0,0 +1,211 @@
Basic Types
===========
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:
.. code-block:: cryptol
(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
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:
.. code-block:: cryptol
(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
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.
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:
.. code-block:: cryptol
(15, 20).0 == 15
(15, 20).1 == 20
{ x = 15, y = 20 }.x == 15
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:
.. code-block:: cryptol
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
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:
.. code-block:: cryptol
getFst (x,_) = x
distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
f p = x + y where
(x, y) = p
Selectors are also lifted through sequence and function types, point-wise,
so that the following equations should hold:
.. code-block:: cryptol
xs.l == [ x.l | x <- xs ] // sequences
f.l == \x -> (f x).l // functions
Thus, if we have a sequence of tuples, ``xs``, then we can quickly obtain a
sequence with only the tuples' first components by writing ``xs.0``.
Similarly, if we have a function, ``f``, that computes a tuple of results,
then we can write ``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.
Updating Fields
~~~~~~~~~~~~~~~
The components of a record or a tuple may be updated using the following
notation:
.. code-block:: cryptol
// 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 }
Sequences
---------
A sequence is a fixed-length collection of elements of the same type.
The type of a finite sequence of length `n`, with elements of type `a`
is ``[n] a``. Often, a finite sequence of bits, ``[n] Bit``, is called a
*word*. We may abbreviate the type ``[n] Bit`` as ``[n]``. An infinite
sequence with elements of type `a` has type ``[inf] a``, and ``[inf]`` is
an infinite stream of bits.
.. code-block:: cryptol
[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
Note: the bounds in finite sequences (those with `..`) are type
expressions, while the bounds in infinite sequences are value
expressions.
.. table:: Sequence operations.
+------------------------------+---------------------------------------------+
| Operator | Description |
+==============================+=============================================+
| ``#`` | Sequence concatenation |
+------------------------------+---------------------------------------------+
| ``>>`` ``<<`` | Shift (right, left) |
+------------------------------+---------------------------------------------+
| ``>>>`` ``<<<`` | Rotate (right, left) |
+------------------------------+---------------------------------------------+
| ``>>$`` | Arithmetic right shift (on bitvectors only) |
+------------------------------+---------------------------------------------+
| ``@`` ``!`` | Access elements (front, back) |
+------------------------------+---------------------------------------------+
| ``@@`` ``!!`` | Access sub-sequence (front, back) |
+------------------------------+---------------------------------------------+
| ``update`` ``updateEnd`` | Update the value of a sequence at |
| | a location |
| | (front, back) |
+------------------------------+---------------------------------------------+
| ``updates`` ``updatesEnd`` | Update multiple values of a sequence |
| | (front, back) |
+------------------------------+---------------------------------------------+
There are also lifted pointwise operations.
.. code-block:: cryptol
[p1, p2, p3, p4] // Sequence pattern
p1 # p2 // Split sequence pattern
Functions
---------
.. code-block:: cryptol
\p1 p2 -> e // Lambda expression
f p1 p2 = e // Function definition

162
docs/RefMan/_build/html/_sources/Expressions.rst.txt Normal file
View File

@ -0,0 +1,162 @@
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`.

730
docs/RefMan/_build/html/_sources/Modules.rst.txt Normal file
View File

@ -0,0 +1,730 @@
Modules
=======
A *module* is used to group some related definitions. Each file may
contain at most one top-level module.
.. code-block:: cryptol
module M where
type T = [8]
f : [8]
f = 10
Hierarchical Module Names
-------------------------
Module may have either simple or *hierarchical* names.
Hierarchical names are constructed by gluing together ordinary
identifiers using the symbol ``::``.
.. code-block:: cryptol
module Hash::SHA256 where
sha256 = ...
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 ``Hash::SHA256``, Cryptol
will look for a file named ``SHA256.cry`` in a directory called
``Hash``, contained in one of the directories specified by ``CRYPTOLPATH``.
Module Imports
--------------
To use the definitions from one module in another module, we use
``import`` declarations:
.. code-block:: cryptol
:caption: module M
// Provide some definitions
module M where
f : [8]
f = 2
.. code-block:: cryptol
:caption: module N
// Uses definitions from `M`
module N where
import M // import all definitions from `M`
g = f // `f` was imported from `M`
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 *import list*.
.. code-block:: cryptol
module M where
f = 0x02
g = 0x03
h = 0x04
.. code-block:: cryptol
module N where
import M(f,g) // Imports only `f` and `g`, but not `h`
x = f + g
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.
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 *hiding* import:
.. code-block:: cryptol
:caption: module M
module M where
f = 0x02
g = 0x03
h = 0x04
.. code-block:: cryptol
:caption: module N
module N where
import M hiding (h) // Import everything but `h`
x = f + g
Qualified Module Imports
~~~~~~~~~~~~~~~~~~~~~~~~
Another way to avoid name collisions is by using a
*qualified* import.
.. code-block:: cryptol
:caption: module M
module M where
f : [8]
f = 2
.. code-block:: cryptol
:caption: module N
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`
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:
.. code-block:: cryptol
:caption: Example
import A as B (f) // introduces B::f
import X as Y hiding (f) // introduces everything but `f` from X
// using the prefix `X`
It is also possible to use the same qualifier prefix for imports
from different modules. For example:
.. code-block:: cryptol
:caption: Example
import A as B
import X as B
Such declarations will introduces all definitions from ``A`` and ``X``
but to use them, you would have to qualify using the prefix ``B::``.
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 *private blocks*:
.. code-block:: cryptol
:caption: Private blocks
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
helper2 : [8]
helper2 = 3
The private block only needs to be indented if it might be followed by
additional public declarations. If all remaining declarations are to be
private then no additional indentation is needed as the ``private`` block will
extend to the end of the module.
.. code-block:: cryptol
:caption: Private blocks
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
helper2 : [8]
helper2 = 3
The keyword ``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:
.. code-block:: cryptol
:caption: Private blocks
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
private
helper2 : [8]
helper2 = 3
Nested Modules
--------------
Module may be declared withing other modules, using the ``submodule`` keword.
.. code-block:: cryptol
:caption: Declaring a nested module called N
module M where
x = 0x02
submodule N where
y = x + 2
Submodules may refer to names in their enclosing scope.
Declarations in a sub-module will shadow names in the outer scope.
Declarations in a submdule may be imported with ``import submodule``,
which works just like an ordinary import except that ``X`` refers
to the name of a submodule.
.. code-block:: cryptol
:caption: Using declarations from a submodule.
module M where
x = 0x02
submodule N where
y = x + 2
import submodule N as P
z = 2 * P::y
Note that recursive definitions across modules are not allowed.
So, in the previous example, it would be an error if ``y`` was
to try to use ``z`` in its definition.
Implicit Imports
~~~~~~~~~~~~~~~~
For convenience, we add an implicit qualified submodule import for
each locally defined submodules.
.. code-block:: cryptol
:caption: Making use of the implicit import for a submodule.
module M where
x = 0x02
submodule N where
y = x + 2
z = 2 * N::y
``N::y`` works in the previous example because Cryptol added
an implicit import ``import submoulde N as N``.
Managing Module Names
~~~~~~~~~~~~~~~~~~~~~
The names of nested modules are managed by the module system just
like the name of any other declaration in Cryptol. Thus, nested
modules may declared in the public or private sections of their
containing module, and need to be imported before they can be used.
Thus, to use a submodule defined in top-level module ``A`` into
another top-level module ``B`` requires two steps:
1. First we need to import ``A`` to bring the name of the submodule in scope
2. Then we need to import the submodule to bring the names defined in it in scope.
.. code-block:: cryptol
:caption: Using a nested module from a different top-level module.
module A where
x = 0x02
submodule N where
y = x + 2
module B where
import A // Brings `N` in scope
import submodule N // Brings `y` in scope
z = 2 * y
Parameterized Modules
---------------------
.. warning::
The documentation in this section is for the upcoming variant of
the feature, which is not yet part of main line Cryptol.
Interface Modules
~~~~~~~~~~~~~~~~~
An *interface module* describes the content of a module
without providing a concrete implementation.
.. code-block:: cryptol
:caption: An interface module.
interface module I where
type n : # // `n` is a numeric type
type constraint (fin n, n >= 1)
// Assumptions about the declared numeric type
x : [n] // A declarations of a constant
Like other modules, interfaces modules may be nested in
other modules:
.. code-block:: cryptol
:caption: A nested interface module
module M where
interface submodule I where
type n : # // `n` is a numeric type
type constraint (fin n, n >= 1)
// Assumptions about the declared numeric type
x : [n] // A declarations of a constant
Importing an Interface Module
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A module may be parameterized by importing an interface,
instead of a concrete module
.. code-block:: cryptol
:caption: A parameterized module
// The interface desribes the parmaeters
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
// This module is parameterized
module F where
import interface I
y : [n]
y = x + 1
To import a nested interface use ``import interface sumbodule I``
and make sure that ``I`` is in scope.
It is also possible to import multiple interface modules,
or the same interface module more than once. Each import
of an interface module maybe be linked to a different concrete
module, as described in :ref:`instantiating_modules`.
.. code-block:: cryptol
:caption: Multiple interface parameters
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
module F where
import interface I as I
import interface I as J
y : [I::n]
y = I::x + 1
z : [J::n]
z = J::x + 1
Interface Constraints
~~~~~~~~~~~~~~~~~~~~~
When working with multiple interfaces, it is to useful
to be able to impose additional constraints on the
types imported from the interface.
.. code-block:: cryptol
:caption: Adding constraints to interface parameters
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
module F where
import interface I as I
import interface I as J
interface constraint (I::n == J::n)
y : [I::n]
y = I::x + J::x
In this example we impose the constraint that ``n``
(the width of ``x``) in both interfaces must be the
same. Note that, of course, the two instantiations
may provide different values for ``x``.
.. _instantiating_modules:
Instantiating a Parameterized Module
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To use a parameterized module we need to provide concrete
implementations for the interfaces that it uses, and provide
a name for the resulting module. This is done as follows:
.. code-block:: cryptol
:caption: Instantiating a parameterized module using a single interface.
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
module F where
import interface I
y : [n]
y = x + 1
module Impl where
type n = 8
x = 26
module MyF = F { Impl }
Here we defined a new module called ``MyF`` which is
obtained by filling in module ``Impl`` for the interface
used by ``F``.
If a module is parameterized my multiple interfaces
we need to provide an implementation module for each
interface, using a slight variation on the previous notation.
.. code-block:: cryptol
:caption: Instantiating a parameterized module by name.
// I is defined as above
module F where
import interface I as I
import interface I as J
interface constraint (I::n == J::n)
y : [I::n]
y = I::x + J::x
module Impl1 where
type n = 8
x = 26
module Impl2 where
type n = 8
x = 30
module MyF = F { I = Impl1, J = Impl 2 }
Each interface import is identified by its name,
which is derived from the ``as`` clause on the
interface import. If there is no ``as`` clause,
then the name of the parameter is derived from
the name of the interface itself.
Since interfaces are identified by name, the
order in which they are provided is not important.
Modules defined by instantiation may be nested,
just like any other module:
.. code-block:: cryptol
:caption: Nested module instantiation.
module M where
import Somewhere // defines G
submodule F = submodule G { I }
In this example, ``submodule F`` is defined
by instantiating some other parameterized
module ``G``, presumably imported from ``Somewhere``.
Note that in this case the argument to the instantiation
``I`` is a top-level module, because it is not
preceded by the ``submodule`` keyword.
To pass a nested module as the argument of a function,
use ``submodule I`` like this:
.. code-block:: cryptol
:caption: Nested module instantiation.
module M where
import Somewhere // defines G and I
submodule F = submodule G { submodule I }
Anonymous Interface Modules
~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we need to just parameterize a module by a couple of types/values,
it is quite cumbersome to have to define a whole separate interface module.
To make this more convenient we provide the following notation for defining
an anonymous interface and using it straight away:
.. code-block:: cryptol
:caption: Simple parameterized module.
module M where
parameter
type n : #
type constraint (fin n, n >= 1)
x : [n]
f : [n]
f = 1 + x
The ``parameter`` block defines an interface module and uses it.
Note that the parameters may not use things defined in ``M`` as
the interface is declared outside of ``M``.
Anonymous Instantiation Arguments
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Sometimes it is also a bit cumbersome to have to define a whole
separate module just to pass it as an argument to some parameterized
module. To make this more convenient we support the following notion
for instantiation a module:
.. code-block:: cryptol
// 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
The declarations in the ``where`` block are treated as the
definition of an anonymous module which is passed as the argument
to parameterized module ``M``.
Anonymous Import Instantiations
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We provide syntactic sugar for importing and instantiating a functor
at the same time:
.. code-block:: cryptol
submodule F where
parameter
x : [8]
y = x + 1
import submodule F where
x = 2
The ``where`` block may is the same as the ``where`` block in
expressions: you may define type synonyms and values, but nothing else
(e.g., no ``newtype``).
It is also possible to import and instantiate using an existing module
like this:
.. code-block:: cryptol
submodule F where
parameter
x : [8]
y = x + 1
submodule G where
x = 7
import submodule F { submodule G }
Semantically, instantiating imports declare a local nested module and
import it. For example, the ``where`` import from above is equivalent
to the following declarations:
.. code-block:: cryptol
submodule F where
parameter
x : [8]
y = x + 1
submodule M where
x = 2
submodule N = submodule F { submodule M }
import submodule N
Passing Through Module Parameters
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Occasionally it is useful to define a functor that instantiates *another*
functor using the same parameters as the functor being defined
(i.e., a functor parameter is passed on to another functor). This can
be done by using the keyword ``interface`` followed by the name of a parameter
in an instantiation. Here is an example:
.. code-block:: cryptol
interface submodule S where
x : [8]
// A functor, parameterized on S
submodule G where
import interface submodule S
y = x + 1
// Another functor, also parameterize on S
submodule F where
import interface submodule S as A
// Instantiate `G` using parameter `A` of `F`
import submodule G { interface A } // Brings `y` in scope
z = A::x + y
// Brings `z` into scope: z = A::x + y
// = 5 + (5 + 1)
// = 11
import submodule F where
x = 5

107
docs/RefMan/_build/html/_sources/OverloadedOperations.rst.txt Normal file
View File

@ -0,0 +1,107 @@
Overloaded Operations
=====================
Equality
--------
.. code-block:: cryptol
Eq
(==) : {a} (Eq a) => a -> a -> Bit
(!=) : {a} (Eq a) => a -> a -> Bit
(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
Comparisons
-----------
.. code-block:: cryptol
Cmp
(<) : {a} (Cmp a) => a -> a -> Bit
(>) : {a} (Cmp a) => a -> a -> Bit
(<=) : {a} (Cmp a) => a -> a -> Bit
(>=) : {a} (Cmp a) => a -> a -> Bit
min : {a} (Cmp a) => a -> a -> a
max : {a} (Cmp a) => a -> a -> a
abs : {a} (Cmp a, Ring a) => a -> a
Signed Comparisons
------------------
.. code-block:: cryptol
SignedCmp
(<$) : {a} (SignedCmp a) => a -> a -> Bit
(>$) : {a} (SignedCmp a) => a -> a -> Bit
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
Zero
----
.. code-block:: cryptol
Zero
zero : {a} (Zero a) => a
Logical Operations
------------------
.. code-block:: cryptol
Logic
(&&) : {a} (Logic a) => a -> a -> a
(||) : {a} (Logic a) => a -> a -> a
(^) : {a} (Logic a) => a -> a -> a
complement : {a} (Logic a) => a -> a
Basic Arithmetic
----------------
.. code-block:: cryptol
Ring
fromInteger : {a} (Ring a) => Integer -> a
(+) : {a} (Ring a) => a -> a -> a
(-) : {a} (Ring a) => a -> a -> a
(*) : {a} (Ring a) => a -> a -> a
negate : {a} (Ring a) => a -> a
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
Integral Operations
-------------------
.. code-block:: cryptol
Integral
(/) : {a} (Integral a) => a -> a -> a
(%) : {a} (Integral a) => a -> a -> a
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
toInteger : {a} (Integral a) => a -> Integer
infFrom : {a} (Integral a) => a -> [inf]a
infFromThen : {a} (Integral a) => a -> a -> [inf]a
Division
--------
.. code-block:: cryptol
Field
recip : {a} (Field a) => a -> a
(/.) : {a} (Field a) => a -> a -> a
Rounding
--------
.. code-block:: cryptol
Round
ceiling : {a} (Round a) => a -> Integer
floor : {a} (Round a) => a -> Integer
trunc : {a} (Round a) => a -> Integer
roundAway : {a} (Round a) => a -> Integer
roundToEven : {a} (Round a) => a -> Integer

1255
docs/RefMan/_build/html/_sources/RefMan.rst.txt
View File

File diff suppressed because it is too large Load Diff

53
docs/RefMan/_build/html/_sources/TypeDeclarations.rst.txt Normal file
View File

@ -0,0 +1,53 @@
Type Declarations
=================
Type Synonyms
-------------
.. code-block:: cryptol
type T a b = [a] b
A ``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.
Newtypes
--------
.. code-block:: cryptol
newtype NewT a b = { seq : [a]b }
A ``newtype`` declaration declares a new named type which is defined by
a record body. Unlike type synonyms, each named ``newtype`` is treated
as a distinct type by the type checker, even if they have the same
bodies. Moreover, types created by a ``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 ``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.
.. code-block:: cryptol
x : NewT 3 Integer
x = NewT { seq = [1,2,3] }
Just as with records, field projections can be used directly on values
of newtypes to extract the values in the body of the type.
.. code-block:: none
> sum x.seq
6

322
docs/RefMan/_build/html/_static/basic.css
View File

@ -4,7 +4,7 @@
*
* Sphinx stylesheet -- basic theme.
*
* :copyright: Copyright 2007-2019 by the Sphinx team, see AUTHORS.
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
@ -15,6 +15,12 @@ div.clearer {
clear: both;
}
div.section::after {
display: block;
content: '';
clear: left;
}
/* -- relbar ---------------------------------------------------------------- */
div.related {
@ -124,7 +130,7 @@ ul.search li a {
font-weight: bold;
}
ul.search li div.context {
ul.search li p.context {
color: #888;
margin: 2px 0 0 30px;
text-align: left;
@ -231,6 +237,16 @@ a.headerlink {
visibility: hidden;
}
a.brackets:before,
span.brackets > a:before{
content: "[";
}
a.brackets:after,
span.brackets > a:after {
content: "]";
}
h1:hover > a.headerlink,
h2:hover > a.headerlink,
h3:hover > a.headerlink,
@ -261,19 +277,25 @@ p.rubric {
font-weight: bold;
}
img.align-left, .figure.align-left, object.align-left {
img.align-left, figure.align-left, .figure.align-left, object.align-left {
clear: left;
float: left;
margin-right: 1em;
}
img.align-right, .figure.align-right, object.align-right {
img.align-right, figure.align-right, .figure.align-right, object.align-right {
clear: right;
float: right;
margin-left: 1em;
}
img.align-center, .figure.align-center, object.align-center {
img.align-center, figure.align-center, .figure.align-center, object.align-center {
display: block;
margin-left: auto;
margin-right: auto;
}
img.align-default, figure.align-default, .figure.align-default {
display: block;
margin-left: auto;
margin-right: auto;
@ -287,30 +309,41 @@ img.align-center, .figure.align-center, object.align-center {
text-align: center;
}
.align-default {
text-align: center;
}
.align-right {
text-align: right;
}
/* -- sidebars -------------------------------------------------------------- */
div.sidebar {
div.sidebar,
aside.sidebar {
margin: 0 0 0.5em 1em;
border: 1px solid #ddb;
padding: 7px 7px 0 7px;
padding: 7px;
background-color: #ffe;
width: 40%;
float: right;
clear: right;
overflow-x: auto;
}
p.sidebar-title {
font-weight: bold;
}
div.admonition, div.topic, blockquote {
clear: left;
}
/* -- topics ---------------------------------------------------------------- */
div.topic {
border: 1px solid #ccc;
padding: 7px 7px 0 7px;
padding: 7px;
margin: 10px 0 10px 0;
}
@ -332,10 +365,6 @@ div.admonition dt {
font-weight: bold;
}
div.admonition dl {
margin-bottom: 0;
}
p.admonition-title {
margin: 0px 10px 5px 0px;
font-weight: bold;
@ -346,9 +375,30 @@ div.body p.centered {
margin-top: 25px;
}
/* -- content of sidebars/topics/admonitions -------------------------------- */
div.sidebar > :last-child,
aside.sidebar > :last-child,
div.topic > :last-child,
div.admonition > :last-child {
margin-bottom: 0;
}
div.sidebar::after,
aside.sidebar::after,
div.topic::after,
div.admonition::after,
blockquote::after {
display: block;
content: '';
clear: both;
}
/* -- tables ---------------------------------------------------------------- */
table.docutils {
margin-top: 10px;
margin-bottom: 10px;
border: 0;
border-collapse: collapse;
}
@ -358,6 +408,11 @@ table.align-center {
margin-right: auto;
}
table.align-default {
margin-left: auto;
margin-right: auto;
}
table caption span.caption-number {
font-style: italic;
}
@ -391,22 +446,34 @@ table.citation td {
border-bottom: none;
}
th > :first-child,
td > :first-child {
margin-top: 0px;
}
th > :last-child,
td > :last-child {
margin-bottom: 0px;
}
/* -- figures --------------------------------------------------------------- */
div.figure {
div.figure, figure {
margin: 0.5em;
padding: 0.5em;
}
div.figure p.caption {
div.figure p.caption, figcaption {
padding: 0.3em;
}
div.figure p.caption span.caption-number {
div.figure p.caption span.caption-number,
figcaption span.caption-number {
font-style: italic;
}
div.figure p.caption span.caption-text {
div.figure p.caption span.caption-text,
figcaption span.caption-text {
}
/* -- field list styles ----------------------------------------------------- */
@ -433,10 +500,71 @@ table.field-list td, table.field-list th {
/* -- hlist styles ---------------------------------------------------------- */
table.hlist {
margin: 1em 0;
}
table.hlist td {
vertical-align: top;
}
/* -- object description styles --------------------------------------------- */
.sig {
font-family: 'Consolas', 'Menlo', 'DejaVu Sans Mono', 'Bitstream Vera Sans Mono', monospace;
}
.sig-name, code.descname {
background-color: transparent;
font-weight: bold;
}
.sig-name {
font-size: 1.1em;
}
code.descname {
font-size: 1.2em;
}
.sig-prename, code.descclassname {
background-color: transparent;
}
.optional {
font-size: 1.3em;
}
.sig-paren {
font-size: larger;
}
.sig-param.n {
font-style: italic;
}
/* C++ specific styling */
.sig-inline.c-texpr,
.sig-inline.cpp-texpr {
font-family: unset;
}
.sig.c .k, .sig.c .kt,
.sig.cpp .k, .sig.cpp .kt {
color: #0033B3;
}
.sig.c .m,
.sig.cpp .m {
color: #1750EB;
}
.sig.c .s, .sig.c .sc,
.sig.cpp .s, .sig.cpp .sc {
color: #067D17;
}
/* -- other body styles ----------------------------------------------------- */
@ -460,11 +588,78 @@ ol.upperroman {
list-style: upper-roman;
}
:not(li) > ol > li:first-child > :first-child,
:not(li) > ul > li:first-child > :first-child {
margin-top: 0px;
}
:not(li) > ol > li:last-child > :last-child,
:not(li) > ul > li:last-child > :last-child {
margin-bottom: 0px;
}
ol.simple ol p,
ol.simple ul p,
ul.simple ol p,
ul.simple ul p {
margin-top: 0;
}
ol.simple > li:not(:first-child) > p,
ul.simple > li:not(:first-child) > p {
margin-top: 0;
}
ol.simple p,
ul.simple p {
margin-bottom: 0;
}
dl.footnote > dt,
dl.citation > dt {
float: left;
margin-right: 0.5em;
}
dl.footnote > dd,
dl.citation > dd {
margin-bottom: 0em;
}
dl.footnote > dd:after,
dl.citation > dd:after {
content: "";
clear: both;
}
dl.field-list {
display: grid;
grid-template-columns: fit-content(30%) auto;
}
dl.field-list > dt {
font-weight: bold;
word-break: break-word;
padding-left: 0.5em;
padding-right: 5px;
}
dl.field-list > dt:after {
content: ":";
}
dl.field-list > dd {
padding-left: 0.5em;
margin-top: 0em;
margin-left: 0em;
margin-bottom: 0em;
}
dl {
margin-bottom: 15px;
}
dd p {
dd > :first-child {
margin-top: 0px;
}
@ -478,6 +673,11 @@ dd {
margin-left: 30px;
}
dl > dd:last-child,
dl > dd:last-child > :last-child {
margin-bottom: 0;
}
dt:target, span.highlighted {
background-color: #fbe54e;
}
@ -491,14 +691,6 @@ dl.glossary dt {
font-size: 1.1em;
}
.optional {
font-size: 1.3em;
}
.sig-paren {
font-size: larger;
}
.versionmodified {
font-style: italic;
}
@ -537,6 +729,12 @@ dl.glossary dt {
font-style: oblique;
}
.classifier:before {
font-style: normal;
margin: 0.5em;
content: ":";
}
abbr, acronym {
border-bottom: dotted 1px;
cursor: help;
@ -549,6 +747,10 @@ pre {
overflow-y: hidden; /* fixes display issues on Chrome browsers */
}
pre, div[class*="highlight-"] {
clear: both;
}
span.pre {
-moz-hyphens: none;
-ms-hyphens: none;
@ -556,22 +758,57 @@ span.pre {
hyphens: none;
}
div[class*="highlight-"] {
margin: 1em 0;
}
td.linenos pre {
padding: 5px 0px;
border: 0;
background-color: transparent;
color: #aaa;
}
table.highlighttable {
margin-left: 0.5em;
display: block;
}
table.highlighttable tbody {
display: block;
}
table.highlighttable tr {
display: flex;
}
table.highlighttable td {
padding: 0 0.5em 0 0.5em;
margin: 0;
padding: 0;
}
table.highlighttable td.linenos {
padding-right: 0.5em;
}
table.highlighttable td.code {
flex: 1;
overflow: hidden;
}
.highlight .hll {
display: block;
}
div.highlight pre,
table.highlighttable pre {
margin: 0;
}
div.code-block-caption + div {
margin-top: 0;
}
div.code-block-caption {
margin-top: 1em;
padding: 2px 5px;
font-size: small;
}
@ -580,8 +817,14 @@ div.code-block-caption code {
background-color: transparent;
}
div.code-block-caption + div > div.highlight > pre {
margin-top: 0;
table.highlighttable td.linenos,
span.linenos,
div.highlight span.gp { /* gp: Generic.Prompt */
user-select: none;
-webkit-user-select: text; /* Safari fallback only */
-webkit-user-select: none; /* Chrome/Safari */
-moz-user-select: none; /* Firefox */
-ms-user-select: none; /* IE10+ */
}
div.code-block-caption span.caption-number {
@ -593,21 +836,7 @@ div.code-block-caption span.caption-text {
}
div.literal-block-wrapper {
padding: 1em 1em 0;
}
div.literal-block-wrapper div.highlight {
margin: 0;
}
code.descname {
background-color: transparent;
font-weight: bold;
font-size: 1.2em;
}
code.descclassname {
background-color: transparent;
margin: 1em 0;
}
code.xref, a code {
@ -648,8 +877,7 @@ span.eqno {
}
span.eqno a.headerlink {
position: relative;
left: 0px;
position: absolute;
z-index: 1;
}

4
docs/RefMan/_build/html/_static/css/theme.css
View File

File diff suppressed because one or more lines are too long

24
docs/RefMan/_build/html/_static/doctools.js
View File

@ -4,7 +4,7 @@
*
* Sphinx JavaScript utilities for all documentation.
*
* :copyright: Copyright 2007-2019 by the Sphinx team, see AUTHORS.
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
@ -29,9 +29,14 @@ if (!window.console || !console.firebug) {
/**
* small helper function to urldecode strings
*
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/decodeURIComponent#Decoding_query_parameters_from_a_URL
*/
jQuery.urldecode = function(x) {
return decodeURIComponent(x).replace(/\+/g, ' ');
if (!x) {
return x
}
return decodeURIComponent(x.replace(/\+/g, ' '));
};
/**
@ -87,14 +92,13 @@ jQuery.fn.highlightText = function(text, className) {
node.nextSibling));
node.nodeValue = val.substr(0, pos);
if (isInSVG) {
var bbox = span.getBBox();
var rect = document.createElementNS("http://www.w3.org/2000/svg", "rect");
rect.x.baseVal.value = bbox.x;
var bbox = node.parentElement.getBBox();
rect.x.baseVal.value = bbox.x;
rect.y.baseVal.value = bbox.y;
rect.width.baseVal.value = bbox.width;
rect.height.baseVal.value = bbox.height;
rect.setAttribute('class', className);
var parentOfText = node.parentNode.parentNode;
addItems.push({
"parent": node.parentNode,
"target": rect});
@ -284,10 +288,12 @@ var Documentation = {
},
initOnKeyListeners: function() {
$(document).keyup(function(event) {
$(document).keydown(function(event) {
var activeElementType = document.activeElement.tagName;
// don't navigate when in search box or textarea
if (activeElementType !== 'TEXTAREA' && activeElementType !== 'INPUT' && activeElementType !== 'SELECT') {
// don't navigate when in search box, textarea, dropdown or button
if (activeElementType !== 'TEXTAREA' && activeElementType !== 'INPUT' && activeElementType !== 'SELECT'
&& activeElementType !== 'BUTTON' && !event.altKey && !event.ctrlKey && !event.metaKey
&& !event.shiftKey) {
switch (event.keyCode) {
case 37: // left
var prevHref = $('link[rel="prev"]').prop('href');
@ -295,12 +301,14 @@ var Documentation = {
window.location.href = prevHref;
return false;
}
break;
case 39: // right
var nextHref = $('link[rel="next"]').prop('href');
if (nextHref) {
window.location.href = nextHref;
return false;
}
break;
}
}
});

4
docs/RefMan/_build/html/_static/documentation_options.js
View File

@ -3,8 +3,10 @@ var DOCUMENTATION_OPTIONS = {
VERSION: '2.11.0',
LANGUAGE: 'None',
COLLAPSE_INDEX: false,
BUILDER: 'html',
FILE_SUFFIX: '.html',
LINK_SUFFIX: '.html',
HAS_SOURCE: true,
SOURCELINK_SUFFIX: '.txt',
NAVIGATION_WITH_KEYS: false,
NAVIGATION_WITH_KEYS: false
};

10872
docs/RefMan/_build/html/_static/jquery-3.5.1.js vendored Normal file
View File

File diff suppressed because it is too large Load Diff

10367
docs/RefMan/_build/html/_static/jquery.js vendored
View File

File diff suppressed because one or more lines are too long

2
docs/RefMan/_build/html/_static/js/theme.js
View File

File diff suppressed because one or more lines are too long

6
docs/RefMan/_build/html/_static/language_data.js
View File

@ -5,7 +5,7 @@
* This script contains the language-specific data used by searchtools.js,
* namely the list of stopwords, stemmer, scorer and splitter.
*
* :copyright: Copyright 2007-2019 by the Sphinx team, see AUTHORS.
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
@ -13,7 +13,8 @@
var stopwords = ["a","and","are","as","at","be","but","by","for","if","in","into","is","it","near","no","not","of","on","or","such","that","the","their","then","there","these","they","this","to","was","will","with"];
/* Non-minified version JS is _stemmer.js if file is provided */
/* Non-minified version is copied as a separate JS file, is available */
/**
* Porter Stemmer
*/
@ -199,7 +200,6 @@ var Stemmer = function() {
var splitChars = (function() {
var result = {};
var singles = [96, 180, 187, 191, 215, 247, 749, 885, 903, 907, 909, 930, 1014, 1648,

115
docs/RefMan/_build/html/_static/searchtools.js
View File

@ -4,7 +4,7 @@
*
* Sphinx JavaScript utilities for the full-text search.
*
* :copyright: Copyright 2007-2019 by the Sphinx team, see AUTHORS.
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
@ -36,8 +36,10 @@ if (!Scorer) {
// query found in title
title: 15,
partialTitle: 7,
// query found in terms
term: 5
term: 5,
partialTerm: 2
};
}
@ -56,6 +58,19 @@ var Search = {
_queued_query : null,
_pulse_status : -1,
htmlToText : function(htmlString) {
var virtualDocument = document.implementation.createHTMLDocument('virtual');
var htmlElement = $(htmlString, virtualDocument);
htmlElement.find('.headerlink').remove();
docContent = htmlElement.find('[role=main]')[0];
if(docContent === undefined) {
console.warn("Content block not found. Sphinx search tries to obtain it " +
"via '[role=main]'. Could you check your theme or template.");
return "";
}
return docContent.textContent || docContent.innerText;
},
init : function() {
var params = $.getQueryParameters();
if (params.q) {
@ -120,7 +135,7 @@ var Search = {
this.out = $('#search-results');
this.title = $('<h2>' + _('Searching') + '</h2>').appendTo(this.out);
this.dots = $('<span></span>').appendTo(this.title);
this.status = $('<p style="display: none"></p>').appendTo(this.out);
this.status = $('<p class="search-summary">&nbsp;</p>').appendTo(this.out);
this.output = $('<ul class="search"/>').appendTo(this.out);
$('#search-progress').text(_('Preparing search...'));
@ -151,8 +166,7 @@ var Search = {
objectterms.push(tmp[i].toLowerCase());
}
if ($u.indexOf(stopwords, tmp[i].toLowerCase()) != -1 || tmp[i].match(/^\d+$/) ||
tmp[i] === "") {
if ($u.indexOf(stopwords, tmp[i].toLowerCase()) != -1 || tmp[i] === "") {
// skip this "word"
continue;
}
@ -234,8 +248,10 @@ var Search = {
// results left, load the summary and display it
if (results.length) {
var item = results.pop();
var listItem = $('<li style="display:none"></li>');
if (DOCUMENTATION_OPTIONS.FILE_SUFFIX === '') {
var listItem = $('<li></li>');
var requestUrl = "";
var linkUrl = "";
if (DOCUMENTATION_OPTIONS.BUILDER === 'dirhtml') {
// dirhtml builder
var dirname = item[0] + '/';
if (dirname.match(/\/index\/$/)) {
@ -243,44 +259,45 @@ var Search = {
} else if (dirname == 'index/') {
dirname = '';
}
listItem.append($('<a/>').attr('href',
DOCUMENTATION_OPTIONS.URL_ROOT + dirname +
highlightstring + item[2]).html(item[1]));
requestUrl = DOCUMENTATION_OPTIONS.URL_ROOT + dirname;
linkUrl = requestUrl;
} else {
// normal html builders
listItem.append($('<a/>').attr('href',
item[0] + DOCUMENTATION_OPTIONS.FILE_SUFFIX +
highlightstring + item[2]).html(item[1]));
requestUrl = DOCUMENTATION_OPTIONS.URL_ROOT + item[0] + DOCUMENTATION_OPTIONS.FILE_SUFFIX;
linkUrl = item[0] + DOCUMENTATION_OPTIONS.LINK_SUFFIX;
}
listItem.append($('<a/>').attr('href',
linkUrl +
highlightstring + item[2]).html(item[1]));
if (item[3]) {
listItem.append($('<span> (' + item[3] + ')</span>'));
Search.output.append(listItem);
listItem.slideDown(5, function() {
setTimeout(function() {
displayNextItem();
});
}, 5);
} else if (DOCUMENTATION_OPTIONS.HAS_SOURCE) {
var suffix = DOCUMENTATION_OPTIONS.SOURCELINK_SUFFIX;
if (suffix === undefined) {
suffix = '.txt';
}
$.ajax({url: DOCUMENTATION_OPTIONS.URL_ROOT + '_sources/' + item[5] + (item[5].slice(-suffix.length) === suffix ? '' : suffix),
$.ajax({url: requestUrl,
dataType: "text",
complete: function(jqxhr, textstatus) {
var data = jqxhr.responseText;
if (data !== '' && data !== undefined) {
listItem.append(Search.makeSearchSummary(data, searchterms, hlterms));
var summary = Search.makeSearchSummary(data, searchterms, hlterms);
if (summary) {
listItem.append(summary);
}
}
Search.output.append(listItem);
listItem.slideDown(5, function() {
setTimeout(function() {
displayNextItem();
});
}, 5);
}});
} else {
// no source available, just display title
Search.output.append(listItem);
listItem.slideDown(5, function() {
setTimeout(function() {
displayNextItem();
});
}, 5);
}
}
// search finished, update title and status message
@ -313,12 +330,13 @@ var Search = {
for (var prefix in objects) {
for (var name in objects[prefix]) {
var fullname = (prefix ? prefix + '.' : '') + name;
if (fullname.toLowerCase().indexOf(object) > -1) {
var fullnameLower = fullname.toLowerCase()
if (fullnameLower.indexOf(object) > -1) {
var score = 0;
var parts = fullname.split('.');
var parts = fullnameLower.split('.');
// check for different match types: exact matches of full name or
// "last name" (i.e. last dotted part)
if (fullname == object || parts[parts.length - 1] == object) {
if (fullnameLower == object || parts[parts.length - 1] == object) {
score += Scorer.objNameMatch;
// matches in last name
} else if (parts[parts.length - 1].indexOf(object) > -1) {
@ -364,6 +382,13 @@ var Search = {
return results;
},
/**
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Regular_Expressions
*/
escapeRegExp : function(string) {
return string.replace(/[.*+\-?^${}()|[\]\\]/g, '\\$&'); // $& means the whole matched string
},
/**
* search for full-text terms in the index
*/
@ -385,6 +410,20 @@ var Search = {
{files: terms[word], score: Scorer.term},
{files: titleterms[word], score: Scorer.title}
];
// add support for partial matches
if (word.length > 2) {
var word_regex = this.escapeRegExp(word);
for (var w in terms) {
if (w.match(word_regex) && !terms[word]) {
_o.push({files: terms[w], score: Scorer.partialTerm})
}
}
for (var w in titleterms) {
if (w.match(word_regex) && !titleterms[word]) {
_o.push({files: titleterms[w], score: Scorer.partialTitle})
}
}
}
// no match but word was a required one
if ($u.every(_o, function(o){return o.files === undefined;})) {
@ -404,7 +443,7 @@ var Search = {
for (j = 0; j < _files.length; j++) {
file = _files[j];
if (!(file in scoreMap))
scoreMap[file] = {}
scoreMap[file] = {};
scoreMap[file][word] = o.score;
}
});
@ -412,7 +451,7 @@ var Search = {
// create the mapping
for (j = 0; j < files.length; j++) {
file = files[j];
if (file in fileMap)
if (file in fileMap && fileMap[file].indexOf(word) === -1)
fileMap[file].push(word);
else
fileMap[file] = [word];
@ -424,8 +463,12 @@ var Search = {
var valid = true;
// check if all requirements are matched
if (fileMap[file].length != searchterms.length)
continue;
var filteredTermCount = // as search terms with length < 3 are discarded: ignore
searchterms.filter(function(term){return term.length > 2}).length
if (
fileMap[file].length != searchterms.length &&
fileMap[file].length != filteredTermCount
) continue;
// ensure that none of the excluded terms is in the search result
for (i = 0; i < excluded.length; i++) {
@ -456,7 +499,11 @@ var Search = {
* words. the first one is used to find the occurrence, the
* latter for highlighting it.
*/
makeSearchSummary : function(text, keywords, hlwords) {
makeSearchSummary : function(htmlText, keywords, hlwords) {
var text = Search.htmlToText(htmlText);
if (text == "") {
return null;
}
var textLower = text.toLowerCase();
var start = 0;
$.each(keywords, function() {
@ -468,7 +515,7 @@ var Search = {
var excerpt = ((start > 0) ? '...' : '') +
$.trim(text.substr(start, 240)) +
((start + 240 - text.length) ? '...' : '');
var rv = $('<div class="context"></div>').text(excerpt);
var rv = $('<p class="context"></p>').text(excerpt);
$.each(hlwords, function() {
rv = rv.highlightText(this, 'highlighted');
});

2042
docs/RefMan/_build/html/_static/underscore-1.13.1.js Normal file
View File

File diff suppressed because it is too large Load Diff

1711
docs/RefMan/_build/html/_static/underscore.js
View File

File diff suppressed because one or more lines are too long

156
docs/RefMan/_build/html/genindex.html
View File

@ -1,70 +1,31 @@
<!DOCTYPE html>
<html class="writer-html4" lang="en" >
<html class="writer-html5" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Index &mdash; Cryptol 2.11.0 documentation</title>
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<!--[if lt IE 9]>
<script src="_static/js/html5shiv.min.js"></script>
<![endif]-->
<script type="text/javascript" id="documentation_options" data-url_root="./" src="_static/documentation_options.js"></script>
<script type="text/javascript" src="_static/jquery.js"></script>
<script type="text/javascript" src="_static/underscore.js"></script>
<script type="text/javascript" src="_static/doctools.js"></script>
<script type="text/javascript" src="_static/language_data.js"></script>
<script type="text/javascript" src="_static/js/theme.js"></script>
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="#" />
<link rel="search" title="Search" href="search.html" />
</head>
<body class="wy-body-for-nav">
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="RefMan.html" class="icon icon-home"> Cryptol
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" />
@ -72,83 +33,40 @@
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
<ul>
<li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a></li>
<li class="toctree-l1"><a class="reference internal" href="Expressions.html">Expressions</a></li>
<li class="toctree-l1"><a class="reference internal" href="BasicTypes.html">Basic Types</a></li>
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
</ul>
</div>
<div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="main navigation">
<!-- Local TOC -->
<div class="local-toc"></div>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap">
<nav class="wy-nav-top" aria-label="top navigation">
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="RefMan.html">Cryptol</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="breadcrumbs navigation">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="RefMan.html" class="icon icon-home"></a> &raquo;</li>
<li>Index</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<h1 id="index">Index</h1>
@ -158,46 +76,30 @@
</div>
</div>
<footer>
<hr/>
<div role="contentinfo">
<p>
&#169; Copyright 2021, The Cryptol Team.
</p>
<p>&#169; Copyright 2021, The Cryptol Team.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script type="text/javascript">
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</script>
</body>
</html>

BIN
docs/RefMan/_build/html/objects.inv
View File

Binary file not shown.

159
docs/RefMan/_build/html/search.html
View File

@ -1,72 +1,34 @@
<!DOCTYPE html>
<html class="writer-html4" lang="en" >
<html class="writer-html5" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Search &mdash; Cryptol 2.11.0 documentation</title>
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<!--[if lt IE 9]>
<script src="_static/js/html5shiv.min.js"></script>
<![endif]-->
<script type="text/javascript" id="documentation_options" data-url_root="./" src="_static/documentation_options.js"></script>
<script type="text/javascript" src="_static/jquery.js"></script>
<script type="text/javascript" src="_static/underscore.js"></script>
<script type="text/javascript" src="_static/doctools.js"></script>
<script type="text/javascript" src="_static/language_data.js"></script>
<script type="text/javascript" src="_static/js/theme.js"></script>
<script type="text/javascript" src="_static/searchtools.js"></script>
<script type="text/javascript" src="_static/language_data.js"></script>
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<script src="_static/searchtools.js"></script>
<script src="_static/language_data.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="#" />
</head>
<body class="wy-body-for-nav">
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="RefMan.html" class="icon icon-home"> Cryptol
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="#" method="get">
<input type="text" name="q" placeholder="Search docs" />
@ -74,81 +36,40 @@
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
<ul>
<li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a></li>
<li class="toctree-l1"><a class="reference internal" href="Expressions.html">Expressions</a></li>
<li class="toctree-l1"><a class="reference internal" href="BasicTypes.html">Basic Types</a></li>
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
</ul>
</div>
<div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="main navigation">
<!-- Local TOC -->
<div class="local-toc"></div>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap">
<nav class="wy-nav-top" aria-label="top navigation">
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="RefMan.html">Cryptol</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="breadcrumbs navigation">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="RefMan.html" class="icon icon-home"></a> &raquo;</li>
<li>Search</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<noscript>
<div id="fallback" class="admonition warning">
<p class="last">
@ -163,51 +84,35 @@
</div>
</div>
</div>
<footer>
<hr/>
<div role="contentinfo">
<p>
&#169; Copyright 2021, The Cryptol Team.
</p>
<p>&#169; Copyright 2021, The Cryptol Team.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script type="text/javascript">
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
<script type="text/javascript">
<script>
jQuery(function() { Search.loadIndex("searchindex.js"); });
</script>
<script type="text/javascript" id="searchindexloader"></script>
<script id="searchindexloader"></script>

2
docs/RefMan/_build/html/searchindex.js
View File

File diff suppressed because one or more lines are too long

8
docs/RefMan/conf.py
View File

@ -11,10 +11,10 @@
# If extensions (or modules to document with autodoc) are in another directory,
# add these directories to sys.path here. If the directory is relative to the
# documentation root, use os.path.abspath to make it absolute, like shown here.
#
# import os
# import sys
# sys.path.insert(0, os.path.abspath('.'))
import os
import sys
sys.path.insert(0, os.path.abspath('.'))
import sphinx_rtd_theme

1
lib/Array.cry
View File

@ -10,6 +10,7 @@ primitive type Array : * -> * -> *
primitive arrayConstant : {a, b} b -> (Array a b)
primitive arrayLookup : {a, b} (Array a b) -> a -> b
primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b)
primitive arrayEq : {n, a} (Array [n] a) -> (Array [n] a) -> Bool
/**
* Copy elements from the source array to the destination array.

1
tests/regression/array.icry.stdout
View File

@ -12,6 +12,7 @@ Symbols
arrayConstant : {a, b} b -> Array a b
arrayCopy :
{n, a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Array [n] a
arrayEq : {n, a} Array [n] a -> Array [n] a -> Bool
arrayLookup : {a, b} Array a b -> a -> b
arrayRangeEqual :
{n, a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Bool