From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 5 Feb 2008 16:06:20 +0000 (+0000)
Subject: oldenv2newenv cache
X-Git-Tag: make_still_working~5630
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=05e05dd130ec57395615de286ee50c6729d226ac;p=helm.git

oldenv2newenv cache
---

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 278f7fff5..9549f3c3c 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -1,8 +1,13 @@
+let cache = NUri.UriHash.create 313;;
 
-let get_checked_obj reference =
-  let ouri = NReference.ouri_of_reference reference in
-  let o,_ = 
-    CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph 
-      ouri 
-  in
-    OCic2NCic.convert_obj o
+let get_checked_obj u =
+  try NUri.UriHash.find cache u
+  with Not_found ->
+    let ouri = NUri.ouri_of_nuri u in
+    let o,_ = 
+      CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph 
+        ouri in
+    let no = OCic2NCic.convert_obj o in
+    NUri.UriHash.add cache u no;
+    no
+;;
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 20945d08d..765198439 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -26,6 +26,6 @@
 (* NG: minimal wrapper on the old cicEnvironment, should provide only the
  * functions strictly necessary to the typechecking algorithm *)
 
-val get_checked_obj : NReference.reference -> NCic.obj
+val get_checked_obj : NUri.uri -> NCic.obj
 
 (* EOF *)
diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml
index ad93584fb..9d9ed88a6 100644
--- a/helm/software/components/ng_kernel/nReference.ml
+++ b/helm/software/components/ng_kernel/nReference.ml
@@ -116,10 +116,8 @@ let string_of_reference (Ref (_,u,indinfo)) =
 ;;
 
 let reference_of_ouri u indinfo =
-  let u = NUri.uri_of_string (UriManager.string_of_uri u) in
+  let u = NUri.nuri_of_ouri u in
   reference_of_string (string_of_reference (Ref (~-1,u,indinfo)))
 ;;
 
-let ouri_of_reference (Ref (_,u,_)) =
-  UriManager.uri_of_string (NUri.string_of_uri u)
-;;
+let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;;
diff --git a/helm/software/components/ng_kernel/nUri.ml b/helm/software/components/ng_kernel/nUri.ml
index 1b7d51943..7e8cf40df 100644
--- a/helm/software/components/ng_kernel/nUri.ml
+++ b/helm/software/components/ng_kernel/nUri.ml
@@ -35,3 +35,7 @@ module HT = struct
 end;;
 
 module UriHash = Hashtbl.Make(HT);;
+
+let ouri_of_nuri u = UriManager.uri_of_string (string_of_uri u);;
+let nuri_of_ouri o = uri_of_string (UriManager.string_of_uri o);;
+
diff --git a/helm/software/components/ng_kernel/nUri.mli b/helm/software/components/ng_kernel/nUri.mli
index d0dcb723a..7330babd6 100644
--- a/helm/software/components/ng_kernel/nUri.mli
+++ b/helm/software/components/ng_kernel/nUri.mli
@@ -5,3 +5,7 @@ val uri_of_string: string -> uri
 val eq: uri -> uri -> bool
 
 module UriHash: Hashtbl.S with type key = uri
+
+(* CACCA *)
+val ouri_of_nuri: uri -> UriManager.uri
+val nuri_of_ouri: UriManager.uri -> uri