From 20003022e190826cee7f56e2de281815518c0966 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 27 Apr 2005 13:43:15 +0000
Subject: [PATCH] added re-hash-consing of URIs embedded in universes

---
 helm/ocaml/cic/cicUniv.ml                     | 26 +++++++++++++++++++
 helm/ocaml/cic/cicUniv.mli                    |  5 ++++
 .../cic_proof_checking/cicEnvironment.ml      |  2 +-
 3 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index 7e6bde44e..44bccc62b 100644
--- 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 71ad1ef00..d2b2483a1 100644
--- 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 6ad00d764..42f0b3880 100644
--- 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
     ;;
 
-- 
2.39.2