chore: make missing records fields an error for cryptol-remote-api

GaloisInc · Feb 23, 2021 · 40ba4a4 · 40ba4a4
1 parent 6b784b1
commit 40ba4a4
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 14 deletions.
diff --git 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,9 @@ common warnings
     -Wno-implicit-prelude
     -Wno-missing-deriving-strategies
 
+common errors
+  ghc-options:
+    -Werror=missing-fields
 
 common deps
   build-depends:
@@ -46,7 +49,7 @@ common deps
   default-language:    Haskell2010
 
 library
-  import:              deps, warnings
+  import:              deps, warnings, errors
   hs-source-dirs:      src
 
   exposed-modules:
@@ -65,7 +68,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 +79,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 +92,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
@@ -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)