X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=2dcd6a8b9c8b4c4aae69a4ccadd4cf81c8529b75;hb=894802b5e169f37e5390683b6b29b4fbb4be1083;hp=91a838ddf5e9f5a588f369342bb6b07f0387b334;hpb=d8f4d935054a6f9fff6de0c171dc4a181389219e;p=helm.git diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 91a838ddf..2dcd6a8b9 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -43,25 +43,22 @@ let uris_of_obj uri = 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 paths_and_uris_of_obj uri = + let resolved = Http_getter.filename' ~writable:true uri in + let basepath = Filename.dirname resolved 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 + 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 ~basedir uri obj ugraph univlist = +let save_object_to_disk uri obj ugraph univlist = let ensure_path_exists path = let dir = Filename.dirname path in HExtlib.mkdir dir @@ -75,7 +72,7 @@ let save_object_to_disk ~basedir uri obj ugraph univlist = in let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, xmlunivgraphpath, univgraphuri = - paths_and_uris_of_obj uri basedir + paths_and_uris_of_obj uri in List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]); (* now write to disk *) @@ -104,7 +101,7 @@ let index_obj = fun ~dbd ~uri -> profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri -let add_single_obj uri obj refinement_toolkit ~basedir = +let add_single_obj uri obj refinement_toolkit = let module RT = RefinementTool in let obj = if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*) @@ -134,7 +131,7 @@ let add_single_obj uri obj refinement_toolkit ~basedir = 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 + let new_stuff = save_object_to_disk uri obj ugraph univlist in try HLog.message (Printf.sprintf "%s defined" (UriManager.string_of_uri uri)) @@ -162,7 +159,7 @@ let remove_single_obj uri = List.iter (fun uri -> (try - let file = Http_getter.resolve' uri in + let file = Http_getter.resolve' ~writable:true uri in HExtlib.safe_remove file; HExtlib.rmdir_descend (Filename.dirname file) with Http_getter_types.Key_not_found _ -> ()); @@ -173,12 +170,12 @@ let remove_single_obj uri = (*** GENERATION OF AUXILIARY LEMMAS ***) -let generate_elimination_principles ~basedir uri refinement_toolkit = +let generate_elimination_principles uri refinement_toolkit = let uris = ref [] in let elim sort = try let uri,obj = CicElim.elim_of ~sort uri 0 in - add_single_obj uri obj refinement_toolkit ~basedir; + add_single_obj uri obj refinement_toolkit; uris := uri :: !uris with CicElim.Can_t_eliminate -> () in @@ -195,7 +192,7 @@ let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; CoercDb.remove_coercion (fun (_,_,u1) -> true) -let add_coercion ~basedir ~add_composites refinement_toolkit uri = +let add_coercion ~add_composites refinement_toolkit uri = let coer_ty,_ = let coer = CicUtil.term_of_uri uri in CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph @@ -230,29 +227,41 @@ let add_coercion ~basedir ~add_composites refinement_toolkit uri = List.iter (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) new_coercions; - CoercDb.add_coercion (src_carr, tgt_carr, uri); - (* add the composites obj and they eventual lemmas *) - let lemmas = - if add_composites then - List.fold_left - (fun acc (_,_,uri,obj) -> - add_single_obj ~basedir uri obj refinement_toolkit; - uri::acc) - composite_uris new_coercions - else + if + List.exists + (fun (s,t,_) -> CoercDb.eq_carr s src_carr && CoercDb.eq_carr t tgt_carr) + (CoercDb.to_list ()) + then + begin + assert (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,if add_composites then composite_uris else []); - lemmas + end + else + begin + CoercDb.add_coercion (src_carr, tgt_carr, uri); + (* add the composites obj and they eventual lemmas *) + let lemmas = + if add_composites then + List.fold_left + (fun acc (_,_,uri,obj) -> + add_single_obj uri obj refinement_toolkit; + uri::acc) + composite_uris new_coercions + else + [] + 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,if add_composites then composite_uris else []); + lemmas + end let remove_coercion uri = try @@ -274,7 +283,7 @@ let remove_coercion uri = Not_found -> () (* mhh..... *) -let generate_projections ~basedir refinement_toolkit uri fields = +let generate_projections refinement_toolkit uri fields = let uris = ref [] in let projections = CicRecord.projections_of uri (List.map fst fields) in try @@ -285,10 +294,10 @@ let generate_projections ~basedir refinement_toolkit uri fields = 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 refinement_toolkit; + add_single_obj uri obj refinement_toolkit; let composites = if coercion then - add_coercion ~basedir ~add_composites:true refinement_toolkit uri + add_coercion ~add_composites:true refinement_toolkit uri else [] in @@ -308,19 +317,17 @@ let generate_projections ~basedir refinement_toolkit uri fields = List.iter remove_single_obj !uris; raise exn - let build_inversion_principle = ref (fun a b -> assert false);; -let generate_inversion refinement_toolkit ~basedir uri obj = +let generate_inversion refinement_toolkit uri obj = match !build_inversion_principle uri obj with None -> [] | Some (ind_uri,ind_obj) -> - add_single_obj ind_uri ind_obj refinement_toolkit ~basedir; + add_single_obj ind_uri ind_obj refinement_toolkit; [ind_uri] - -let add_obj refinement_toolkit uri obj ~basedir = - add_single_obj uri obj refinement_toolkit ~basedir; +let add_obj refinement_toolkit uri obj = + add_single_obj uri obj refinement_toolkit; let uris = ref [] in try begin @@ -328,8 +335,8 @@ let add_obj refinement_toolkit uri obj ~basedir = | Cic.Constant _ -> () | Cic.InductiveDefinition (_,_,_,attrs) -> uris := !uris @ - generate_elimination_principles ~basedir uri refinement_toolkit; - uris := !uris @ generate_inversion refinement_toolkit ~basedir uri obj; + generate_elimination_principles uri refinement_toolkit; + (* uris := !uris @ generate_inversion refinement_toolkit uri obj; *) let rec get_record_attrs = function | [] -> None @@ -340,7 +347,7 @@ let add_obj refinement_toolkit uri obj ~basedir = | None -> () (* not a record *) | Some fields -> uris := !uris @ - (generate_projections ~basedir refinement_toolkit uri fields)) + (generate_projections refinement_toolkit uri fields)) | Cic.CurrentProof _ | Cic.Variable _ -> assert false end;