Add a tcSmtFile REPL option

`tcSmtFile` is to `tcSolver` as `smtFile` is to `prover`. The `tcSmtFile`
option allows users to record typechecker-related SMT solver interactions to a
file.

This requires using a more recent `simple-smt` version to bring in the changes
from yav/simple-smt#25 and
yav/simple-smt#27, which are needed to plumb the
relevant information down to the `simple-smt` API.

Fixes #1782.

CHANGES.md

@@ -21,6 +21,9 @@
   invoked as `:dumptests - <EXPR>` allowing for easier experimentation and
   testing.
 
+* Add a REPL option `tcSmtFile` that allows writing typechecker-related SMT
+  solver interactions to a file.
+
 # 3.2.0 -- 2024-08-20
 
 ## Language changes

cabal.project

@@ -3,3 +3,10 @@ packages:
     cryptol-remote-api
     tests
     deps/argo/argo
+
+-- TODO RGS: Remove this once the changes from
+-- https://github.com/yav/simple-smt/pull/27 are released to Hackage
+source-repository-package
+  type: git
+  location: https://github.com/RyanGlScott/simple-smt
+  tag: 519d76a51c3c992120c69532f76311d7ac16718c

src/Cryptol/REPL/Monad.hs

@@ -972,6 +972,17 @@ userOptions  = mkOptionMap
                           setModuleEnv me { M.meMonoBinds = b }
           _         -> return ()
 
+  , OptionDescr "tcSmtFile" ["tc-smt-file"] (EnvString "-") noCheck
+    (unlines
+      [ "The file to record SMT solver interactions in the type checker (for debugging or offline proving)."
+      , "Use \"-\" for stdout." ]) $
+    \case EnvString fileName -> do let mfile = if fileName == "-" then Nothing else Just fileName
+                                   modifyRW_ (\rw -> rw { eTCConfig = (eTCConfig rw)
+                                                                       { T.solverSmtFile = mfile
+                                                                       }})
+                                   resetTCSolver
+          _                  -> return ()
+
   , OptionDescr "tcSolver" ["tc-solver"] (EnvProg "z3" [ "-smt2", "-in" ])
     noCheck  -- TODO: check for the program in the path
     "The solver that will be used by the type checker." $

src/Cryptol/TypeCheck/InferTypes.hs

@@ -45,6 +45,9 @@ data SolverConfig = SolverConfig
   , solverVerbose :: Int        -- ^ How verbose to be when type-checking
   , solverPreludePath :: [FilePath]
     -- ^ Look for the solver prelude in these locations.
+  , solverSmtFile :: Maybe FilePath
+    -- ^ The optional file to record SMT solver interactions in the type
+    -- checker. If 'Nothing', this will print to @stdout@ instead.
   } deriving (Show, Generic, NFData)
 
 
@@ -58,6 +61,7 @@ defaultSolverConfig searchPath =
   , solverArgs = [ "-smt2", "-in" ]
   , solverVerbose = 0
   , solverPreludePath = searchPath
+  , solverSmtFile = Nothing
   }
 
 -- | The types of variables in the environment.
@@ -389,7 +393,7 @@ instance PP (WithNames DelayedCt) where
   ppPrec _ (WithNames d names) =
     sig $$
     hang "we need to show that"
-       2 (vcat ( vars ++ asmps ++ 
+       2 (vcat ( vars ++ asmps ++
                [ hang "the following constraints hold:"
                     2 (vcat
                        $ bullets

src/Cryptol/TypeCheck/Solver/SMT.hs

@@ -47,6 +47,7 @@ import           Control.Exception
 import           Control.Monad(msum,zipWithM,void)
 import           Data.Char(isSpace)
 import           Text.Read(readMaybe)
+import           System.IO(Handle, IOMode(..), hClose, openFile, stdout)
 import qualified System.IO.Strict as StrictIO
 import           System.FilePath((</>))
 import           System.Directory(doesFileExist)
@@ -70,6 +71,9 @@ data Solver = Solver
 
   , logger    :: SMT.Logger
     -- ^ For debugging
+
+  , loggerHandle :: Maybe Handle
+    -- ^ The 'Handle' that the 'logger' writes to
   }
 
 setupSolver :: Solver -> SolverConfig -> IO ()
@@ -80,13 +84,24 @@ setupSolver s cfg = do
 -- | Start a fresh solver instance
 startSolver :: IO () -> SolverConfig -> IO Solver
 startSolver onExit sCfg =
-   do logger <- if (solverVerbose sCfg) > 0 then SMT.newLogger 0
-
-                                     else return quietLogger
+   do (logger, mbLoggerHdl) <-
+        if (solverVerbose sCfg) > 0
+        then do loggerHdl <-
+                  case solverSmtFile sCfg of
+                    Nothing   -> pure stdout
+                    Just file -> openFile file WriteMode
+                logger <- SMT.newLoggerWithHandle loggerHdl 0
+                pure (logger, Just loggerHdl)
+        else pure (quietLogger, Nothing)
       let smtDbg = if (solverVerbose sCfg) > 1 then Just logger else Nothing
-      solver <- SMT.newSolverNotify
-                    (solverPath sCfg) (solverArgs sCfg) smtDbg (Just (const onExit))
-      let sol = Solver solver logger
+      solver <- SMT.newSolverWithConfig
+                  (SMT.defaultConfig (solverPath sCfg) (solverArgs sCfg))
+                    { SMT.solverOnExit =
+                        Just (const onExit)
+                    , SMT.solverLogger =
+                        maybe SMT.noSolverLogger SMT.smtSolverLogger smtDbg
+                    }
+      let sol = Solver solver logger mbLoggerHdl
       setupSolver sol sCfg
       return sol
 
@@ -100,7 +115,9 @@ startSolver onExit sCfg =
 
 -- | Shut down a solver instance
 stopSolver :: Solver -> IO ()
-stopSolver s = void $ SMT.stop (solver s)
+stopSolver s =
+  do void $ SMT.stop (solver s)
+     mapM_ hClose (loggerHandle s)
 
 resetSolver :: Solver -> SolverConfig -> IO ()
 resetSolver s sCfg = do
@@ -150,7 +167,7 @@ loadString s str = go (dropComments str)
 
 debugBlock :: Solver -> String -> IO a -> IO a
 debugBlock s@Solver { .. } name m =
-  do debugLog s name
+  do debugLog s (";;; " ++ name)
      SMT.logTab logger
      a <- m
      SMT.logUntab logger