1 files changed, 81 insertions, 18 deletions

diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 28f8ab97..a718392b 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -5,6 +5,10 @@ struct
 open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory
 
+val debug = ref false
+
+fun print_dbg msg = if !debug then print msg else ()
+
 (* Remark: below, we also have conversions *)
 val gsym = GSYM
 
@@ -241,7 +245,7 @@ val th = SPEC_ALL NUM_SUB_1_EQ
  *)
 fun inst_match_in_terms
   (try_match: string Redblackset.set -> term -> term * thm)
-  (tl : term list) : thm list =
+  (tml : term list) : thm list =
   let
     (* We use a map when storing the theorems, to avoid storing the same theorem twice *)
     val inst_thms: (term, thm) Redblackmap.dict ref = ref (Redblackmap.mkDict Term.compare);
@@ -253,7 +257,7 @@ fun inst_match_in_terms
       end
       handle HOL_ERR _ => ();
     (* Explore the term *)
-    val _ = app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tl;
+    val _ = List.app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tml;
   in
     map snd (Redblackmap.listItems (!inst_thms))
   end
@@ -265,20 +269,24 @@ fun inst_match_in_terms
    [keep]: if this function returns false on an instantiated theorem, ignore
    the theorem.
  *)
-fun inst_match_concl_in_terms (keep : thm -> bool) (th : thm) (tl : term list) : thm list =
+fun inst_match_concl_in_terms (keep : thm -> bool) (th : thm) (tml : term list) : thm list =
   let
     val th = (UNDISCH_ALL o SPEC_ALL) th;
     fun try_match bvars t =
       let
-        val inst_th = inst_match_concl bvars th t;
-        val c = concl inst_th;
+        val _ = print_dbg ("inst_match_concl_in_terms: " ^ term_to_string t ^ "\n")
+        val inst_th = inst_match_concl bvars th t
+        val c = concl inst_th
+        val _ = print_dbg ("inst_match_concl_in_terms: matched with success\n")
       in
         (* Check that we mustn't ignore the theorem *)
         if keep inst_th then (lhs (concl inst_th), inst_th)
-        else failwith "inst_match_concl_in_terms: ignore theorem"
+        else
+          let val _ = print_dbg ("inst_match_concl_in_terms: matched failed\n") in
+          failwith "inst_match_concl_in_terms: ignore theorem" end
       end;
   in
-    inst_match_in_terms try_match tl
+    inst_match_in_terms try_match tml
   end
 
 (*
@@ -293,7 +301,7 @@ val thms = inst_match_concl_in_terms int_to_u32_id [t]
    instantiations of this theorem which make its first premise match subterms
    in the provided list of term.
  *)
-fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tl : term list) : thm list =
+fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tml : term list) : thm list =
   let
     val th = SPEC_ALL th;
     fun try_match bvars t =
@@ -304,7 +312,7 @@ fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tl : term
         else failwith "inst_match_first_premise_in_terms: ignore theorem"
       end;
   in
-    inst_match_in_terms try_match tl
+    inst_match_in_terms try_match tml
   end
 
 (*
@@ -321,13 +329,15 @@ val thms = inst_match_first_premise_in_terms th [t]
    Leaves the premises as subgoals if [prove_premise] doesn't prove them.
  *)
 fun apply_dep_rewrites_match_concl_with_terms_tac
-  (prove_premise : tactic) (then_tac : thm_tactic) (tl : term list) (th : thm) : tactic =
+  (prove_premise : tactic) (then_tac : thm_tactic)
+  (ignore_tml : term list)
+  (tml : term list) (th : thm) : tactic =
   let
-    val ignore = Redblackset.fromList Term.compare tl;
-    fun keep th = not (Redblackset.member (ignore, concl th));
+    val ignore = Redblackset.fromList Term.compare ignore_tml
+    fun keep th = not (Redblackset.member (ignore, concl th))
     (* Discharge the assumptions so that the goal is one single term *)
