From dd1e32766b155ab902e3bb656216a66e84c4adbb Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 20 Nov 2020 09:39:14 -0800
Subject: [PATCH] Add saw-script functions `term_eval` and `term_eval_unint`.

These are analogous to the `goal_eval` and `goal_eval_unint` proof
tactics, but instead of proof goals they work on arbitrary terms.
---
 deps/saw-core                |  2 +-
 src/SAWScript/Builtins.hs    |  9 +++++++++
 src/SAWScript/Interpreter.hs | 11 +++++++++++
 3 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/deps/saw-core b/deps/saw-core
index c8316b86c3..e3a9620ad8 160000
--- a/deps/saw-core
+++ b/deps/saw-core
@@ -1 +1 @@
-Subproject commit c8316b86c384e45a592ae866ed5a2186a92fd137
+Subproject commit e3a9620ad8ea1076cf50c77ec049579f9642e6fa
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 57b6972925..535eec3959 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -1127,6 +1127,15 @@ beta_reduce_term (TypedTerm schema t) = do
   t' <- io $ betaNormalize sc t
   return (TypedTerm schema t')
 
+term_eval :: [String] -> TypedTerm -> TopLevel TypedTerm
+term_eval unints (TypedTerm schema t0) =
+  do sc <- getSharedContext
+     unintSet <- resolveNames unints
+     let gen = globalNonceGenerator
+     sym <- liftIO $ Crucible.newSAWCoreBackend FloatRealRepr sc gen
+     t1 <- liftIO $ W4Sim.w4EvalTerm sym sc Map.empty unintSet t0
+     pure (TypedTerm schema t1)
+
 addsimp :: Theorem -> Simpset -> TopLevel Simpset
 addsimp (Theorem (Prop t) _stats) ss =
   case ruleOfProp t of
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 45f87bda04..9f86ae4b92 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -1566,6 +1566,17 @@ primitives = Map.fromList
     Current
     [ "Reduce the given term to beta-normal form." ]
 
+  , prim "term_eval"           "Term -> Term"
+    (funVal1 (term_eval []))
+    Current
+    [ "Evaluate the term to a first-order combination of primitives." ]
+
+  , prim "term_eval_unint"     "[String] -> Term -> Term"
+    (funVal2 term_eval)
+    Current
+    [ "Evaluate the term to a first-order combination of primitives."
+    , "Leave the given names, as defined with 'define', as uninterpreted." ]
+
   , prim "cryptol_load"        "String -> TopLevel CryptolModule"
     (pureVal (cryptol_load BS.readFile))
     Current