added re-hash-consing of URIs embedded in universes

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 *)

diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli
index 71ad1ef00b7b73f5e10092c97f723d4ffcfc50d7..d2b2483a19b5b331b7c9a601d5ebe674e9051950 100644 (file)
--- a/helm/ocaml/cic/cicUniv.mli
+++ b/helm/ocaml/cic/cicUniv.mli
@@ -113,6 +113,11 @@ val ugraph_of_xml:
 val restart_numbering:
   unit -> unit
 
+  (** re-hash-cons URIs contained in the given universe so that phisicaly
+   * equality could be enforced. Mainly used by
+   * CicEnvironment.restore_from_channel *)
+val recons_graph: universe_graph -> universe_graph
+
 (*
   Benchmarking stuff
 *)

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 6ad00d7643d948e2d8144a8b05b339893caa8729..42f0b3880e676e4bcdfac8e200c912dd978ddeb5 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -299,7 +299,7 @@ module Cache :
             (***********************************************
                TSSI: FIXME add channel stuff for universes
             ************************************************)
-           (restore_uris v,u))
+           (restore_uris v, CicUniv.recons_graph u))
        restored
     ;;