let inlining in goal printing

saw-core/src/Verifier/SAW/Term/Pretty.hs

@@ -55,6 +55,8 @@ import qualified Data.Foldable as Fold
 import qualified Data.Text as Text
 import qualified Data.Text.Lazy as Text.Lazy
 import qualified Data.Map as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
 import qualified Data.Vector as V
 import Numeric (showIntAtBase)
 import Prettyprinter
@@ -106,11 +108,14 @@ data PPOpts = PPOpts { ppBase :: Int
                      , ppColor :: Bool
                      , ppShowLocalNames :: Bool
                      , ppMaxDepth :: Maybe Int
+                     , ppNoInlineMemo :: [MemoVar]
+                     , ppNoInlineIdx :: Set TermIndex -- move to PPState?
                      , ppMinSharing :: Int }
 
 -- | Default options for pretty-printing
 defaultPPOpts :: PPOpts
 defaultPPOpts = PPOpts { ppBase = 10, ppColor = False,
+                         ppNoInlineMemo = mempty, ppNoInlineIdx = mempty,
                          ppShowLocalNames = True, ppMaxDepth = Nothing, ppMinSharing = 2 }
 
 -- | Options for printing with a maximum depth
@@ -289,22 +294,45 @@ withBoundVarM basename m =
                               ppLocalMemoTable = IntMap.empty }) m
      return (var, ret)
 
--- | Run a computation in the context of a fresh "memoization variable" that is
--- bound to the given term index, passing the new memoization variable to the
--- computation. If the flag is true, use the global table, otherwise use the
--- local table.
-withMemoVar :: Bool -> TermIndex -> (MemoVar -> PPM a) -> PPM a
+-- | Attempt to memoize the given term (index) 'idx' and run a computation in
+-- the context that the attempt produces. If memoization succeeds, the context
+-- will contain a binding (global in scope if 'global_p' is set, local if not)
+-- of a fresh memoization variable to the term, and the fresh variable will be
+-- supplied to the computation. If memoization fails, the context will not
+-- contain such a binding, and no fresh variable will be supplied.
+withMemoVar :: Bool -> TermIndex -> (Maybe MemoVar -> PPM a) -> PPM a
 withMemoVar global_p idx f =
-  do memo_var <- ppNextMemoVar <$> ask
-     local (\s -> add_to_table global_p memo_var s) (f memo_var)
-       where
-         add_to_table True v st =
-           st { ppNextMemoVar = v + 1,
-                ppGlobalMemoTable = IntMap.insert idx v (ppGlobalMemoTable st) }
-         add_to_table False v st =
-           st { ppNextMemoVar = v + 1,
-                ppLocalMemoTable = IntMap.insert idx v (ppLocalMemoTable st) }
+  do
+    memoVar <- asks ppNextMemoVar
+    memoSkips <- asks (ppNoInlineMemo . ppOpts)
+    idxSkips <- asks (ppNoInlineIdx . ppOpts)
+    case memoSkips of
+      -- Even if we must skip this memoization variable, we still want to
+      -- "pretend" we memoized by calling `updateMemoVar`, so that non-inlined
+      -- memoization identifiers are kept constant between two
+      -- otherwise-identical terms with differing inline strategies.
+      (skip:skips) 
+        | skip == memoVar -> local (updateMemoVar . addIdxSkip . setMemoSkips skips) (f Nothing)
+      _ 
+        | idx `Set.member` idxSkips -> f Nothing
+        | otherwise -> local (updateMemoVar . bind memoVar) (f (Just memoVar))
+  where
+    bind = if global_p then bindGlobal else bindLocal
+
+    bindGlobal memoVar PPState{ .. } =
+      PPState { ppGlobalMemoTable = IntMap.insert idx memoVar ppGlobalMemoTable, .. }
+
+    bindLocal memoVar PPState{ .. } =
+      PPState { ppLocalMemoTable = IntMap.insert idx memoVar ppLocalMemoTable, .. }
 
+    setMemoSkips memoSkips PPState{ ppOpts = PPOpts{ .. }, .. } =
+      PPState { ppOpts = PPOpts { ppNoInlineMemo = memoSkips, ..}, ..}
+
+    addIdxSkip PPState{ ppOpts = PPOpts{ .. }, .. } =
+      PPState { ppOpts = PPOpts { ppNoInlineIdx = Set.insert idx ppNoInlineIdx, .. }, .. }
+
+    updateMemoVar PPState{ .. } =
+      PPState { ppNextMemoVar = ppNextMemoVar + 1, .. }
 
 --------------------------------------------------------------------------------
 -- * The Pretty-Printing of Specific Constructs
@@ -664,9 +692,11 @@ ppLets global_p ((idx, (t_rhs,_)):idxs) bindings baseDoc =
   do isBound <- isJust <$> memoLookupM idx
      if isBound then ppLets global_p idxs bindings baseDoc else
        do doc_rhs <- ppTerm' PrecTerm t_rhs
-          withMemoVar global_p idx $ \memo_var ->
-            ppLets global_p idxs ((memo_var, doc_rhs):bindings) baseDoc
-
+          withMemoVar global_p idx $ \memoVarM ->
+            let bindings' = case memoVarM of 
+                  Just memoVar -> (memoVar, doc_rhs):bindings
+                  Nothing -> bindings
+            in  ppLets global_p idxs bindings' baseDoc
 
 -- | Pretty-print a term inside a binder for a variable of the given name,
 -- returning both the result of pretty-printing and the fresh name actually used

src/SAWScript/Builtins.hs

@@ -36,7 +36,7 @@ import qualified Data.ByteString.Lazy as BS
 import qualified Data.ByteString.Lazy.UTF8 as B
 import qualified Data.IntMap as IntMap
 import Data.IORef
-import Data.List (isPrefixOf, isInfixOf)
+import Data.List (isPrefixOf, isInfixOf, sort)
 import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
 import Data.Set (Set)
@@ -463,6 +463,21 @@ print_goal =
      let output = prettySequent opts nenv (goalSequent goal)
      printOutLnTop Info (unlines [goalSummary goal, output])
 
+-- | Print the current goal that a proof script is attempting to prove, without
+-- generating @let@ bindings for the provided indices. For example,
+-- @print_goal_inline [1,9,3]@ will print the goal without inlining the
+-- variables that would otherwise be abstracted as @x\@1@, @x\@9@, and @x\@3@.
+print_goal_inline :: [Int] -> ProofScript ()
+print_goal_inline noInline =
+  execTactic $ tacticId $ \goal ->
+    do
+      opts <- getTopLevelPPOpts
+      let opts' = opts { ppNoInlineMemo = sort noInline } 
+      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

@@ -1848,6 +1848,17 @@ primitives = Map.fromList
     (pureVal print_goal)
     Current
     [ "Print the current goal that a proof script is attempting to prove." ]
+  , prim "print_goal_inline"   "[Int] -> ProofScript ()"
+    (pureVal print_goal_inline)
+    Current
+    [ "Print the current goal that a proof script is attempting to prove,"
+    , "without generating `let` bindings for the provided indices. For"
+    , "example, `print_goal_inline [1,9,3]` will print the goal without"
+    , "inlining the variables that would otherwise be abstracted as `x@1`,"
+    , " `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."
+    ]
   , prim "write_goal" "String -> ProofScript ()"
     (pureVal write_goal)
     Current