From 4a471b61f30e144a01bb0ddc6d0ed96169f0f338 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 28 Apr 2021 13:08:15 -0700
Subject: [PATCH] Make `goal_eval_unint` handle `Z n` types.

Fixes #1120.
---
 .../src/Verifier/SAW/Simulator/What4.hs          | 16 ++++++++++++++++
 saw-core/src/Verifier/SAW/SharedTerm.hs          |  7 +++++++
 2 files changed, 23 insertions(+)

diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index be2114cd59..cab2c98114 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -1193,6 +1193,9 @@ parseUninterpretedSAW sym st sc ref trm app ty =
     VIntType
       -> VInt  <$> mkUninterpretedSAW sym st ref trm app BaseIntegerRepr
 
+    VIntModType n
+      -> VIntMod n <$> mkUninterpretedSAW sym st ref (ArgTermFromIntMod n trm) app BaseIntegerRepr
+
     -- 0 width bitvector is a constant
     VVecType 0 VBoolType
       -> return $ VWord ZBV
@@ -1247,6 +1250,8 @@ mkUninterpretedSAW sym st ref trm (UnintApp nm args tys) ret =
 data ArgTerm
   = ArgTermVar
   | ArgTermBVZero -- ^ scBvNat 0 0
+  | ArgTermToIntMod Natural ArgTerm -- ^ toIntMod n x
+  | ArgTermFromIntMod Natural ArgTerm -- ^ fromIntMod n x
   | ArgTermVector Term [ArgTerm] -- ^ element type, elements
   | ArgTermUnit
   | ArgTermPair ArgTerm ArgTerm
@@ -1278,6 +1283,16 @@ reconstructArgTerm atrm sc ts =
           do z <- scNat sc 0
              x <- scBvNat sc z z
              return (x, ts0)
+        ArgTermToIntMod n at1 ->
+          do n' <- scNat sc n
+             (x1, ts1) <- parse at1 ts0
+             x <- scToIntMod sc n' x1
+             pure (x, ts1)
+        ArgTermFromIntMod n at1 ->
+          do n' <- scNat sc n
+             (x1, ts1) <- parse at1 ts0
+             x <- scFromIntMod sc n' x1
+             pure (x, ts1)
         ArgTermVector ty ats ->
           do (xs, ts1) <- parseList ats ts0
              x <- scVector sc ty xs
@@ -1336,6 +1351,7 @@ mkArgTerm sc ty val =
     (_, VWord ZBV)       -> return ArgTermBVZero     -- 0-width bitvector is a constant
     (_, VWord (DBV _))   -> return ArgTermVar
     (VUnitType, VUnit)   -> return ArgTermUnit
+    (VIntModType n, VIntMod _ _) -> pure (ArgTermToIntMod n ArgTermVar)
 
     (VVecType _ ety, VVector vv) ->
       do vs <- traverse force (V.toList vv)
diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
index 165f7e4fb3..dc9063e696 100644
--- a/saw-core/src/Verifier/SAW/SharedTerm.hs
+++ b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -185,6 +185,7 @@ module Verifier.SAW.SharedTerm
     -- *** IntMod
   , scIntModType
   , scToIntMod
+  , scFromIntMod
     -- *** Vectors
   , scAppend
   , scJoin
@@ -1829,6 +1830,12 @@ scIntModType sc n = scGlobalApply sc "Prelude.IntMod" [n]
 scToIntMod :: SharedContext -> Term -> Term -> IO Term
 scToIntMod sc n x = scGlobalApply sc "Prelude.toIntMod" [n, x]
 
+-- | Convert an integer mod n to an integer.
+--
+-- > fromIntMod : (n : Nat) -> IntMod n -> Integer;
+scFromIntMod :: SharedContext -> Term -> Term -> IO Term
+scFromIntMod sc n x = scGlobalApply sc "Prelude.fromIntMod" [n, x]
+
 
 -- Primitive operations on bitvectors