added re-hash-consing of URIs embedded in universes

[helm.git] / helm / ocaml / cic / cicUniv.ml

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index 7e6bde44ebcb2b29000171317e69efadf7c80909..44bccc62b281715cbb7c35d882747dd8f25f157a 100644 (file)
--- a/helm/ocaml/cic/cicUniv.ml
+++ b/helm/ocaml/cic/cicUniv.ml
@@ -903,4 +903,30 @@ let _ =
 
  *)
 
+let recons_univ u =
+  match u with
+  | i, None -> u
+  | i, Some uri ->
+      i, Some (UriManager.uri_of_string (UriManager.string_of_uri uri))
+
+let recons_entry entry =
+  let recons_set set =
+    SOF.fold (fun univ set -> SOF.add (recons_univ univ) set) set SOF.empty
+  in
+  {
+    eq_closure = recons_set entry.eq_closure;
+    ge_closure = recons_set entry.ge_closure;
+    gt_closure = recons_set entry.gt_closure;
+    in_gegt_of = recons_set entry.in_gegt_of;
+    one_s_eq = recons_set entry.one_s_eq;
+    one_s_ge = recons_set entry.one_s_ge;
+    one_s_gt = recons_set entry.one_s_gt;
+  }
+
+let recons_graph graph =
+  MAL.fold
+    (fun universe entry map ->
+      MAL.add (recons_univ universe) (recons_entry entry) map)
+    graph MAL.empty
+
 (* EOF *)