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 *)
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
if add_composites then
List.fold_left
(fun acc (_,_,uri,obj) ->
- add_single_obj ~basedir uri obj refinement_toolkit;
+ add_single_obj uri obj refinement_toolkit;
uri::acc)
composite_uris new_coercions
else
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 ~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
| 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
| 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