diff --git a/docs/RefMan/OverloadedOperations.rst b/docs/RefMan/OverloadedOperations.rst index 98312b4e2..d77103718 100644 --- a/docs/RefMan/OverloadedOperations.rst +++ b/docs/RefMan/OverloadedOperations.rst @@ -12,6 +12,28 @@ Equality (===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit) (!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit) + +.. list-table:: Instances + + * - Type + - Condition + * - ``Bit`` + - + * - ``Integer`` + - + * - ``Rational`` + - + * - ``Z n`` + - ``fin n``, ``n >= 1`` + * - ``Float e p`` + - ``ValidFloat e p`` + * - ``[n] a`` + - ``fin n``, ``Eq a`` + * - ``(a,b)`` + - ``Eq a``, ``Eq b`` + + + Comparisons ----------- @@ -27,6 +49,27 @@ Comparisons abs : {a} (Cmp a, Ring a) => a -> a +.. list-table:: Instances + + * - Type + - Condition + * - ``Bit`` + - + * - ``Integer`` + - + * - ``Rational`` + - + * - ``Float e p`` + - ``ValidFloat e p`` + * - ``[n] a`` + - ``fin n``, ``Cmp a`` + * - ``(a,b)`` + - ``Cmp a``, ``Cmp b`` + + + + + Signed Comparisons ------------------ @@ -38,6 +81,17 @@ Signed Comparisons (<=$) : {a} (SignedCmp a) => a -> a -> Bit (>=$) : {a} (SignedCmp a) => a -> a -> Bit +.. list-table:: Instances + + * - Type + - Condition + * - ``[n] Bit`` + - ``fin n``, ``n >= 1`` + * - ``[n] a`` + - ``fin n``, ``SignedCmp a``, ``a /= Bit`` + * - ``(a,b)`` + - ``SignedCmp a``, ``SignedCmp b`` + Zero ---- @@ -47,6 +101,27 @@ Zero Zero zero : {a} (Zero a) => a +.. list-table:: Instances + + * - Type + - Condition + * - ``Bit`` + - + * - ``Integer`` + - + * - ``Rational`` + - + * - ``Z n`` + - ``fin n``, ``n >= 1`` + * - ``Float e p`` + - ``ValidFloat e p`` + * - ``[n] a`` + - ``Zero a`` + * - ``a -> b`` + - ``Zero b`` + * - ``(a,b)`` + - ``Zero a``, ``Zero b`` + Logical Operations ------------------ @@ -58,6 +133,21 @@ Logical Operations (^) : {a} (Logic a) => a -> a -> a complement : {a} (Logic a) => a -> a +.. list-table:: Instances + + * - Type + - Condition + * - ``Bit`` + - + * - ``[n] a`` + - ``Logic a`` + * - ``a -> b`` + - ``Logic b`` + * - ``(a,b)`` + - ``Logic a``, ``Logic b`` + + + Basic Arithmetic ---------------- @@ -71,6 +161,29 @@ Basic Arithmetic negate : {a} (Ring a) => a -> a (^^) : {a, e} (Ring a, Integral e) => a -> e -> a +.. list-table:: Instances + + * - Type + - Condition + * - ``Integer`` + - + * - ``Rational`` + - + * - ``Z n`` + - ``fin n``, ``n >= 1`` + * - ``Float e p`` + - ``ValidFloat e p`` + * - ``[n] Bit`` + - ``fin n`` + * - ``[n] a`` + - ``Ring a``, ``a /= Bit`` + * - ``a -> b`` + - ``Ring b`` + * - ``(a,b)`` + - ``Ring a``, ``Ring b`` + + + Integral Operations ------------------- @@ -84,6 +197,18 @@ Integral Operations infFrom : {a} (Integral a) => a -> [inf]a infFromThen : {a} (Integral a) => a -> a -> [inf]a +.. list-table:: Instances + + * - Type + - Condition + * - ``Integer`` + - + * - ``[n] Bit`` + - ``fin n`` + + + + Division -------- @@ -94,6 +219,20 @@ Division recip : {a} (Field a) => a -> a (/.) : {a} (Field a) => a -> a -> a + +.. list-table:: Instances + + * - Type + - Condition + * - ``Rational`` + - + * - ``Z n`` + - ``prime n`` + * - ``Float e p`` + - ``ValidFloat e p`` + + + Rounding -------- @@ -105,3 +244,13 @@ Rounding trunc : {a} (Round a) => a -> Integer roundAway : {a} (Round a) => a -> Integer roundToEven : {a} (Round a) => a -> Integer + + +.. list-table:: Instances + + * - Type + - Condition + * - ``Float e p`` + - ``ValidFloat e p`` + + diff --git a/docs/RefMan/_build/doctrees/BasicSyntax.doctree b/docs/RefMan/_build/doctrees/BasicSyntax.doctree index 61a0b9c4a..71e9f8f57 100644 Binary files a/docs/RefMan/_build/doctrees/BasicSyntax.doctree and b/docs/RefMan/_build/doctrees/BasicSyntax.doctree differ diff --git a/docs/RefMan/_build/doctrees/BasicTypes.doctree b/docs/RefMan/_build/doctrees/BasicTypes.doctree index dade46df2..b926627f5 100644 Binary files a/docs/RefMan/_build/doctrees/BasicTypes.doctree and b/docs/RefMan/_build/doctrees/BasicTypes.doctree differ diff --git a/docs/RefMan/_build/doctrees/Expressions.doctree b/docs/RefMan/_build/doctrees/Expressions.doctree index 3b164e8fa..fcbe41616 100644 Binary files a/docs/RefMan/_build/doctrees/Expressions.doctree and b/docs/RefMan/_build/doctrees/Expressions.doctree differ diff --git a/docs/RefMan/_build/doctrees/FFI.doctree b/docs/RefMan/_build/doctrees/FFI.doctree index 4223404b1..f04546bef 100644 Binary files a/docs/RefMan/_build/doctrees/FFI.doctree and b/docs/RefMan/_build/doctrees/FFI.doctree differ diff --git a/docs/RefMan/_build/doctrees/Modules.doctree b/docs/RefMan/_build/doctrees/Modules.doctree index 5de0831f5..5d454794f 100644 Binary files a/docs/RefMan/_build/doctrees/Modules.doctree and b/docs/RefMan/_build/doctrees/Modules.doctree differ diff --git a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree index 8797caaeb..cc25280c8 100644 Binary files a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree and b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree differ diff --git a/docs/RefMan/_build/doctrees/RefMan.doctree b/docs/RefMan/_build/doctrees/RefMan.doctree index b6debdce8..591dca751 100644 Binary files a/docs/RefMan/_build/doctrees/RefMan.doctree and b/docs/RefMan/_build/doctrees/RefMan.doctree differ diff --git a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree index 353c3286b..8fcbf879e 100644 Binary files a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree and b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree differ diff --git a/docs/RefMan/_build/doctrees/environment.pickle b/docs/RefMan/_build/doctrees/environment.pickle index a6a301772..6ee73c587 100644 Binary files a/docs/RefMan/_build/doctrees/environment.pickle and b/docs/RefMan/_build/doctrees/environment.pickle differ diff --git a/docs/RefMan/_build/html/.buildinfo b/docs/RefMan/_build/html/.buildinfo index b0149fc3a..31b3902b4 100644 --- a/docs/RefMan/_build/html/.buildinfo +++ b/docs/RefMan/_build/html/.buildinfo @@ -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: 69485412ee215e2257ea16f8a42506fe +config: 49d6d89345e8bba027ef627e0adeb689 tags: 645f666f9bcd5a90fca523b33c5a78b7 diff --git a/docs/RefMan/_build/html/BasicSyntax.html b/docs/RefMan/_build/html/BasicSyntax.html index 3bbc07fbb..ce1524dff 100644 --- a/docs/RefMan/_build/html/BasicSyntax.html +++ b/docs/RefMan/_build/html/BasicSyntax.html @@ -1,85 +1,46 @@ - - - - + - - - - - Basic Syntax — Cryptol 2.11.0 documentation - - - - - - + + + Basic Syntax — Cryptol 2.11.0 documentation + + - - - - + + - - - - - - - - + + - - - +
- -
- - -
-
-

