Persist solver instances across a longer lifetime.

The solver instance is now passed down into the typechecking
actions from outside rather than being created on each
invocation of a typechecking action.  Likewise, the solver
has been pulled out as a parameter of the `ModuleInput`
record that is passed into a `ModuleCmd`.

At present, these are still created fresh for each module command
inside `liftModuleCmd`.  However, it would be relatively easy
to continue this lifting process and persist the solver across
and entire REPL session.

The current refactoring should, I believe, be sufficent to address
GaloisInc/saw-script#953

Fixes #996

src/Cryptol/ModuleSystem/Base.hs

@@ -40,6 +40,7 @@ import qualified Cryptol.TypeCheck     as T
 import qualified Cryptol.TypeCheck.AST as T
 import qualified Cryptol.TypeCheck.PP as T
 import qualified Cryptol.TypeCheck.Sanity as TcSanity
+
 import Cryptol.Transform.AddModParams (addModParams)
 import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
                            , preludeReferenceName, interactiveName, modNameChunks
@@ -527,12 +528,12 @@ typecheck act i params env = do
          typeCheckingFailed nameMap errs
 
 -- | Generate input for the typechecker.
-genInferInput :: Range -> PrimMap ->
-                          IfaceParams -> IfaceDecls -> ModuleM T.InferInput
+genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM T.InferInput
 genInferInput r prims params env = do
   seeds <- getNameSeeds
   monoBinds <- getMonoBinds
   cfg <- getSolverConfig
+  solver <- getTCSolver
   supply <- getSupply
   searchPath <- getSearchPath
   callStacks <- getCallStacks
@@ -554,10 +555,10 @@ genInferInput r prims params env = do
     , T.inpParamTypes       = ifParamTypes params
     , T.inpParamConstraints = ifParamConstraints params
     , T.inpParamFuns        = ifParamFuns params
+    , T.inpSolver           = solver
     }
 
 
-
 -- Evaluation ------------------------------------------------------------------
 
 evalExpr :: T.Expr -> ModuleM Concrete.Value

src/Cryptol/ModuleSystem/Monad.hs

@@ -29,6 +29,8 @@ import qualified Cryptol.Parser.NoPat as NoPat
 import qualified Cryptol.Parser.NoInclude as NoInc
 import qualified Cryptol.TypeCheck as T
 import qualified Cryptol.TypeCheck.AST as T
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
+
 import           Cryptol.Parser.Position (Range)
 import           Cryptol.Utils.Ident (interactiveName, noModuleName)
 import           Cryptol.Utils.PP
@@ -304,6 +306,7 @@ data RO m =
      , roEvalOpts   :: m EvalOpts
      , roCallStacks :: Bool
      , roFileReader :: FilePath -> m ByteString
+     , roTCSolver   :: SMT.Solver
      }
 
 emptyRO :: ModuleInput m -> RO m
@@ -312,6 +315,7 @@ emptyRO minp =
      , roEvalOpts   = minpEvalOpts minp
      , roCallStacks = minpCallStacks minp
      , roFileReader = minpByteReader minp
+     , roTCSolver   = minpTCSolver minp
      }
 
 newtype ModuleT m a = ModuleT
@@ -364,6 +368,7 @@ data ModuleInput m =
   , minpEvalOpts   :: m EvalOpts
   , minpByteReader :: FilePath -> m ByteString
   , minpModuleEnv  :: ModuleEnv
+  , minpTCSolver   :: SMT.Solver
   }
 
 runModuleT ::
@@ -406,6 +411,9 @@ readBytes fn = do
 getModuleEnv :: Monad m => ModuleT m ModuleEnv
 getModuleEnv = ModuleT get
 
+getTCSolver :: Monad m => ModuleT m SMT.Solver
+getTCSolver = ModuleT (roTCSolver <$> ask)
+
 setModuleEnv :: Monad m => ModuleEnv -> ModuleT m ()
 setModuleEnv = ModuleT . set
 

src/Cryptol/REPL/Command.hs

@@ -1648,13 +1648,16 @@ liftModuleCmd cmd =
   do evo <- getEvalOptsAction
      env <- getModuleEnv
      callStacks <- getCallStacks
-     let minp = M.ModuleInput
+     let cfg = M.meSolverConfig env
+     let minp s =
+             M.ModuleInput
                 { minpCallStacks = callStacks
                 , minpEvalOpts   = evo
                 , minpByteReader = BS.readFile
                 , minpModuleEnv  = env
+                , minpTCSolver   = s
                 }
-     moduleCmdResult =<< io (cmd minp)
+     moduleCmdResult =<< io (SMT.withSolver cfg (cmd . minp))
 
 moduleCmdResult :: M.ModuleRes a -> REPL a
 moduleCmdResult (res,ws0) = do

src/Cryptol/TypeCheck.hs

@@ -52,6 +52,8 @@ import           Cryptol.Utils.Ident (exprModName,packIdent)
 import           Cryptol.Utils.PP
 import           Cryptol.Utils.Panic(panic)
 
+
+
 tcModule :: P.Module Name -> InferInput -> IO (InferOutput Module)
 tcModule m inp = runInferM inp (inferModule m)
 

src/Cryptol/TypeCheck/InferTypes.hs

@@ -47,6 +47,7 @@ data SolverConfig = SolverConfig
     -- ^ Look for the solver prelude in these locations.
   } deriving (Show, Generic, NFData)
 
+
 -- | The types of variables in the environment.
 data VarType = ExtVar Schema
                -- ^ Known type

src/Cryptol/TypeCheck/Monad.hs

@@ -85,8 +85,9 @@ data InferInput = InferInput
     -- identifier (e.g., @number@).
 
   , inpSupply :: !Supply              -- ^ The supply for fresh name generation
-  } deriving Show
 
+  , inpSolver :: SMT.Solver           -- ^ Solver connection for typechecking
+  }
 
 -- | This is used for generating various names.
 data NameSeeds = NameSeeds
@@ -116,7 +117,7 @@ bumpCounter = do RO { .. } <- IM ask
                  io $ modifyIORef' iSolveCounter (+1)
 
 runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
-runInferM info (IM m) = SMT.withSolver (inpSolverConfig info) $ \solver ->
+runInferM info (IM m) =
   do counter <- newIORef 0
      rec ro <- return RO { iRange     = inpRange info
                          , iVars          = Map.map ExtVar (inpVars info)
@@ -131,7 +132,7 @@ runInferM info (IM m) = SMT.withSolver (inpSolverConfig info) $ \solver ->
                          , iSolvedHasLazy = iSolvedHas finalRW     -- RECURSION
                          , iMonoBinds     = inpMonoBinds info
                          , iCallStacks    = inpCallStacks info
-                         , iSolver        = solver
+                         , iSolver        = inpSolver info
                          , iPrimNames     = inpPrimNames info
                          , iSolveCounter  = counter
                          }