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/
28 let object_declaration_hook = ref []
29 let add_object_declaration_hook f =
30 object_declaration_hook := f :: !object_declaration_hook
32 exception AlreadyDefined of UriManager.uri
35 UriManager.uri -> int (* arity *) ->
36 int (* saturations *) -> string (* baseuri *) ->
37 UriManager.uri list (* lemmas (new objs) *)
43 stack := CoercDb.dump () :: !stack;
44 CoercDb.restore CoercDb.empty_coerc_db;
49 | [] -> raise (Failure "Unable to POP from librarySync.ml")
56 let innertypesuri = UriManager.innertypesuri_of_uri uri in
57 let bodyuri = UriManager.bodyuri_of_uri uri in
58 let univgraphuri = UriManager.univgraphuri_of_uri uri in
59 innertypesuri,bodyuri,univgraphuri
61 let paths_and_uris_of_obj uri =
62 let resolved = Http_getter.filename' ~local:true ~writable:true uri in
63 let basepath = Filename.dirname resolved in
64 let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
65 let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
66 let innertypespath = basepath ^ "/" ^ innertypesfilename in
67 let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in
68 let xmlpath = basepath ^ "/" ^ xmlfilename in
69 let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in
70 let xmlbodypath = basepath ^ "/" ^ xmlbodyfilename in
71 let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in
72 let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in
73 xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
74 xmlunivgraphpath, univgraphuri
76 let save_object_to_disk uri obj ugraph univlist =
79 if not (Helm_registry.get_opt_default
80 Helm_registry.bool "matita.nodisk" ~default:false)
84 let ensure_path_exists path =
85 let dir = Filename.dirname path in
88 (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
89 let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
90 if Helm_registry.get_bool "matita.system" &&
91 not (Helm_registry.get_bool "matita.noinnertypes")
93 let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
94 Cic2acic.acic_object_of_cic_object obj
97 Cic2Xml.print_inner_types
98 uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false
100 annobj, Some innertypesxml, Some ids_to_inner_sorts, false
102 let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
103 annobj, None, None, true
108 uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false
109 ~generate_attributes annobj
111 let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
112 xmlunivgraphpath, univgraphuri =
113 paths_and_uris_of_obj uri
115 write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]);
116 (* now write to disk *)
117 write ensure_path_exists xmlpath;
118 write (Xml.pp ~gzip:true xml) (Some xmlpath);
119 write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist;
120 (* we return a list of uri,path we registered/created *)
122 (univgraphuri,xmlunivgraphpath) ::
123 (* now the optional inner types, both write and register *)
124 (match innertypes with
126 | Some innertypesxml ->
127 write ensure_path_exists innertypespath;
128 write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath);
129 [innertypesuri, innertypespath]
131 (* now the optional body, both write and register *)
132 (match bodyxml,bodyuri with
134 | Some bodyxml,Some bodyuri->
135 write ensure_path_exists xmlbodypath;
136 write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath);
137 [bodyuri, xmlbodypath]
143 let profiler = HExtlib.profile "add_obj.typecheck_obj" in
145 assert false (* MATITA 1.0
146 profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
150 let profiler = HExtlib.profile "add_obj.index_obj" in
152 assert false (* MATITA 1.0
153 profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
157 assert false (* MATITA 1.0
158 let derived_uris_of_uri uri =
159 let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
160 innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
163 if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
165 let files_to_remove = uri :: derived_uris_of_uri uri in
169 let file = Http_getter.resolve' ~local:true ~writable:true uri in
170 HExtlib.safe_remove file;
171 HExtlib.rmdir_descend (Filename.dirname file)
172 with Http_getter_types.Key_not_found _ -> ());
174 List.iter (fun uri -> ignore (LibraryDb.remove_uri uri)) uris_to_remove ;
175 CicEnvironment.remove_obj uri
179 let rec add_obj uri obj ~pack_coercion_obj =
180 assert false (* MATITA 1.0
182 if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None
183 then pack_coercion_obj obj
186 let dbd = LibraryDb.instance () in
187 if CicEnvironment.in_library uri then raise (AlreadyDefined uri);
189 typecheck_obj uri obj; (* 1 *)
190 let obj, ugraph, univlist =
191 try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri
192 with CicEnvironment.Object_not_found _ -> assert false
195 index_obj ~dbd ~uri; (* 2 must be in the env *)
198 let new_stuff = save_object_to_disk uri obj ugraph univlist in
201 (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
203 List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *)
206 ignore(LibraryDb.remove_uri uri); (* -2 *)
209 CicEnvironment.remove_obj uri; (* -1 *)
212 let added = ref [] in
213 let add_obj_with_parachute u o =
214 added := u :: !added;
215 add_obj u o ~pack_coercion_obj in
216 let old_db = CoercDb.dump () in
220 f ~add_obj:add_obj_with_parachute
221 ~add_coercion:(add_coercion ~add_composites:true ~pack_coercion_obj)
223 [] !object_declaration_hook
225 List.iter remove_obj !added;
227 CoercDb.restore old_db;
233 add_coercion ~add_composites ~pack_coercion_obj uri arity saturations baseuri
235 assert false (* MATITA 1.0
237 let coer = CicUtil.term_of_uri uri in
238 CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph
240 (* we have to get the source and the tgt type uri
241 * in Coq syntax we have already their names, but
242 * since we don't support Funclass and similar I think
243 * all the coercion should be of the form
245 * So we should be able to extract them from the coercion type
247 * Currently only (_:T1)T2 is supported.
248 * should we saturate it with metas in case we insert it?
252 let rec aux = function
253 | Cic.Prod( _, src, tgt) -> src::aux tgt
258 let src_carr, tgt_carr, no_args =
259 let get_classes arity saturations l =
260 (* this is the ackerman's function revisited *)
261 let rec aux = function
262 0,0,None,tgt::src::_ -> src,Some (`Class tgt)
263 | 0,0,target,src::_ -> src,target
264 | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl)
265 | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl)
266 | arity,saturations,None,_::tl ->
267 aux (arity, saturations, Some `Funclass, tl)
268 | arity,saturations,target,_::tl ->
269 aux (arity - 1, saturations, target, tl)
272 aux (arity,saturations,None,List.rev l)
274 let types = spine2list coer_ty in
275 let src,tgt = get_classes arity saturations types in
276 CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0,
278 | None -> assert false
279 | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity
280 | Some (`Class tgt) ->
281 CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0),
282 List.length types - 1
284 let already_in_obj src_carr tgt_carr uri obj =
287 if not (CoercDb.eq_carr s src_carr &&
288 CoercDb.eq_carr t tgt_carr)
295 | Cic.Constant (_, Some bo, ty, _, _) -> bo, ty
297 (* this is not a composite coercion, thus the uri is valid *)
298 let bo = CicUtil.term_of_uri uri in
300 fst (CicTypeChecker.type_of_aux' [] [] bo
301 CicUniv.oblivion_ugraph)
303 let are_body_convertible =
304 fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
305 CicUniv.oblivion_ugraph)
307 if not are_body_convertible then
310 UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
311 uri^" are not convertible, but are between the same nodes.\n"^
312 "From now on unification can fail randomly.");
315 match t, tgt_carr with
316 | CoercDb.Sort (Cic.Type i), CoercDb.Sort (Cic.Type j)
317 | CoercDb.Sort (Cic.CProp i), CoercDb.Sort (Cic.CProp j)
318 when not (CicUniv.eq i j) ->
320 ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^
321 "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^
322 "different universe : " ^
323 CicUniv.string_of_universe j ^ " <> " ^
324 CicUniv.string_of_universe i); false)
325 | CoercDb.Sort Cic.Prop , CoercDb.Sort Cic.Prop
326 | CoercDb.Sort (Cic.Type _) , CoercDb.Sort (Cic.Type _)
327 | CoercDb.Sort (Cic.CProp _), CoercDb.Sort (Cic.CProp _) ->
329 ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
330 "it is a duplicate of " ^ UriManager.string_of_uri u);
332 | CoercDb.Sort s1, CoercDb.Sort s2 ->
334 ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^
335 "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^
336 "different universe : " ^
337 CicPp.ppterm (Cic.Sort s1) ^ " <> " ^
338 CicPp.ppterm (Cic.Sort s2)); false)
341 CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u)
342 CicUniv.oblivion_ugraph
344 if CicUtil.alpha_equivalence ty ty' then
346 ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
347 "it is a duplicate of " ^ UriManager.string_of_uri u);
353 (CoercDb.to_list (CoercDb.dump ()))
355 let cpos = no_args - arity - saturations - 1 in
356 if not add_composites then
357 (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); [])
360 if already_in_obj src_carr tgt_carr uri
361 (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)) then
362 raise (AlreadyDefined uri);
365 CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
369 List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj))
375 (fun acc (src,tgt,uri,saturations,obj,arity,cpos) ->
376 CoercDb.add_coercion (src,tgt,uri,saturations,cpos);
377 let acc = add_obj uri obj pack_coercion_obj @ uri::acc in
381 CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
382 (* CoercDb.prefer uri; *)