diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-02 21:22:55 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-18 17:22:29 +0200 |
commit | 6795bc07f53a842bcec76ad0329d0b4444a625ab (patch) | |
tree | 22dedb36cd806f7c145ed2a85206eba84410166e /kernel/uGraph.ml | |
parent | beb3acd2fd3831404f0be2da61d3f28e210e8349 (diff) |
Replacing costly merges in UGraph.
Diffstat (limited to 'kernel/uGraph.ml')
-rw-r--r-- | kernel/uGraph.ml | 16 |
1 files changed, 9 insertions, 7 deletions
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 = |