# HG changeset patch
# User wenzelm
# Date 1751806400 -7200
# Node ID be1fb22d9e2a1355aedeabad30f64c95b199b639
# Parent  ad5a3159b95dc498247588779252af94528d92e6
clarified signature: more explicit type Bires.kind;

diff -r ad5a3159b95d -r be1fb22d9e2a src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sun Jul 06 13:58:41 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sun Jul 06 14:53:20 2025 +0200
@@ -37,35 +37,11 @@
 
 (** rule declaration contexts **)
 
-(* rule kinds *)
-
-val intro_bangK = (0, false);
-val elim_bangK = (0, true);
-val introK = (1, false);
-val elimK = (1, true);
-val intro_queryK = (2, false);
-val elim_queryK = (2, true);
-
-val kind_names =
- [(intro_bangK, "safe introduction rules (intro!)"),
-  (elim_bangK, "safe elimination rules (elim!)"),
-  (introK, "introduction rules (intro)"),
-  (elimK, "elimination rules (elim)"),
-  (intro_queryK, "extra introduction rules (intro?)"),
-  (elim_queryK, "extra elimination rules (elim?)")];
-
-val rule_kinds = map #1 kind_names;
-val rule_indexes = distinct (op =) (map #1 rule_kinds);
-
-
 (* context data *)
 
-val empty_netpairs: Bires.netpair list =
-  replicate (length rule_indexes) Bires.empty_netpair;
-
 datatype rules = Rules of
  {next: int,
-  rules: (int * ((int * bool) * thm)) list,
+  rules: (int * (Bires.kind * thm)) list,
   netpairs: Bires.netpair list,
   wrappers:
     ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list *
@@ -74,23 +50,25 @@
 fun make_rules next rules netpairs wrappers =
   Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
 
-fun add_rule (i, b) opt_weight th (Rules {next, rules, netpairs, wrappers}) =
+fun add_rule kind opt_weight th (Rules {next, rules, netpairs, wrappers}) =
   let
-    val weight = opt_weight |> \<^if_none>\<open>Bires.subgoals_of (b, th)\<close>;
+    val weight = opt_weight |> \<^if_none>\<open>Bires.subgoals_of (Bires.kind_rule kind th)\<close>;
     val tag = {weight = weight, index = next};
     val th' = Thm.trim_context th;
-  in
-    make_rules (next - 1) ((weight, ((i, b), th')) :: rules)
-      (nth_map i (Bires.insert_tagged_rule (tag, (b, th'))) netpairs) wrappers
-  end;
+    val rules' = (weight, (kind, th')) :: rules;
+    val netpairs' = netpairs
+      |> Bires.kind_map kind (Bires.insert_tagged_rule (tag, Bires.kind_rule kind th'));
+  in make_rules (next - 1) rules' netpairs' wrappers end;
 
 fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) =
   let
     fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
     fun del b netpair = Bires.delete_tagged_rule (b, th) netpair handle Net.DELETE => netpair;
+    val rules' = filter_out eq_th rules;
+    val netpairs' = map (del false o del true) netpairs;
   in
     if not (exists eq_th rules) then rs
-    else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
+    else make_rules next rules' netpairs' wrappers
   end;
 
 fun del_rule th = del_rule0 th o del_rule0 (Tactic.make_elim th);
@@ -98,7 +76,7 @@
 structure Data = Generic_Data
 (
   type T = rules;
-  val empty = make_rules ~1 [] empty_netpairs ([], []);
+  val empty = make_rules ~1 [] Bires.kind_netpairs ([], []);
   fun merge
     (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
       Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
@@ -108,21 +86,23 @@
       val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
           k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
       val next = ~ (length rules);
-      val netpairs = fold (fn (index, (weight, ((i, b), th))) =>
-          nth_map i (Bires.insert_tagged_rule ({weight = weight, index = index}, (b, th))))
-        (next upto ~1 ~~ rules) empty_netpairs;
+      val netpairs =
+        fold (fn (index, (weight, (kind, th))) =>
+          Bires.kind_map kind
+            (Bires.insert_tagged_rule ({weight = weight, index = index}, (Bires.kind_elim kind, th))))
+        (next upto ~1 ~~ rules) Bires.kind_netpairs;
     in make_rules (next - 1) rules netpairs wrappers end;
 );
 
 fun print_rules ctxt =
   let
     val Rules {rules, ...} = Data.get (Context.Proof ctxt);
-    fun prt_kind (i, b) =
-      Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
-        (map_filter (fn (_, (k, th)) =>
-            if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE)
+    fun prt_kind kind =
+      Pretty.big_list (Bires.kind_title kind ^ ":")
+        (map_filter (fn (_, (kind', th)) =>
+            if kind = kind' then SOME (Thm.pretty_thm_item ctxt th) else NONE)
           (sort (int_ord o apply2 fst) rules));
-  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
+  in Pretty.writeln (Pretty.chunks (map prt_kind Bires.kind_domain)) end;
 
 
 (* access data *)
@@ -188,15 +168,15 @@
 fun rule_add k view opt_w =
   Thm.declaration_attribute (fn th => Data.map (add_rule k opt_w (view th) o del_rule th));
 
-val intro_bang  = rule_add intro_bangK I;
-val elim_bang   = rule_add elim_bangK I;
-val dest_bang   = rule_add elim_bangK Tactic.make_elim;
-val intro       = rule_add introK I;
-val elim        = rule_add elimK I;
-val dest        = rule_add elimK Tactic.make_elim;
-val intro_query = rule_add intro_queryK I;
-val elim_query  = rule_add elim_queryK I;
-val dest_query  = rule_add elim_queryK Tactic.make_elim;
+val intro_bang  = rule_add Bires.intro_bang_kind I;
+val elim_bang   = rule_add Bires.elim_bang_kind I;
+val dest_bang   = rule_add Bires.elim_bang_kind Tactic.make_elim;
+val intro       = rule_add Bires.intro_kind I;
+val elim        = rule_add Bires.elim_kind I;
+val dest        = rule_add Bires.elim_kind Tactic.make_elim;
+val intro_query = rule_add Bires.intro_query_kind I;
+val elim_query  = rule_add Bires.elim_query_kind I;
+val dest_query  = rule_add Bires.elim_query_kind Tactic.make_elim;
 
 val _ = Theory.setup
   (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]);
diff -r ad5a3159b95d -r be1fb22d9e2a src/Pure/bires.ML
--- a/src/Pure/bires.ML	Sun Jul 06 13:58:41 2025 +0200
+++ b/src/Pure/bires.ML	Sun Jul 06 14:53:20 2025 +0200
@@ -35,6 +35,21 @@
   val filt_resolve_from_net_tac: Proof.context -> int -> net -> int -> tactic
   val resolve_from_net_tac: Proof.context -> net -> int -> tactic
   val match_from_net_tac: Proof.context -> net -> int -> tactic
+
+  eqtype kind
+  val intro_bang_kind: kind
+  val elim_bang_kind: kind
+  val intro_kind: kind
+  val elim_kind: kind
+  val intro_query_kind: kind
+  val elim_query_kind: kind
+  val kind_index: kind -> int
+  val kind_elim: kind -> bool
+  val kind_domain: kind list
+  val kind_netpairs: netpair list
+  val kind_map: kind -> ('a -> 'a) -> 'a list -> 'a list
+  val kind_rule: kind -> thm -> rule
+  val kind_title: kind -> string
 end
 
 structure Bires: BIRES =
@@ -121,6 +136,42 @@
 fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt tag_ord NONE true;
 
 
+(** Rule kinds and declarations **)
+
+datatype kind = Kind of int * bool;
+
+val intro_bang_kind = Kind (0, false);
+val elim_bang_kind = Kind (0, true);
+val intro_kind = Kind (1, false);
+val elim_kind = Kind (1, true);
+val intro_query_kind = Kind (2, false);
+val elim_query_kind = Kind (2, true);
+
+val kind_infos =
+ [(intro_bang_kind, ("safe introduction", "(intro!)")),
+  (elim_bang_kind, ("safe elimination", "(elim!)")),
+  (intro_kind, ("introduction", "(intro)")),
+  (elim_kind, ("elimination", "(elim)")),
+  (intro_query_kind, ("extra introduction", "(intro?)")),
+  (elim_query_kind, ("extra elimination", "(elim?)"))];
+
+fun kind_index (Kind (i, _)) = i;
+fun kind_elim (Kind (_, b)) = b;
+
+val kind_domain = map #1 kind_infos;
+val kind_netpairs =
+  replicate (length (distinct (op =) (map kind_index kind_domain))) empty_netpair;
+
+fun kind_map kind f = nth_map (kind_index kind) f;
+fun kind_rule kind thm : rule = (kind_elim kind, thm);
+
+val the_kind_info = the o AList.lookup (op =) kind_infos;
+
+fun kind_title kind =
+  let val (a, b) = the_kind_info kind
+  in a ^ " rules " ^ b end;
+
+
 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
 
 type net = (int * thm) Net.net;
@@ -150,4 +201,3 @@
 fun match_from_net_tac ctxt = filt_resolution_from_net_tac ctxt true (K true);
 
 end;
-