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
15 exception LibraryOutOfSync of string Lazy.t
18 (NUri.uri * NCic.obj) list *
19 (NUri.uri * string * NReference.reference) list *
20 NCic.obj NUri.UriMap.t;;
22 let time0 = [],[],NUri.UriMap.empty;;
23 let storage = ref [];;
24 let aliases = ref [];;
25 let cache = ref NUri.UriMap.empty;;
27 let time_travel (sto,ali,cac) = storage := sto; aliases := ali; cache := cac;;
32 (fun (_,name',nref) -> if name'=name then Some nref else None) !aliases
34 Not_found -> raise (ObjectNotFound (lazy name))
40 (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !aliases
42 Not_found -> raise (ObjectNotFound (lazy (NUri.string_of_uri uri)))
46 storage := (u,obj)::!storage;
47 let _,height,_,_,obj = obj in
50 NCic.Constant (_,name,None,_,_) ->
51 [u,name,NReference.reference_of_spec u NReference.Decl]
52 | NCic.Constant (_,name,Some _,_,_) ->
53 [u,name,NReference.reference_of_spec u (NReference.Def height)]
54 | NCic.Fixpoint (is_ind,fl,_) ->
56 (fun (_,name,recno,_,_) i ->
58 u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height))
60 u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl
61 | NCic.Inductive (inductive,leftno,il,_) ->
64 (fun (_,iname,_,cl) i ->
68 NReference.reference_of_spec u (NReference.Con (i,j+1,leftno))
71 NReference.reference_of_spec u
72 (NReference.Ind (inductive,i,leftno))]
75 aliases := references @ !aliases;
76 !storage,!aliases,!cache
80 try List.assq u !storage
82 try NUri.UriMap.find u !cache
84 (* in the final implementation should get it from disk *)
85 let ouri = NCic2OCic.ouri_of_nuri u in
87 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
88 let l = OCic2NCic.convert_obj ouri o in
89 List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l;
91 with CicEnvironment.Object_not_found u ->
93 (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u))))
96 let clear_cache () = cache := NUri.UriMap.empty;;
100 let path_of_baseuri baseuri =
101 let uri = NUri.string_of_uri baseuri in
102 let path = String.sub uri 4 (String.length uri - 4) in
103 let path = Helm_registry.get "matita.basedir" ^ path in
104 let dirname = Filename.dirname path in
105 HExtlib.mkdir dirname;
109 let serialize ~baseuri dump =
110 let ch = open_out (path_of_baseuri baseuri) in
111 Marshal.to_channel ch (magic,dump) [Marshal.Closures];
115 let require ~baseuri =
116 let ch = open_in (path_of_baseuri baseuri) in
117 let mmagic,dump = Marshal.from_channel ch in
119 if mmagic <> magic then
120 raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library."))
125 let decompile ~baseuri =
126 Unix.unlink (path_of_baseuri baseuri)