From e7530a4270563a9a1e8942bdceabb4d3d050a6f0 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Thu, 5 Jan 2023 15:40:25 -0800 Subject: [PATCH 1/9] PoC: a command for printing goals with inlined `let`s --- saw-core/src/Verifier/SAW/Term/Pretty.hs | 45 +++++++++++++++++------- src/SAWScript/Builtins.hs | 13 ++++++- src/SAWScript/Interpreter.hs | 9 +++++ 3 files changed, 54 insertions(+), 13 deletions(-) diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index f574da49b3..d70e9a3135 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/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 @@ -293,18 +298,33 @@ withBoundVarM basename m = -- 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 +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 + (skip:_) | skip == memoVar -> local (updateMemoVar . addIdxSkip . removeMemoSkip) (f Nothing) + _ | idx `Set.member` idxSkips -> f Nothing + _ -> 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, .. } + + removeMemoSkip PPState{ ppOpts = PPOpts{ .. }, .. } = + PPState { ppOpts = PPOpts { ppNoInlineMemo = tail ppNoInlineMemo, .. }, .. } + + 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,8 +684,9 @@ 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 $ \case + Just memo_var -> ppLets global_p idxs ((memo_var, doc_rhs):bindings) baseDoc + Nothing -> ppLets global_p idxs bindings baseDoc -- | Pretty-print a term inside a binder for a variable of the given name, diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 6bd35e14e9..be2bd8aa29 100644 --- a/src/SAWScript/Builtins.hs +++ b/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,17 @@ print_goal = let output = prettySequent opts nenv (goalSequent goal) printOutLnTop Info (unlines [goalSummary goal, output]) +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 -> diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index cf4436979c..a26934457b 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1824,6 +1824,15 @@ 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) + Experimental + [ "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`." + ] , prim "write_goal" "String -> ProofScript ()" (pureVal write_goal) Current From 71bf9468def0d2f49ac527227886519bb0d4cb57 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Thu, 5 Jan 2023 15:56:20 -0800 Subject: [PATCH 2/9] Update docs --- saw-core/src/Verifier/SAW/Term/Pretty.hs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index d70e9a3135..9c7166bc01 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -294,10 +294,12 @@ 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. +-- | 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 @@ -305,6 +307,10 @@ withMemoVar global_p idx f = 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:_) | skip == memoVar -> local (updateMemoVar . addIdxSkip . removeMemoSkip) (f Nothing) _ | idx `Set.member` idxSkips -> f Nothing _ -> local (updateMemoVar . bind memoVar) (f (Just memoVar)) From ec89833bcb8c8e2edba8ce6446b98072ffb4643f Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Thu, 9 Feb 2023 08:58:01 -0800 Subject: [PATCH 3/9] 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 From ec6cac353c09ef9824763f6a0cc497942da331aa Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Fri, 3 Mar 2023 11:22:01 -0800 Subject: [PATCH 4/9] Revert "Try inlining by term string" This reverts commit ec89833bcb8c8e2edba8ce6446b98072ffb4643f. --- src/SAWScript/Builtins.hs | 13 ------------- src/SAWScript/Interpreter.hs | 8 -------- 2 files changed, 21 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 03a175bd02..d1d46152a6 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -474,19 +474,6 @@ 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 41e28274d9..d77673eabe 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1833,14 +1833,6 @@ 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 From 68a647eb0c67a6f94ea34b0ad18a80bd9a62c71e Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Thu, 9 Mar 2023 08:37:46 -0800 Subject: [PATCH 5/9] Haddock --- src/SAWScript/Builtins.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index d1d46152a6..50cf2a5e45 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -463,6 +463,10 @@ 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 -> From 0f8a539d8b31b830476b78ae0a5801e8b925fb8e Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Thu, 9 Mar 2023 08:38:02 -0800 Subject: [PATCH 6/9] Make `print_goal_inline` non-experimental --- src/SAWScript/Interpreter.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index d77673eabe..0a449fdcf5 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1826,7 +1826,7 @@ primitives = Map.fromList [ "Print the current goal that a proof script is attempting to prove." ] , prim "print_goal_inline" "[Int] -> ProofScript ()" (pureVal print_goal_inline) - Experimental + 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" From 3a71946f4e3f8730b04afc8e132e889366ecbd61 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Tue, 16 May 2023 09:49:33 -0700 Subject: [PATCH 7/9] Alert users to fragility of memoization indices --- src/SAWScript/Interpreter.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 05870a5eaa..4b8017ae34 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1849,7 +1849,9 @@ primitives = Map.fromList , "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`." + , " `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) From 04b7f9e077722f80cb6928c633f4a05fb9588e6c Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Tue, 16 May 2023 09:57:14 -0700 Subject: [PATCH 8/9] Simplify memoization casing --- saw-core/src/Verifier/SAW/Term/Pretty.hs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index b4e5dbbce0..3705259cd2 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -690,10 +690,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 $ \case - Just memo_var -> ppLets global_p idxs ((memo_var, doc_rhs):bindings) baseDoc - Nothing -> ppLets global_p idxs 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 From 2ec0016f050b891705084c35383070ce2d740fe2 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Tue, 16 May 2023 09:57:53 -0700 Subject: [PATCH 9/9] Remove `tail` --- saw-core/src/Verifier/SAW/Term/Pretty.hs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index 3705259cd2..6f82c44cea 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -311,9 +311,11 @@ withMemoVar global_p idx f = -- "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:_) | skip == memoVar -> local (updateMemoVar . addIdxSkip . removeMemoSkip) (f Nothing) - _ | idx `Set.member` idxSkips -> f Nothing - _ -> local (updateMemoVar . bind memoVar) (f (Just memoVar)) + (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 @@ -323,8 +325,8 @@ withMemoVar global_p idx f = bindLocal memoVar PPState{ .. } = PPState { ppLocalMemoTable = IntMap.insert idx memoVar ppLocalMemoTable, .. } - removeMemoSkip PPState{ ppOpts = PPOpts{ .. }, .. } = - PPState { ppOpts = PPOpts { ppNoInlineMemo = tail ppNoInlineMemo, .. }, .. } + setMemoSkips memoSkips PPState{ ppOpts = PPOpts{ .. }, .. } = + PPState { ppOpts = PPOpts { ppNoInlineMemo = memoSkips, ..}, ..} addIdxSkip PPState{ ppOpts = PPOpts{ .. }, .. } = PPState { ppOpts = PPOpts { ppNoInlineIdx = Set.insert idx ppNoInlineIdx, .. }, .. }