Termcode.Pairing: fixed two bugs

src/session/termcode.ml

@@ -370,7 +370,7 @@ module Pairing(Old: S)(New: S) = struct
 
   type any_goal = Old of Old.t | New of New.t
 
-  (* doubly linked lists *)
+  (* doubly linked lists; left and right bounds point to themselves *)
 
   type node = {
     mutable  prev: node;
@@ -390,6 +390,13 @@ module Pairing(Old: S)(New: S) = struct
 
   let build_list = iter_pairs (fun x y -> x.next <- y; y.prev <- x)
 
+  let remove x =
+    x.valid <- false;
+    let p = x.prev and n = x.next in
+    if p == x then n.prev <- n (* left bound *)
+    else if n == x then p.next <- p (* right bound *)
+    else begin p.next <- n; n.prev <- p end
+
   (* priority queues for pairs of nodes *)
 
   module E = struct
@@ -444,14 +451,13 @@ module Pairing(Old: S)(New: S) = struct
       while not (PQ.is_empty pq) do
         let _, (x, y) = PQ.extract_min pq in
         if x.valid && y.valid then begin
-          x.valid <- false; y.valid <- false;
           let o, n = match x.elt, y.elt with
             | New n, Old o | Old o, New n -> o, n | _ -> assert false in
           dprintf "[assoc] new pairing@.";
           result.(new_goal_index n) <- n, Some (o, true);
           if x.prev != x && y.next != y then add x.prev y.next;
-          if x.prev != x then x.prev.next <- y.next else y.next.prev <- y.next;
-          if y.next != y then y.next.prev <- x.prev else x.prev.next <- x.prev
+          remove x;
+          remove y
         end
       done
     end;

src/util/pqueue.ml

@@ -52,7 +52,7 @@ end
 module Make(X: Set.OrderedType) = struct
   type elt = X.t
   type t = elt RA.t
-  let create ~dummy = RA.make 16 dummy
+  let create ~dummy = RA.make 0 dummy
   let is_empty h = RA.length h = 0
   let clear h = RA.resize h 0