Numeric Constraint Guards

+ +
+

Numeric Constraint Guards

A declaration with a signature can use numeric constraint guards, which are used to change the behavior of a functoin depending on its numeric type parameters. For example:

-
len : {n} (fin n) => [n]a -> Integer
-len xs | n == 0 => 0
-       | n >  0 => 1 + len (drop `{1} xs)
+
len : {n} (fin n) => [n]a -> Integer
+len xs | n == 0 => 0
+       | n >  0 => 1 + len (drop `{1} xs)
 

 

 
Each behavior starts with | and lists some constraints on the numeric
@@ -194,9 +117,9 @@ 
Numeric Constraint Guardsif statement:

-
len' : {n} (fin n) => [n]a -> Integer
-len' xs = if `n == 0 => 0
-           | `n >  0 => 1 + len (drop `{1} xs)
+
len' : {n} (fin n) => [n]a -> Integer
+len' xs = if `n == 0 => 0
+           | `n >  0 => 1 + len (drop `{1} xs)
 

 

 
The definition of len' is rejected, because the value based if
@@ -222,30 +145,30 @@ 
Numeric Constraint Guards
-
Layout

+
+
+

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:

-
f x = x + y + z
-  where
-  y = x * x
-  z = x + y
+
f x = x + y + z
+  where
+  y = x * x
+  z = x + y
 
