Rename prelude function width to length, and generalize its type.

Fixes #550.

examples/ChaChaPolyCryptolIETF.md

@@ -1168,10 +1168,10 @@ AeadCT = ChaCha20EncryptBytes AeadPt AeadKey AeadNonce 1
 AeadPolyKey = GeneratePolyKeyUsingChaCha AeadKey (AeadC # AeadIV) 0
 
 ADleLen : [8][8]
-ADleLen = groupBy`{8}(littleendian (groupBy`{8}((width AeadAAD):[64])))
+ADleLen = groupBy`{8}(littleendian (groupBy`{8}((length AeadAAD):[64])))
 
 CTleLen : [8][8]
-CTleLen = groupBy`{8}(littleendian (groupBy`{8}((width AeadCT):[64])))
+CTleLen = groupBy`{8}(littleendian (groupBy`{8}((length AeadCT):[64])))
 
 AeadTag = Poly1305 AeadPolyKey (AeadConstruction AeadAAD AeadCT)
 ```

examples/DES.cry

@@ -22,7 +22,7 @@ des pt keys = (swap (split lst)) @@ FPz
         iv  = [ round (k, split lr)
               | k  <- keys
               | lr <- [pt'] # iv ]
-        lst = iv @ (width keys - 1)
+        lst = iv @ (length keys - 1)
 
 round : ([48],[2][32]) -> [64]
 round (k, [l, r]) = r # (l ^ f (r, k))

examples/MD5.cry

@@ -123,7 +123,7 @@ pad msg =
     msg # [True] # zero # htonll sz
     where
       sz : [64]
-      sz = width msg
+      sz = length msg
 
 
 

examples/MiniLock/File.md

@@ -124,7 +124,7 @@ The minilock file format is a concatenation of the magic, header length field, h
             -> [ctBytes][8]
             -> [8 + 4 + 89 + (DecryptInfoSize + 1) * nrRecip + ctBytes - 1][8]
   mkMiniLock rs senderKeys ephemKeys fileInfo ct =
-      magic # put32le (width header) # header # ct
+      magic # put32le (length header) # header # ct
    where
     header = mkHeader rs senderKeys ephemKeys fileInfo
 ```

examples/contrib/EvenMansour.cry

@@ -9,7 +9,7 @@
 /** Pick some permutation F (here we select one at random) */
 F = (generate_random_permutation 1942611697)
 
-property is_a_permutation a = (unique a) /\ (leq a (width(a)-1))
+property is_a_permutation a = (unique a) /\ (leq a (length(a)-1))
 // Main> is_a_permutation (F:[10][4])
 // True
 

examples/contrib/mkrand.cry

@@ -79,7 +79,7 @@ field s = new
  * keep the center column of the second.
  */
 sha30: Seg -> Seg
-sha30 s = take`{0x80} (drop`{0x80} [ r @ ((((width r) / 2)-1):[8]) | r <- field s])
+sha30 s = take`{0x80} (drop`{0x80} [ r @ ((((length r) / 2)-1):[8]) | r <- field s])
 
 
 /*

examples/width.cry

@@ -1,2 +1,2 @@
 x : [8]
-x = width (252 : [8])
+x = length (252 : [8])

lib/Cryptol.cry

@@ -573,8 +573,12 @@ head xs = xs @ 0
 last : {n, a} (fin n) => [1 + n]a -> a
 last xs = xs ! 0
 
-width : {bits, n, a} (fin n, fin bits, bits >= width n) => [n]a -> [bits]
-width _ = `n
+/**
+ * Return the length of a sequence.  Note that the result depends only
+ * on the type of the argument, not its value.
+ */
+length : {n, a, b} (fin n, Literal n b) => [n]a -> b
+length _ = `n
 
 undefined : {a} a
 undefined = error "undefined"

tests/issues/issue226.icry.stdout

@@ -88,6 +88,7 @@ Symbols
     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
@@ -129,8 +130,6 @@ Symbols
     updatesEnd :
       {n, k, ix, a} (fin n, fin ix, fin k) =>
         [n]a -> [k][ix] -> [k]a -> [n]a
-    width :
-      {bits, n, a} (fin n, fin bits, bits >= width n) => [n]a -> [bits]
     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)

tests/issues/issue389.cry

@@ -1,7 +1,7 @@
 pad : {n, m, b} (64>=width(n), b==512-((n+65)%512), m==65+n+b) => [n]->[m]
-pad message = (message#[True])#(0:[b])#sz 
-     where 
+pad message = (message#[True])#(0:[b])#sz
+     where
                 sz : [64]
-                sz = width message
+                sz = length message
 
 test = pad

tests/regression/check16-tab.cry

@@ -1,4 +1,4 @@
-check16 = width x == 8
+check16 = length x == 8
   where
 	x : [8]
 	x = 0x3f

tests/regression/check16-tab.icry.stdout

@@ -1,6 +1,6 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] at ./check16-tab.cry:1:11--1:16:
-  Defaulting type argument 'bits' of 'width' to 4
+[warning] at ./check16-tab.cry:1:23--1:24:
+  Defaulting type argument 'rep' of 'number' to [4]
 True

tests/regression/check16.cry

@@ -1,4 +1,4 @@
-check16 = width x == 8
+check16 = length x == 8
   where
     x : [8]
     x = 0x3f

tests/regression/check16.icry.stdout

@@ -1,6 +1,6 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] at ./check16.cry:1:11--1:16:
-  Defaulting type argument 'bits' of 'width' to 4
+[warning] at ./check16.cry:1:23--1:24:
+  Defaulting type argument 'rep' of 'number' to [4]
 True

tests/regression/check21.cry

@@ -1,7 +1,7 @@
 irred : [8]
 irred = 0x1b
 // endianness difference from Cryptol-1 test
-xtimes a = (if a ! (width a - 1) then a' ^ irred else a')
+xtimes a = (if a ! (length a - 1) then a' ^ irred else a')
   where a' = a << 1
 
 check21 = [ xtimes y | y <- [ 1, 12, 192 ] ] == [ 2, 24, 155 ]

tests/regression/check21.icry.stdout

@@ -1,6 +1,6 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] at ./check21.cry:4:21--4:26:
-  Defaulting type argument 'bits' of 'width' to 4
+[warning] at ./check21.cry:4:16--4:34:
+  Defaulting type argument 'ix' of '(!)' to 4
 True

tests/regression/check22.cry

@@ -1,6 +1,6 @@
 irred : [8]
 irred = 0x1b
-xtimes a = (if a ! (width a - 1) then a' ^ irred else a')
+xtimes a = (if a ! (length a - 1) then a' ^ irred else a')
   where a' = a << 1
 
 gtimes : ([8], [8]) -> [8]

tests/regression/check22.icry.stdout

@@ -1,6 +1,6 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] at ./check22.cry:3:21--3:26:
-  Defaulting type argument 'bits' of 'width' to 4
+[warning] at ./check22.cry:3:16--3:34:
+  Defaulting type argument 'ix' of '(!)' to 4
 True

tests/regression/check23.cry

@@ -8,7 +8,7 @@ pad : {msgLen, padding, contentLen, chunks}
     ) => [msgLen] -> [chunks * 512]
 pad msg = msg # [True] # (zero:[padding]) # sz  //or: (`msgLen:[64])
       where  sz : [64]
-             sz = (width msg):[64]
+             sz = (length msg):[64]
 
 tmsg : [4]
 tmsg = 13