X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;fp=components%2Flibrary%2FlibrarySync.ml;h=8a0c2bcc4406f8832a2fbe0e6fac5300ee4232ba;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml new file mode 100644 index 000000000..8a0c2bcc4 --- /dev/null +++ b/components/library/librarySync.ml @@ -0,0 +1,562 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +let object_declaration_hook = ref (fun _ _ -> ());; +let set_object_declaration_hook f = + object_declaration_hook := f + +exception AlreadyDefined of UriManager.uri + +let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 + +(* uri |--> (derived_coercions_in_the_coercion_DB, derived_coercions_in_lib) + * + * in case of remove_coercion uri, the first component is removed from the + * coercion DB, while the second is passed to remove_obj (and is not [] only if + * add_coercion is called with add_composites + * *) +let coercion_hashtbl = UriManager.UriHashtbl.create 3 + +let uris_of_obj uri = + let innertypesuri = UriManager.innertypesuri_of_uri uri in + let bodyuri = UriManager.bodyuri_of_uri uri in + let univgraphuri = UriManager.univgraphuri_of_uri uri in + innertypesuri,bodyuri,univgraphuri + +let paths_and_uris_of_obj uri = + let resolved = Http_getter.filename' ~local:true ~writable:true uri in + let basepath = Filename.dirname resolved in + let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in + let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in + let innertypespath = basepath ^ "/" ^ innertypesfilename in + let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in + let xmlpath = basepath ^ "/" ^ xmlfilename in + let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in + let xmlbodypath = basepath ^ "/" ^ xmlbodyfilename in + let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in + let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in + xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, + xmlunivgraphpath, univgraphuri + +let save_object_to_disk uri obj ugraph univlist = + let write f x = + if not (Helm_registry.get_opt_default + Helm_registry.bool "matita.nodisk" ~default:false) + then + f x + in + let ensure_path_exists path = + let dir = Filename.dirname path in + HExtlib.mkdir dir + in + (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) + let annobj, innertypes, ids_to_inner_sorts, generate_attributes = + if Helm_registry.get_bool "matita.system" && + not (Helm_registry.get_bool "matita.noinnertypes") + then + let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ = + Cic2acic.acic_object_of_cic_object obj + in + let innertypesxml = + Cic2Xml.print_inner_types + uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false + in + annobj, Some innertypesxml, Some ids_to_inner_sorts, false + else + let annobj = Cic2acic.plain_acic_object_of_cic_object obj in + annobj, None, None, true + in + (* prepare XML *) + let xml, bodyxml = + Cic2Xml.print_object + uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false + ~generate_attributes annobj + in + let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, + xmlunivgraphpath, univgraphuri = + paths_and_uris_of_obj uri + in + write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]); + (* now write to disk *) + write ensure_path_exists xmlpath; + write (Xml.pp ~gzip:true xml) (Some xmlpath); + write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist; + (* we return a list of uri,path we registered/created *) + (uri,xmlpath) :: + (univgraphuri,xmlunivgraphpath) :: + (* now the optional inner types, both write and register *) + (match innertypes with + | None -> [] + | Some innertypesxml -> + write ensure_path_exists innertypespath; + write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath); + [innertypesuri, innertypespath] + ) @ + (* now the optional body, both write and register *) + (match bodyxml,bodyuri with + None,_ -> [] + | Some bodyxml,Some bodyuri-> + write ensure_path_exists xmlbodypath; + write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath); + [bodyuri, xmlbodypath] + | _-> assert false) + + +let typecheck_obj = + let profiler = HExtlib.profile "add_obj.typecheck_obj" in + fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) + (Unshare.fresh_types obj) + +let index_obj = + let profiler = HExtlib.profile "add_obj.index_obj" in + fun ~dbd ~uri -> + profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri + +let add_single_obj uri obj refinement_toolkit = + let module RT = RefinementTool in + let obj = + if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*) + not (CoercDb.is_a_coercion' (Cic.Const (uri, []))) + then + refinement_toolkit.RT.pack_coercion_obj obj + else + obj + in + let dbd = LibraryDb.instance () in + if CicEnvironment.in_library uri then + raise (AlreadyDefined uri) + else begin + (*CicUniv.reset_spent_time (); + let before = Unix.gettimeofday () in*) + typecheck_obj uri obj; (* 1 *) + (*let after = Unix.gettimeofday () in + let univ_time = CicUniv.get_spent_time () in + let total_time = after -. before in + prerr_endline + (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" + (univ_time *. 100. /. total_time) (total_time) (univ_time) + (UriManager.name_of_uri uri));*) + let _, ugraph, univlist = + CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in + try + index_obj ~dbd ~uri; (* 2 must be in the env *) + try + (*3*) + let new_stuff = save_object_to_disk uri obj ugraph univlist in + (* EXPERIMENTAL: pretty print the object in natural language *) + (try !object_declaration_hook uri obj + with exc -> + prerr_endline ("Error: object_declaration_hook failed"^ + Printexc.to_string exc)); + try + HLog.message + (Printf.sprintf "%s defined" (UriManager.string_of_uri uri)) + with exc -> + List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *) + raise exc + with exc -> + ignore(LibraryDb.remove_uri uri); (* -2 *) + raise exc + with exc -> + CicEnvironment.remove_obj uri; (* -1 *) + raise exc + end + +let remove_single_obj uri = + let derived_uris_of_uri uri = + let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in + innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u]) + in + let uris_to_remove = + if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri] + in + let files_to_remove = uri :: derived_uris_of_uri uri in + List.iter + (fun uri -> + (try + let file = Http_getter.resolve' ~local:true ~writable:true uri in + HExtlib.safe_remove file; + HExtlib.rmdir_descend (Filename.dirname file) + with Http_getter_types.Key_not_found _ -> ()); + ) files_to_remove ; + List.iter + (fun uri -> + ignore (LibraryDb.remove_uri uri); + (*CoercGraph.remove_coercion uri;*) + ) uris_to_remove ; + CicEnvironment.remove_obj uri + +(*** GENERATION OF AUXILIARY LEMMAS ***) + +let generate_elimination_principles uri refinement_toolkit = + let uris = ref [] in + let elim i = + let elim sort = + try + let uri,obj = CicElim.elim_of ~sort uri i in + add_single_obj uri obj refinement_toolkit; + uris := uri :: !uris + with CicElim.Can_t_eliminate -> () + in + try + List.iter + elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; + with exn -> + List.iter remove_single_obj !uris; + raise exn + in + let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in + match obj with + | Cic.InductiveDefinition (indTypes, _, _, _) -> + let counter = ref 0 in + List.iter (fun _ -> elim !counter; counter := !counter+1) indTypes; + !uris + | _ -> + failwith (Printf.sprintf "not an inductive definition (%s)" + (UriManager.string_of_uri uri)) + +(* COERCIONS ***********************************************************) + +let remove_all_coercions () = + UriManager.UriHashtbl.clear coercion_hashtbl; + CoercDb.remove_coercion (fun (_,_,_,_) -> true) + +let stack = ref [];; + +let h2l h = + UriManager.UriHashtbl.fold + (fun k v acc -> (k,v) :: acc) h [] +;; + +let push () = + stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack; + remove_all_coercions () +;; + +let pop () = + match !stack with + | [] -> raise (Failure "Unable to POP from librarySync.ml") + | (db,h) :: tl -> + stack := tl; + remove_all_coercions (); + CoercDb.restore db; + List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v) + h +;; + +let add_coercion ~add_composites refinement_toolkit uri arity saturations + baseuri += + let coer_ty,_ = + let coer = CicUtil.term_of_uri uri in + CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph + in + (* we have to get the source and the tgt type uri + * in Coq syntax we have already their names, but + * since we don't support Funclass and similar I think + * all the coercion should be of the form + * (A:?)(B:?)T1->T2 + * So we should be able to extract them from the coercion type + * + * Currently only (_:T1)T2 is supported. + * should we saturate it with metas in case we insert it? + * + *) + let spine2list ty = + let rec aux = function + | Cic.Prod( _, src, tgt) -> src::aux tgt + | t -> [t] + in + aux ty + in + let src_carr, tgt_carr = + let get_classes arity saturations l = + (* this is the ackerman's function revisited *) + let rec aux = function + 0,0,None,tgt::src::_ -> src,Some (`Class tgt) + | 0,0,target,src::_ -> src,target + | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl) + | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl) + | arity,saturations,None,_::tl -> + aux (arity, saturations, Some `Funclass, tl) + | arity,saturations,target,_::tl -> + aux (arity - 1, saturations, target, tl) + | _ -> assert false + in + aux (arity,saturations,None,List.rev l) + in + let types = spine2list coer_ty in + let src,tgt = get_classes arity saturations types in + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src), + match tgt with + None -> assert false + | Some `Funclass -> CoercDb.Fun arity + | Some (`Class tgt) -> + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) + in + let already_in_obj src_carr tgt_carr uri obj = + List.exists + (fun (s,t,ul) -> + List.exists + (fun u,_ -> + let bo = + match obj with + | Cic.Constant (_, Some bo, _, _, _) -> bo + | _ -> assert false + in + CoercDb.eq_carr s src_carr && + CoercDb.eq_carr t tgt_carr && + if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo + CicUniv.oblivion_ugraph) + then true else + (HLog.warn + ("Coercions " ^ + UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri + uri^" are not convertible, but are between the same nodes.\n"^ + "From now on unification can fail randomly."); + false)) + ul) + (CoercDb.to_list ()) + in + if not add_composites then + (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); + UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]); + []) + else + let new_coercions = + CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations + baseuri + in + let new_coercions = + List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj)) + new_coercions + in + let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in + (* update the DB *) + List.iter + (fun (src,tgt,uri,saturations,_,_) -> + CoercDb.add_coercion (src,tgt,uri,saturations)) + new_coercions; + CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); + (* add the composites obj and they eventual lemmas *) + let lemmas = + List.fold_left + (fun acc (_,tgt,uri,saturations,obj,arity) -> + add_single_obj uri obj refinement_toolkit; + (uri,arity,saturations)::acc) + [] new_coercions + in + (* store that composite_uris are related to uri. the first component is + * the stuff in the DB while the second is stuff for remove_obj *) + (* + prerr_endline ("adding: " ^ + string_of_bool add_composites ^ UriManager.string_of_uri uri); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) + composite_uris; + *) + UriManager.UriHashtbl.add + coercion_hashtbl uri (composite_uris,composite_uris); + (* + prerr_endline ("lemmas:"); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) + lemmas; + prerr_endline ("lemmas END");*) + lemmas +;; + +let remove_coercion uri = + try + let (composites_in_db, composites_in_lib) = + UriManager.UriHashtbl.find coercion_hashtbl uri + in + (*prerr_endline ("removing: " ^UriManager.string_of_uri uri); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) + composites_in_db;*) + UriManager.UriHashtbl.remove coercion_hashtbl uri; + CoercDb.remove_coercion + (fun (_,_,u,_) -> UriManager.eq uri u); + (* remove from the DB *) + List.iter + (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1)) + composites_in_db; + (* remove composites from the lib *) + List.iter remove_single_obj composites_in_lib + with + Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *) + + +let generate_projections refinement_toolkit uri fields = + let uris = ref [] in + let projections = + CicRecord.projections_of uri + (List.map (fun (x,_,_) -> x) fields) + in + try + List.iter2 + (fun (uri, name, bo) (_name, coercion, arity) -> + let saturations = 0 in + try + let ty, ugraph = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in + let attrs = [`Class `Projection; `Generated] in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + add_single_obj uri obj refinement_toolkit; + let composites = + if coercion then + begin +(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*) + (*CSC: I think there is a bug here. The composite coercions + are not remembered in the .moo file. Thus they are re-generated + every time. Right? *) + let x = + add_coercion ~add_composites:true refinement_toolkit uri arity + saturations (UriManager.buri_of_uri uri) + in +(*prerr_endline ("are: "); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x; + prerr_endline "---"; +*) + (*CSC: I throw the arity away. See comment above *) + List.map (fun u,_,_ -> u) x + end + else + [] + in + uris := uri :: composites @ !uris + with + CicTypeChecker.TypeCheckerFailure s -> + HLog.message + ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s); + | CicEnvironment.Object_not_found uri -> + let depend = UriManager.name_of_uri uri in + HLog.message + ("Unable to create projection " ^ name ^ " because it requires " ^ + depend) + ) projections fields; + !uris + with exn -> + List.iter remove_single_obj !uris; + raise exn + +let build_inversion_principle = ref (fun a b -> assert false);; + +let generate_inversion refinement_toolkit uri obj = + List.map + (fun (ind_uri,ind_obj) -> + add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri) + (!build_inversion_principle uri obj) + +let + generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid += + function + Cic.Fix (_,funs) -> + snd ( + List.fold_right + (fun (name,idx,ty,bo) (n,uris) -> + if name = name_to_avoid then + (n+1,uris) + else + let uri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in + let bo = Cic.Fix (n,funs) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + add_single_obj uri obj refinement_toolkit; + (n+1,uri::uris) + ) funs (1,[])) + | Cic.CoFix (_,funs) -> + snd ( + List.fold_right + (fun (name,ty,bo) (n,uris) -> + if name = name_to_avoid then + (n+1,uris) + else + let uri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in + let bo = Cic.CoFix (n,funs) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + add_single_obj uri obj refinement_toolkit; + (n+1,uri::uris) + ) funs (1,[])) + | _ -> assert false + +let add_obj refinement_toolkit uri obj = + add_single_obj uri obj refinement_toolkit; + let uris = ref [] in + let not_debug = not (Helm_registry.get_bool "matita.debug") in + try + begin + match obj with + | Cic.Constant (name,Some bo,_,_,attrs) when + List.mem (`Flavour `MutualDefinition) attrs -> + uris := + !uris @ + generate_sibling_mutual_definitions refinement_toolkit uri attrs + name bo + | Cic.Constant _ -> () + | Cic.InductiveDefinition (inductivefuns,_,_,attrs) -> + let _,inductive,_,_ = List.hd inductivefuns in + if inductive then + begin + uris := !uris @ + generate_elimination_principles uri refinement_toolkit; + uris := !uris @ generate_inversion refinement_toolkit uri obj; + end ; + let rec get_record_attrs = + function + | [] -> None + | (`Class (`Record fields))::_ -> Some fields + | _::tl -> get_record_attrs tl + in + (match get_record_attrs attrs with + | None -> () (* not a record *) + | Some fields -> + uris := !uris @ + (generate_projections refinement_toolkit uri fields)) + | Cic.CurrentProof _ + | Cic.Variable _ -> assert false + end; + UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris; + !uris + with + | exn when not_debug -> + List.iter remove_single_obj !uris; + raise exn + +let remove_obj uri = + let uris = + try + let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in + UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri; + res + with + Not_found -> [] (*assert false*) + in + List.iter remove_single_obj (uri::uris) +