Remove MRSolver commands.

Author: brianhuffman

.github/workflows/ci.yml

@@ -502,7 +502,6 @@ jobs:
         shell: bash
         run: |
           saw monadify.saw
-          saw mr_solver_unit_tests.saw
 
   crux-mir-comp-tests:
     needs: [build]

doc/developer/issue-labels.md

@@ -259,9 +259,6 @@ Cryptol-to-saw-core translation in the cryptol-saw-core package.
 
 * _subsystem: hardware_ - issues related to verification of hardware.
 
-* _subsystem: MRSolver_ - issues related to the Mr. Solver
-monadic-recursive solver in Heapster.
-
 * _subsystem: saw-core_ - issues related to the saw-core
 representation or the saw-core subsystem.
 

examples/mr_solver/mr_solver_unit_tests.saw

@@ -23,7 +23,7 @@ term_eval : Term -> Term
 term_eval_unint : [String] -> Term -> Term
 time : {a} TopLevel a -> TopLevel a
 unfold_term : [String] -> Term -> Term
-22 more matches tagged experimental; use enable_experimental to see them
+19 more matches tagged experimental; use enable_experimental to see them
 2 more matches tagged deprecated; use enable_deprecated to see them
  --------------------------------
  -- {a} (a -> String)

intTests/test_search/search02.log.good

@@ -27,7 +27,6 @@ import Control.Monad.Except (MonadError(..))
 import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.Reader (asks)
 import Control.Monad.State (MonadState(..), gets, modify)
-import Control.Monad.Trans.Class (MonadTrans(..))
 import qualified Control.Exception as Ex
 import qualified Data.ByteString as StrictBS
 import qualified Data.ByteString.Lazy as BS
@@ -64,7 +63,7 @@ import qualified CryptolSAWCore.Simpset as Cryptol
 import qualified CryptolSAWCore.Monadify as Monadify
 
 -- saw-support
-import qualified SAWSupport.Pretty as PPS (Doc, MemoStyle(..), Opts(..), defaultOpts, render, pShow)
+import qualified SAWSupport.Pretty as PPS (MemoStyle(..), Opts(..), pShow)
 
 -- saw-core
 import qualified SAWCore.Parser.AST as Un
@@ -75,7 +74,6 @@ import SAWCore.FiniteValue
   , FirstOrderValue(..)
   , scFirstOrderValue
   )
-import SAWCore.Module (ModuleMap)
 import SAWCore.Name (ecShortName)
 import SAWCore.SATQuery
 import SAWCore.SCTypeCheck
@@ -152,7 +150,6 @@ import qualified SAWCentral.Prover.RME as Prover
 import qualified SAWCentral.Prover.ABC as Prover
 import qualified SAWCentral.Prover.What4 as Prover
 import qualified SAWCentral.Prover.Exporter as Prover
-import qualified SAWCentral.Prover.MRSolver as Prover
 import SAWCentral.VerificationSummary
 
 showPrim :: SV.Value -> TopLevel Text
@@ -2246,151 +2243,22 @@ monadifyTypedTerm sc t =
 ensureMonadicTerm :: SharedContext -> TypedTerm -> TopLevel TypedTerm
 ensureMonadicTerm sc t
   | TypedTermOther tp <- ttType t =
-    io (Prover.isSpecFunType sc tp) >>= \case
+    io (isSpecFunType sc tp) >>= \case
       True -> return t
       False -> monadifyTypedTerm sc t
 ensureMonadicTerm sc t = monadifyTypedTerm sc t
 
