Fix lots of wrong types for primitives in appendix B

docs/ProgrammingCryptol/prims/Primitives.tex

@@ -14,12 +14,12 @@ primsPlaceHolder=1;
 \paragraph*{Comparisons}
 \begin{Verbatim}
     ==, !=        : {a} (Cmp a) => a -> a -> Bit
-    <, >, <=, >=  : {a} (Cmp a) => [a] -> [a] -> Bit
+    <, >, <=, >=  : {a} (Cmp a) => a -> a -> Bit
 \end{Verbatim}
 \paragraph*{Arithmetic}
 \begin{Verbatim}
     +, -, *, /, %, ** : {a} (Arith a) => a -> a -> a
-    lg2               : {a, b} (Arith a) => a -> a
+    lg2               : {a} (Arith a) => a -> a
 \end{Verbatim}
 %    negate            : {a b} (a >= 1) => [a]b -> [a]b
 \paragraph*{Polynomial arithmetic}
@@ -30,44 +30,46 @@ primsPlaceHolder=1;
 \end{Verbatim}
 \paragraph*{Sequences}
 \begin{Verbatim}
-    take  : {front, back, elem} (fin front) 
+    take  : {front, back, elem} (fin front)
          => [front + back]elem -> [front]elem
-    drop  : {front, back, elem} (fin front) 
+    drop  : {front, back, elem} (fin front)
          => [front + back]elem -> [front]elem
     tail  : {a, b} [a+1]b -> [a]b
-    #     : {a, b, c} (fin a) => ([a]b,[c]b) -> [a+c]b
-    join  : {parts, each, a} (fin each) 
+    #     : {front, back, a} (fin front) =>
+         => [front]a -> [back]a -> [front + back]a
+    join  : {parts, each, a} (fin each)
          => [parts][each]a -> [parts * each]a
     split : {parts, each, a} (fin a)
          => [parts * each]a -> [parts][each]a
 
-    groupBy : {each, parts, elem} (fin each) 
+    groupBy : {each, parts, elem} (fin each)
            => [parts * each]elem -> [parts][each]elem
     reverse : {a, b} (fin a) => [a]b -> [a]b
-    @       : {a, b, c} ([a]b,[c]) -> b
-    !       : {a, b, c} (fin a) => ([a]b,[c]) -> b
-    @@      : {a, b, c, d} ([a]b,[c][d]) -> [c]b
-    !!      : {a, b, c, d} (fin a) => ([a]b,[c][d]) -> [c]b
-    width   : {a, b, c} (c >= width a) => [a]b -> [c]
+    @       : {a, b, c} (fin c) => [a]b -> [c] -> b
+    !       : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b
+    @@      : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
+    !!      : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
+    width   : {bits,len,elem} (fin len, fin bits, bits >= width len)
+           => [len] elem -> [bits]
 \end{Verbatim}
 \paragraph*{Shifting, rotating}
 \begin{Verbatim}
-    >>, <<, >>>, <<< : {a b c} (fin a,c >= lg2 a) 
-                     => ([a]b,[c]) -> [a]b
+    >>, <<   : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
+    >>>, <<< : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
 \end{Verbatim}
 \paragraph*{Miscellaneous}
 \begin{Verbatim}
     zero      : {a} a
     transpose : {a, b, c} [a][b]c -> [b][a]c
-    min, max  : {a} (fin a) => ([a],[a]) -> [a]
+    min, max  : {a} (Cmp a) => a -> a -> a
 \end{Verbatim}
 %   parity    : {a} (fin a) => [a] -> Bit
 \paragraph*{Representing exceptions}
 \begin{Verbatim}
     error     : {a, b} [a][8] -> b
     undefined : {a} a
-    trace : {n, a, b} [n][8] -> a -> b -> b
-    traceVal : {n, a} [n][8] -> a -> a
+    trace     : {n, a, b} [n][8] -> a -> b -> b
+    traceVal  : {n, a} [n][8] -> a -> a
 \end{Verbatim}
 \todo[inline]{\texttt{error} and \texttt{undefined} are not covered in
   the book at the moment.}