Merge pull request #1128 from GaloisInc/persist-solver2

Persist solver, part 2

cryptol-remote-api/cryptol-eval-server/Main.hs

@@ -21,10 +21,9 @@ import Options.Applicative
 import CryptolServer.ClearState
     ( clearState, clearStateDescr, clearAllStates, clearAllStatesDescr)
 import Cryptol.Eval (EvalOpts(..), defaultPPOpts)
-import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName, meSolverConfig)
+import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName)
 import Cryptol.ModuleSystem.Monad (runModuleM, setFocusedModule)
 import Cryptol.TypeCheck.AST (mName)
-import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import Cryptol.Utils.Ident (ModName, modNameToText, textToModName, preludeName)
 import Cryptol.Utils.Logger (quietLogger)
 
@@ -34,7 +33,7 @@ import qualified Argo.Doc as Doc
 
 
 import CryptolServer
-    ( ServerState, moduleEnv, initialState, setSearchPath, command, notification )
+    ( ServerState, moduleEnv, tcSolver, initialState, setSearchPath, command, notification )
 import CryptolServer.Call ( call )
 import CryptolServer.EvalExpr
     ( evalExpressionDescr, evalExpression )
@@ -58,19 +57,20 @@ main = customMain initMod initMod initMod initMod description buildApp
     startingState (StartingFile file) reader =
       do paths <- getSearchPaths
          initSt <- setSearchPath paths <$> initialState
+         let s    = view tcSolver initSt
          let menv = view moduleEnv initSt
-         let minp s = ModuleInput False (pure evOpts) reader menv s
+         let minp = ModuleInput False (pure evOpts) reader menv s
          let die =
                \err ->
                  do hPutStrLn stderr $ "Failed to load " ++ either ("file " ++) (("module " ++) . show) file ++ ":\n" ++ show err
                     exitFailure
-         menv' <- SMT.withSolver (meSolverConfig menv) $ \s ->
-           do (res, _warnings) <- either loadModuleByPath loadModuleByName file (minp s)
+         menv' <-
+           do (res, _warnings) <- either loadModuleByPath loadModuleByName file minp
               -- NB Warnings suppressed when running server
               case res of
                 Left err -> die err
                 Right (m, menv') ->
-                  do res' <- fst <$> runModuleM (minp s){ minpModuleEnv = menv' } (setFocusedModule (mName (snd m)))
+                  do res' <- fst <$> runModuleM minp{ minpModuleEnv = menv' } (setFocusedModule (mName (snd m)))
                      case res' of
                        Left err -> die err
                        Right (_, menv'') -> pure menv''

cryptol-remote-api/src/CryptolServer.hs

@@ -15,9 +15,10 @@ import Cryptol.Eval (EvalOpts(..))
 import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv, ModuleInput(..))
 import Cryptol.ModuleSystem.Env
   (getLoadedModules, lmFilePath, lmFingerprint, meLoadedModules,
-   initialModuleEnv, meSearchPath, ModulePath(..), meSolverConfig)
+   initialModuleEnv, meSearchPath, ModulePath(..))
 import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile )
 import Cryptol.Parser.AST (ModName)
+import Cryptol.TypeCheck( SolverConfig(..) )
 import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 
 import qualified Argo
@@ -71,6 +72,8 @@ instance CryptolMethod CryptolNotification where
 getModuleEnv :: CryptolCommand ModuleEnv
 getModuleEnv = CryptolCommand $ const $ view moduleEnv <$> Argo.getState
 
+getTCSolver :: CryptolCommand SMT.Solver
+getTCSolver = CryptolCommand $ const $ view tcSolver <$> Argo.getState
 
 setModuleEnv :: ModuleEnv -> CryptolCommand ()
 setModuleEnv me =
@@ -81,15 +84,14 @@ runModuleCmd cmd =
     do Options callStacks evOpts <- getOptions
        s <- CryptolCommand $ const Argo.getState
        reader <- CryptolCommand $ const Argo.getFileReader
-       let minp solver = ModuleInput
+       let minp = ModuleInput
                   { minpCallStacks = callStacks
                   , minpEvalOpts   = pure evOpts
                   , minpByteReader = reader
                   , minpModuleEnv  = view moduleEnv s
-                  , minpTCSolver = solver
+                  , minpTCSolver   = view tcSolver s
                   }
-       let solverCfg = meSolverConfig (view moduleEnv s)
-       out <- liftIO $ SMT.withSolver solverCfg (cmd . minp)
+       out <- liftIO (cmd minp)
        case out of
          (Left x, warns) ->
            raise (cryptolError x warns)
@@ -114,6 +116,7 @@ loadedPath = lens _loadedPath (\v n -> v { _loadedPath = n })
 data ServerState =
   ServerState { _loadedModule :: Maybe LoadedModule
               , _moduleEnv :: ModuleEnv
+              , _tcSolver :: SMT.Solver
               }
 
 loadedModule :: Lens' ServerState (Maybe LoadedModule)
