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.

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

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