-    val thms = inst_match_concl_in_terms keep th tl;
-    val thms = map thm_to_conj_implies thms;
+    val thms = inst_match_concl_in_terms keep th tml
+    val thms = map thm_to_conj_implies thms
   in
     (* Apply each theorem *)
     map_every_tac (try_tac o sg_premise_then prove_premise then_tac) thms
@@ -340,14 +350,16 @@ fun apply_dep_rewrites_match_concl_with_terms_tac
  *)
 fun apply_dep_rewrites_match_concl_with_all_tac
   (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
-  fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac (g :: asms) th (asms, g)
+  fn (asms, g) =>
+  apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac asms (g :: asms) th (asms, g)
 
 (* Same as {!apply_dep_rewrites_match_concl_with_all_tac} but we only match the
    conclusion of the goal.
  *)
 fun apply_dep_rewrites_match_concl_with_goal_tac
   (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
-  fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac [g] th (asms, g)
+  fn (asms, g) =>
+  apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac asms [g] th (asms, g)
 
 (* A theorem might be of the shape: [H => A = B /\ C = D], in which
    case we can split it into:
@@ -362,7 +374,7 @@ fun split_rewrite_thm (th : thm) : thm list =
     val t = concl th;
     val (vars, t) = strip_forall t;
     val (impl, t) = strip_imp t;
-    val tl = strip_conj t;
+    val tml = strip_conj t;
     fun mk_goal (t : term) = list_mk_forall (vars, (list_mk_imp (impl, t)))
     val prove_tac =
       rpt gen_tac >> rpt disch_tac >>
@@ -375,7 +387,7 @@ fun split_rewrite_thm (th : thm) : thm list =
     fun transform_th (th : thm) : thm =
       (GEN_ALL o thm_to_conj_implies o SPEC_ALL o UNDISCH_ALL o SPEC_ALL) th
   in
-    map (transform_th o mk_th) tl
+    map (transform_th o mk_th) tml
   end
 
 (* A dependent rewrite tactic which introduces the premises in a new goal.
@@ -528,4 +540,55 @@ fun int_tac (asms, g) =
     first_tac [cooper_tac, exfalso >> cooper_tac]) (asms, g)
  end
 
+(* Repeatedly destruct cases and return the last scrutinee we get *)
+fun strip_all_cases_get_scrutinee (t : term) : term =
+  if TypeBase.is_case t
+  then
+    (* Remark.: [strip_case] is too smart for what we want.
+       For instance: (fst o strip_case) “if i = 0 then ... else ...”
+       returns “i” while we want to get “i = 0”.
+
+       We use [dest_case] for this reason.
+     *)
+    (strip_all_cases_get_scrutinee o (fn (_, x, _) => x) o TypeBase.dest_case) t
+  else t
+
+(*
+TypeBase.dest_case “case ls of [] => T | _ => F”
+TypeBase.strip_case “case ls of [] => T | _ => F”
+TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F”
+TypeBase.strip_case “3”
+TypeBase.dest_case “3”
+
+strip_all_cases_get_scrutinee “case ls of [] => T | _ => F”
+strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F”
+strip_all_cases_get_scrutinee “3”
+*)
+
+(* Lexicographic order over pairs *)
+fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order)
+  ((p1, p2) : (('a * 'b) * ('a * 'b))) : order =
+  let
+    val (x1, y1) = p1;
+    val (x2, y2) = p2;
+  in
+    case comp1 (x1, x2) of
+      LESS => LESS
+    | GREATER => GREATER
+    | EQUAL => comp2 (y1, y2)
+  end
+
+(* A constant name (theory, constant name) *)
+type const_name = string * string
+
+val const_name_compare = pair_compare String.compare String.compare
+
+(* Given a function call [f y0 ... yn] return the name of the function *)
+fun get_fun_name_from_app (t : term) : const_name =
+  let
+    val f = (fst o strip_comb) t;
+    val {Name=name, Thy=thy, Ty=_} = dest_thy_const f;
+    val cn = (thy, name);
+  in cn end
+
 end