From 6795bc07f53a842bcec76ad0329d0b4444a625ab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 2 Apr 2017 21:22:55 +0200 Subject: Replacing costly merges in UGraph. --- kernel/uGraph.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'kernel/uGraph.ml') diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 4884d0deb..6971c0a2b 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -354,13 +354,15 @@ let get_new_edges g to_merge = UMap.empty to_merge in let ltle = - UMap.fold (fun _ n acc -> - UMap.merge (fun _ strict1 strict2 -> - match strict1, strict2 with - | Some true, _ | _, Some true -> Some true - | _, _ -> Some false) - acc n.ltle) - to_merge_lvl UMap.empty + let fold _ n acc = + let fold u strict acc = + if strict then UMap.add u strict acc + else if UMap.mem u acc then acc + else UMap.add u false acc + in + UMap.fold fold n.ltle acc + in + UMap.fold fold to_merge_lvl UMap.empty in let ltle, _ = clean_ltle g ltle in let ltle = -- cgit v1.2.3