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
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 *)
(univgraphuri,xmlunivgraphpath) ::
(* now the optional body, both write and register *)
(match bodyxml,bodyuri with
- None,None -> []
+ None,_ -> []
| Some bodyxml,Some bodyuri->
ensure_path_exists xmlbodypath;
Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
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) &&*)
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))
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 _ -> ());
(*** 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
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
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
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
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
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 =
+ match !build_inversion_principle uri obj with
+ None -> []
+ | Some (ind_uri,ind_obj) ->
+ 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
| Cic.Constant _ -> ()
| Cic.InductiveDefinition (_,_,_,attrs) ->
uris := !uris @
- generate_elimination_principles ~basedir uri refinement_toolkit;
+ generate_elimination_principles uri refinement_toolkit;
+ uris := !uris @ generate_inversion refinement_toolkit uri obj;
let rec get_record_attrs =
function
| [] -> None
| 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;
projects / helm.git / blobdiff