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

@@ -41,12 +41,13 @@ import qualified SimpleSMT as SMT
 import           Data.Map ( Map )
 import qualified Data.Map as Map
 import qualified Data.Set as Set
-import           Data.Maybe(catMaybes)
+import           Data.Maybe(catMaybes,isJust)
 import           Data.List(partition)
 import           Control.Exception
 import           Control.Monad(msum,zipWithM,void)
 import           Data.Char(isSpace)
 import           Text.Read(readMaybe)
+import           System.IO(IOMode(..), hClose, openFile)
 import qualified System.IO.Strict as StrictIO
 import           System.FilePath((</>))
 import           System.Directory(doesFileExist)
@@ -80,12 +81,38 @@ 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
-      let smtDbg = if (solverVerbose sCfg) > 1 then Just logger else Nothing
-      solver <- SMT.newSolverNotify
-                    (solverPath sCfg) (solverArgs sCfg) smtDbg (Just (const onExit))
+   do let smtFileEnabled = isJust (solverSmtFile sCfg)
+      (logger, mbLoggerCloseHdl) <-
+        -- There are two scenarios under which we want to explicitly log SMT
+        -- solver interactions:
+        --
+        -- 1. The user wants to debug-print interactions with the `tcDebug`
+        --    option
+        -- 2. The user wants to write interactions to the `tcSmtFile` option
+        --
+        -- We enable logging if either one is true.
+        if (solverVerbose sCfg) > 0 || smtFileEnabled
+        then case solverSmtFile sCfg of
+               Nothing ->
+                 do logger <- SMT.newLogger 0
+                    pure (logger, Nothing)
+               Just file ->
+                 do loggerHdl <- openFile file WriteMode
+                    logger <- SMT.newLoggerWithHandle loggerHdl 0
+                    pure (logger, Just (hClose loggerHdl))
+        else pure (quietLogger, Nothing)
+      let smtDbg = if (solverVerbose sCfg) > 1 || smtFileEnabled
+                   then Just logger
+                   else Nothing
+      solver <- SMT.newSolverWithConfig
+                  (SMT.defaultConfig (solverPath sCfg) (solverArgs sCfg))
+                    { SMT.solverOnExit =
+                        Just $ \_exitCode ->
+                        do onExit
+                           sequence_ mbLoggerCloseHdl
+                    , SMT.solverLogger =
+                        maybe SMT.noSolverLogger SMT.smtSolverLogger smtDbg
+                    }
       let sol = Solver solver logger
       setupSolver sol sCfg
       return sol
@@ -150,7 +177,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