Merge pull request #703 from GaloisInc/issue702

issue702

src/Cryptol/Eval/Concrete.hs

@@ -24,8 +24,14 @@ module Cryptol.Eval.Concrete
   ) where
 
 import Control.Monad (join,guard,zipWithM)
+import Data.List(sortBy)
+import Data.Ord(comparing)
+import Data.Bits (Bits(..))
 import MonadLib( ChoiceT, findOne, lift )
 
+import qualified Data.Map.Strict as Map
+import qualified Data.Text as T
+
 import Cryptol.TypeCheck.Solver.InfNat (Nat'(..))
 import Cryptol.Eval.Backend
 import Cryptol.Eval.Concrete.Value
@@ -41,10 +47,6 @@ import Cryptol.Utils.Ident (Ident,mkIdent)
 import Cryptol.Utils.PP
 import Cryptol.Utils.Logger(logPrint)
 
-import Data.Bits (Bits(..))
-
-import qualified Data.Map.Strict as Map
-import qualified Data.Text as T
 
 
 -- Value to Expression conversion ----------------------------------------------
@@ -61,7 +63,7 @@ toExpr prims t0 v0 = findOne (go t0 v0)
 
   go :: AST.Type -> Value -> ChoiceT Eval Expr
   go ty val = case (tNoUser ty, val) of
-    (TRec tfs, VRecord vfs) -> do
+    (TRec (sortBy (comparing fst) -> tfs), VRecord vfs) -> do
       let fns = Map.keys vfs
       guard (map fst tfs == fns)
       fes <- zipWithM go (map snd tfs) =<< lift (sequence (Map.elems vfs))

src/Cryptol/Symbolic.hs

@@ -41,7 +41,7 @@ import           Cryptol.Utils.PP
 
 import Prelude ()
 import Prelude.Compat
-
+import qualified Data.Map as Map
 import Data.Time (NominalDiffTime)
 
 type SatResult = [(Type, Expr, Concrete.Value)]
@@ -105,7 +105,7 @@ data FinType
     | FTIntMod Integer
     | FTSeq Int FinType
     | FTTuple [FinType]
-    | FTRecord [(Ident, FinType)]
+    | FTRecord (Map.Map Ident FinType)
 
 numType :: Integer -> Maybe Int
 numType n
@@ -123,7 +123,7 @@ finType ty =
     TVIntMod n       -> Just (FTIntMod n)
     TVSeq n t        -> FTSeq <$> numType n <*> finType t
     TVTuple ts       -> FTTuple <$> traverse finType ts
-    TVRec fields     -> FTRecord <$> traverse (traverseSnd finType) fields
+    TVRec fields     -> FTRecord . Map.fromList <$> traverse (traverseSnd finType) fields
     TVAbstract {}    -> Nothing
     _                     -> Nothing
 
@@ -135,7 +135,4 @@ unFinType fty =
     FTIntMod n   -> tIntMod (tNum n)
     FTSeq l ety  -> tSeq (tNum l) (unFinType ety)
     FTTuple ftys -> tTuple (unFinType <$> ftys)
-    FTRecord fs  -> tRec (zip fns tys)
-      where
-        fns = fst <$> fs
-        tys = unFinType . snd <$> fs
+    FTRecord fs  -> tRec (Map.toList (fmap unFinType fs))

src/Cryptol/Symbolic/SBV.hs

@@ -274,7 +274,7 @@ parseValue (FTSeq n t) cvs =
 parseValue (FTTuple ts) cvs = (Eval.VTuple (map Eval.ready vs), cvs')
   where (vs, cvs') = parseValues ts cvs
 parseValue (FTRecord fs) cvs = (Eval.VRecord (Map.fromList (zip ns (map Eval.ready vs))), cvs')
-  where (ns, ts) = unzip fs
+  where (ns, ts)   = unzip (Map.toList fs)
         (vs, cvs') = parseValues ts cvs
 
 inBoundsIntMod :: Integer -> Eval.SInteger SBV -> Eval.SBit SBV
@@ -296,7 +296,7 @@ forallFinType ty =
     FTSeq n t     -> do vs <- replicateM n (forallFinType t)
                         return $ Eval.VSeq (toInteger n) $ Eval.finiteSeqMap SBV (map pure vs)
     FTTuple ts    -> Eval.VTuple <$> mapM (fmap pure . forallFinType) ts
-    FTRecord fs   -> Eval.VRecord <$> mapM (fmap pure . forallFinType) (Map.fromList fs)
+    FTRecord fs   -> Eval.VRecord <$> mapM (fmap pure . forallFinType) fs
 
 existsFinType :: FinType -> WriterT [Eval.SBit SBV] SBV.Symbolic Value
 existsFinType ty =
@@ -311,4 +311,4 @@ existsFinType ty =
     FTSeq n t     -> do vs <- replicateM n (existsFinType t)
                         return $ Eval.VSeq (toInteger n) $ Eval.finiteSeqMap SBV (map pure vs)
     FTTuple ts    -> Eval.VTuple <$> mapM (fmap pure . existsFinType) ts
-    FTRecord fs   -> Eval.VRecord <$> mapM (fmap pure . existsFinType) (Map.fromList fs)
+    FTRecord fs   -> Eval.VRecord <$> mapM (fmap pure . existsFinType) fs

tests/issues/issue702.icry

@@ -0,0 +1,2 @@
+:sat \(x : {b:Bit, a:Bit}) -> x.a && x.b
+:sat \(x : {b:[8], a:Bit}) -> x.b == 0 /\ x.a

tests/issues/issue702.icry.stdout

@@ -0,0 +1,5 @@
+Loading module Cryptol
+(\(x : {b : Bit, a : Bit}) -> x.a && x.b)
+  {a = True, b = True} = True
+(\(x : {b : [8], a : Bit}) -> x.b == 0 /\ x.a)
+  {a = True, b = 0x00} = True