From ec89833bcb8c8e2edba8ce6446b98072ffb4643f Mon Sep 17 00:00:00 2001
From: Sam Cowger <sam@galois.com>
Date: Thu, 9 Feb 2023 08:58:01 -0800
Subject: [PATCH] Try inlining by term string

---
 src/SAWScript/Builtins.hs    | 13 +++++++++++++
 src/SAWScript/Interpreter.hs |  8 ++++++++
 2 files changed, 21 insertions(+)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index d1d46152a6..03a175bd02 100644
--- a/src/SAWScript/Builtins.hs
+++ b/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 ->
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 7438a030fe..911c5f1c39 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/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