oldenv2newenv cache

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 278f7fff5802764d013951d9f457532c703a46ef..9549f3c3cbcd92f260762b9e3aa5cf5ab8d0963a 100644 (file)
--- 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 20945d08d4479bd5d8fb367458e074a9aafeb623..76519843950daf401345169620af4e157b64dc83 100644 (file)
--- 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 ad93584fbc2a7ed3281df5018e13368e6cc6fda3..9d9ed88a6a4098b18c446d530bade36934e8171f 100644 (file)
--- 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 1b7d519431ed419d92791269553d24b3e9f802f0..7e8cf40df876c5b4a084e35898a7a448c0c542aa 100644 (file)
--- 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 d0dcb723a2c95903b7743beebe9fca6c6c7c9aa9..7330babd6c609fb210c9b74ad9f4904fa3857384 100644 (file)
--- 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