New, better algorithm.

src/basis/PersistentTable.ml

@@ -7,6 +7,7 @@ sig
   val set : 'k -> 'a -> ('k, 'a) t -> ('k, 'a) t
   val mem : 'k -> ('k, 'a) t -> bool
   val remove : 'k -> ('k, 'a) t -> ('k, 'a) t
+  val set_opt : 'k -> 'a option -> ('k, 'a) t -> ('k, 'a) t
   val find : 'k -> ('k, 'a) t -> 'a option
   val fold : ('k-> 'a -> 'b -> 'b) -> ('k, 'a) t -> 'b -> 'b
   val merge : ('k, 'a) t -> ('k, 'a) t -> ('k, 'a) t
@@ -24,7 +25,7 @@ struct
   let init ~size =
     ref @@ Tbl (Hashtbl.create size)
 
-  let set_opt tbl k ov =
+  let raw_set_opt tbl k ov =
     match ov with
     | None -> Hashtbl.remove tbl k
     | Some v -> Hashtbl.replace tbl k v
@@ -39,7 +40,7 @@ struct
         match !t' with
         | Tbl a as n ->
           let ov' = Hashtbl.find_opt a k in
-          set_opt a k ov;
+          raw_set_opt a k ov;
           t := n;
           t' := Diff (k, ov', t)
         | _ ->
@@ -104,6 +105,11 @@ struct
     | _ ->
       raise Fatal
 
+  let set_opt k ov t =
+    match ov with
+    | None -> remove k t
+    | Some v -> set k v t
+
   let fold f t e =
     reroot t;
     match !t with

src/basis/PersistentTable.mli

@@ -9,6 +9,7 @@ sig
   val set : 'k -> 'a -> ('k, 'a) t -> ('k, 'a) t
   val mem : 'k -> ('k, 'a) t -> bool
   val remove : 'k -> ('k, 'a) t -> ('k, 'a) t
+  val set_opt : 'k -> 'a option -> ('k, 'a) t -> ('k, 'a) t
   val find : 'k -> ('k, 'a) t -> 'a option
   val fold : ('k -> 'a -> 'b -> 'b) -> ('k, 'a) t -> 'b -> 'b
   val merge : ('k, 'a) t -> ('k, 'a) t -> ('k, 'a) t

src/core/NewRestriction.ml

@@ -158,10 +158,10 @@ let subst' r x h =
   get_m h @@ subst r x h
 
 let swap (x : atom) (y : atom) (h : t) =
-  if x == y then h else
-  let x', h = reserve_index_aux x h in
-  let y', h = reserve_index_aux y h in
-  {h with index = T.set y x' (T.set x y' h.index)}
+  match T.find x h.index, T.find y h.index with
+  | None, None -> h
+  | Some idx, Some idy when idx = idy -> h
+  | oidx, oidy -> {h with index = T.set_opt y oidx (T.set_opt x oidy h.index)}
 
 
 let pp_cls fmt =