--- | Normalizes the given 'TypedTerm's for calling 'Prover.askMRSolver' or
--- 'Prover.refinementTerm' and ensures they are of the expected form.
--- Additionally, if the second argument is @Just str@, prints out @str@
--- followed by an abridged version of the refinement represented by the two
--- terms.
-mrSolverNormalizeAndPrintArgs ::
-  SharedContext -> Maybe PPS.Doc ->
-  TypedTerm -> TypedTerm -> TopLevel (Term, Term)
-mrSolverNormalizeAndPrintArgs sc printStr tt1 tt2 =
-  do mm <- io $ scGetModuleMap sc
-     let ?mm = mm
-     m1 <- ttTerm <$> ensureMonadicTerm sc tt1
-     m2 <- ttTerm <$> ensureMonadicTerm sc tt2
-     m1' <- io $ collapseEta <$> betaNormalize sc m1
-     m2' <- io $ collapseEta <$> betaNormalize sc m2
-     case printStr of
-       Nothing -> return ()
-       Just str -> printOutLnTop Info $ PPS.render PPS.defaultOpts $
-         "[MRSolver] " <> str <> ": " <> ppTmHead m1' <>
-                               " |= " <> ppTmHead m2'
-     return (m1', m2')
-  where -- Turn a term of the form @\x1 ... xn -> f x1 ... xn@ into @f@
-        collapseEta :: Term -> Term
-        collapseEta (asLambdaList -> (lamVars,
-                     asApplyAll -> (t@(smallestLooseVar -> Nothing),
-                                    mapM asLocalVar -> Just argVars)))
-          | argVars == [(length lamVars - 1), (length lamVars - 2) .. 0] = t
-        collapseEta t = t
-        -- Pretty-print the name of the top-level function call, followed by
-        -- "..." if it is given any arguments, or just "..." if there is no
-        -- top-level call
-        ppTmHead :: (?mm :: ModuleMap) => Term -> PPS.Doc
-        ppTmHead (asLambdaList -> (_,
-                  asApplyAll -> (t@(
-                  Prover.asProjAll -> (
-                  Monadify.asTypedGlobalDef -> Just _, _)), args))) =
-          ppTerm PPS.defaultOpts t <> if length args > 0 then " ..." else ""
-        ppTmHead _ = "..."
-
--- | The calback to be used by MRSolver for making SMT queries
-mrSolverAskSMT :: Set VarIndex -> Sequent -> TopLevel (SolverStats, SolveResult)
-mrSolverAskSMT = applyProverToGoal [What4, Z3] [] (Prover.proveWhat4_z3 True)
-
--- | Given the result of calling 'Prover.askMRSolver' or
--- 'Prover.refinementTerm', fails and prints out@`err@ followed by the second
--- argument if the given result is @Left err@ for some @err@, or otherwise
--- returns @a@ if the result is@`Right a@ for some @a@. Additionally, if the
--- third argument is @Just str@, prints out @str@ on success (i.e. 'Right').
-mrSolverGetResultOrFail ::
-  Prover.MREnv ->
-  String {- The string to print out on failure -} ->
-  Maybe String {- The string to print out on success, if any -} ->
-  Either Prover.MRFailure a {- The result, printed out on error -} ->
-  TopLevel a
-mrSolverGetResultOrFail env errStr succStr res = case res of
-  Left err | Prover.mreDebugLevel env == 0 ->
-    fail (Prover.showMRFailure env err ++ "\n[MRSolver] " ++ errStr)
-  Left err ->
-    -- we ignore the MRFailure context here since it will have already
-    -- been printed by the debug trace
-    fail (Prover.showMRFailureNoCtx env err ++ "\n[MRSolver] " ++ errStr)
-  Right a | Just s <- succStr ->
-    printOutLnTop Info s >> return a
-  Right a -> return a
-
--- | Invokes MRSolver to attempt to solve a focused goal of the form
--- @(a1:A1) -> ... -> (an:An) -> refinesS_eq ...@, assuming the refinements
--- in the given 'Refnset', and printing an error message and exiting if
--- this cannot be done
-mrSolver :: SV.SAWRefnset -> ProofScript ()
-mrSolver rs = execTactic $ Tactic $ \goal -> lift $
-  getSharedContext >>= \sc ->
-  case sequentState (goalSequent goal) of
-    Unfocused -> fail "mrsolver: focus required"
-    HypFocus _ _ -> fail "mrsolver: cannot apply mrsolver in a hypothesis"
-    ConclFocus (Prover.asRefinesS . unProp ->
-                Just (Prover.RefinesS args ev rtp1 rtp2 t1 t2)) _ ->
-      do tp1 <- liftIO $ scGlobalApply sc "SpecM.SpecM" [ev, rtp1]
-         tp2 <- liftIO $ scGlobalApply sc "SpecM.SpecM" [ev, rtp2]
-         let tt1 = TypedTerm (TypedTermOther tp1) t1
-             tt2 = TypedTerm (TypedTermOther tp2) t2
-         (m1, m2) <- mrSolverNormalizeAndPrintArgs sc (Just $ "Tactic call") tt1 tt2
-         env <- rwMRSolverEnv <$> get
-         time1 <- liftIO getCurrentTime
-         res <- Prover.askMRSolver sc env Nothing mrSolverAskSMT rs args m1 m2
-         time2 <- liftIO getCurrentTime
-         let diff = show $ diffUTCTime time2 time1
-             errStr = printf "Failure in %s" diff
-             succStr = printf "Success in %s" diff
-         (stats, mre) <- mrSolverGetResultOrFail env errStr (Just succStr) res
-         return ((), stats, [], leafEvidence $ MrSolverEvidence mre)
-    _ -> error "mrsolver: cannot apply mrsolver to a non-refinement goal"
-
--- | Add a proved refinement theorem to a given refinement set
-addrefn :: Theorem -> SV.SAWRefnset -> TopLevel SV.SAWRefnset
-addrefn thm rs =
-  getSharedContext >>= \sc ->
-  io (scGetModuleMap sc) >>= \mm ->
-  let ?mm = mm in
-  case Prover.asFunAssump (Just (thmNonce thm)) (unProp $ thmProp thm) of
-    Nothing -> fail "addrefn: theorem is not a refinement"
-    Just fassump -> pure (Prover.addFunAssump fassump rs)
-
--- | Add proved refinement theorems to a given refinement set
-addrefns :: [Theorem] -> SV.SAWRefnset -> TopLevel SV.SAWRefnset
-addrefns thms ss = foldM (flip addrefn) ss thms
-
--- | Set the debug level of the 'Prover.MREnv'
-mrSolverSetDebug :: Int -> TopLevel ()
-mrSolverSetDebug dlvl =
-  modify (\rw -> rw { rwMRSolverEnv =
-                        Prover.mrEnvSetDebugLevel dlvl (rwMRSolverEnv rw) })
-
--- | Modify the 'PPOpts' of the current 'MREnv' to have a maximum printing depth
-mrSolverSetDebugDepth :: Int -> TopLevel ()
-mrSolverSetDebugDepth depth =
-  modify (\rw -> rw { rwMRSolverEnv = (rwMRSolverEnv rw) {
-                        Prover.mrePPOpts = (Prover.mrePPOpts (rwMRSolverEnv rw)) {
-                          PPS.ppMaxDepth = Just depth }}})
-
--- | Given a list of names and types representing variables over which to
--- quantify as as well as two terms containing those variables, which may be
--- terms or functions in the SpecM monad, construct the SAWCore term which is
--- the refinement (@SpecM.refinesS@) of the given terms, with the given
--- variables generalized with a Pi type.
-refinesTerm :: [TypedTerm] -> TypedTerm -> TypedTerm -> TopLevel TypedTerm
-refinesTerm vars tt1 tt2 =
-  do sc <- getSharedContext
-     tt1' <- lambdas vars tt1
-     tt2' <- lambdas vars tt2
-     (m1, m2) <- mrSolverNormalizeAndPrintArgs sc Nothing tt1' tt2'
-     env <- rwMRSolverEnv <$> get
-     time1 <- liftIO getCurrentTime
-     res <- Prover.refinementTerm sc env Nothing mrSolverAskSMT
-                                  Prover.emptyRefnset [] m1 m2
-     time2 <- liftIO getCurrentTime
-     let diff = show $ diffUTCTime time2 time1
-         errStr = printf "[MRSolver] Failed to build refinement term (%s)" diff
-     ttRes <- mrSolverGetResultOrFail env errStr Nothing res
-     io $ mkTypedTerm sc ttRes
+-- | Match a type as being of the form @SpecM E a@ for some @E@ and @a@
+asSpecM :: Term -> Maybe (Term, Term)
+asSpecM (asApplyAll -> (isGlobalDef "SpecM.SpecM" -> Just (), [ev, tp])) =
+  return (ev, tp)
+asSpecM _ = fail "not a SpecM type, or event type is not closed!"
+
+-- | Test if a type normalizes to a monadic function type of 0 or more arguments
+isSpecFunType :: SharedContext -> Term -> IO Bool
+isSpecFunType sc t = scWhnf sc t >>= \case
+  (asPiList -> (_, asSpecM -> Just _)) -> return True
+  _ -> return False
 
 setMonadification :: SharedContext -> Text -> Text -> Bool -> TopLevel ()
 setMonadification sc cry_str saw_str poly_p =