-g y = 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

+
+
+

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.

@@ -258,9 +181,9 @@

CommentsTodo

Document /** */

- -
-

Identifiers

+ +
+

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, @@ -268,19 +191,19 @@

IdentifiersKeywords and Built-in Operators).

-
Examples of identifiers
-
name    name1    name'    longer_name
-Name    Name2    Name''   longerName
+
Examples of identifiers

+
name    name1    name'    longer_name
+Name    Name2    Name''   longerName
-
-
-

Keywords and Built-in Operators

+

+
+

Keywords and Built-in Operators

The following identifiers have special meanings in Cryptol, and may not be used for programmer defined names:

-
Keywords
+
Keywords
as              extern      include      interface      parameter      property      where
 by              hiding      infix        let            pragma         submodule     else
 constraint      if          infixl       module         primitive      then
@@ -292,11 +215,7 @@ 
Keywords and Built-in Operators
-Operator precedences
-
-
-
-
+Operator precedences
 
 
Operator

 
Associativity

@@ -351,17 +270,13 @@ 
Keywords and Built-in Operators
-
Built-in Type-level Operators

+
+
+

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.

- ---- + @@ -406,21 +321,21 @@

Built-in Type-level Operators -

Numeric Literals

+ +
+

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.

-
Examples of literals
-
254                 // Decimal literal
-0254                // Decimal literal
-0b11111110          // Binary literal
-0o376               // Octal literal
-0xFE                // Hexadecimal literal
-0xfe                // Hexadecimal literal
+
Examples of literals

+
254                 // Decimal literal
+0254                // Decimal literal
+0b11111110          // Binary literal
+0o376               // Octal literal
+0xFE                // Hexadecimal literal
+0xfe                // Hexadecimal literal
@@ -430,13 +345,13 @@

Numeric Literals -
Literals and their types
-
0b1010              // : [4],   1 * number of digits
-0o1234              // : [12],  3 * number of digits
-0x1234              // : [16],  4 * number of digits
+
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
+10                  // : {a}. (Literal 10 a) => a
+                    // a = Integer or [n] where n >= width 10
@@ -445,9 +360,9 @@

Numeric Literals -
Polynomial literals
-
<| x^^6 + x^^4 + x^^2 + x^^1 + 1 |>  // : [7], equal to 0b1010111
-<| x^^4 + x^^3 + x |>                // : [5], equal to 0b11010
+
Polynomial literals

+
<| x^^6 + x^^4 + x^^2 + x^^1 + 1 |>  // : [7], equal to 0b1010111
+<| x^^4 + x^^3 + x |>                // : [5], equal to 0b11010
@@ -459,11 +374,11 @@

Numeric Literalse. Examples:

-
Fractional literals
+
Fractional literals
10.2
-10.2e3            // 10.2 * 10^3
-0x30.1            // 3 * 64 + 1/16
-0x30.1p4          // (3 * 64 + 1/16) * 2^4
+10.2e3            // 10.2 * 10^3
+0x30.1            // 3 * 64 + 1/16
+0x30.1p4          // (3 * 64 + 1/16) * 2^4
@@ -476,62 +391,44 @@

Numeric Literals_, which has no effect on the literal value but may be used to improve readability. Here are some examples:

-
Using _
+
Using _
0b_0000_0010
 0x_FFFF_FFEA
-

-

+

