Take bitLit out of the SEval monad. The backends all support

a non-monadic version of bit literals, and it's somewhat more convenient.

src/Cryptol/Eval/Backend.hs

@@ -76,7 +76,7 @@ class MonadIO (SEval sym) => Backend sym where
   wordLen :: sym -> SWord sym -> Integer
 
   -- | Construct a literal bit value from a boolean.
-  bitLit :: sym -> Bool -> SEval sym (SBit sym)
+  bitLit :: sym -> Bool -> SBit sym
 
   -- | Determine if this symbolic bit is a boolean literal
   bitAsLit :: sym -> SBit sym -> Maybe Bool

src/Cryptol/Eval/Concrete.hs

@@ -108,8 +108,8 @@ primTable :: Map.Map Ident Value
 primTable = let sym = Concrete in
   Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
   [ -- Literals
-    ("True"       , VBit True)
-  , ("False"      , VBit False)
+    ("True"       , VBit (bitLit sym True))
+  , ("False"      , VBit (bitLit sym False))
   , ("number"     , {-# SCC "Prelude::number" #-}
                     ecNumberV sym)
 

src/Cryptol/Eval/Concrete/Value.hs

@@ -163,7 +163,7 @@ instance Backend Concrete where
 
   ppInteger _ _opts i = integer i
 
-  bitLit _ b = pure b
+  bitLit _ b = b
   bitAsLit _ b = Just b
 
   bitEq _  x y = pure $! x == y

src/Cryptol/Eval/Generic.hs

@@ -413,7 +413,7 @@ bitGreaterThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit
 bitGreaterThan sym x y = bitLessThan sym y x
 
 valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
-valEq sym ty v1 v2 = cmpValue sym fb fw fi fz ty v1 v2 (bitLit sym True)
+valEq sym ty v1 v2 = cmpValue sym fb fw fi fz ty v1 v2 (pure $ bitLit sym True)
   where
   fb x y k   = eqCombine sym (bitEq sym x y)      k
   fw x y k   = eqCombine sym (wordEq sym x y)     k
@@ -421,8 +421,8 @@ valEq sym ty v1 v2 = cmpValue sym fb fw fi fz ty v1 v2 (bitLit sym True)
   fz m x y k = eqCombine sym (intModEq sym m x y) k
 
 valLt :: Backend sym =>
-  sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
-valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz ty v1 v2 final
+  sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
+valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz ty v1 v2 (pure final)
   where
   fb x y k   = lexCombine sym (bitLessThan sym x y)      (bitEq sym x y)      k
   fw x y k   = lexCombine sym (wordLessThan sym x y)     (wordEq sym x y)     k
@@ -430,8 +430,8 @@ valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz ty v1 v2 final
   fz m x y k = lexCombine sym (intModLessThan sym m x y) (intModEq sym m x y) k
 
 valGt :: Backend sym =>
-  sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
-valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz ty v1 v2 final
+  sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
+valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz ty v1 v2 (pure final)
   where
   fb x y k   = lexCombine sym (bitGreaterThan sym y x)      (bitEq sym x y)      k
   fw x y k   = lexCombine sym (wordGreaterThan sym x y)     (wordEq sym x y)     k
@@ -475,7 +475,7 @@ greaterThanEqV :: Backend sym => sym -> Binary sym
 greaterThanEqV sym ty v1 v2 = VBit <$> valGt sym ty v1 v2 (bitLit sym True)
 
 signedLessThanV :: Backend sym => sym -> Binary sym
-signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz ty v1 v2 (bitLit sym False)
+signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz ty v1 v2 (pure $ bitLit sym False)
   where
   fb _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on bit type"]
   fw x y k   = lexCombine sym (wordSignedLessThan sym x y) (wordEq sym x y) k
@@ -508,7 +508,7 @@ zeroV sym ty = case ty of
 
   -- bits
   TVBit ->
-    VBit <$> bitLit sym False
+    pure (VBit (bitLit sym False))
 
   -- integers
   TVInteger ->

src/Cryptol/Eval/SBV.hs

@@ -197,7 +197,7 @@ instance Backend SBV where
 
   bitAsLit _ b = svAsBool b
 
-  bitLit _ b     = pure $! svBool b
+  bitLit _ b     = svBool b
   wordLit _ n x  = pure $! svInteger (KBounded False (fromInteger n)) x
   integerLit _ x = pure $! svInteger KUnbounded x
 
@@ -387,8 +387,8 @@ primTable :: Map.Map Ident Value
 primTable  = let sym = SBV in
   Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
   [ -- Literals
-    ("True"        , VBit SBV.svTrue)
-  , ("False"       , VBit SBV.svFalse)
+    ("True"        , VBit (bitLit sym True))
+  , ("False"       , VBit (bitLit sym False))
   , ("number"      , ecNumberV sym) -- Converts a numeric type into its corresponding value.
                                     -- { val, rep } (Literal val rep) => rep
 
@@ -566,7 +566,7 @@ logicShift nm wop reindex =
                    do idx_bits <- enumerateWordValue SBV idx
                       let op bs shft = memoMap $ IndexSeqMap $ \i ->
                                          case reindex (Nat w) i shft of
-                                           Nothing -> VBit <$> bitLit SBV False
+                                           Nothing -> pure (VBit (bitLit SBV False))
                                            Just i' -> lookupSeqMap bs i'
                       LargeBitsVal n <$> shifter (mergeSeqMap SBV) op bs0 idx_bits
 

src/Cryptol/Testing/Random.hs

@@ -169,7 +169,7 @@ randomValue sym ty =
 randomBit :: (Backend sym, RandomGen g) => sym -> Gen g sym
 randomBit sym _ g =
   let (b,g1) = random g
-  in (VBit <$> bitLit sym b, g1)
+  in (pure (VBit (bitLit sym b)), g1)
 
 randomSize :: RandomGen g => Int -> Int -> g -> (Int, g)
 randomSize k n g