diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index 45b36a328..3280b3cf2 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -12,7 +12,7 @@ data-files: test-scripts/**/*.py common warnings ghc-options: - -Weverything + -Wall -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations @@ -24,6 +24,12 @@ common warnings -Wno-implicit-prelude -Wno-missing-deriving-strategies +common errors + ghc-options: + -Werror=missing-fields + -Werror=incomplete-patterns + -Werror=missing-methods + -Werror=overlapping-patterns common deps build-depends: @@ -46,7 +52,7 @@ common deps default-language: Haskell2010 library - import: deps, warnings + import: deps, warnings, errors hs-source-dirs: src exposed-modules: @@ -65,7 +71,7 @@ library CryptolServer.TypeCheck executable cryptol-remote-api - import: deps, warnings + import: deps, warnings, errors main-is: Main.hs hs-source-dirs: cryptol-remote-api ghc-options: @@ -76,7 +82,7 @@ executable cryptol-remote-api sbv < 8.10 executable cryptol-eval-server - import: deps, warnings + import: deps, warnings, errors main-is: Main.hs hs-source-dirs: cryptol-eval-server ghc-options: @@ -89,7 +95,7 @@ executable cryptol-eval-server test-suite test-cryptol-remote-api - import: deps, warnings + import: deps, warnings, errors type: exitcode-stdio-1.0 hs-source-dirs: test main-is: Test.hs diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs index ade4ff4a0..7e568ead1 100644 --- a/cryptol-remote-api/src/CryptolServer.hs +++ b/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(..)) -import Cryptol.ModuleSystem.Fingerprint + initialModuleEnv, meSearchPath, ModulePath(..), meSolverConfig) +import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile ) import Cryptol.Parser.AST (ModName) +import qualified Cryptol.TypeCheck.Solver.SMT as SMT import qualified Argo import qualified Argo.Doc as Doc @@ -61,13 +62,15 @@ runModuleCmd cmd = do Options callStacks evOpts <- getOptions s <- CryptolMethod $ const Argo.getState reader <- CryptolMethod $ const Argo.getFileReader - let minp = ModuleInput - { minpCallStacks = callStacks - , minpEvalOpts = pure evOpts - , minpByteReader = reader - , minpModuleEnv = view moduleEnv s - } - out <- liftIO $ cmd minp + let minp solver = ModuleInput + { minpCallStacks = callStacks + , minpEvalOpts = pure evOpts + , minpByteReader = reader + , minpModuleEnv = view moduleEnv s + , minpTCSolver = solver + } + let solverCfg = meSolverConfig (view moduleEnv s) + out <- liftIO $ SMT.withSolver solverCfg (cmd . minp) case out of (Left x, warns) -> raise (cryptolError x warns)