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 (file)
index 0000000..f25a0c5
--- /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 (file)
index 0000000..ca1aed2
--- /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 *)