Support deepseq in reference evaluator

Checks off one box in #1249.

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
 

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 ->

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

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