Try inlining by term string

src/SAWScript/Builtins.hs

@@ -474,6 +474,19 @@ print_goal_inline noInline =
       let output = prettySequent opts' nenv (goalSequent goal)
       printOutLnTop Info (unlines [goalSummary goal, output])
 
+print_goal_inline_term :: [String] -> ProofScript ()
+print_goal_inline_term termStrs =
+  execTactic $ tacticId $ \goal ->
+    do
+      terms <- mapM parseCore termStrs
+      let idxs = Set.fromList [idx | STApp idx _ _ <- terms]
+      opts <- getTopLevelPPOpts
+      let opts' = opts { ppNoInlineIdx = idxs }
+      sc <- getSharedContext
+      nenv <- io (scGetNamingEnv sc)
+      let output = prettySequent opts' nenv (goalSequent goal)
+      printOutLnTop Info (unlines [goalSummary goal, output])
+
 print_goal_summary :: ProofScript ()
 print_goal_summary =
   execTactic $ tacticId $ \goal ->

src/SAWScript/Interpreter.hs

@@ -1833,6 +1833,14 @@ primitives = Map.fromList
     , "inlining the variables that would otherwise be abstracted as `x@1`,"
     , " `x@9`, and `x@3`."
     ]
+  , prim "print_goal_inline_term"      "[String] -> ProofScript ()"
+    (pureVal print_goal_inline_term)
+    Experimental
+    [ "Print the current goal that a proof script is attempting to prove,"
+    , "without generating `let` bindings for the provided terms. For example"
+    , "`print_goal_inline [\"Vec 8 Bool\"]` will print the goal without"
+    , "inlining any occurrence of `Vec 8 Bool`."
+    ]
   , prim "write_goal" "String -> ProofScript ()"
     (pureVal write_goal)
     Current