Merge pull request #1678 from GaloisInc/issue_1490

Fixes #1490

lib/Cryptol.cry

@@ -725,16 +725,16 @@ scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
 scarry x y = (sx == sy) && (sx != sz)
   where
     z  = x + y
-    sx = x@0
-    sy = y@0
-    sz = z@0
+    sx = head x
+    sy = head y
+    sz = head z
 
 /**
  * Signed borrow.  Returns true if the 2's complement signed subtraction of the
  * given bitvector arguments would result in a signed overflow.
  */
 sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
-sborrow x y = ( x <$ (x-y) ) ^ y@0
+sborrow x y = ( x <$ (x-y) ) ^ head y
 
 /**
  * Zero extension of a bitvector.
@@ -747,7 +747,7 @@ zext x = zero # x
  */
 sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
 sext x = newbits # x
-  where newbits = if x@0 then ~zero else zero
+  where newbits = if head x then ~zero else zero
 
 /**
  * 2's complement signed (arithmetic) right shift.  The first argument
@@ -850,13 +850,13 @@ tail xs = drop`{1} xs
  * Return the first (left-most) element of a sequence.
  */
 head : {n, a} [1 + n]a -> a
-head xs = xs @ 0
+head xs = xs @ (0 : Integer)
 
 /**
  * Return the right-most element of a sequence.
  */
 last : {n, a} (fin n) => [1 + n]a -> a
