Support toSignedInteger and deepseq in the reference evaluator

CHANGES.md

@@ -15,6 +15,9 @@
   were incorrectly computed.
   ([#1773](https://github.com/GaloisInc/cryptol/issues/1773))
 
+* The reference evaluator now evaluates the `toSignedInteger` and `deepseq`
+  primitives instead of panicking.
+
 ## New features
 
 * REPL command `:dumptests <FILE> <EXPR>` updated to write to stdout when

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
 ------------
@@ -758,6 +779,10 @@ by corresponding type classes:
 >   , "lg2"        ~> vFinPoly $ \n -> pure $
 >                     VFun $ \v ->
 >                       vWord n <$> appOp1 lg2Wrap (fromVWord =<< v)
+>   , "toSignedInteger"
+>                  ~> vFinPoly $ \_n -> pure $
+>                     VFun $ \x ->
+>                     VInteger <$> (fromSignedVWord =<< x)
 >   -- Rational
 >   , "ratio"      ~> VFun $ \l -> pure $
 >                     VFun $ \r ->
@@ -944,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

@@ -0,0 +1,17 @@
+// toSignedInteger
+
+toSignedInteger (0 : [64])
+:eval toSignedInteger (0 : [64])
+toSignedInteger (1 : [64])
+:eval toSignedInteger (1 : [64])
+toSignedInteger (2^^63 - 1 : [64])
+:eval toSignedInteger (2^^63 - 1 : [64])
+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

@@ -0,0 +1,18 @@
+Loading module Cryptol
+0
+0
+1
+1
+9223372036854775807
+9223372036854775807
+-1
+-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