Merge branch 'master' of github.com:GaloisInc/cryptol

docs/CryptolPrims.md

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