+ - - - - - - - - - - - - - + \ No newline at end of file diff --git a/docs/RefMan/_build/html/BasicTypes.html b/docs/RefMan/_build/html/BasicTypes.html index edb6151cf..a7450dd39 100644 --- a/docs/RefMan/_build/html/BasicTypes.html +++ b/docs/RefMan/_build/html/BasicTypes.html @@ -1,85 +1,46 @@ - - - - + - - - - - Basic Types — Cryptol 2.11.0 documentation - + + + Basic Types — Cryptol 2.11.0 documentation + + - - - - - - - - - + + - - - - - - - - + + - - - +
- -
- - -

Type-level operators Type-level operators

Operator

Meaning

- ---- + @@ -340,67 +259,49 @@

Sequences
[p1, p2, p3, p4]          // Sequence pattern
-p1 # p2                   // Split sequence pattern
+
[p1, p2, p3, p4]          // Sequence pattern
+p1 # p2                   // Split sequence pattern
 

 

-
-
-

Functions

-
\p1 p2 -> e              // Lambda expression
-f p1 p2 = e              // Function definition
+
+

+
Functions

+
\p1 p2 -> e              // Lambda expression
+f p1 p2 = e              // Function definition
 

 

-
-
+ +
- - - - - - - - - - - - - + \ No newline at end of file diff --git a/docs/RefMan/_build/html/Expressions.html b/docs/RefMan/_build/html/Expressions.html index 2541b6491..d1f610aae 100644 --- a/docs/RefMan/_build/html/Expressions.html +++ b/docs/RefMan/_build/html/Expressions.html @@ -1,85 +1,46 @@ - - - - + - - - - - Expressions — Cryptol 2.11.0 documentation - - - - - - + + + Expressions — Cryptol 2.11.0 documentation + + - - - - + + - - - - - - - - + + - - - +
- -
- - -
-
-

Type Annotations

+ +
+

Type Annotations

Explicit type annotations may be added on expressions, patterns, and in argument definitions.

-
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
+
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

+
+
+

Explicit Type Instantiation

If f is a polymorphic value with type:

-
f : { tyParam } tyParam
-f = zero
+
f : { tyParam } tyParam
+f = zero
 

 

 
you can evaluate f, passing it a type parameter:

-
f `{ tyParam = 13 }
+
f `{ tyParam = 13 }
 

 

-

-

-
Local Declarations

+
+
+

Local Declarations

Local declarations have the weakest precedence of all expressions.

-
2 + x : [T]
-  where
-  type T = 8
-  x      = 2          // `T` and `x` are in scope of `2 + x : `[T]`
+
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`
+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`
+\y -> x + y
+  where x = 2         // `y` is not in scope in the defintion of `x`
 

 

-
-
-

Block Arguments

+
+
+

Block Arguments

When used as the last argument to a function call, if and lambda expressions do not need parens:

-
f \x -> x       // call `f` with one argument `x -> x`
-2 + if x
-      then y
-      else z    // call `+` with two arguments: `2` and `if ...`
+
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

+
+
+

Conditionals

The if ... then ... else construct can be used with multiple branches. For example:

-
x = if y % 2 == 0 then 22 else 33
+
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
+x = if y % 2 == 0 then 1
+     | y % 3 == 0 then 2
+     | y % 5 == 0 then 3
+     else 7
 

 

-
-
-

Demoting Numeric Types to Values

+
+
+

Demoting Numeric Types to Values

The value corresponding to a numeric type may be accessed using the following notation:

`t
@@ -279,66 +202,48 @@ 
Demoting Numeric Types to Values
`t : {a} (Literal t a) => a
+
`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:

-
number`{t} : {a} (Literal t a) => a
+
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.

-

-

+
+
- - - - - - - - - - - - - + \ No newline at end of file diff --git a/docs/RefMan/_build/html/FFI.html b/docs/RefMan/_build/html/FFI.html index 2b0c8aea4..6033a3a55 100644 --- a/docs/RefMan/_build/html/FFI.html +++ b/docs/RefMan/_build/html/FFI.html @@ -1,84 +1,45 @@ - - - - + - - - - - Foreign Function Interface — Cryptol 2.11.0 documentation - - - - - - + + + Foreign Function Interface — Cryptol 2.11.0 documentation + + - - - - + + - - - - - - - - + + - - - +
- -
- - -

Sequence operations. Sequence operations.

Operator

Description

---- @@ -314,14 +233,10 @@

Type parameters< 2^^64 instead of just fin, in practice this would be too cumbersome.)

- -
-

Bit

+ +
+

Bit

Cryptol kind

C type

