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))
31 (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !aliases
33 Not_found -> raise (ObjectNotFound (lazy (NUri.string_of_uri uri)))
37 storage := (u,obj)::!storage;
38 let _,height,_,_,obj = obj in
41 NCic.Constant (_,name,None,_,_) ->
42 [u,name,NReference.reference_of_spec u NReference.Decl]
43 | NCic.Constant (_,name,Some _,_,_) ->
44 [u,name,NReference.reference_of_spec u (NReference.Def height)]
45 | NCic.Fixpoint (is_ind,fl,_) ->
47 (fun (_,name,recno,_,_) i ->
49 u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height))
51 u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl
52 | NCic.Inductive (inductive,leftno,il,_) ->
55 (fun (_,iname,_,cl) i ->
59 NReference.reference_of_spec u (NReference.Con (i,j+1,leftno))
62 NReference.reference_of_spec u
63 (NReference.Ind (inductive,i,leftno))]
66 aliases := references @ !aliases
69 let cache = NUri.UriHash.create 313;;
72 try List.assq u !storage
74 try NUri.UriHash.find cache u
76 (* in the final implementation should get it from disk *)
77 let ouri = NCic2OCic.ouri_of_nuri u in
79 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
80 let l = OCic2NCic.convert_obj ouri o in
81 List.iter (fun (u,_,_,_,_ as o) ->
82 (* prerr_endline ("+"^NUri.string_of_uri u); *)
83 NUri.UriHash.add cache u o) l;
85 with CicEnvironment.Object_not_found u ->
87 (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u))))
90 let clear_cache () = NUri.UriHash.clear cache;;