diff --git a/CHANGES.md b/CHANGES.md index ab73fa9a6..9e8ba0982 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -15,8 +15,8 @@ were incorrectly computed. ([#1773](https://github.com/GaloisInc/cryptol/issues/1773)) -* The reference evaluator now evaluates the `toSignedInteger` primitive instead - of panicking. +* The reference evaluator now evaluates the `toSignedInteger` and `deepseq` + primitives instead of panicking. ## New features diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index 4ce7e99fb..d6eff26c7 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -247,7 +247,28 @@ Operations on Values > where > g (Nat n) = f n > g Inf = evalPanic "vFinPoly" ["Expected finite numeric type"] - +> +> -- | Reduce a value to normal form. +> forceValue :: Value -> E () +> forceValue v = +> case v of +> -- Values where the field is already is normal form +> VBit{} -> pure () +> VInteger{} -> pure () +> VRational{} -> pure () +> VFloat{} -> pure () +> -- Values with fields containing other values to reduce to normal form +> VList _ xs -> forceValues xs +> VTuple xs -> forceValues xs +> VRecord fs -> forceValues $ map snd fs +> VEnum _ xs -> forceValues xs +> -- Lambdas and other abstractions are already in normal form +> VFun{} -> pure () +> VPoly{} -> pure () +> VNumPoly{} -> pure () +> where +> forceValues :: [E Value] -> E () +> forceValues = mapM_ (\x -> forceValue =<< x) Environments ------------ @@ -948,6 +969,13 @@ by corresponding type classes: > -- executes parmap sequentially > pure $ VList n (map f' xs') > +> , "deepseq" ~> VPoly $ \_a -> pure $ +> VPoly $ \_b -> pure $ +> VFun $ \x -> pure $ +> VFun $ \y -> +> do forceValue =<< x +> y +> > , "error" ~> VPoly $ \_a -> pure $ > VNumPoly $ \_ -> pure $ > VFun $ \s -> diff --git a/tests/issues/issue1249.icry b/tests/issues/issue1249.icry index e89f65c3d..46d009c6d 100644 --- a/tests/issues/issue1249.icry +++ b/tests/issues/issue1249.icry @@ -10,3 +10,8 @@ toSignedInteger (-1 : [64]) :eval toSignedInteger (-1 : [64]) toSignedInteger (-(2^^63) : [64]) :eval toSignedInteger (-(2^^63) : [64]) + +// deepseq + +deepseq ((), undefined`{()}) True +:eval deepseq ((), undefined`{()}) True diff --git a/tests/issues/issue1249.icry.stdout b/tests/issues/issue1249.icry.stdout index 562bc3d33..4550eea81 100644 --- a/tests/issues/issue1249.icry.stdout +++ b/tests/issues/issue1249.icry.stdout @@ -9,3 +9,10 @@ Loading module Cryptol -1 -9223372036854775808 -9223372036854775808 + +Run-time error: undefined +-- Backtrace -- +Cryptol::error called at Cryptol:1062:13--1062:18 +Cryptol::undefined called at issue1249.icry:16:14--16:23 +Cryptol::deepseq called at issue1249.icry:16:1--16:8 +Run-time error: undefined