---- @@ -336,16 +251,12 @@

BitWhen converting to C, True is converted to 1 and False to 0. When converting to Cryptol, any nonzero number is converted to True and 0 is converted to False.

- -
-

Bit Vector Types

+ +
+

Bit Vector Types

Let K : # be a Cryptol type. Note K must be an actual fixed numeric type and not a type variable.

Cryptol type

C type

---- @@ -375,14 +286,10 @@

Bit Vector Types -

Floating point types

+ +
+

Floating point types

Cryptol type

C type

---- @@ -399,15 +306,11 @@

Floating point types

Note: the Cryptol Float types are defined in the built-in module Float. Other sizes of floating points are not supported.

- -
-

Math Types

+ +
+

Math Types

Values of high precision types and Z are represented using the GMP library.

Cryptol type

C type

---- @@ -433,18 +336,14 @@

Math Typesinit before their use and clear after.

- -
-

Sequences

+ +
+

Sequences

Let n1, n2, ..., nk : # be Cryptol types (with k >= 1), possibly containing type variables, that satisfy fin n1, fin n2, ..., fin nk, and T be one of the above Cryptol bit vector types, floating point types, or math types. Let U be the C type that T corresponds to.

Cryptol type

C type

---- @@ -462,18 +361,14 @@

Sequencessize_t’s earlier, so the C code can always know the dimensions of the array.

- -
-

Tuples and records

+ +
+

Tuples and records

Let T1, T2, ..., Tn be Cryptol types supported by the FFI (which may be any of the types mentioned above, or tuples and records themselves). Let U1, U2, ..., Un be the C types that T1, T2, ..., Tn respectively correspond to. Let f1, f2, ..., fn be arbitrary field names.

Cryptol type

C type

---- @@ -492,14 +387,14 @@

Tuples and records -

Type synonyms

+ +
+

Type synonyms

All type synonyms are expanded before applying the above rules, so you can use type synonyms in foreign declarations to improve readability.

- -
-

Return values

+
+
+

Return values

If the Cryptol return type is Bit or one of the above bit vector types or floating point types, the value is returned directly from the C function. In that case, the return type of the C function will be the C type corresponding to @@ -511,16 +406,10 @@

Return valuesU will be a pointer U* instead, except in the case of math types and sequences, where the output and input versions are the same type, because it is already a pointer.

- -

+
+

Quick reference

Cryptol type

C types

------ @@ -603,10 +492,10 @@

Quick referenceK is a constant number, ni are variable numbers, Ti is a type, Ui is its C argument type, and Vi is its C output argument type.

- - -
-

Memory

+ + +
+

Memory

When pointers are involved, namely in the cases of sequences and output arguments, they point to memory. This memory is always allocated and deallocated by Cryptol; the C code does not need to manage this memory.

@@ -619,71 +508,54 @@

Memory -

Evaluation

+

+
+

Evaluation

All Cryptol arguments are fully evaluated when a foreign function is called.

-
-
-

Example

+ +
+

Example

The Cryptol signature

-
foreign f : {n} (fin n) => [n][10] -> {a : Bit, b : [64]}
-                           -> (Float64, [n + 1][20])
+
foreign f : {n} (fin n) => [n][10] -> {a : Bit, b : [64]}
+                           -> (Float64, [n + 1][20])
 

 

 
corresponds to the C signature

-
void f(size_t n, uint16_t *in0, uint8_t in1_a, uint64_t in1_b,
-       double *out_0, uint32_t *out_1);
+
void f(size_t n, uint16_t *in0, uint8_t in1_a, uint64_t in1_b,
+       double *out_0, uint32_t *out_1);
 

 

-

-

+
+
- - - - - - - - - - - - - + \ No newline at end of file diff --git a/docs/RefMan/_build/html/Modules.html b/docs/RefMan/_build/html/Modules.html index 967ba8d57..a41dde384 100644 --- a/docs/RefMan/_build/html/Modules.html +++ b/docs/RefMan/_build/html/Modules.html @@ -1,85 +1,46 @@ - - - - + - - - - - Modules — Cryptol 2.11.0 documentation - - - - - - + + + Modules — Cryptol 2.11.0 documentation + + - - - - + + - - - - - - - - + + - - - +
- -
- - -
+
- - - - - - - - - - - - - + \ No newline at end of file diff --git a/docs/RefMan/_build/html/OverloadedOperations.html b/docs/RefMan/_build/html/OverloadedOperations.html index 06753d4fe..3d2eecdc3 100644 --- a/docs/RefMan/_build/html/OverloadedOperations.html +++ b/docs/RefMan/_build/html/OverloadedOperations.html @@ -1,85 +1,46 @@ - - - - + - - - - - Overloaded Operations — Cryptol 2.11.0 documentation - - - - - - + + + Overloaded Operations — Cryptol 2.11.0 documentation + + - - - - + + - - - - - - - - + + - - - +
- -
- - -

