more accurate "next" counter for each insert operation: subtle change of semantics wrt. Item_Net.length, due to delete operation;
authorwenzelm
Thu, 10 Jul 2025 17:29:25 +0200
changeset 82838 ca600cbfd4bf
parent 82837 cd566dbe9f48
child 82839 60ec2b2dc55a
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;
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};