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
xmlunivgraphpath, univgraphuri =
paths_and_uris_of_obj uri
in
- List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
+ write (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;
+ 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) ::
(match bodyxml,bodyuri with
None,_ -> []
| Some bodyxml,Some bodyuri->
- ensure_path_exists xmlbodypath;
- Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
+ write ensure_path_exists xmlbodypath;
+ write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath);
[bodyuri, xmlbodypath]
| _-> assert false)
in
aux ty
in
+ let already_in =
+ List.exists
+ (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+ (CoercDb.to_list ())
+ in
let ty_src, ty_tgt = extract_last_two_p coer_ty in
let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
- let new_coercions =
- CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri in
- let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
- (* update the DB *)
- List.iter
- (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
- new_coercions;
- 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 = []);
- []
- end
+ if not add_composites then
+ (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
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 new_coercions =
+ CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri
+ in
+ let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
+ if already_in then
+ (* this if starts here just to be sure the closure function works fine *)
+ begin
+ assert (new_coercions = []);
+ HLog.warn
+ (UriManager.string_of_uri uri ^
+ " is already declared as a coercion! skipping...");
+ []
+ end
+ else
+ begin
+ (* update the DB *)
+ 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 uri obj refinement_toolkit;
+ uri::acc)
+ [] 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 []);
+ (*
+ prerr_endline ("lemmas:");
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ lemmas;
+ prerr_endline ("lemmas END");*)
+ lemmas
+ end
+;;
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);
+ (*prerr_endline ("removing: " ^UriManager.string_of_uri uri);
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- composites_in_db;
+ composites_in_db;*)
UriManager.UriHashtbl.remove coercion_hashtbl uri;
CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
(* remove from the DB *)
add_single_obj uri obj refinement_toolkit;
let composites =
if coercion then
- add_coercion ~add_composites:true refinement_toolkit uri
+ begin
+(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
+ let x = add_coercion ~add_composites:true refinement_toolkit uri
+ in
+(*prerr_endline ("are: ");
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
+ prerr_endline "---";
+*)
+ x
+ end
else
[]
in
| Cic.InductiveDefinition (_,_,_,attrs) ->
uris := !uris @
generate_elimination_principles uri refinement_toolkit;
- uris := !uris @ generate_inversion refinement_toolkit uri obj;
+ uris := !uris @ generate_inversion refinement_toolkit uri obj;
let rec get_record_attrs =
function
| [] -> None
projects / helm.git / blobdiff