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;;
29 let path_of_baseuri baseuri =
30 let uri = NUri.string_of_uri baseuri in
31 let path = String.sub uri 4 (String.length uri - 4) in
32 let path = Helm_registry.get "matita.basedir" ^ path in
33 let dirname = Filename.dirname path in
34 HExtlib.mkdir dirname;
40 let require0 ~baseuri =
41 let ch = open_in (path_of_baseuri baseuri) in
42 let mmagic,dump = Marshal.from_channel ch in
44 if mmagic <> magic then
45 raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library."))
50 let serialize ~baseuri dump =
51 let ch = open_out (path_of_baseuri baseuri) in
52 Marshal.to_channel ch (magic,dump) [Marshal.Closures];
56 let ch = open_out (path_of_baseuri uri) in
57 Marshal.to_channel ch (magic,obj) [];
63 module type Serializer =
67 val register: string -> ('a -> status -> status) -> ('a -> obj)
68 val serialize: baseuri:NUri.uri -> obj list -> unit
69 val require: baseuri:NUri.uri -> status -> status
72 module Serializer(S: sig type status end) =
74 type status = S.status
77 let require1 = ref (fun _ -> assert false (* unknown data*))
78 let already_registered = ref []
80 let register tag require =
81 assert (not (List.mem tag !already_registered));
82 already_registered := tag :: !already_registered;
84 (fun (tag',data) as x ->
85 if tag=tag' then Obj.magic require data else Obj.magic !require1 x);
86 Obj.magic (fun x -> tag,x)
88 let serialize = serialize
90 let require ~baseuri status =
91 let dump = require0 ~baseuri in
92 List.fold_right (Obj.magic !require1) dump status
95 let decompile ~baseuri =
96 Unix.unlink (path_of_baseuri baseuri)
97 (* WE ARE NOT REMOVING ALL THE OBJECTS YET! *)
100 (* the miracles of Marshal... *)
102 let obj = require0 ~baseuri:uri in
103 (* here we need to refresh the URIs! *)
110 (fun (_,name',nref) -> if name'=name then Some nref else None) !aliases
112 Not_found -> raise (ObjectNotFound (lazy name))
118 (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !aliases
120 Not_found -> raise (ObjectNotFound (lazy (NUri.string_of_uri uri)))
124 storage := (u,obj)::!storage;
125 let _,height,_,_,obj = obj in
128 NCic.Constant (_,name,None,_,_) ->
129 [u,name,NReference.reference_of_spec u NReference.Decl]
130 | NCic.Constant (_,name,Some _,_,_) ->
131 [u,name,NReference.reference_of_spec u (NReference.Def height)]
132 | NCic.Fixpoint (is_ind,fl,_) ->
134 (fun (_,name,recno,_,_) i ->
136 u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height))
138 u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl
139 | NCic.Inductive (inductive,leftno,il,_) ->
142 (fun (_,iname,_,cl) i ->
146 NReference.reference_of_spec u (NReference.Con (i,j+1,leftno))
149 NReference.reference_of_spec u
150 (NReference.Ind (inductive,i,leftno))]
153 aliases := references @ !aliases;
154 !storage,!aliases,!cache
158 try List.assq u !storage
162 try NUri.UriMap.find u !cache
164 let ouri = NCic2OCic.ouri_of_nuri u in
166 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
167 let l = OCic2NCic.convert_obj ouri o in
168 List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l;
170 with CicEnvironment.Object_not_found u ->
171 raise (ObjectNotFound
172 (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u))))
175 let clear_cache () = cache := NUri.UriMap.empty;;