rename prove_refinement tactic to mrsolver

GaloisInc · Mar 30, 2023 · c0f364c · c0f364c
1 parent 6d81c44
commit c0f364c
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 28 deletions.
diff --git a/examples/mr_solver/mr_solver_unit_tests.saw b/examples/mr_solver/mr_solver_unit_tests.saw
@@ -27,43 +27,43 @@ const1 <- parse_core const1_core;
 
 // const0 <= const0
 run_test "const0 |= const0" (mr_solver_query const0 const0) true;
-// (using prove_refinement tactic)
+// (using mrsolver tactic)
 let const0_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", const0_core, ") x) ", "((", const0_core, ") x)"];
-prove_extcore prove_refinement (parse_core const0_refines);
+prove_extcore mrsolver (parse_core const0_refines);
 
 // The function test_fun0 = const0
 test_fun0 <- parse_core_mod "test_funs" "test_fun0";
 run_test "const0 |= test_fun0" (mr_solver_query const0 test_fun0) true;
-// (using prove_refinement tactic)
+// (using mrsolver tactic)
 let const0_test_fun0_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", const0_core, ") x) ", "(test_fun0 x)"];
-prove_extcore prove_refinement (parse_core_mod "test_funs" const0_test_fun0_refines);
+prove_extcore mrsolver (parse_core_mod "test_funs" const0_test_fun0_refines);
 
 // not const0 <= const1
 run_test "const0 |= const1" (mr_solver_query const0 const1) false;
-// (using prove_refinement tactic - fails as expected)
+// (using mrsolver tactic - fails as expected)
 // let const0_const1_refines =
 //   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
 //                "((", const0_core, ") x) ", "((", const1_core, ") x)"];
-// prove_extcore prove_refinement (parse_core const0_const1_refines);
+// prove_extcore mrsolver (parse_core const0_const1_refines);
 
 // The function test_fun1 = const1
 test_fun1 <- parse_core_mod "test_funs" "test_fun1";
 run_test "const1 |= test_fun1" (mr_solver_query const1 test_fun1) true;
 run_test "const0 |= test_fun1" (mr_solver_query const0 test_fun1) false;
-// (using prove_refinement tactic)
+// (using mrsolver tactic)
 let const1_test_fun1_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", const1_core, ") x) ", "(test_fun1 x)"];
-prove_extcore prove_refinement (parse_core_mod "test_funs" const1_test_fun1_refines);
-// (using prove_refinement tactic - fails as expected)
+prove_extcore mrsolver (parse_core_mod "test_funs" const1_test_fun1_refines);
+// (using mrsolver tactic - fails as expected)
 // let const0_test_fun1_refines =
 //   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
 //                "((", const0_core, ") x) ", "(test_fun1 x)"];
-// prove_extcore prove_refinement (parse_core_mod "test_funs" const0_test_fun1_refines);
+// prove_extcore mrsolver (parse_core_mod "test_funs" const0_test_fun1_refines);
 
 // ifxEq0 x = If x == 0 then x else 0; should be equal to 0
 let ifxEq0_core = "\\ (x:Vec 64 Bool) -> \
@@ -75,19 +75,19 @@ ifxEq0 <- parse_core ifxEq0_core;
 
 // ifxEq0 <= const0
 run_test "ifxEq0 |= const0" (mr_solver_query ifxEq0 const0) true;
-// (using prove_refinement tactic)
+// (using mrsolver tactic)
 let ifxEq0_const0_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", ifxEq0_core, ") x) ", "((", const0_core, ") x)"];
-prove_extcore prove_refinement (parse_core ifxEq0_const0_refines);
+prove_extcore mrsolver (parse_core ifxEq0_const0_refines);
 
 // not ifxEq0 <= const1
 run_test "ifxEq0 |= const1" (mr_solver_query ifxEq0 const1) false;
-// (using prove_refinement tactic - fails as expected)
+// (using mrsolver tactic - fails as expected)
 // let ifxEq0_const1_refines =
 //   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
 //                "((", ifxEq0_core, ") x) ", "((", const1_core, ") x)"];
-// prove_extcore prove_refinement (parse_core ifxEq0_const1_refines);
+// prove_extcore mrsolver (parse_core ifxEq0_const1_refines);
 
 // noErrors1 x = existsS x. retS x
 let noErrors1_core =
@@ -96,19 +96,19 @@ noErrors1 <- parse_core noErrors1_core;
 
 // const0 <= noErrors
 run_test "noErrors1 |= noErrors1" (mr_solver_query noErrors1 noErrors1) true;