-last xs = xs ! 0
+last xs = xs ! (0 : Integer)
 
 /**
  * Same as 'split', but with a different type argument order.
@@ -985,13 +985,13 @@ sort = sortBy (<=)
 sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a
 sortBy le ((xs : [n/2]a) # (ys : [n/^2]a)) = take zs.0
   where
-    xs' = if `(n/2)  == 1 then xs else sortBy le xs
-    ys' = if `(n/^2) == 1 then ys else sortBy le ys
+    xs' = if `(n/2)  == (1 : Integer) then xs else sortBy le xs
+    ys' = if `(n/^2) == (1 : Integer) then ys else sortBy le ys
     zs  = [ if i == `(n/2)        then (ys'@j, i  , j+1)
              | j == `(n/^2)       then (xs'@i, i+1, j  )
              | le (xs'@i) (ys'@j) then (xs'@i, i+1, j  )
             else                       (ys'@j, i  , j+1)
-          | (_, i, j) <- [ (undefined, 0, 0) ] # zs
+          | (_, i , j) <- [ (undefined, 0 : Integer, 0 : Integer) ] # zs
           ]
 
 // GF_2^n polynomial computations -------------------------------------------

tests/ffi/ffi-runtime-errors.icry.stdout

@@ -4,7 +4,7 @@ Loading module Main
 Loading dynamic library ffi-runtime-errors.so
 
 numeric type argument to foreign function is too large: 18446744073709551616
-in type parameter n`902 of function Main::f
+in type parameter n`892 of function Main::f
 type arguments must fit in a C `size_t`
 -- Backtrace --
 Main::f called at ffi-runtime-errors.icry:4:1--4:2

tests/ffi/ffi-runtime-errors.icry.stdout.darwin

@@ -4,7 +4,7 @@ Loading module Main
 Loading dynamic library ffi-runtime-errors.dylib
 
 numeric type argument to foreign function is too large: 18446744073709551616
-in type parameter n`902 of function Main::f
+in type parameter n`892 of function Main::f
 type arguments must fit in a C `size_t`
 -- Backtrace --
 Main::f called at ffi-runtime-errors.icry:4:1--4:2

tests/ffi/ffi-runtime-errors.icry.stdout.mingw32

@@ -4,7 +4,7 @@ Loading module Main
 Loading dynamic library ffi-runtime-errors.dll
 
 numeric type argument to foreign function is too large: 18446744073709551616
-in type parameter n`902 of function Main::f
+in type parameter n`892 of function Main::f
 type arguments must fit in a C `size_t`
 -- Backtrace --
 Main::f called at ffi-runtime-errors.icry:4:1--4:2

tests/ffi/ffi-type-errors.icry.stdout

@@ -35,23 +35,23 @@ Loading module Main
   When checking the type of 'Main::badFloatSizes'
 [error] at ffi-type-errors.cry:5:9--6:59:
   Type unsupported for FFI:
-    [n`972] -> [n`972]([16], [16]) -> [n`972][4][8]{a : [n`972],
+    [n`962] -> [n`962]([16], [16]) -> [n`962][4][8]{a : [n`962],
      b : [2]}
     Due to:
       Type unsupported for FFI:
-        [n`972]
+        [n`962]
         Due to:
         Unsupported sequence element type
         Only words or floats are supported as the element type of
         (possibly multidimensional) sequences
       Type unsupported for FFI:
-        [n`972]([16], [16])
+        [n`962]([16], [16])
         Due to:
         Unsupported sequence element type
         Only words or floats are supported as the element type of
         (possibly multidimensional) sequences
       Type unsupported for FFI:
-        [n`972][4][8]{a : [n`972], b : [2]}
+        [n`962][4][8]{a : [n`962], b : [2]}
         Due to:
         Unsupported sequence element type
         Only words or floats are supported as the element type of
@@ -65,7 +65,7 @@ Loading module Main
   When checking the type of 'Main::notFunction'
 [error] at ffi-type-errors.cry:8:9--8:32:
   Kind of type variable unsupported for FFI: 
-    t`973 : *
+    t`963 : *
     Only type variables of kind # are supported
     When checking the type of 'Main::badKind'
 [error] at ffi-type-errors.cry:9:9--9:43:

tests/issues/T146.icry.stdout

@@ -4,15 +4,15 @@ Loading module Main
 
 [error] at T146.cry:11:10--11:12:
   The type ?b is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`905
+    It cannot depend on quantified variables: fv`895
     When checking signature variable 'fv'
   where
   ?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
-  fv`905 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`895 is signature variable 'fv' at T146.cry:11:10--11:12
 [error] at T146.cry:12:11--12:21:
   The type ?a is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`905
+    It cannot depend on quantified variables: fv`895
     When checking type of field 'v0'
   where
   ?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
-  fv`905 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`895 is signature variable 'fv' at T146.cry:11:10--11:12

tests/issues/issue1024.icry.stdout

@@ -13,20 +13,20 @@ Loading module Main
     Unused name: g
 
 [error] at issue1024a.cry:1:6--1:24:
-  Illegal kind assigned to type variable: f`902
+  Illegal kind assigned to type variable: f`892
   Unexpected: # -> *
   where
-  f`902 is signature variable 'f' at issue1024a.cry:1:13--1:14
+  f`892 is signature variable 'f' at issue1024a.cry:1:13--1:14
 [error] at issue1024a.cry:2:6--2:24:
-  Illegal kind assigned to type variable: f`903
+  Illegal kind assigned to type variable: f`893
   Unexpected: Prop
   where
-  f`903 is signature variable 'f' at issue1024a.cry:2:15--2:16
+  f`893 is signature variable 'f' at issue1024a.cry:2:15--2:16
 [error] at issue1024a.cry:4:13--4:49:
-  Illegal kind assigned to type variable: f`905
+  Illegal kind assigned to type variable: f`895
   Unexpected: # -> *
   where
-  f`905 is signature variable 'f' at issue1024a.cry:4:22--4:32
+  f`895 is signature variable 'f' at issue1024a.cry:4:22--4:32
 Loading module Cryptol
 Loading module Main
 0xffff

tests/issues/issue290v2.icry.stdout

@@ -17,9 +17,9 @@ Loading module Main
             at issue290v2.cry:2:1--2:19
 [error] at issue290v2.cry:2:8--2:11:
   Unsolved constraints:
-    • n`902 == 1
+    • n`892 == 1
         arising from
         checking a pattern: type of 1st argument of Main::minMax
         at issue290v2.cry:2:8--2:11
   where
-  n`902 is signature variable 'n' at issue290v2.cry:1:11--1:12
+  n`892 is signature variable 'n' at issue290v2.cry:1:11--1:12

tests/issues/issue723.icry.stdout

@@ -10,9 +10,9 @@ Loading module Main
       assuming
         • fin k
       the following constraints hold:
-        • k == n`902
+        • k == n`892
             arising from
             matching types
             at issue723.cry:7:17--7:19
   where
-  n`902 is signature variable 'n' at issue723.cry:1:6--1:7
+  n`892 is signature variable 'n' at issue723.cry:1:6--1:7

tests/regression/tc-errors.icry.stdout

@@ -84,19 +84,19 @@ Loading module Main
 
 [error] at tc-errors-5.cry:2:1--2:7:
   Inferred type is not sufficiently polymorphic.
-    Quantified variable: a`902
+    Quantified variable: a`892
     cannot match type: [0]?a
     When checking the type of 'Main::f'
   where
   ?a is type of sequence member at tc-errors-5.cry:2:5--2:7
-  a`902 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
+  a`892 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
 Loading module Cryptol
 Loading module Main
 
 [error] at tc-errors-6.cry:4:3--4:8:
   The type ?a is not sufficiently polymorphic.
-    It cannot depend on quantified variables: b`906
+    It cannot depend on quantified variables: b`896
     When checking the type of 'g'
   where
   ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4
-  b`906 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
+  b`896 is signature variable 'b' at tc-errors-6.cry:3:8--3:9