Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Commit

Permalink
Fix implementation of fromIntMod in concrete evaluation backend.
Browse files Browse the repository at this point in the history
It had been broken since #93 introduced a separate value constructor
for the `IntMod` type.

(GaloisInc/saw-script#936)
  • Loading branch information
Brian Huffman committed Nov 24, 2020
1 parent 296bc6d commit 2d04786
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion saw-core/src/Verifier/SAW/Simulator/Concrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -254,7 +254,7 @@ constMap =
, ("Prelude.sbvToInt", sbvToIntOp)
-- Integers mod n
, ("Prelude.toIntMod" , toIntModOp)
, ("Prelude.fromIntMod", constFun (VFun force))
, ("Prelude.fromIntMod", fromIntModOp)
, ("Prelude.intModEq" , intModEqOp)
, ("Prelude.intModAdd" , intModBinOp (+))
, ("Prelude.intModSub" , intModBinOp (-))
Expand Down Expand Up @@ -320,6 +320,12 @@ toIntModOp =
Prims.intFun "toIntModOp" $ \x -> return $
VIntMod n (x `mod` toInteger n)

fromIntModOp :: CValue
fromIntModOp =
constFun $
Prims.intModFun "fromIntModOp" $ \x -> pure $
VInt x

intModEqOp :: CValue
intModEqOp =
constFun $
Expand Down

0 comments on commit 2d04786

Please sign in to comment.