# HG changeset patch # User wenzelm # Date 1752161365 -7200 # Node ID ca600cbfd4bfc8def14fb03ca953253e7d90d768 # Parent cd566dbe9f48eb159ae4efb28e9b5d33d38352cb more accurate "next" counter for each insert operation: subtle change of semantics wrt. Item_Net.length, due to delete operation; avoid costly Item_Net.length, which is linear in size; diff -r cd566dbe9f48 -r ca600cbfd4bf src/Provers/classical.ML --- a/src/Provers/classical.ML Thu Jul 10 15:08:26 2025 +0200 +++ b/src/Provers/classical.ML Thu Jul 10 17:29:25 2025 +0200 @@ -99,7 +99,8 @@ type info = {rl: rl, dup_rl: rl} type rule = thm * info val rep_cs: claset -> - {safeIs: rule Item_Net.T, + {next: int, + safeIs: rule Item_Net.T, safeEs: rule Item_Net.T, unsafeIs: rule Item_Net.T, unsafeEs: rule Item_Net.T, @@ -233,7 +234,8 @@ datatype claset = CS of - {safeIs: rule Item_Net.T, (*safe introduction rules*) + {next: int, (*index for next rule: decreasing*) + safeIs: rule Item_Net.T, (*safe introduction rules*) safeEs: rule Item_Net.T, (*safe elimination rules*) unsafeIs: rule Item_Net.T, (*unsafe introduction rules*) unsafeEs: rule Item_Net.T, (*unsafe elimination rules*) @@ -250,7 +252,8 @@ val empty_cs = CS - {safeIs = empty_rules, + {next = ~1, + safeIs = empty_rules, safeEs = empty_rules, unsafeIs = empty_rules, unsafeEs = empty_rules, @@ -282,13 +285,12 @@ | tag_weight_brls w k (brl::brls) = ({weight = w, index = k}, brl) :: tag_weight_brls w (k + 1) brls; -(*Insert into netpair that already has nI intr rules and nE elim rules. - Count the intr rules double (to account for swapped rules). Negate to give the +(*Insert into netpair from next index, which is negative to give the new insertions the lowest priority.*) -fun insert (nI, nE) = Bires.insert_tagged_rules o (tag_brls (~(2*nI+nE))) o joinrules; +fun insert k = Bires.insert_tagged_rules o (tag_brls (2 * k)) o joinrules; -fun insert_default_weight w0 w (nI, nE) = - Bires.insert_tagged_rules o tag_weight_brls (the_default w0 w) (~(nI + nE)) o single; +fun insert_default_weight w0 w k = + Bires.insert_tagged_rules o tag_weight_brls (the_default w0 w) k o single; fun delete x = Bires.delete_tagged_rules (joinrules x); @@ -315,7 +317,7 @@ (*** add rules ***) fun add_safe_intro w (r: rule) - (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + (cs as CS {next, safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = if Item_Net.member safeIs r then cs else @@ -323,13 +325,12 @@ val (th, {rl, ...}) = r; val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) List.partition (Thm.no_prems o fst) [rl]; - val nI = Item_Net.length safeIs + 1; - val nE = Item_Net.length safeEs; in CS - {safeIs = Item_Net.update r safeIs, - safe0_netpair = insert (nI, nE) (map fst safe0_rls, maps (the_list o snd) safe0_rls) safe0_netpair, - safep_netpair = insert (nI, nE) (map fst safep_rls, maps (the_list o snd) safep_rls) safep_netpair, + {next = next - 1, + safeIs = Item_Net.update r safeIs, + safe0_netpair = insert next (map fst safe0_rls, maps (the_list o snd) safe0_rls) safe0_netpair, + safep_netpair = insert next (map fst safep_rls, maps (the_list o snd) safep_rls) safep_netpair, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, @@ -337,11 +338,11 @@ uwrappers = uwrappers, unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, - extra_netpair = insert_default_weight 0 w (nI, nE) (false, th) extra_netpair} + extra_netpair = insert_default_weight 0 w next (false, th) extra_netpair} end; fun add_safe_elim w (r: rule) - (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + (cs as CS {next, safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = if Item_Net.member safeEs r then cs else @@ -349,13 +350,12 @@ val (th, {rl, ...}) = r; val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) List.partition (Thm.one_prem o #1) [rl]; - val nI = Item_Net.length safeIs; - val nE = Item_Net.length safeEs + 1; in CS - {safeEs = Item_Net.update r safeEs, - safe0_netpair = insert (nI, nE) ([], map fst safe0_rls) safe0_netpair, - safep_netpair = insert (nI, nE) ([], map fst safep_rls) safep_netpair, + {next = next - 1, + safeEs = Item_Net.update r safeEs, + safe0_netpair = insert next ([], map fst safe0_rls) safe0_netpair, + safep_netpair = insert next ([], map fst safep_rls) safep_netpair, safeIs = safeIs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, @@ -363,23 +363,22 @@ uwrappers = uwrappers, unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, - extra_netpair = insert_default_weight 0 w (nI, nE) (true, th) extra_netpair} + extra_netpair = insert_default_weight 0 w next (true, th) extra_netpair} end; fun add_unsafe_intro w (r: rule) - (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + (cs as CS {next, safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = if Item_Net.member unsafeIs r then cs else let val (th, {rl, dup_rl}) = r; - val nI = Item_Net.length unsafeIs + 1; - val nE = Item_Net.length unsafeEs; in CS - {unsafeIs = Item_Net.update r unsafeIs, - unsafe_netpair = insert (nI, nE) ([fst rl], the_list (snd rl)) unsafe_netpair, - dup_netpair = insert (nI, nE) ([fst dup_rl], the_list (snd dup_rl)) dup_netpair, + {next = next - 1, + unsafeIs = Item_Net.update r unsafeIs, + unsafe_netpair = insert next ([fst rl], the_list (snd rl)) unsafe_netpair, + dup_netpair = insert next ([fst dup_rl], the_list (snd dup_rl)) dup_netpair, safeIs = safeIs, safeEs = safeEs, unsafeEs = unsafeEs, @@ -387,23 +386,22 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - extra_netpair = insert_default_weight 1 w (nI, nE) (false, th) extra_netpair} + extra_netpair = insert_default_weight 1 w next (false, th) extra_netpair} end; fun add_unsafe_elim w (r: rule) - (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + (cs as CS {next, safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = if Item_Net.member unsafeEs r then cs else let val (th, {rl, dup_rl}) = r; - val nI = Item_Net.length unsafeIs; - val nE = Item_Net.length unsafeEs + 1; in CS - {unsafeEs = Item_Net.update r unsafeEs, - unsafe_netpair = insert (nI, nE) ([], [fst rl]) unsafe_netpair, - dup_netpair = insert (nI, nE) ([], [fst dup_rl]) dup_netpair, + {next = next - 1, + unsafeEs = Item_Net.update r unsafeEs, + unsafe_netpair = insert next ([], [fst rl]) unsafe_netpair, + dup_netpair = insert next ([], [fst dup_rl]) dup_netpair, safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, @@ -411,7 +409,7 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - extra_netpair = insert_default_weight 1 w (nI, nE) (true, th) extra_netpair} + extra_netpair = insert_default_weight 1 w next (true, th) extra_netpair} end; fun trim_context_rl (th1, opt_th2) = @@ -470,14 +468,15 @@ local fun del_safe_intro (r: rule) - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + (CS {next, safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = let val (th, {rl, ...}) = r; val (safe0_rls, safep_rls) = List.partition (Thm.no_prems o fst) [rl]; in CS - {safe0_netpair = delete (map fst safe0_rls, maps (the_list o snd) safe0_rls) safe0_netpair, + {next = next, + safe0_netpair = delete (map fst safe0_rls, maps (the_list o snd) safe0_rls) safe0_netpair, safep_netpair = delete (map fst safep_rls, maps (the_list o snd) safep_rls) safep_netpair, safeIs = Item_Net.remove r safeIs, safeEs = safeEs, @@ -491,14 +490,15 @@ end; fun del_safe_elim (r: rule) - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + (CS {next, safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = let val (th, {rl, ...}) = r; val (safe0_rls, safep_rls) = List.partition (Thm.one_prem o #1) [rl]; in CS - {safe0_netpair = delete ([], map fst safe0_rls) safe0_netpair, + {next = next, + safe0_netpair = delete ([], map fst safe0_rls) safe0_netpair, safep_netpair = delete ([], map fst safep_rls) safep_netpair, safeIs = safeIs, safeEs = Item_Net.remove r safeEs, @@ -512,10 +512,11 @@ end; fun del_unsafe_intro (r as (th, {rl = (th', swapped_th'), dup_rl = (dup_th', swapped_dup_th')})) - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + (CS {next, safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = CS - {unsafe_netpair = delete ([th'], the_list swapped_th') unsafe_netpair, + {next = next, + unsafe_netpair = delete ([th'], the_list swapped_th') unsafe_netpair, dup_netpair = delete ([dup_th'], the_list swapped_dup_th') dup_netpair, safeIs = safeIs, safeEs = safeEs, @@ -528,10 +529,11 @@ extra_netpair = delete ([th], []) extra_netpair}; fun del_unsafe_elim (r as (th, {rl = (th', _), dup_rl = (dup_th', _)})) - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + (CS {next, safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = CS - {unsafe_netpair = delete ([], [th']) unsafe_netpair, + {next = next, + unsafe_netpair = delete ([], [th']) unsafe_netpair, dup_netpair = delete ([], [dup_th']) dup_netpair, safeIs = safeIs, safeEs = safeEs, @@ -577,17 +579,17 @@ (* wrappers *) fun map_swrappers f - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + (CS {next, safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, + CS {next = next, safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, swrappers = f swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; fun map_uwrappers f - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + (CS {next, safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, + CS {next = next, safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, swrappers = swrappers, uwrappers = f uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair};