Add function scToIntMod to SharedTerm library.

GaloisInc · Nov 3, 2020 · e2f714d · e2f714d
1 parent 80c40b5
commit e2f714d
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -172,6 +172,7 @@ module Verifier.SAW.SharedTerm
   , scIntToBv, scBvToInt, scSbvToInt
     -- *** IntMod
   , scIntModType
+  , scToIntMod
     -- *** Vectors
   , scAppend
   , scJoin
@@ -1709,6 +1710,12 @@ scSbvToInt sc n x = scGlobalApply sc "Prelude.sbvToInt" [n,x]
 scIntModType :: SharedContext -> Term -> IO Term
 scIntModType sc n = scGlobalApply sc "Prelude.IntMod" [n]
 
+-- | Convert an integer to an integer mod n.
+--
+-- > toIntMod : (n : Nat) -> Integer -> IntMod n;
+scToIntMod :: SharedContext -> Term -> Term -> IO Term
+scToIntMod sc n x = scGlobalApply sc "Prelude.toIntMod" [n, x]
+
 
 -- Primitive operations on bitvectors