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;;
31 let path_of_baseuri baseuri =
32 let uri = NUri.string_of_uri baseuri in
33 let path = String.sub uri 4 (String.length uri - 4) in
34 let path = Helm_registry.get "matita.basedir" ^ path in
35 let dirname = Filename.dirname path in
36 HExtlib.mkdir dirname;
40 let serialize ~baseuri dump =
41 let ch = open_out (path_of_baseuri baseuri) in
42 Marshal.to_channel ch (magic,dump) [Marshal.Closures];
46 let ch = open_out (path_of_baseuri uri) in
47 Marshal.to_channel ch (magic,obj) [];
53 let require ~baseuri =
54 let ch = open_in (path_of_baseuri baseuri) in
55 let mmagic,dump = Marshal.from_channel ch in
57 if mmagic <> magic then
58 raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library."))
63 let decompile ~baseuri =
64 Unix.unlink (path_of_baseuri baseuri)
65 (* WE ARE NOT REMOVING ALL THE OBJECTS YET! *)
68 (* the miracles of Marshal... *)
70 let obj = require ~baseuri:uri in
71 (* here we need to refresh the URIs! *)
78 (fun (_,name',nref) -> if name'=name then Some nref else None) !aliases
80 Not_found -> raise (ObjectNotFound (lazy name))
86 (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !aliases
88 Not_found -> raise (ObjectNotFound (lazy (NUri.string_of_uri uri)))
92 storage := (u,obj)::!storage;
93 let _,height,_,_,obj = obj in
96 NCic.Constant (_,name,None,_,_) ->
97 [u,name,NReference.reference_of_spec u NReference.Decl]
98 | NCic.Constant (_,name,Some _,_,_) ->
99 [u,name,NReference.reference_of_spec u (NReference.Def height)]
100 | NCic.Fixpoint (is_ind,fl,_) ->
102 (fun (_,name,recno,_,_) i ->
104 u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height))
106 u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl
107 | NCic.Inductive (inductive,leftno,il,_) ->
110 (fun (_,iname,_,cl) i ->
114 NReference.reference_of_spec u (NReference.Con (i,j+1,leftno))
117 NReference.reference_of_spec u
118 (NReference.Ind (inductive,i,leftno))]
121 aliases := references @ !aliases;
122 !storage,!aliases,!cache
126 try List.assq u !storage
130 try NUri.UriMap.find u !cache
132 let ouri = NCic2OCic.ouri_of_nuri u in
134 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
135 let l = OCic2NCic.convert_obj ouri o in
136 List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l;
138 with CicEnvironment.Object_not_found u ->
139 raise (ObjectNotFound
140 (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u))))
143 let clear_cache () = cache := NUri.UriMap.empty;;