From b9b2a68456b383cd20d3274ce454e41d3aded764 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Thu, 30 May 2024 15:43:26 +1000
Subject: [PATCH] Expose the resolution "primitive" behind resolve_then

resolve_then requires the output of the resolution to be passed to a
theorem-tactic (and will backtrack if the theorem-tactic fails with a HOL_ERR);
the new gen_resolve_then will pass to any consumer/continuation, backtracking
if *that* fails with a HOL_ERR.  The old resolve_then is then an easy
instance of the new function.
---
 src/1/resolve_then.sig |  1 +
 src/1/resolve_then.sml | 14 +++++++++-----
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/1/resolve_then.sig b/src/1/resolve_then.sig
index 34dc5ed474..134c13df9a 100644
--- a/src/1/resolve_then.sig
+++ b/src/1/resolve_then.sig
@@ -3,6 +3,7 @@ sig
 
   include Abbrev
   datatype match_position = datatype thmpos_dtype.match_position
+  val gen_resolve_then : match_position -> thm -> thm -> (thm -> 'a) -> 'a
   val resolve_then : match_position -> thm_tactic -> thm -> thm -> tactic
 
 end
diff --git a/src/1/resolve_then.sml b/src/1/resolve_then.sml
index 537272c7a7..84244a1eee 100644
--- a/src/1/resolve_then.sml
+++ b/src/1/resolve_then.sml
@@ -92,7 +92,9 @@ fun liftconcl th =
 (* val th2 = prim_recTheory.LESS_REFL
    val th1 = arithmeticTheory.LESS_TRANS
 *)
-fun resolve_then mpos ttac th1 th2 (g as (asl,w)) =
+
+
+fun gen_resolve_then mpos th1 th2 kont =
     (* conclusion of th1 unifies with some part of th2 *)
     let
       val th1 = GEN_ALL (GEN_TYVARIFY th1)
@@ -140,7 +142,7 @@ fun resolve_then mpos ttac th1 th2 (g as (asl,w)) =
                       PROVE_HYP (INSTT sigma th1_ud) (INSTT sigma th2_ud) |>
                       postprocess sigma
               in
-                ttac kth g handle HOL_ERR _ => k()
+                kont kth handle HOL_ERR _ => k()
               end
       val max = length cs2
       val fail = mk_HOL_ERR "Tactic" "resolve_then" "No unifier"
@@ -162,9 +164,7 @@ fun resolve_then mpos ttac th1 th2 (g as (asl,w)) =
           let
             open TermParse
             val pats =
-                prim_ctxt_termS Parse.Absyn (Parse.term_grammar())
-                                (HOLset.listItems (FVL (w::asl) empty_tmset))
-                                q
+                prim_ctxt_termS Parse.Absyn (Parse.term_grammar()) [] q
             fun doit ps n =
                 if n > max then raise fail
                 else
@@ -179,4 +179,8 @@ fun resolve_then mpos ttac th1 th2 (g as (asl,w)) =
           end
         | Concl => try con (fn _ => raise fail)
     end
+
+fun resolve_then mpos ttac th1 th2 g =
+    gen_resolve_then mpos th1 th2 (fn th => ttac th g)
+
 end (* struct *)