mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-25 08:54:31 +03:00
Update CryptolPrims.md for prims with changed types and new instances.
This commit is contained in:
parent
9597082be4
commit
220afb51d7
@ -17,8 +17,9 @@ Comparisons and Ordering
|
||||
instance Cmp Bit
|
||||
// No instance for functions.
|
||||
instance (Cmp a, fin n) => Cmp [n]a
|
||||
instance (Cmp a, Cmp b) => Cmp (a,b)
|
||||
instance (Cmp a, Cmp b) => Cmp (a, b)
|
||||
instance (Cmp a, Cmp b) => Cmp { x : a, y : b }
|
||||
instance Cmp Integer
|
||||
|
||||
Signed Comparisons
|
||||
---------------------
|
||||
@ -33,7 +34,7 @@ Signed Comparisons
|
||||
instance (fin n, n >= 1) => SignedCmp [n]
|
||||
instance (SignedCmp a, fin n) => SignedCmp [n]a
|
||||
// (for [n]a, where a is other than Bit)
|
||||
instance (SignedCmp a, SignedCmp b) => SignedCmp (a,b)
|
||||
instance (SignedCmp a, SignedCmp b) => SignedCmp (a, b)
|
||||
instance (SignedCmp a, SignedCmp b) => SignedCmp { x : a, y : b }
|
||||
|
||||
|
||||
@ -48,39 +49,49 @@ Arithmetic
|
||||
(^^) : {a} (Arith a) => a -> a -> a
|
||||
(/$) : {a} (Arith a) => a -> a -> a
|
||||
(%$) : {a} (Arith a) => a -> a -> a
|
||||
lg2 : {a} (Arith a) => a -> a
|
||||
negate : {a} (Arith a) => a -> a
|
||||
|
||||
The prefix notation `- x` is syntactic sugar for `negate x`.
|
||||
|
||||
// No instance for `Bit`.
|
||||
instance (fin n) => Arith ( [n] Bit)
|
||||
instance (Arith a) => Arith ( [n] a)
|
||||
instance (fin n) => Arith ([n]Bit)
|
||||
instance (Arith a) => Arith ([n]a)
|
||||
instance (Arith b) => Arith (a -> b)
|
||||
instance (Arith a, Arith b) => Arith (a,b)
|
||||
instance (Arith a, Arith b) => Arith (a, b)
|
||||
instance (Arith a, Arith b) => Arith { x : a, y : b }
|
||||
instance Arith Integer
|
||||
|
||||
Note that because there is no instances for `Arith Bit`
|
||||
Note that because there is no instance for `Arith Bit`
|
||||
the top two instances do not actually overlap.
|
||||
|
||||
Boolean
|
||||
-------
|
||||
|
||||
False : Bit
|
||||
True : Bit
|
||||
False : Bit
|
||||
True : Bit
|
||||
|
||||
zero : a
|
||||
(&&) : a -> a -> a
|
||||
(||) : a -> a -> a
|
||||
(^) : a -> a -> a
|
||||
(~) : a -> a
|
||||
zero : {a} (Zero 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
|
||||
|
||||
(==>) : Bit -> Bit -> Bit
|
||||
(/\) : Bit -> Bit -> Bit
|
||||
(\/) : Bit -> Bit -> Bit
|
||||
(==>) : Bit -> Bit -> Bit
|
||||
(/\) : Bit -> Bit -> Bit
|
||||
(\/) : Bit -> Bit -> Bit
|
||||
|
||||
instance Logic Bit
|
||||
instance (Logic a) => Logic ([n]a)
|
||||
instance (Logic b) => Logic (a -> b)
|
||||
instance (Logic a, Logic b) => Logic (a, b)
|
||||
instance (Logic a, Logic b) => Logic { x : a, y : b }
|
||||
// No instance for `Logic Integer`.
|
||||
|
||||
Sequences
|
||||
---------
|
||||
|
||||
length : {n,a,m} (m >= width n) => [n]a -> [m]
|
||||
|
||||
join : {parts,ench,a} (fin each) => [parts][each]a -> [parts * each]a
|
||||
join : {parts,each,a} (fin each) => [parts][each]a -> [parts * each]a
|
||||
split : {parts,each,a} (fin each) => [parts * each]a -> [parts][each]a
|
||||
|
||||
(#) : {front,back,a} (fin front) => [front]a -> [back]a -> [front + back]a
|
||||
@ -98,25 +109,22 @@ Sequences
|
||||
updates : {n,a,m,d} (fin m, fin d) => [n]a -> [d][m] -> [d]a -> [n]a
|
||||
updatesEnd : {n,a,m,d} (fin n, fin m, fin d) => [n]a -> [d][m] -> [d]a -> [n]a
|
||||
|
||||
// Abbreviations
|
||||
groupBy n = split`{each = n}
|
||||
tail n = splitAt`{front = 1}.1
|
||||
take n = splitAt`{front = n}.0
|
||||
drop n = splitAt`{front = n}.1
|
||||
take : {front,back,elem} (fin front) => [front + back]elem -> [front]elem
|
||||
drop : {front,back,elem} (fin front) => [front + back]elem -> [back]elem
|
||||
head : {a, b} [1 + a]b -> b
|
||||
tail : {a, b} [1 + a]b -> [a]b
|
||||
last : {a, b} [1 + a]b -> b
|
||||
|
||||
/* Also, `length` is not really needed:
|
||||
length : {n,a,m} (m >= width n) => [n]a -> [m]
|
||||
length _ = `n
|
||||
*/
|
||||
groupBy : {each,parts,elem} (fin each) => [parts * each]elem -> [parts][each]elem
|
||||
|
||||
Function `groupBy` is the same as `split` but with its type arguments
|
||||
in a different order.
|
||||
|
||||
Shift And Rotate
|
||||
----------------
|
||||
|
||||
New types:
|
||||
|
||||
(<<) : {n,a,m} (fin n) => [n]a -> [m] -> [n]a
|
||||
(>>) : {n,a,m} (fin n) => [n]a -> [m] -> [n]a
|
||||
(<<) : {n,a,m} (fin n, Zero a) => [n]a -> [m] -> [n]a
|
||||
(>>) : {n,a,m} (fin n, Zero a) => [n]a -> [m] -> [n]a
|
||||
(<<<) : {n,a,m} (fin n) => [n]a -> [m] -> [n]a
|
||||
(>>>) : {n,a,m} (fin n) => [n]a -> [m] -> [n]a
|
||||
|
||||
@ -135,4 +143,3 @@ Debugging
|
||||
error : {n a} [n][8] -> a
|
||||
trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
|
||||
traceVal : {n, a} (fin n) => [n][8] -> a -> a
|
||||
|
Binary file not shown.
Loading…
Reference in New Issue
Block a user