# HG changeset patch # User wenzelm # Date 1752227563 -7200 # Node ID 60ec2b2dc55a58dcd1cfed70c22361659531784c # Parent ca600cbfd4bfc8def14fb03ca953253e7d90d768 clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule); diff -r ca600cbfd4bf -r 60ec2b2dc55a src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Thu Jul 10 17:29:25 2025 +0200 +++ b/src/Pure/Isar/context_rules.ML Fri Jul 11 11:52:43 2025 +0200 @@ -37,10 +37,26 @@ (** rule declaration contexts **) +(* rule declarations *) + +type decl = thm Bires.decl; +type decls = thm Bires.decls; + +fun init_decl kind opt_weight th : decl = + let val weight = opt_weight |> \<^if_none>\Bires.subgoals_of (Bires.kind_rule kind th)\; + in {kind = kind, tag = Bires.weight_tag weight, info = th} end; + +fun insert_decl ({kind, tag, info = th}: decl) = + Bires.insert_tagged_rule (tag, Bires.kind_rule kind th); + +fun remove_decl ({info = th, ...}: decl) = + Bires.delete_tagged_rule (false, th) o Bires.delete_tagged_rule (true, th); + + (* context data *) datatype rules = Rules of - {decls: unit Bires.decls, + {decls: decls, netpairs: Bires.netpair list, wrappers: ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list * @@ -51,21 +67,24 @@ fun add_rule kind opt_weight th (rules as Rules {decls, netpairs, wrappers}) = let - val weight = opt_weight |> \<^if_none>\Bires.subgoals_of (Bires.kind_rule kind th)\; - val decl = {kind = kind, tag = Bires.weight_tag weight, info = ()}; + val th' = Thm.trim_context th; + val decl' = init_decl kind opt_weight th'; in - (case Bires.extend_decls (Thm.trim_context th, decl) decls of - NONE => rules - | SOME (new_rule, decls') => - let val netpairs' = netpairs |> Bires.kind_map kind (Bires.insert_rule new_rule) + (case Bires.extend_decls (th', decl') decls of + (NONE, _) => rules + | (SOME new_decl, decls') => + let val netpairs' = Bires.kind_map kind (insert_decl new_decl) netpairs in make_rules decls' netpairs' wrappers end) end; fun del_rule0 th (rules as Rules {decls, netpairs, wrappers}) = (case Bires.remove_decls th decls of - NONE => rules - | SOME decls' => - let val netpairs' = map (Bires.remove_rule th) netpairs + ([], _) => rules + | (old_decls, decls') => + let + val netpairs' = + fold (fn decl as {kind, ...} => Bires.kind_map kind (remove_decl decl)) + old_decls netpairs; in make_rules decls' netpairs' wrappers end); fun del_rule th = del_rule0 th o del_rule0 (Tactic.make_elim th); @@ -81,8 +100,8 @@ val (new_rules, decls) = Bires.merge_decls (decls1, decls2); val netpairs = netpairs1 |> map_index (uncurry (fn i => - new_rules |> fold (fn (th, decl) => - Bires.kind_index (#kind decl) = i ? Bires.insert_rule (th, decl)))); + new_rules |> fold (fn decl => + if Bires.kind_index (#kind decl) = i then insert_decl decl else I))) val wrappers = (Library.merge (eq_snd (op =)) (ws1, ws2), Library.merge (eq_snd (op =)) (ws1', ws2')); diff -r ca600cbfd4bf -r 60ec2b2dc55a src/Pure/bires.ML --- a/src/Pure/bires.ML Thu Jul 10 17:29:25 2025 +0200 +++ b/src/Pure/bires.ML Fri Jul 11 11:52:43 2025 +0200 @@ -39,11 +39,12 @@ val decl_ord: 'a decl ord type 'a decls val has_decls: 'a decls -> thm -> bool + val get_decls: 'a decls -> thm -> 'a decl list val list_decls: (thm * 'a decl -> bool) -> 'a decls -> (thm * 'a decl) list val pretty_decls: Proof.context -> kind list -> 'a decls -> Pretty.T list - val merge_decls: 'a decls * 'a decls -> (thm * 'a decl) list * 'a decls - val extend_decls: thm * 'a decl -> 'a decls -> ((thm * 'a decl) * 'a decls) option - val remove_decls: thm -> 'a decls -> 'a decls option + val merge_decls: 'a decls * 'a decls -> 'a decl list * 'a decls + val extend_decls: thm * 'a decl -> 'a decls -> 'a decl option * 'a decls + val remove_decls: thm -> 'a decls -> 'a decl list * 'a decls val empty_decls: 'a decls type netpair = (tag * rule) Net.net * (tag * rule) Net.net @@ -52,8 +53,6 @@ val insert_tagged_rules: (tag * rule) list -> netpair -> netpair val delete_tagged_rule: rule -> netpair -> netpair val delete_tagged_rules: rule list -> netpair -> netpair - val insert_rule: thm * 'a decl -> netpair -> netpair - val remove_rule: thm -> netpair -> netpair val biresolution_from_nets_tac: Proof.context -> tag ord -> (rule -> bool) option -> bool -> netpair -> int -> tactic @@ -169,12 +168,14 @@ let val decl' = next_decl next decl; val decls' = Decls {next = next - 1, rules = Thmtab.cons_list (thm, decl') rules}; - in ((thm, decl'), decls') end; + in (decl', decls') end; in fun has_decls (Decls {rules, ...}) = Thmtab.defined rules; +fun get_decls (Decls {rules, ...}) = Thmtab.lookup_list rules; + fun list_decls pred = dest_decls pred #> sort (rev_order o decl_ord o apply2 #2); @@ -189,13 +190,13 @@ decls1 |> fold_map add_decls (list_decls (not o dup_decls decls1) decls2); fun extend_decls (thm, decl) decls = - if dup_decls decls (thm, decl) then NONE - else SOME (add_decls (thm, decl) decls); + if dup_decls decls (thm, decl) then (NONE, decls) + else add_decls (thm, decl) decls |>> SOME; fun remove_decls thm (decls as Decls {next, rules}) = - if has_decls decls thm - then SOME (Decls {next = next, rules = Thmtab.delete thm rules}) - else NONE; + (case get_decls decls thm of + [] => ([], decls) + | old_decls => (old_decls, Decls {next = next, rules = Thmtab.delete thm rules})); val empty_decls = Decls {next = ~1, rules = Thmtab.empty}; @@ -242,13 +243,6 @@ fun delete_tagged_rules rls = fold_rev delete_tagged_rule rls; -fun insert_rule (thm, {kind, tag, ...}: 'a decl) netpair = - insert_tagged_rule (tag, kind_rule kind thm) netpair; - -fun remove_rule thm = - delete_tagged_rule (false, thm) o delete_tagged_rule (true, thm); - - (*biresolution using a pair of nets rather than rules: boolean "match" indicates matching or unification.*) fun biresolution_from_nets_tac ctxt ord pred match ((inet, enet): netpair) =