GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-29 02:42:45 +03:00
Code Issues Projects Releases Wiki Activity

Update eval server

Browse Source
This commit is contained in:
Rob Dockins 2021-02-11 18:00:49 -08:00
parent d30f039f24
commit d6fd9ee983
1 changed files with 6 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
cryptol-remote-api/cryptol-eval-server/Main.hs
View File

@ -12,9 +12,10 @@ import System.IO (hPutStrLn, stderr)
import Options.Applicative
import Cryptol.Eval (EvalOpts(..), defaultPPOpts)
import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName)
import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName, meSolverConfig)
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)
@ -41,18 +42,18 @@ main = customMain initMod initMod initMod initMod description buildApp
do paths <- getSearchPaths
initSt <- setSearchPath paths <$> initialState
let menv = view moduleEnv initSt
let minp = ModuleInput False (pure evOpts) reader menv
let minp s = 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' <-
do (res, _warnings) <- either loadModuleByPath loadModuleByName file minp
menv' <- SMT.withSolver (meSolverConfig menv) $ \s ->
do (res, _warnings) <- either loadModuleByPath loadModuleByName file (minp s)
-- NB Warnings suppressed when running server
case res of
Left err -> die err
Right (m, menv') ->
do res' <- fst <$> runModuleM minp { minpModuleEnv = menv' } (setFocusedModule (mName (snd m)))
do res' <- fst <$> runModuleM (minp s){ minpModuleEnv = menv' } (setFocusedModule (mName (snd m)))
case res' of
Left err -> die err
Right (_, menv'') -> pure menv''