saw-script: let-inlining only works with incremental memoization

Author: samcowger

src/SAWScript/Builtins.hs

@@ -80,6 +80,7 @@ import qualified Verifier.SAW.SCTypeCheck as TC (TypedTerm(..))
 import Verifier.SAW.Recognizer
 import Verifier.SAW.Prelude (scEq)
 import Verifier.SAW.SharedTerm
+import Verifier.SAW.Term.Pretty (MemoStyle(..))
 import Verifier.SAW.TypedTerm
 import qualified Verifier.SAW.Simulator.Concrete as Concrete
 import Verifier.SAW.Prim (rethrowEvalError)
@@ -478,11 +479,22 @@ print_goal_inline noInline =
   execTactic $ tacticId $ \goal ->
     do
       opts <- getTopLevelPPOpts
-      let opts' = opts { ppNoInlineMemoFresh = sort noInline }
+      opts' <-
+        case ppMemoStyle opts of
+          Incremental -> pure opts { ppNoInlineMemoFresh = sort noInline }
+          HashIncremental _ -> pure opts { ppNoInlineMemoFresh = sort noInline }
+          Hash _ -> warnIncremental >> pure opts
       sc <- getSharedContext
       nenv <- io (scGetNamingEnv sc)
       let output = prettySequent opts' nenv (goalSequent goal)
       printOutLnTop Info (unlines [goalSummary goal, output])
+  where
+    warnIncremental =
+      printOutLnTop Warn $
+        unlines
+          [ "`print_goal_inline` is incompatible with non-incremental"
+          , "memoization strategies. Printing goal without inlining..."
+          ]
 
 print_goal_summary :: ProofScript ()
 print_goal_summary =

src/SAWScript/Interpreter.hs

@@ -2230,6 +2230,9 @@ primitives = Map.fromList
     , " `x@9`, and `x@3`. These indices are assigned deterministically with"
     , "regard to a particular goal, but are not persistent across goals. As"
     , "such, this should be used primarily when debugging a proof."
+    , ""
+    , "Note: incompatible with non-incremental memoization strategies - see"
+    , "`set_memoization_incremental` and `set_memoization_hash_incremental`."
     ]
   , prim "write_goal" "String -> ProofScript ()"
     (pureVal write_goal)