@@ -122,8 +125,23 @@ loadedModule = lens _loadedModule (\v n -> v { _loadedModule = n })
 moduleEnv :: Lens' ServerState ModuleEnv
 moduleEnv = lens _moduleEnv (\v n -> v { _moduleEnv = n })
 
+tcSolver :: Lens' ServerState SMT.Solver
+tcSolver = lens _tcSolver (\v n -> v { _tcSolver = n })
+
 initialState :: IO ServerState
-initialState = ServerState Nothing <$> initialModuleEnv
+initialState =
+  do modEnv <- initialModuleEnv
+     s <- SMT.startSolver (defaultSolverConfig (meSearchPath modEnv))
+     pure (ServerState Nothing modEnv s)
+
+defaultSolverConfig :: [FilePath] -> SolverConfig
+defaultSolverConfig searchPath =
+  SolverConfig
+  { solverPath = "z3"
+  , solverArgs = [ "-smt2", "-in" ]
+  , solverVerbose = 0
+  , solverPreludePath = searchPath
+  }
 
 setSearchPath :: [FilePath] -> ServerState -> ServerState
 setSearchPath paths =

cryptol-remote-api/src/CryptolServer/EvalExpr.hs

@@ -12,13 +12,12 @@ import Data.Aeson as JSON
 
 
 import Cryptol.ModuleSystem (checkExpr, evalExpr)
-import Cryptol.ModuleSystem.Env (meSolverConfig,deEnv,meDynEnv)
+import Cryptol.ModuleSystem.Env (deEnv,meDynEnv)
 import Cryptol.TypeCheck.Solve (defaultReplExpr)
 import Cryptol.TypeCheck.Subst (apSubst, listParamSubst)
 import Cryptol.TypeCheck.Type (Schema(..))
 import qualified Cryptol.Parser.AST as P
 import Cryptol.Parser.Name (PName)
-import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import Cryptol.Utils.PP (pretty)
 import qualified Cryptol.Eval.Env as E
 import qualified Cryptol.Eval.Type as E
@@ -43,9 +42,8 @@ evalExpression' e =
      -- TODO: see Cryptol REPL for how to check whether we
      -- can actually evaluate things, which we can't do in
      -- a parameterized module
-     me <- getModuleEnv
-     let cfg = meSolverConfig me
-     perhapsDef <- liftIO $ SMT.withSolver cfg (\s -> defaultReplExpr s ty schema)
+     s <- getTCSolver
+     perhapsDef <- liftIO (defaultReplExpr s ty schema)
      case perhapsDef of
        Nothing ->
          raise (evalPolyErr schema)

cryptol-remote-api/src/CryptolServer/Sat.hs

@@ -23,13 +23,12 @@ import qualified Data.Text as T
 import Cryptol.Eval.Concrete (Value)
 import Cryptol.Eval.Type (TValue, tValTy)
 import Cryptol.ModuleSystem (checkExpr)
-import Cryptol.ModuleSystem.Env (DynamicEnv(..), meDynEnv, meSolverConfig)
+import Cryptol.ModuleSystem.Env (DynamicEnv(..), meDynEnv)
 import Cryptol.Symbolic ( ProverCommand(..), ProverResult(..), QueryType(..)
                         , SatNum(..), CounterExampleType(..))
 import Cryptol.Symbolic.SBV (proverNames, satProve, setupProver)
 import Cryptol.TypeCheck.AST (Expr)
 import Cryptol.TypeCheck.Solve (defaultReplExpr)
-import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 
 import CryptolServer
 import CryptolServer.Exceptions (evalPolyErr, proverError)
@@ -49,8 +48,9 @@ proveSat (ProveSatParams queryType (Prover name) jsonExpr) =
      -- TODO validEvalContext expr, ty, schema
      me <- getModuleEnv
      let decls = deDecls (meDynEnv me)
-     let cfg = meSolverConfig me
-     perhapsDef <- liftIO $ SMT.withSolver cfg (\s -> defaultReplExpr s ty schema)
+     s <- getTCSolver
+
+     perhapsDef <- liftIO (defaultReplExpr s ty schema)
      case perhapsDef of
        Nothing ->
          raise (evalPolyErr schema)

cryptol-remote-api/src/CryptolServer/TypeCheck.hs

@@ -11,7 +11,6 @@ import qualified Argo.Doc as Doc
 import Data.Aeson as JSON
 
 import Cryptol.ModuleSystem (checkExpr)
-import Cryptol.ModuleSystem.Env (meSolverConfig)
 
 import CryptolServer
 import CryptolServer.Exceptions
