Add a proof_checkpoint command that captures and

allows the user to restore proof states.

Author: robdockins

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

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