Variable width char

src/Cryptol/TypeCheck/Infer.hs

@@ -133,12 +133,10 @@ desugarLiteral lit =
          in P.EAppT fracPrim [ arg numerator, arg denominator, rnd ]
 
        P.ECChar c ->
-         number [ ("val", P.TNum (toInteger (fromEnum c)))
-                , ("rep", tBits (8 :: Integer)) ]
+         number [ ("val", P.TNum (toInteger (fromEnum c))) ]
 
        P.ECString s ->
-          P.ETyped (P.EList [ P.ELit (P.ECChar c) | c <- s ])
-                   (P.TSeq P.TWild (P.TSeq (P.TNum 8) P.TBit))
+          P.EList [ P.ELit (P.ECChar c) | c <- s ]
 
 
 

tests/issues/T146.icry.stdout

@@ -3,14 +3,14 @@ Loading module Cryptol
 Loading module Main
 
 [error] at T146.cry:1:18--6:10:
-  The type ?fv`958 is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`942
+  The type ?fv`968 is not sufficiently polymorphic.
+    It cannot depend on quantified variables: fv`952
   where
-  ?fv`958 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
-  fv`942 is signature variable 'fv' at T146.cry:11:10--11:12
+  ?fv`968 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
+  fv`952 is signature variable 'fv' at T146.cry:11:10--11:12
 [error] at T146.cry:5:19--5:24:
-  The type ?fv`960 is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`942
+  The type ?fv`970 is not sufficiently polymorphic.
+    It cannot depend on quantified variables: fv`952
   where
-  ?fv`960 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
-  fv`942 is signature variable 'fv' at T146.cry:11:10--11:12
+  ?fv`970 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
+  fv`952 is signature variable 'fv' at T146.cry:11:10--11:12

tests/issues/issue138.icry

@@ -1,4 +1,4 @@
 :l issue138.cry
 down
 down'
-take_some`{4,3} "abcd"
+take_some`{4,3,[8]} "abcd"

tests/issues/issue290v2.icry.stdout

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

tests/issues/issue389.icry

@@ -1,3 +1,3 @@
 :l issue389.cry
-pad (join "a") 
-test (join "a")
+pad (join "a" : [8])
+test (join "a" : [8])

tests/issues/issue474.icry

@@ -1,3 +1,3 @@
 let mapping = ['A' .. 'Z'] <<< 13
 let mapped c = if (('A' <= c) && (c <= 'Z')) then (mapping @ (c - 'A')) else c
-:sat \x -> mapped x == 'N'
+:sat \(x : [8]) -> mapped x == 'N'

tests/issues/issue474.icry.stdout

@@ -1,3 +1,3 @@
 Loading module Cryptol
 Satisfiable
-(\x -> mapped x == 'N') 0x41 = True
+(\(x : [8]) -> mapped x == 'N') 0x41 = True

tests/issues/issue723.icry.stdout

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

tests/regression/check17.cry

@@ -1 +1 @@
-check17 = "" == []
+check17 = ("" : [0][8]) == []