From 816523df10ff862dcc1ce3d525fb22795d05cc58 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki <iavor.diatchki@gmail.com> Date: Tue, 29 Jun 2021 15:22:04 -0700 Subject: [PATCH] Fixes #1167 This requires newer version simple-smt, which supports calling back into the program when the solver exits --- cryptol.cabal | 3 ++- src/Cryptol/REPL/Monad.hs | 7 ++++++- src/Cryptol/TypeCheck/Solver/SMT.hs | 11 ++++++----- 3 files changed, 14 insertions(+), 7 deletions(-) diff --git a/cryptol.cabal b/cryptol.cabal index c140f87dd..ad6b5be49 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -65,7 +65,7 @@ library pretty >= 1.1, process >= 1.2, sbv >= 8.6 && < 8.15, - simple-smt >= 0.7.1, + simple-smt >= 0.9.7, stm >= 2.4, strict, text >= 1.1, @@ -231,6 +231,7 @@ executable cryptol , directory , filepath , haskeline >= 0.7 && < 0.9 + , exceptions , monad-control , text , transformers diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 49892a764..5cc9bf039 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -415,13 +415,18 @@ getPrompt = mkPrompt `fmap` getRW getCallStacks :: REPL Bool getCallStacks = eCallStacks <$> getRW +clearTCSolverAction :: REPL (IO ()) +clearTCSolverAction = + REPL (\ref -> pure (modifyIORef ref (\rw -> rw { eTCSolver = Nothing }))) + getTCSolver :: REPL SMT.Solver getTCSolver = do rw <- getRW case eTCSolver rw of Just s -> return s Nothing -> - do s <- io (SMT.startSolver (eTCConfig rw)) + do onExit <- clearTCSolverAction + s <- io (SMT.startSolver onExit (eTCConfig rw)) modifyRW_ (\rw' -> rw'{ eTCSolver = Just s }) return s diff --git a/src/Cryptol/TypeCheck/Solver/SMT.hs b/src/Cryptol/TypeCheck/Solver/SMT.hs index c2fae2362..ba81cab0e 100644 --- a/src/Cryptol/TypeCheck/Solver/SMT.hs +++ b/src/Cryptol/TypeCheck/Solver/SMT.hs @@ -69,13 +69,14 @@ data Solver = Solver -- | Start a fresh solver instance -startSolver :: SolverConfig -> IO Solver -startSolver SolverConfig { .. } = +startSolver :: IO () -> SolverConfig -> IO Solver +startSolver onExit SolverConfig { .. } = do logger <- if solverVerbose > 0 then SMT.newLogger 0 else return quietLogger let smtDbg = if solverVerbose > 1 then Just logger else Nothing - solver <- SMT.newSolver solverPath solverArgs smtDbg + solver <- SMT.newSolverNotify + solverPath solverArgs smtDbg (Just (const onExit)) _ <- SMT.setOptionMaybe solver ":global-decls" "false" -- SMT.setLogic solver "QF_LIA" let sol = Solver { .. } @@ -95,8 +96,8 @@ stopSolver :: Solver -> IO () stopSolver s = void $ SMT.stop (solver s) -- | Execute a computation with a fresh solver instance. -withSolver :: SolverConfig -> (Solver -> IO a) -> IO a -withSolver cfg = bracket (startSolver cfg) stopSolver +withSolver :: IO () -> SolverConfig -> (Solver -> IO a) -> IO a +withSolver onExit cfg = bracket (startSolver onExit cfg) stopSolver -- | Load the definitions used for type checking. loadTcPrelude :: Solver -> [FilePath] {- ^ Search in this paths -} -> IO ()