From b7b4d9fa762eda85815de9ad683676c126f2fc6f Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 30 Jul 2020 10:13:22 -0700 Subject: [PATCH 1/3] Add recognizer functions `tIsRational` and `tIsFloat`. --- src/Cryptol/TypeCheck/Type.hs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index a7e070afe..73835d483 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/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 From aac3c943f41567e03ddab5f3ca239a2d303a049e Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 30 Jul 2020 10:16:10 -0700 Subject: [PATCH 2/3] Rewrite function `toExpr` using a complete pattern match. Fixes #851. --- src/Cryptol/Eval/Concrete.hs | 84 ++++++++++++++++++------------------ 1 file changed, 42 insertions(+), 42 deletions(-) diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs index ef01d73b4..624ebdd13 100644 --- a/src/Cryptol/Eval/Concrete.hs +++ b/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 From 331725e1353df680561b6c2c92adbfbd15ab0baf Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 30 Jul 2020 10:53:37 -0700 Subject: [PATCH 3/3] Add regression test for #851. --- tests/issues/issue851.cry | 16 ++++++++++++++++ tests/issues/issue851.icry | 2 ++ tests/issues/issue851.icry.stdout | 5 +++++ 3 files changed, 23 insertions(+) create mode 100644 tests/issues/issue851.cry create mode 100644 tests/issues/issue851.icry create mode 100644 tests/issues/issue851.icry.stdout diff --git a/tests/issues/issue851.cry b/tests/issues/issue851.cry new file mode 100644 index 000000000..7e778d471 --- /dev/null +++ b/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 diff --git a/tests/issues/issue851.icry b/tests/issues/issue851.icry new file mode 100644 index 000000000..a30c1c9e7 --- /dev/null +++ b/tests/issues/issue851.icry @@ -0,0 +1,2 @@ +:l issue851.cry +:exhaust problem diff --git a/tests/issues/issue851.icry.stdout b/tests/issues/issue851.icry.stdout new file mode 100644 index 000000000..d1a51af0b --- /dev/null +++ b/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