From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 May 2008 16:51:14 +0000 (+0000)
Subject: Library factorized out.
X-Git-Tag: make_still_working~5225
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cf2b1084c561a6842d7cbc5691943ef53b151aca;hp=e0ac9442fc6cc033a3a5bb9d7288b9ce5da99767;p=helm.git

Library factorized out.
---

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
new file mode 100644
index 000000000..f25a0c54c
--- /dev/null
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -0,0 +1,27 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+exception ObjectNotFound of string Lazy.t
+
+let cache = NUri.UriHash.create 313;;
+
+let get_obj u =
+  try NUri.UriHash.find cache u
+  with Not_found ->
+    (* in the final implementation should get it from disk *)
+    let ouri = NUri.ouri_of_nuri u in
+    let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
+    let l = OCic2NCic.convert_obj ouri o in
+    List.iter (fun (u,_,_,_,_ as o) -> 
+(*       prerr_endline ("+"^NUri.string_of_uri u);  *)
+      NUri.UriHash.add cache u o) l;
+    HExtlib.list_last l
+;;
diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
new file mode 100644
index 000000000..ca1aed271
--- /dev/null
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -0,0 +1,19 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* NG: minimal wrapper on the old cicEnvironment, should provide only the
+ * functions strictly necessary to the typechecking algorithm *)
+
+exception ObjectNotFound of string Lazy.t
+
+val get_obj: NUri.uri -> NCic.obj
+
+(* EOF *)