WIP, add a proof script version of subshell

saw/Main.hs

@@ -43,12 +43,13 @@ main = do
         [] -> checkZ3 opts'' *> REPL.run opts''
         _ | runInteractively opts'' -> checkZ3 opts'' *> REPL.run opts''
         [file] -> checkZ3 opts'' *>
-          processFile (AIGProxy AIG.compactProxy) opts'' file subsh `catch`
+          processFile (AIGProxy AIG.compactProxy) opts'' file subsh proofSubsh`catch`
           (\(ErrorCall msg) -> err opts'' msg)
         (_:_) -> err opts'' "Multiple files not yet supported."
     (_, _, errs) -> do hPutStrLn stderr (concat errs ++ usageInfo header options)
                        exitProofUnknown
   where subsh = Just (REPL.subshell (REPL.replBody Nothing (return ())))
+        proofSubsh = Just (REPL.proof_subshell (REPL.replBody Nothing (return ())))
         header = "Usage: saw [OPTION...] [-I | file]"
         checkZ3 opts = do
           p <- findExecutable "z3"

saw/SAWScript/REPL/Command.hs

@@ -221,7 +221,11 @@ sawScriptCmd str = do
   let tokens = SAWScript.Lexer.lexSAW replFileName str
   case SAWScript.Parser.parseStmtSemi tokens of
     Left err -> io $ print err
-    Right stmt -> void $ liftTopLevel (interpretStmt True stmt)
+    Right stmt ->
+      do mr <- getProofStateRef
+         case mr of
+           Nothing -> void $ liftTopLevel (interpretStmt True stmt)
+           Just r  -> void $ liftProofScript (interpretStmt True stmt) r
 
 replFileName :: String
 replFileName = "<stdin>"

saw/SAWScript/REPL/Monad.hs

@@ -22,7 +22,9 @@ module SAWScript.REPL.Monad (
   , catchOther
   , exceptionProtect
   , liftTopLevel
+  , liftProofScript
   , subshell
+  , proof_subshell
   , Refs(..)
 
     -- ** Errors
@@ -50,6 +52,7 @@ module SAWScript.REPL.Monad (
   , getValueEnvironment
   , getEnvironment, modifyEnvironment, putEnvironment
   , getEnvironmentRef
+  , getProofStateRef
   , getSAWScriptNames
   ) where
 
@@ -69,7 +72,8 @@ import Control.Applicative (Applicative(..), pure, (<*>))
 #endif
 import Control.Monad (unless, ap, void)
 import Control.Monad.Reader (ask)
-import Control.Monad.State (put, get)
+import Control.Monad.State (put, get, StateT(..))
+import Control.Monad.Except (ExceptT(..), runExceptT)
 import Control.Monad.IO.Class (liftIO)
 import qualified Control.Monad.Fail as Fail
 import Data.IORef (IORef, newIORef, readIORef, modifyIORef, writeIORef)
@@ -91,9 +95,13 @@ import qualified Data.AIG.CompactGraph as AIG
 import SAWScript.AST (Located(getVal))
 import SAWScript.Interpreter (buildTopLevelEnv)
 import SAWScript.Options (Options)
+import SAWScript.Proof (ProofState, ProofResult(..))
 import SAWScript.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..), runTopLevel,
                             makeCheckpoint, restoreCheckpoint)
-import SAWScript.Value (AIGProxy(..), mergeLocalEnv, IsValue, Value)
+import SAWScript.Value
+  ( AIGProxy(..), mergeLocalEnv, IsValue, Value
+  , ProofScript(..), showsProofResult, toValue
+  )
 import Verifier.SAW (SharedContext)
 
 deriving instance Typeable AIG.Proxy
@@ -106,6 +114,7 @@ data Refs = Refs
   , eIsBatch    :: Bool
   , eTopLevelRO :: TopLevelRO
   , environment :: IORef TopLevelRW
+  , proofState  :: Maybe (IORef ProofState)
   }
 
 -- | Initial, empty environment.
