(* 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/ *) exception AlreadyDefined of UriManager.uri 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 ~basedir = let basedir = basedir ^ "/xml" in let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in let innertypespath = basedir ^ "/" ^ innertypesfilename in let xmlfilename = Str.replace_first (Str.regexp "^cic:/") "" (UriManager.string_of_uri uri) ^ ".xml.gz" in let xmlpath = basedir ^ "/" ^ xmlfilename in let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" (UriManager.string_of_uri uri) ^ ".body.xml.gz" in let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") "" (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, xmlunivgraphpath, univgraphuri let save_object_to_disk ~basedir uri obj ugraph univlist = 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 = Cic2acic.plain_acic_object_of_cic_object obj in (* prepare XML *) let xml, bodyxml = Cic2Xml.print_object uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj in let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, xmlunivgraphpath, univgraphuri = paths_and_uris_of_obj uri basedir in List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]); (* now write to disk *) ensure_path_exists xmlpath; Xml.pp ~gzip:true xml (Some xmlpath); 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 body, both write and register *) (match bodyxml,bodyuri with None,None -> [] | Some bodyxml,Some bodyuri-> ensure_path_exists xmlbodypath; 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) 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 ~basedir = let dbd = LibraryDb.instance () in if CicEnvironment.in_library uri then raise (AlreadyDefined uri) else begin typecheck_obj uri obj; (* 1 *) 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 ~basedir uri obj ugraph univlist in 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 to_remove = uri :: (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @ derived_uris_of_uri uri in List.iter (fun uri -> (try let file = Http_getter.resolve' uri in HExtlib.safe_remove file; HExtlib.rmdir_descend (Filename.dirname file) with Http_getter_types.Key_not_found _ -> ()); ignore (LibraryDb.remove_uri uri); CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri); CicEnvironment.remove_obj uri) to_remove (*** GENERATION OF AUXILIARY LEMMAS ***) let generate_elimination_principles ~basedir uri = let uris = ref [] in let elim sort = try let uri,obj = CicElim.elim_of ~sort uri 0 in add_single_obj uri obj ~basedir; uris := uri :: !uris with CicElim.Can_t_eliminate -> () in try List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; !uris with exn -> List.iter remove_single_obj !uris; raise exn let generate_projections ~basedir uri fields = let uris = ref [] in let projections = CicRecord.projections_of uri fields in try List.iter (fun (uri, name, bo) -> 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 ~basedir uri obj; uris := uri :: !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; !uris with exn -> List.iter remove_single_obj !uris; raise exn let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 let add_obj uri obj ~basedir = add_single_obj uri obj ~basedir; let uris = ref [] in try begin match obj with | Cic.Constant _ -> () | Cic.InductiveDefinition (_,_,_,attrs) -> uris := !uris @ generate_elimination_principles ~basedir uri; 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 ~basedir uri fields)) | Cic.CurrentProof _ | Cic.Variable _ -> assert false end; UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris; !uris with exn -> List.iter remove_single_obj !uris; raise exn let remove_obj uri = let uris = try UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri with Not_found -> [] in List.iter remove_single_obj (uri::uris)