Add a normalize_term command to experiment with the results

of the TermModel evaluator.

Author: robdockins

src/SAWScript/Builtins.hs

@@ -74,6 +74,7 @@ import Verifier.SAW.Prim (rethrowEvalError)
 import Verifier.SAW.Rewriter
 import Verifier.SAW.Testing.Random (prepareSATQuery, runManyTests)
 import Verifier.SAW.TypedAST
+import qualified Verifier.SAW.Simulator.TermModel as TM
 
 import SAWScript.Position
 
@@ -492,6 +493,14 @@ resolveName sc nm =
  fallback = fst <$> io (scResolveUnambiguous sc tnm)
 
 
+normalize_term :: TypedTerm -> TopLevel TypedTerm
+normalize_term tt =
+  do sc <- getSharedContext
+     modmap <- io (scGetModuleMap sc)
+     tm' <- io (TM.normalizeSharedTerm sc modmap mempty mempty (ttTerm tt))
+     pure tt{ ttTerm = tm' }
+
+
 unfoldGoal :: [String] -> ProofScript ()
 unfoldGoal unints =
   execTactic $ tacticChange $ \goal ->

src/SAWScript/Interpreter.hs

@@ -1209,6 +1209,11 @@ primitives = Map.fromList
     Experimental
     [ "hoist ifs in the current proof goal" ]
 
+  , prim "normalize_term"      "Term -> Term"
+    (funVal1 normalize_term)
+    Experimental
+    [ "Normalize the given term by performing evaluation in SAWCore." ]
+
   , prim "goal_eval"           "ProofScript ()"
     (pureVal (goal_eval []))
     Current