mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-18 13:31:50 +03:00
72068cb961
For the time being, there is still some information about them that is duplicated in Cryptol.TypeCheck.TCon, but we at least the parsed syntax does not depend on the typechecked syntax.
171 lines
6.3 KiB
Plaintext
171 lines
6.3 KiB
Plaintext
Loading module Cryptol
|
|
Loading module Cryptol
|
|
Loading module issue226r2
|
|
Loading module issue226
|
|
Type Synonyms
|
|
=============
|
|
type Bool = Bit
|
|
type Char = [8]
|
|
type lg2 n = width (max 1 n - 1)
|
|
type String n = [n][8]
|
|
type Word n = [n]
|
|
|
|
Constraint Synonyms
|
|
===================
|
|
type constraint i < j = j >= 1 + i
|
|
type constraint i <= j = j >= i
|
|
type constraint i > j = i >= 1 + j
|
|
|
|
Primitive Types
|
|
===============
|
|
(!=) : # -> # -> Prop
|
|
(==) : # -> # -> Prop
|
|
(>=) : # -> # -> Prop
|
|
(+) : # -> # -> #
|
|
(-) : # -> # -> #
|
|
(%) : # -> # -> #
|
|
(%^) : # -> # -> #
|
|
(*) : # -> # -> #
|
|
(/) : # -> # -> #
|
|
(/^) : # -> # -> #
|
|
(^^) : # -> # -> #
|
|
Arith : * -> Prop
|
|
Bit : *
|
|
Cmp : * -> Prop
|
|
fin : * -> Prop
|
|
Integer : *
|
|
inf : #
|
|
Literal : # -> * -> Prop
|
|
Logic : * -> Prop
|
|
lengthFromThenTo : # -> # -> # -> #
|
|
max : # -> # -> #
|
|
min : # -> # -> #
|
|
SignedCmp : * -> Prop
|
|
width : # -> #
|
|
Z : # -> *
|
|
Zero : * -> Prop
|
|
|
|
Symbols
|
|
=======
|
|
(==>) : Bit -> Bit -> Bit
|
|
(\/) : Bit -> Bit -> Bit
|
|
(/\) : Bit -> Bit -> Bit
|
|
(!=) : {a} (Cmp a) => a -> a -> Bit
|
|
(!==) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
|
|
(==) : {a} (Cmp a) => a -> a -> Bit
|
|
(===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
|
|
(<) : {a} (Cmp a) => a -> a -> Bit
|
|
(<$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
(<=) : {a} (Cmp a) => a -> a -> Bit
|
|
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
(>) : {a} (Cmp a) => a -> a -> Bit
|
|
(>$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
(>=) : {a} (Cmp a) => a -> a -> Bit
|
|
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
(||) : {a} (Logic a) => a -> a -> a
|
|
(^) : {a} (Logic a) => a -> a -> a
|
|
(&&) : {a} (Logic a) => a -> a -> a
|
|
(#) :
|
|
{front, back, a} (fin front) =>
|
|
[front]a -> [back]a -> [front + back]a
|
|
(<<) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
|
|
(<<<) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
|
|
(>>) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
|
|
(>>$) : {n, ix} (fin n, n >= 1, fin ix) => [n] -> [ix] -> [n]
|
|
(>>>) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
|
|
(+) : {a} (Arith a) => a -> a -> a
|
|
(-) : {a} (Arith a) => a -> a -> a
|
|
(%) : {a} (Arith a) => a -> a -> a
|
|
(%$) : {a} (Arith a) => a -> a -> a
|
|
(*) : {a} (Arith a) => a -> a -> a
|
|
(/) : {a} (Arith a) => a -> a -> a
|
|
(/$) : {a} (Arith a) => a -> a -> a
|
|
(^^) : {a} (Arith a) => a -> a -> a
|
|
(!) : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a
|
|
(!!) : {n, k, ix, a} (fin n, fin ix) => [n]a -> [k][ix] -> [k]a
|
|
(@) : {n, a, ix} (fin ix) => [n]a -> [ix] -> a
|
|
(@@) : {n, k, ix, a} (fin ix) => [n]a -> [k][ix] -> [k]a
|
|
all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
|
|
and : {n} (fin n) => [n] -> Bit
|
|
any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
|
|
carry : {n} (fin n) => [n] -> [n] -> Bit
|
|
complement : {a} (Logic a) => a -> a
|
|
curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
|
|
demote : {val, rep} (Literal val rep) => rep
|
|
drop : {front, back, a} (fin front) => [front + back]a -> [back]a
|
|
elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
|
|
error : {a, len} (fin len) => [len][8] -> a
|
|
False : Bit
|
|
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
|
|
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
|
|
foo : {a} a -> a
|
|
fromInteger : {a} (Arith a) => Integer -> a
|
|
fromThenTo :
|
|
{first, next, last, a, len} (fin first, fin next, fin last,
|
|
Literal first a, Literal next a, Literal last a, first != next,
|
|
lengthFromThenTo first next last == len) =>
|
|
[len]a
|
|
fromTo :
|
|
{first, last, a} (fin last, last >= first, Literal last a) =>
|
|
[1 + (last - first)]a
|
|
fromZ : {n} (fin n, n >= 1) => Z n -> Integer
|
|
generate :
|
|
{n, ix, a} (fin ix, n >= 1, ix >= width (n - 1)) =>
|
|
([ix] -> a) -> [n]a
|
|
groupBy :
|
|
{each, parts, a} (fin each) => [each * parts]a -> [parts][each]a
|
|
head : {n, a} [1 + n]a -> a
|
|
infFrom : {a} (Arith a) => a -> [inf]a
|
|
infFromThen : {a} (Arith a) => a -> a -> [inf]a
|
|
iterate : {a} (a -> a) -> a -> [inf]a
|
|
join :
|
|
{parts, each, a} (fin each) => [parts][each]a -> [parts * each]a
|
|
last : {n, a} (fin n) => [1 + n]a -> a
|
|
length : {n, a, b} (fin n, Literal n b) => [n]a -> b
|
|
lg2 : {a} (Arith a) => a -> a
|
|
map : {n, a, b} (a -> b) -> [n]a -> [n]b
|
|
max : {a} (Cmp a) => a -> a -> a
|
|
min : {a} (Cmp a) => a -> a -> a
|
|
negate : {a} (Arith a) => a -> a
|
|
number : {val, rep} (Literal val rep) => rep
|
|
or : {n} (fin n) => [n] -> Bit
|
|
pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
|
|
pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
|
|
pmult :
|
|
{u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)]
|
|
random : {a} [256] -> a
|
|
repeat : {n, a} a -> [n]a
|
|
reverse : {n, a} (fin n) => [n]a -> [n]a
|
|
sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
|
|
scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [1 + n]b
|
|
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b
|
|
scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
|
|
sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
|
|
split :
|
|
{parts, each, a} (fin each) => [parts * each]a -> [parts][each]a
|
|
splitAt :
|
|
{front, back, a} (fin front) =>
|
|
[front + back]a -> ([front]a, [back]a)
|
|
sum : {n, a} (fin n, Arith a) => [n]a -> a
|
|
True : Bit
|
|
tail : {n, a} [1 + n]a -> [n]a
|
|
take : {front, back, a} (fin front) => [front + back]a -> [front]a
|
|
toInteger : {bits} (fin bits) => [bits] -> Integer
|
|
trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
|
|
traceVal : {n, a} (fin n) => [n][8] -> a -> a
|
|
transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
|
|
uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
|
|
undefined : {a} a
|
|
update : {n, a, ix} (fin ix) => [n]a -> [ix] -> a -> [n]a
|
|
updateEnd : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a -> [n]a
|
|
updates :
|
|
{n, k, ix, a} (fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a
|
|
updatesEnd :
|
|
{n, k, ix, a} (fin n, fin ix, fin k) =>
|
|
[n]a -> [k][ix] -> [k]a -> [n]a
|
|
zero : {a} (Zero a) => a
|
|
zext : {m, n} (fin m, m >= n) => [n] -> [m]
|
|
zip : {n, a, b} [n]a -> [n]b -> [n](a, b)
|
|
zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c
|
|
|