diff --git a/src/basis/PersistentTable.ml b/src/basis/PersistentTable.ml index 67bf228be..62bdde23c 100644 --- a/src/basis/PersistentTable.ml +++ b/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 diff --git a/src/basis/PersistentTable.mli b/src/basis/PersistentTable.mli index 5c8f77de2..499b4f37a 100644 --- a/src/basis/PersistentTable.mli +++ b/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 diff --git a/src/core/NewRestriction.ml b/src/core/NewRestriction.ml index 83d574ea0..b0e04fca0 100644 --- a/src/core/NewRestriction.ml +++ b/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 =