2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 exception ObjectNotFound of string Lazy.t
16 let storage = ref [];;
18 let aliases = ref [];;
23 (fun (name',nref) -> if name'=name then Some nref else None) !aliases
25 Not_found -> raise (ObjectNotFound (lazy name))
29 storage := (u,obj)::!storage;
30 let _,height,_,_,obj = obj in
33 NCic.Constant (_,name,None,_,_) ->
34 [name,NReference.reference_of_spec u NReference.Decl]
35 | NCic.Constant (_,name,Some _,_,_) ->
36 [name,NReference.reference_of_spec u (NReference.Def height)]
37 | NCic.Fixpoint (is_ind,fl,_) ->
39 (fun (_,name,recno,_,_) i ->
41 name,NReference.reference_of_spec u (NReference.Fix(i,recno,height))
43 name,NReference.reference_of_spec u (NReference.CoFix i)) fl
44 | NCic.Inductive (inductive,leftno,il,_) ->
47 (fun (_,iname,_,cl) i ->
50 cname,NReference.reference_of_spec u (NReference.Con (i,j,leftno))
53 NReference.reference_of_spec u
54 (NReference.Ind (inductive,i,leftno))]
57 aliases := references @ !aliases
60 let cache = NUri.UriHash.create 313;;
63 try List.assq u !storage
65 try NUri.UriHash.find cache u
67 (* in the final implementation should get it from disk *)
68 let ouri = NCic2OCic.ouri_of_nuri u in
70 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
71 let l = OCic2NCic.convert_obj ouri o in
72 List.iter (fun (u,_,_,_,_ as o) ->
73 (* prerr_endline ("+"^NUri.string_of_uri u); *)
74 NUri.UriHash.add cache u o) l;
76 with CicEnvironment.Object_not_found u ->
78 (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u))))
81 let clear_cache () = NUri.UriHash.clear cache;;