Merge pull request #1165 from GaloisInc/expose-utils

Expose `modPathSplit` and `defaultSolverConfig` for downstream use
GaloisInc · Apr 19, 2021 · 51e5d91 · 51e5d91
2 parents 3474960 + a279e78
commit 51e5d91
Show file tree

Hide file tree

Showing 6 changed files with 18 additions and 18 deletions.
diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs
@@ -19,7 +19,7 @@ import Cryptol.ModuleSystem.Env
    initialModuleEnv, meSearchPath, ModulePath(..))
 import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile )
 import Cryptol.Parser.AST (ModName)
-import Cryptol.TypeCheck( SolverConfig(..) )
+import Cryptol.TypeCheck( defaultSolverConfig )
 import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 
 import qualified Argo
@@ -135,15 +135,6 @@ initialState =
      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
-  }
-
 extendSearchPath :: [FilePath] -> ServerState -> ServerState
 extendSearchPath paths =
   over moduleEnv $ \me -> me { meSearchPath = nubOrd $ paths ++ meSearchPath me }

diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs
@@ -183,13 +183,7 @@ defaultRW :: Bool -> Bool -> Logger -> IO RW
 defaultRW isBatch callStacks l = do
   env <- M.initialModuleEnv
   let searchPath = M.meSearchPath env
-  let solverConfig =
-             T.SolverConfig
-             { T.solverPath = "z3"
-             , T.solverArgs = [ "-smt2", "-in" ]
-             , T.solverVerbose = 0
-             , T.solverPreludePath = searchPath
-             }
+  let solverConfig = T.defaultSolverConfig searchPath
   return RW
     { eLoadedMod   = Nothing
     , eEditFile    = Nothing

diff --git a/src/Cryptol/TypeCheck.hs b/src/Cryptol/TypeCheck.hs
@@ -15,6 +15,7 @@ module Cryptol.TypeCheck
   , InferInput(..)
   , InferOutput(..)
   , SolverConfig(..)
+  , defaultSolverConfig
   , NameSeeds
   , nameSeeds
   , Error(..)
@@ -49,7 +50,7 @@ import           Cryptol.TypeCheck.Monad
                    , io
                    )
 import Cryptol.TypeCheck.Infer (inferModule, inferBinds, checkTopDecls)
-import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..))
+import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..), defaultSolverConfig)
 import Cryptol.TypeCheck.Solve(proveModuleTopLevel)
 import Cryptol.TypeCheck.CheckModuleInstance(checkModuleInstance)
 -- import Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints)

diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs
@@ -48,6 +48,18 @@ data SolverConfig = SolverConfig
   } deriving (Show, Generic, NFData)
 
 
+-- | A default configuration for using Z3, where
+--   the solver prelude is expected to be found
+--   in the given search path.
+defaultSolverConfig :: [FilePath] -> SolverConfig
+defaultSolverConfig searchPath =
+  SolverConfig
+  { solverPath = "z3"
+  , solverArgs = [ "-smt2", "-in" ]
+  , solverVerbose = 0
+  , solverPreludePath = searchPath
+  }
+
 -- | The types of variables in the environment.
 data VarType = ExtVar Schema
                -- ^ Known type

diff --git a/src/Cryptol/TypeCheck/Solver/SMT.hs b/src/Cryptol/TypeCheck/Solver/SMT.hs
@@ -67,6 +67,7 @@ data Solver = Solver
     -- ^ For debugging
   }
 
+
 -- | Start a fresh solver instance
 startSolver :: SolverConfig -> IO Solver
 startSolver SolverConfig { .. } =

diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs
@@ -15,6 +15,7 @@ module Cryptol.Utils.Ident
   , apPathRoot
   , modPathCommon
   , topModuleFor
+  , modPathSplit
 
   , ModName
   , modNameToText