From 0907c55850a36328096a3eb6fa73325fe8c790b2 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 25 Jul 2022 12:44:45 -0700 Subject: [PATCH] Add a `proof_checkpoint` command that captures and allows the user to restore proof states. --- src/SAWScript/Interpreter.hs | 14 ++++++++++++++ src/SAWScript/Value.hs | 9 +++++++++ 2 files changed, 23 insertions(+) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 57404c920a..b8497e09f5 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -896,6 +896,20 @@ primitives = Map.fromList , "subshell and resume execution." ] + , prim "proof_checkpoint" "ProofScript (() -> ProofScript ())" + (pureVal proof_checkpoint) + Experimental + [ "Capture the current state of the proof and return a" + , "ProofScript monadic action that, if invoked, will reset the" + , "state of the proof back to to what it was at the" + , "moment checkpoint was invoked." + , "" + , "NOTE that this facility is highly experimental and may not" + , "be entirely reliable. It is intended only for proof development" + , "where it can speed up the process of experimenting with" + , "mid-proof changes. Finalized proofs should not use this facility." + ] + , prim "define" "String -> Term -> TopLevel Term" (pureVal definePrim) Current diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index d041f08770..3ea01878f6 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -624,6 +624,15 @@ checkpoint = TopLevel_ $ do printOutLnTop Info "Restoring state from checkpoint" restoreCheckpoint chk +-- | Capture the current proof state and return an +-- action that, if invoked, resets the state back to that point. +proof_checkpoint :: ProofScript (() -> ProofScript ()) +proof_checkpoint = + do ps <- get + return $ \_ -> + do scriptTopLevel (printOutLnTop Info "Restoring proof state from checkpoint") + put ps + throwTopLevel :: String -> TopLevel a throwTopLevel msg = do pos <- getPosition