@@ -26,8 +25,6 @@ checkType :: TypeCheckParams -> CryptolCommand JSON.Value
 checkType (TypeCheckParams e) =
   do e' <- getExpr e
      (_expr, _ty, schema) <- runModuleCmd (checkExpr e')
-     -- FIXME: why are we running this command if the result isn't used?
-     _cfg <- meSolverConfig <$> getModuleEnv
      return (JSON.object [ "type schema" .= JSONSchema schema ])
   where
     -- FIXME: Why is this check not being used?

src/Cryptol/ModuleSystem/Base.hs

@@ -532,7 +532,6 @@ genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM T.Infe
 genInferInput r prims params env = do
   seeds <- getNameSeeds
   monoBinds <- getMonoBinds
-  cfg <- getSolverConfig
   solver <- getTCSolver
   supply <- getSupply
   searchPath <- getSearchPath
@@ -548,7 +547,6 @@ genInferInput r prims params env = do
     , T.inpNameSeeds = seeds
     , T.inpMonoBinds = monoBinds
     , T.inpCallStacks = callStacks
-    , T.inpSolverConfig = cfg
     , T.inpSearchPath = searchPath
     , T.inpSupply    = supply
     , T.inpPrimNames = prims

src/Cryptol/ModuleSystem/Env.hs

@@ -60,9 +60,6 @@ data ModuleEnv = ModuleEnv
   , meNameSeeds     :: T.NameSeeds
     -- ^ A source of new names for the type checker.
 
-  , meSolverConfig  :: T.SolverConfig
-    -- ^ Configuration settings for the SMT solver used for type-checking.
-
   , meEvalEnv       :: EvalEnv
     -- ^ The evaluation environment.  Contains the values for all loaded
     -- modules, both public and private.
@@ -150,12 +147,6 @@ initialModuleEnv = do
     , meSearchPath    = searchPath
     , meDynEnv        = mempty
     , meMonoBinds     = True
-    , meSolverConfig  = T.SolverConfig
-                          { T.solverPath = "z3"
-                          , T.solverArgs = [ "-smt2", "-in" ]
-                          , T.solverVerbose = 0
-                          , T.solverPreludePath = searchPath
-                          }
     , meCoreLint      = NoCoreLint
     , meSupply        = emptySupply
     }

src/Cryptol/ModuleSystem/Monad.hs

@@ -570,16 +570,6 @@ setDynEnv denv = ModuleT $ do
   me <- get
   set $! me { meDynEnv = denv }
 
-setSolver :: T.SolverConfig -> ModuleM ()
-setSolver cfg = ModuleT $ do
-  me <- get
-  set $! me { meSolverConfig = cfg }
-
-getSolverConfig :: ModuleM T.SolverConfig
-getSolverConfig  = ModuleT $ do
-  me <- get
-  return (meSolverConfig me)
-
 -- | Usefule for logging.  For example: @withLogger logPutStrLn "Hello"@
 withLogger :: (Logger -> a -> IO b) -> a -> ModuleM b
 withLogger f a = do l <- getEvalOpts

src/Cryptol/REPL/Command.hs

@@ -81,7 +81,6 @@ import qualified Cryptol.TypeCheck.Error as T
 import qualified Cryptol.TypeCheck.Parseable as T
 import qualified Cryptol.TypeCheck.Subst as T
 import           Cryptol.TypeCheck.Solve(defaultReplExpr)
-import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import           Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap)
 import           Cryptol.Utils.PP
 import           Cryptol.Utils.Panic(panic)
@@ -1648,16 +1647,16 @@ liftModuleCmd cmd =
   do evo <- getEvalOptsAction
      env <- getModuleEnv
      callStacks <- getCallStacks
-     let cfg = M.meSolverConfig env
-     let minp s =
+     tcSolver <- getTCSolver
+     let minp =
              M.ModuleInput
                 { minpCallStacks = callStacks
                 , minpEvalOpts   = evo
                 , minpByteReader = BS.readFile
                 , minpModuleEnv  = env
-                , minpTCSolver   = s
+                , minpTCSolver   = tcSolver
                 }
-     moduleCmdResult =<< io (SMT.withSolver cfg (cmd . minp))
+     moduleCmdResult =<< io (cmd minp)
 
 moduleCmdResult :: M.ModuleRes a -> REPL a
 moduleCmdResult (res,ws0) = do
@@ -1735,9 +1734,8 @@ replEvalCheckedExpr def sig =
   do validEvalContext def
      validEvalContext sig
 
-     me <- getModuleEnv
-     let cfg = M.meSolverConfig me
-     mbDef <- io $ SMT.withSolver cfg (\s -> defaultReplExpr s def sig)
+     s <- getTCSolver
+     mbDef <- io (defaultReplExpr s def sig)
 
      (def1,ty) <-
         case mbDef of