Cryptol type (or kind)

C argument type(s)

+ + + + + + + + + + + + + + + + + + + + + + + + + + + +
Instances

Type

Condition

Bit

Integer

Rational

Z n

fin n, n >= 1

Float e p

ValidFloat e p

[n] a

fin n, Eq a

(a,b)

Eq a, Eq b

+
+
+

Comparisons

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
+  (<)         : {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

+ + + + + + + + + + + + + + + + + + + + + + + + + +
Instances

Type

Condition

Bit

Integer

Rational

Float e p

ValidFloat e p

[n] a

fin n, Cmp a

(a,b)

Cmp a, Cmp b

+ +
+

Signed Comparisons

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
+  (<$)        : {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

+ + + + + + + + + + + + + + + + +
Instances

Type

Condition

[n] Bit

fin n, n >= 1

[n] a

fin n, SignedCmp a, a /= Bit

(a,b)

SignedCmp a, SignedCmp b

+ +
+

Zero

Zero
-  zero        : {a} (Zero a) => a
+  zero        : {a} (Zero a) => a
-
-
-

Logical Operations

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Instances

Type

Condition

Bit

Integer

Rational

Z n

fin n, n >= 1

Float e p

ValidFloat e p

[n] a

Zero a

a -> b

Zero b

(a,b)

Zero a, Zero b

+ +
+

Logical Operations

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
+  (&&)        : {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

+ + + + + + + + + + + + + + + + + + + +
Instances

Type

Condition

Bit

[n] a

Logic a

a -> b

Logic b

(a,b)

Logic a, Logic b

+ +
+

Basic Arithmetic

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
+  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

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Instances

Type

Condition

Integer

Rational

Z n

fin n, n >= 1

Float e p

ValidFloat e p

[n] Bit

fin n

[n] a

Ring a, a /=  Bit

a -> b

Ring b

(a,b)

Ring a, Ring b

+ +
+

Integral Operations

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
+  (/)         : {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

+ + + + + + + + + + + + + +
Instances

Type

Condition

Integer

[n] Bit

fin n

+ +
+

Division

Field
-  recip       : {a} (Field a) => a -> a
-  (/.)        : {a} (Field a) => a -> a -> a
+  recip       : {a} (Field a) => a -> a
+  (/.)        : {a} (Field a) => a -> a -> a
-
-
-

Rounding

+ + + + + + + + + + + + + + + + +
Instances

Type

Condition

Rational

Z n

prime n

Float e p

ValidFloat e p

+ +
+

Rounding

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
+  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
-
- + + + + + + + + + + +
Instances

Type

Condition

Float e p

ValidFloat e p

+ + - - - - - - - - - - - - - + \ No newline at end of file diff --git a/docs/RefMan/_build/html/RefMan.html b/docs/RefMan/_build/html/RefMan.html index b721a33da..4903676a4 100644 --- a/docs/RefMan/_build/html/RefMan.html +++ b/docs/RefMan/_build/html/RefMan.html @@ -1,84 +1,45 @@ - - - - + - - - - - Cryptol Reference Manual — Cryptol 2.11.0 documentation - - - - - - + + + Cryptol Reference Manual — Cryptol 2.11.0 documentation + + - - - - + + - - - - - - - - + + - - - +
- -
- - -
- - - - - - - - - + \ No newline at end of file diff --git a/docs/RefMan/_build/html/TypeDeclarations.html b/docs/RefMan/_build/html/TypeDeclarations.html index f895b09fb..5e9883d7e 100644 --- a/docs/RefMan/_build/html/TypeDeclarations.html +++ b/docs/RefMan/_build/html/TypeDeclarations.html @@ -1,85 +1,46 @@ - - - - + - - - - - Type Declarations — Cryptol 2.11.0 documentation - - - - - - + + + Type Declarations — Cryptol 2.11.0 documentation + + - - - - + + - - - - - - - - + + - - - +
- -
- - -