-// (using prove_refinement tactic)
+// (using mrsolver tactic)
 let noErrors1_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", noErrors1_core, ") x) ", "((", noErrors1_core, ") x)"];
-prove_extcore prove_refinement (parse_core noErrors1_refines);
+prove_extcore mrsolver (parse_core noErrors1_refines);
 
 // const1 <= noErrors
 run_test "const1 |= noErrors1" (mr_solver_query const1 noErrors1) true;
-// (using prove_refinement tactic)
+// (using mrsolver tactic)
 let const1_noErrors1_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", const1_core, ") x) ", "((", noErrors1_core, ") x)"];
-prove_extcore prove_refinement (parse_core const1_noErrors1_refines);
+prove_extcore mrsolver (parse_core const1_noErrors1_refines);
 
 // noErrorsRec1 _ = orS (existsM x. returnM x) (noErrorsRec1 x)
 // Intuitively, this specifies functions that either return a value or loop
@@ -136,8 +136,8 @@ loop1 <- parse_core loop1_core;
 
 // loop1 <= noErrorsRec1
 run_test "loop1 |= noErrorsRec1" (mr_solver_query loop1 noErrorsRec1) true;
-// (using prove_refinement tactic)
+// (using mrsolver tactic)
 let loop1_noErrorsRec1_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", loop1_core, ") x) ", "((", noErrorsRec1_core, ") x)"];
-prove_extcore prove_refinement (parse_core loop1_noErrorsRec1_refines);
+prove_extcore mrsolver (parse_core loop1_noErrorsRec1_refines);
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
@@ -2187,19 +2187,19 @@ mrSolver f printStr sc top_args tt1 tt2 =
 -- @(a1:A1) -> ... -> (an:A1) -> refinesS_eq ...@, printing an error message
 -- and exiting if this cannot be done. This function will not modify the
 -- 'Prover.MREnv'.
-proveRefinement :: SharedContext -> ProofScript ()
-proveRefinement sc = execTactic $ Tactic $ \goal -> lift $ do
+mrSolverTactic :: SharedContext -> ProofScript ()
+mrSolverTactic sc = execTactic $ Tactic $ \goal -> lift $ do
   dlvl <- Prover.mreDebugLevel <$> rwMRSolverEnv <$> get
   case sequentState (goalSequent goal) of
-    Unfocused -> fail "prove_refinement: focus required"
-    HypFocus _ _ -> fail "prove_refinement: cannot apply prove_refinement in a hypothesis"
+    Unfocused -> fail "mrsolver: focus required"
+    HypFocus _ _ -> fail "mrsolver: cannot apply mrsolver in a hypothesis"
     ConclFocus (asPiList . unProp -> (args, asApplyAll ->
                                       (asGlobalDef -> Just "Prelude.refinesS_eq",
                                        [ev, stack, rtp, t1, t2]))) _ ->
       do tp <- liftIO $ scGlobalApply sc "Prelude.SpecM" [ev, stack, rtp]
          let tt1 = TypedTerm (TypedTermOther tp) t1
          let tt2 = TypedTerm (TypedTermOther tp) t2
-         (diff, res) <- mrSolver Prover.askMRSolver (Just "prove_refinement") sc args tt1 tt2
+         (diff, res) <- mrSolver Prover.askMRSolver (Just "mrsolver") sc args tt1 tt2
          case res of
            Left err | dlvl == 0 ->
              io (putStrLn $ Prover.showMRFailure err) >>
@@ -2215,7 +2215,7 @@ proveRefinement sc = execTactic $ Tactic $ \goal -> lift $ do
              printOutLnTop Info (printf "[MRSolver] Success in %s" (show diff)) >>
              let stats = solverStats "MRSOLVER ADMITTED" (sequentSharedSize (goalSequent goal)) in
              return ((), stats, [], leafEvidence MrSolverEvidence)
-    _ -> error "prove_refinement tactic not applied to a refinesS_eq goal"
+    _ -> error "mrsolver tactic not applied to a refinesS_eq goal"
 
 -- | Run Mr Solver to prove that the first term refines the second, adding
 -- any relevant 'Prover.FunAssump's to the 'Prover.MREnv' if the first argument

diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
@@ -3785,8 +3785,8 @@ primitives = Map.fromList
     , " 1 = basic debug output, 2 = verbose debug output,"
     , " 3 = all debug output" ]
 
-  , prim "prove_refinement" "ProofScript ()"
-    (scVal proveRefinement)
+  , prim "mrsolver" "ProofScript ()"
+    (scVal mrSolverTactic)
     Experimental
     [ "Use MRSolver to prove a current goal of the form:"
     , "(a1:A1) -> ... -> (an:A1) -> refinesS_eq ..." ]