1 (* Copyright (C) 2004-2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 (** given a uri and a type list (the contructors types) builds a list of pairs
31 * (name,uri) that is used to generate authomatic aliases **)
32 let extract_alias types uri =
34 fun (acc,i) (name, _, _, cl) ->
35 ((name, UriManager.string_of_uriref (uri,[i]))
38 fun (acc,j) (name,_) ->
39 (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
43 (** adds a (name,uri) list l to a disambiguation environment e **)
45 let module DT = DisambiguateTypes in
46 let module DTE = DisambiguateTypes.Environment in
51 (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
55 let add_aliases_for_object status suri =
56 let uri = UriManager.uri_of_string suri in
57 let name = UriManager.name_of_uri uri in
58 let new_env = env_of_list [(name,suri)] status.aliases in
59 {status with aliases = new_env }
61 let add_aliases_for_inductive_def status types suri =
62 let uri = UriManager.uri_of_string suri in
63 (* aliases for the constructors and types *)
64 let aliases = env_of_list (extract_alias types uri) status.aliases in
65 (* aliases for the eliminations principles *)
66 let base = String.sub suri 0 (String.length suri - 4) in
72 fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
74 let u = base ^ suffix in
75 (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
78 ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
80 {status with aliases = aliases }
82 let paths_and_uris_of_obj uri status =
83 let basedir = get_string_option status "basedir" in
84 let innertypesuri = UriManager.innertypesuri_of_uri uri in
85 let bodyuri = UriManager.bodyuri_of_uri uri in
86 let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
87 (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
88 let innertypespath = basedir ^ "/" ^ innertypesfilename in
89 let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
90 (UriManager.string_of_uri uri) ^ ".xml.gz" in
91 let xmlpath = basedir ^ "/" ^ xmlfilename in
92 let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
93 (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
94 let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in
95 xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri
97 let save_object_to_disk status uri obj =
98 let ensure_path_exists path =
99 let dir = Filename.dirname path in
102 (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
103 let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
104 Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
108 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
112 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
113 ~ask_dtd_to_the_getter:false
115 let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri =
116 paths_and_uris_of_obj uri status
118 let path_scheme_of path = "file://" ^ path in
119 List.iter MatitaMisc.mkdir
120 (List.map Filename.dirname [innertypespath; xmlpath]);
121 (* now write to disk *)
122 ensure_path_exists innertypespath;
123 Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ;
124 ensure_path_exists xmlpath;
125 Xml.pp ~gzip:true xml (Some xmlpath) ;
126 (* now register to the getter *)
127 Http_getter.register' innertypesuri (path_scheme_of innertypespath);
128 Http_getter.register' uri (path_scheme_of xmlpath);
129 (* we return a list of uri,path we registered/created *)
130 (uri,xmlpath) :: (innertypesuri,innertypespath) ::
131 (* now the optional body, both write and register *)
132 (match bodyxml,bodyuri with
134 | Some bodyxml,Some bodyuri->
135 ensure_path_exists xmlbodypath;
136 Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ;
137 Http_getter.register' bodyuri (path_scheme_of xmlbodypath);
138 [bodyuri,xmlbodypath]
141 let unregister_if_some = function
142 | Some u -> Http_getter.unregister' u | None -> ()
144 let remove_object_from_disk uri path =
146 Http_getter.unregister' uri
148 let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status =
149 let dbd = MatitaDb.instance () in
150 let suri = UriManager.string_of_uri uri in
151 if CicEnvironment.in_library uri then
152 command_error (sprintf "%s constant already defined" suri)
154 let name = UriManager.name_of_uri uri in
155 let obj = Cic.Constant (name, body, ty, params, attrs) in
156 let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
157 CicEnvironment.add_type_checked_term uri (obj, ugraph);
158 MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
159 let new_stuff = save_object_to_disk status uri obj in
160 MatitaLog.message (sprintf "%s constant defined" suri);
161 let status = add_aliases_for_object status suri in
162 { status with objects = new_stuff @ status.objects }
165 let split_obj = function
166 | Cic.Constant (name, body, ty, _, attrs)
167 | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs)
170 let add_inductive_def
171 ~uri ~types ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph status
173 let dbd = MatitaDb.instance () in
174 let suri = UriManager.string_of_uri uri in
175 if CicEnvironment.in_library uri then
176 command_error (sprintf "%s inductive type already defined" suri)
178 let name = UriManager.name_of_uri uri in
179 let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in
180 let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
181 CicEnvironment.put_inductive_definition uri (obj, ugraph);
182 MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
183 let new_stuff = save_object_to_disk status uri obj in
184 MatitaLog.message (sprintf "%s inductive type defined" suri);
185 let status = add_aliases_for_inductive_def status types suri in
186 let status = { status with objects = new_stuff @ status.objects } in
187 let elim sort status =
189 let obj = CicElim.elim_of ~sort uri 0 in
190 let (name, body, ty, attrs) = split_obj obj in
191 let suri = MatitaMisc.qualify status name ^ ".con" in
192 let uri = UriManager.uri_of_string suri in
193 (* TODO Zack: make CicElim returns a universe *)
194 let ugraph = CicUniv.empty_ugraph in
195 add_constant ~uri ?body ~ty ~attrs ~ugraph status;
196 with CicElim.Can_t_eliminate -> status
199 (fun status sort -> elim sort status)
201 [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
204 let add_record_def (suri, params, ty, fields) status =
205 let module CTC = CicTypeChecker in
206 let uri = UriManager.uri_of_string suri in
207 let buri = UriManager.buri_of_uri uri in
208 let record_spec = suri, params, ty, fields in
209 let types, leftno, obj, ugraph = CicRecord.inductive_of_record record_spec in
210 let status = add_inductive_def ~uri ~types ~leftno ~ugraph status in
211 let projections = CicRecord.projections_of record_spec in
214 fun status (suri, name, t) ->
217 CTC.type_of_aux' [] [] t CicUniv.empty_ugraph
219 (* THIS MUST BE IN SYNC WITH CicRecord *)
220 let uri = UriManager.uri_of_string suri in
221 let t = Unshare.unshare t in
222 let ty = Unshare.unshare ty in
223 let status = add_constant ~uri ~body:t ~ty ~ugraph status in
224 add_aliases_for_object status suri
226 | CTC.TypeCheckerFailure s ->
228 ("Unable to create projection " ^ name ^ " cause: " ^ s);
230 | Http_getter_types.Key_not_found s ->
231 let depend = UriManager.uri_of_string s in
232 let depend = UriManager.name_of_uri depend in
234 ("Unable to create projection " ^ name ^ " cause uses " ^ depend);
242 type t = UriManager.uri * string
243 let compare (u1, _) (u2, _) = UriManager.compare u1 u2
246 module UriSet = Set.Make (OrderedUri)
248 (* returns the uri of objects that were added in the meanwhile...
249 * status1 ----> status2
250 * assumption: objects defined in status2 are a superset of those defined in
253 let delta_status status1 status2 =
254 let module S = UriSet in
256 let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
257 let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
258 let diff = S.diff s2 s1 in
259 S.fold (fun uri uris -> uri :: uris) diff []
261 diff status1.objects status2.objects
263 let remove_coercion uri =
264 CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)
266 let time_travel ~present ~past =
267 let list_of_objs_to_remove = List.rev (delta_status past present) in
268 (* List.rev is just for the debugging code, which otherwise may list both
269 * something.ind and something.ind#xpointer ... (ask Enrico :-) *)
270 let debug_list = ref [] in
271 List.iter (fun (uri,p) ->
272 remove_object_from_disk uri p;
275 CicEnvironment.remove_obj uri
276 with CicEnvironment.Object_not_found _ ->
278 (sprintf "time_travel removes from cache %s that is not in"
279 (UriManager.string_of_uri uri)));
280 let l = MatitaDb.remove_uri uri in
281 debug_list := UriManager.string_of_uri uri :: !debug_list @ l)
282 list_of_objs_to_remove;
284 (* this is debug code
285 * idea: debug_list is the list of objects to be removed as computed from the
286 * db, while list_of_objs_to_remove is the same list but computer from the
287 * differences between statuses *)
288 let l1 = List.sort Pervasives.compare !debug_list in
289 let l2 = List.sort Pervasives.compare
290 (List.map (fun (x,_) -> UriManager.string_of_uri x) list_of_objs_to_remove)
292 let rec uniq = function
295 | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl)
296 | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl
301 List.iter2 (fun x y -> if x <> y then raise Exit) l1 l2
303 | Invalid_argument _ | Exit ->
304 MatitaLog.debug "It seems you garbaged something...";
305 MatitaLog.debug "l1:";
306 List.iter MatitaLog.debug l1;
307 MatitaLog.debug "l2:";
308 List.iter MatitaLog.debug l2
310 let alias_diff ~from status =
311 let module Map = DisambiguateTypes.Environment in
313 (fun domain_item codomain_item acc ->
314 if not (Map.mem domain_item from.aliases) then
315 Map.add domain_item codomain_item acc
318 status.aliases Map.empty