Support literal 0 and 1 at type Bit.

src/Cryptol/Eval/Generic.hs

@@ -49,6 +49,7 @@ import Cryptol.Utils.RecordMap
 mkLit :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)
 mkLit sym ty i =
   case ty of
+    TVBit                        -> pure $ VBit (bitLit sym (i > 0))
     TVInteger                    -> VInteger <$> integerLit sym i
     TVIntMod m
       | m == 0                   -> evalPanic "mkLit" ["0 modulus not allowed"]

src/Cryptol/TypeCheck/Solver/Class.hs

@@ -531,6 +531,9 @@ solveLiteralInst val ty
       -- Literal n Error -> fails
       TCon (TError _ e) _ -> Unsolvable e
 
+      -- (1 >= val) => Literal val Bit
+      TCon (TC TCBit) [] -> SolvedIf [ tOne >== val ]
+
       -- (fin val) => Literal val Integer
       TCon (TC TCInteger) [] -> SolvedIf [ pFin val ]
 

tests/issues/issue913.icry

@@ -0,0 +1,5 @@
+or [0,1,0,1]
+and [1,0,1,1]
+[0,1,0,1,1,0,1,1:Bit]
+:t number`{rep=Bit}
+2 : Bit

tests/issues/issue913.icry.stdout

@@ -0,0 +1,13 @@
+Loading module Cryptol
+True
+False
+0x5b
+number`{rep = Bit} : {n} (1 >= n) => Bit
+
+[error] at <interactive>:1:1--1:2:
+  Unsolvable constraints:
+    • 1 >= 2
+        arising from
+        use of literal or demoted expression
+        at <interactive>:1:1--1:2
+    • Reason: It is not the case that 1 >= 2

tests/regression/instance.cry

@@ -348,6 +348,10 @@ signedCmpRecord = (<$)
 ////////////////////////////////////////////////////////////////////////////////
 // Literal
 
+/** instance (1 >= val) => Literal val Bit */
+literalBit : {val} (1 >= val) => Bit
+literalBit = `val
+
 /** instance (fin val) => Literal val Integer */
 literalInteger : {val} (fin val) => Integer
 literalInteger = `val