Merge pull request #855 from GaloisInc/issue851

Issue851

src/Cryptol/Eval/Concrete.hs

@@ -24,7 +24,7 @@ module Cryptol.Eval.Concrete
   , toExpr
   ) where
 
-import Control.Monad (join,guard,zipWithM,mzero)
+import Control.Monad (join, guard, zipWithM)
 import Data.Bits (Bits(..))
 import Data.Ratio(numerator,denominator)
 import MonadLib( ChoiceT, findOne, lift )
@@ -55,8 +55,6 @@ import Cryptol.Utils.RecordMap
 
 -- | Given an expected type, returns an expression that evaluates to
 -- this value, if we can determine it.
---
--- XXX: View patterns would probably clean up this definition a lot.
 toExpr :: PrimMap -> AST.Type -> Value -> Eval (Maybe AST.Expr)
 toExpr prims t0 v0 = findOne (go t0 v0)
   where
@@ -65,45 +63,47 @@ 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
-      -- NB, vfs first argument to keep their display order
-      res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs
-      case res of
-        Left _ -> mzero -- different fields
-        Right efs -> pure (ERec efs)
-    (TCon (TC (TCTuple tl)) ts, VTuple tvs) -> do
-      guard (tl == (length tvs))
-      ETuple `fmap` (zipWithM go ts =<< lift (sequence tvs))
-    (TCon (TC TCBit) [], VBit True ) -> return (prim "True")
-    (TCon (TC TCBit) [], VBit False) -> return (prim "False")
-    (TCon (TC TCInteger) [], VInteger i) ->
-      return $ ETApp (ETApp (prim "number") (tNum i)) ty
-    (TCon (TC TCIntMod) [_n], VInteger i) ->
-      return $ ETApp (ETApp (prim "number") (tNum i)) ty
-    (TCon (TC TCRational) [], VRational (SRational n d)) ->
-      do let n' = ETApp (ETApp (prim "number") (tNum n)) (TCon (TC TCInteger) [])
-             d' = ETApp (ETApp (prim "number") (tNum d)) (TCon (TC TCInteger) [])
-         return $ EApp (EApp (prim "ratio") n') d'
-    (TCon (TC TCFloat) [eT,pT], VFloat i) ->
-      pure (floatToExpr prims eT pT (bfValue i))
-
-    (TCon (TC TCSeq) [a,b], VSeq 0 _) -> do
-      guard (a == tZero)
-      return $ EList [] b
-    (TCon (TC TCSeq) [a,b], VSeq n svs) -> do
-      guard (a == tNum n)
-      ses <- mapM (go b) =<< lift (sequence (enumerateSeqMap n svs))
-      return $ EList ses b
-    (TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord _ wval) -> do
-      BV w v <- lift (asWordVal Concrete =<< wval)
-      guard (a == tNum w)
-      return $ ETApp (ETApp (prim "number") (tNum v)) ty
-    (_, VStream _) -> fail "cannot construct infinite expressions"
-    (_, VFun    _) -> fail "cannot convert function values to expressions"
-    (_, VPoly   _) -> fail "cannot convert polymorphic values to expressions"
-    _ -> do doc <- lift (ppValue Concrete defaultPPOpts val)
-            panic "Cryptol.Eval.Concrete.toExpr"
+  go ty val =
+    case val of
+      VRecord vfs ->
+        do tfs <- maybe mismatch pure (tIsRec ty)
+           -- NB, vfs first argument to keep their display order
+           res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs
+           case res of
+             Left _ -> mismatch -- different fields
+             Right efs -> pure (ERec efs)
+      VTuple tvs ->
+        do ts <- maybe mismatch pure (tIsTuple ty)
+           guard (length ts == length tvs)
+           ETuple <$> (zipWithM go ts =<< lift (sequence tvs))
+      VBit b ->
+        pure (prim (if b then "True" else "False"))
+      VInteger i ->
+        -- This works uniformly for values of type Integer or Z n
+        pure $ ETApp (ETApp (prim "number") (tNum i)) ty
+      VRational (SRational n d) ->
+        do let n' = ETApp (ETApp (prim "number") (tNum n)) tInteger
+           let d' = ETApp (ETApp (prim "number") (tNum d)) tInteger
+           pure $ EApp (EApp (prim "ratio") n') d'
+      VFloat i ->
+        do (eT, pT) <- maybe mismatch pure (tIsFloat ty)
+           pure (floatToExpr prims eT pT (bfValue i))
+      VSeq n svs ->
+        do (_a, b) <- maybe mismatch pure (tIsSeq ty)
+           ses <- traverse (go b) =<< lift (sequence (enumerateSeqMap n svs))
+           pure $ EList ses b
+      VWord _ wval ->
+        do BV _ v <- lift (asWordVal Concrete =<< wval)
+           pure $ ETApp (ETApp (prim "number") (tNum v)) ty
+      VStream _  -> fail "cannot construct infinite expressions"
+      VFun _     -> fail "cannot convert function values to expressions"
+      VPoly _    -> fail "cannot convert polymorphic values to expressions"
+      VNumPoly _ -> fail "cannot convert polymorphic values to expressions"
+    where
+      mismatch :: forall a. ChoiceT Eval a
+      mismatch =
+        do doc <- lift (ppValue Concrete defaultPPOpts val)
+           panic "Cryptol.Eval.Concrete.toExpr"
              ["type mismatch:"
              , pretty ty
              , render doc

src/Cryptol/TypeCheck/Type.hs

@@ -393,6 +393,18 @@ tIsIntMod ty = case tNoUser ty of
                  TCon (TC TCIntMod) [n] -> Just n
                  _                      -> Nothing
 
+tIsRational :: Type -> Bool
+tIsRational ty =
+  case tNoUser ty of
+    TCon (TC TCRational) [] -> True
+    _                       -> False
+
+tIsFloat :: Type -> Maybe (Type, Type)
+tIsFloat ty =
+  case tNoUser ty of
+    TCon (TC TCFloat) [e, p] -> Just (e, p)
+    _                        -> Nothing
+
 tIsTuple :: Type -> Maybe [Type]
 tIsTuple ty = case tNoUser ty of
                 TCon (TC (TCTuple _)) ts -> Just ts

tests/issues/issue851.cry

@@ -0,0 +1,16 @@
+type base t = { zero: t }
+
+B: base Bool
+B = { zero = False }
+
+foo: {t,k} (fin k) => base t -> [k]t
+foo b = repeat b.zero
+
+bar: {t,k} (fin k, k>=1) => [k]t -> [k]t -> [k]t -> [k]t
+bar p q m = p
+
+baz: {k,t} (fin k, k >= 1) => [k]t -> [k]t -> [k]t
+baz p q = q
+
+property problem p =
+  p != foo B ==> bar p (baz p 0x03) 0x03 == foo B

tests/issues/issue851.icry

@@ -0,0 +1,2 @@
+:l issue851.cry
+:exhaust problem

tests/issues/issue851.icry.stdout

@@ -0,0 +1,5 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Using exhaustive testing.
+Testing... problem 0x01 = False