@@ -119,6 +128,7 @@ defaultRefs isBatch opts =
        , eIsBatch    = isBatch
        , eTopLevelRO = ro
        , environment = rwRef
+       , proofState  = Nothing
        }
 
 -- | Build up the prompt for the REPL.
@@ -154,11 +164,33 @@ subshell (REPL m) = TopLevel_ $
                      , eIsBatch  = False
                      , eTopLevelRO = ro
                      , environment = rwRef
+                     , proofState  = Nothing
                      }
           m refs
           readIORef rwRef
      put rw'
 
+proof_subshell :: REPL () -> ProofScript ()
+proof_subshell (REPL m) =
+  ProofScript $ ExceptT $ StateT $ \proofSt ->
+  do ro <- ask
+     rw <- get
+     (rw', outProofSt) <- liftIO $
+       do contRef <- newIORef True
+          rwRef <- newIORef rw
+          proofRef <- newIORef proofSt
+          let refs = Refs
+                     { eContinue = contRef
+                     , eIsBatch  = False
+                     , eTopLevelRO = ro
+                     , environment = rwRef
+                     , proofState  = Just proofRef
+                     }
+          m refs
+          (,) <$> readIORef rwRef <*> readIORef proofRef
+     put rw'
+     return (Right (), outProofSt)
+
 instance Functor REPL where
   {-# INLINE fmap #-}
   fmap f m = REPL (\ ref -> fmap f (unREPL m ref))
@@ -292,6 +324,18 @@ liftTopLevel m =
              writeIORef ref rw'
              return v
 
+liftProofScript :: IsValue a => ProofScript a -> IORef ProofState -> REPL Value
+liftProofScript m ref =
+  liftTopLevel $
+  do st <- liftIO $ readIORef ref
+     (res, st') <- runStateT (runExceptT (unProofScript m)) st
+     liftIO $ writeIORef ref st'
+     case res of
+       Left (stats, cex) ->
+         do ppOpts <- rwPPOpts <$> get
+            fail (showsProofResult ppOpts (InvalidProof stats cex st') "")
+       Right x -> return (toValue x)
+
 -- Primitives ------------------------------------------------------------------
 
 io :: IO a -> REPL a
@@ -420,6 +464,9 @@ getTopLevelRO = REPL (return . eTopLevelRO)
 getEnvironmentRef :: REPL (IORef TopLevelRW)
 getEnvironmentRef = environment <$> getRefs
 
+getProofStateRef :: REPL (Maybe (IORef ProofState))
+getProofStateRef = proofState <$> getRefs
+
 getEnvironment :: REPL TopLevelRW
 getEnvironment = readRef environment
 
@@ -449,4 +496,3 @@ data EnvVal
   | EnvNum    !Int
   | EnvBool   Bool
     deriving (Show)
-

src/SAWScript/Interpreter.hs

@@ -15,6 +15,7 @@ Stability   : provisional
 {-# LANGUAGE OverlappingInstances #-}
 #endif
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE ViewPatterns #-}
@@ -26,6 +27,7 @@ module SAWScript.Interpreter
   , processFile
   , buildTopLevelEnv
   , primDocEnv
+  , InteractiveMonad(..)
   )
   where
 
@@ -262,34 +264,40 @@ stmtInterpreter :: StmtInterpreter
 stmtInterpreter ro rw stmts =
   fst <$> runTopLevel (withLocalEnv emptyLocal (interpretStmts stmts)) ro rw
 
-processStmtBind :: Bool -> SS.Pattern -> Maybe SS.Type -> SS.Expr -> TopLevel ()
+processStmtBind ::
+  InteractiveMonad m =>
+  Bool ->
+  SS.Pattern ->
+  Maybe SS.Type ->
+  SS.Expr ->
+  m ()
 processStmtBind printBinds pat _mc expr = do -- mx mt
   let (mx, mt) = case pat of
         SS.PWild t -> (Nothing, t)
         SS.PVar x t -> (Just x, t)
         _ -> (Nothing, Nothing)
   let it = SS.Located "it" "it" SS.PosREPL
   let lname = maybe it id mx
-  let ctx = SS.tContext SS.TopLevel
+  ctx <- SS.tContext <$> getMonadContext
   let expr' = case mt of
                 Nothing -> expr
                 Just t -> SS.TSig expr (SS.tBlock ctx t)
   let decl = SS.Decl (SS.getPos expr) pat Nothing expr'
-  rw <- getMergedEnv
+  rw <- liftTopLevel getMergedEnv
   let opts = rwPPOpts rw
 
-  ~(SS.Decl _ _ (Just schema) expr'') <-
+  ~(SS.Decl _ _ (Just schema) expr'') <- liftTopLevel $
     either failTypecheck return $ checkDecl (rwTypes rw) (rwTypedef rw) decl
 
-  val <- interpret expr''
+  val <- liftTopLevel $ interpret expr''
 
   -- Run the resulting TopLevel action.
   (result, ty) <-
     case schema of
       SS.Forall [] t ->
         case t of
           SS.TyCon SS.BlockCon [c, t'] | c == ctx -> do
-            result <- SAWScript.Value.fromValue val
+            result <- actionFromValue val
             return (result, t')
           _ -> return (val, t)
       _ -> fail $ "Not a monomorphic type: " ++ SS.pShow schema
@@ -299,39 +307,70 @@ processStmtBind printBinds pat _mc expr = do -- mx mt
   -- Print non-unit result if it was not bound to a variable
   case pat of
     SS.PWild _ | printBinds && not (isVUnit result) ->
-      printOutLnTop Info (showsPrecValue opts 0 result "")
+      liftTopLevel $ printOutLnTop Info (showsPrecValue opts 0 result "")
     _ -> return ()
 
   -- Print function type if result was a function
   case ty of
-    SS.TyCon SS.FunCon _ -> printOutLnTop Info $ getVal lname ++ " : " ++ SS.pShow ty
+    SS.TyCon SS.FunCon _ ->
+      liftTopLevel $ printOutLnTop Info $ getVal lname ++ " : " ++ SS.pShow ty
     _ -> return ()
 
-  rw' <- getTopLevelRW
-  putTopLevelRW =<< bindPatternEnv pat (Just (SS.tMono ty)) result rw'
+  liftTopLevel $
+   do rw' <- getTopLevelRW
+      putTopLevelRW =<< bindPatternEnv pat (Just (SS.tMono ty)) result rw'
+
+
+class (Monad m, MonadFail m) => InteractiveMonad m where
+  liftTopLevel :: TopLevel a -> m a
+  withTopLevel :: (forall b. TopLevel b -> TopLevel b) -> m a -> m a
+  actionFromValue :: FromValue a => Value -> m a
+  getMonadContext :: m SS.Context
+
+instance InteractiveMonad TopLevel where
+  liftTopLevel m = m
+  withTopLevel f m = f m
+  actionFromValue = fromValue
+  getMonadContext = return SS.TopLevel
+
+instance InteractiveMonad ProofScript where
+  liftTopLevel m = scriptTopLevel m
+  withTopLevel f (ProofScript m) = ProofScript (underExceptT (underStateT f) m)
+  actionFromValue = fromValue
+  getMonadContext = return SS.ProofScript
 
 -- | Interpret a block-level statement in the TopLevel monad.
-interpretStmt ::
+interpretStmt :: InteractiveMonad m =>
   Bool {-^ whether to print non-unit result values -} ->
   SS.Stmt ->
-  TopLevel ()
+  m ()
 interpretStmt printBinds stmt =
   let ?fileReader = BS.readFile in
   case stmt of
-    SS.StmtBind pos pat mc expr -> withPosition pos (processStmtBind printBinds pat mc expr)
-    SS.StmtLet _ dg           -> do rw <- getTopLevelRW
-                                    dg' <- either failTypecheck return $
-                                           checkDeclGroup (rwTypes rw) (rwTypedef rw) dg
-                                    env <- interpretDeclGroup dg'
-                                    withLocalEnv env getMergedEnv >>= putTopLevelRW
-    SS.StmtCode _ lstr        -> do rw <- getTopLevelRW
-                                    sc <- getSharedContext
-                                    --io $ putStrLn $ "Processing toplevel code: " ++ show lstr
-                                    --showCryptolEnv
-                                    cenv' <- io $ CEnv.parseDecls sc (rwCryptol rw) $ locToInput lstr
-                                    putTopLevelRW $ rw { rwCryptol = cenv' }
-                                    --showCryptolEnv
+
+    SS.StmtBind pos pat mc expr ->
+      withTopLevel (withPosition pos) (processStmtBind printBinds pat mc expr)
+
+    SS.StmtLet _ dg           ->
+      liftTopLevel $
+      do rw <- getTopLevelRW
+         dg' <- either failTypecheck return $
+                checkDeclGroup (rwTypes rw) (rwTypedef rw) dg
+         env <- interpretDeclGroup dg'
+         withLocalEnv env getMergedEnv >>= putTopLevelRW
+
+    SS.StmtCode _ lstr ->
+      liftTopLevel $
+      do rw <- getTopLevelRW
+         sc <- getSharedContext
+         --io $ putStrLn $ "Processing toplevel code: " ++ show lstr
+         --showCryptolEnv
+         cenv' <- io $ CEnv.parseDecls sc (rwCryptol rw) $ locToInput lstr
+         putTopLevelRW $ rw { rwCryptol = cenv' }
+         --showCryptolEnv
+
     SS.StmtImport _ imp ->
+      liftTopLevel $
       do rw <- getTopLevelRW
          sc <- getSharedContext
          --showCryptolEnv
@@ -342,8 +381,10 @@ interpretStmt printBinds stmt =
          putTopLevelRW $ rw { rwCryptol = cenv' }
          --showCryptolEnv
 
-    SS.StmtTypedef _ name ty   -> do rw <- getTopLevelRW
-                                     putTopLevelRW $ addTypedef (getVal name) ty rw
+    SS.StmtTypedef _ name ty ->
+      liftTopLevel $
+      do rw <- getTopLevelRW
+         putTopLevelRW $ addTypedef (getVal name) ty rw
 
 interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel ()
 interpretFile file runMain = do
@@ -414,6 +455,7 @@ buildTopLevelEnv proxy opts =
                    , roBasicSS = ss
                    , roStackTrace = []
                    , roSubshell = fail "Subshells not supported"
+                   , roProofSubshell = fail "Proof subshells not supported"
                    , roLocalEnv = []
                    }
        let bic = BuiltinContext {
@@ -464,16 +506,20 @@ processFile ::
   Options ->
   FilePath ->
   Maybe (TopLevel ()) ->
+  Maybe (ProofScript ()) ->
   IO ()
-processFile proxy opts file mbSubshell = do
+processFile proxy opts file mbSubshell mbProofSubshell = do
   (_, ro, rw) <- buildTopLevelEnv proxy opts
   let ro' = case mbSubshell of
               Nothing -> ro
               Just m  -> ro{ roSubshell = m }
+  let ro'' = case mbProofSubshell of
+              Nothing -> ro'
+              Just m  -> ro'{ roProofSubshell = m }
   oldpath <- getCurrentDirectory
   file' <- canonicalizePath file
   setCurrentDirectory (takeDirectory file')
-  _ <- runTopLevel (interpretFile file' True) ro' rw
+  _ <- runTopLevel (interpretFile file' True) ro'' rw
             `X.catch` (handleException opts)
   setCurrentDirectory oldpath
   return ()
@@ -817,6 +863,11 @@ primitives = Map.fromList
     Experimental
     []
 
+  , prim "proof_subshell"      "() -> ProofScript ()"
+    (\ _ _ -> proofScriptSubshell)
+    Experimental
+    []
+
   , prim "define"              "String -> Term -> TopLevel Term"
     (pureVal definePrim)
     Current