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)
let module RT = RefinementTool in
let obj =
if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
- not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
+ not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
then
refinement_toolkit.RT.pack_coercion_obj obj
else
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
+ let uris_to_remove =
+ if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
+ in
+ let files_to_remove = uri :: derived_uris_of_uri uri in
List.iter
- (fun uri ->
- (try
- 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 _ -> ());
- ignore (LibraryDb.remove_uri uri);
- (*CoercGraph.remove_coercion uri;*)
- CicEnvironment.remove_obj uri)
- to_remove
+ (fun uri ->
+ (try
+ 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 _ -> ());
+ ) files_to_remove ;
+ List.iter
+ (fun uri ->
+ ignore (LibraryDb.remove_uri uri);
+ (*CoercGraph.remove_coercion uri;*)
+ ) uris_to_remove ;
+ CicEnvironment.remove_obj uri
(*** GENERATION OF AUXILIARY LEMMAS ***)
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;
- uris := uri :: !uris
- with CicElim.Can_t_eliminate -> ()
+ let elim i =
+ let elim sort =
+ try
+ let uri,obj = CicElim.elim_of ~sort uri i in
+ add_single_obj uri obj refinement_toolkit;
+ uris := uri :: !uris
+ with CicElim.Can_t_eliminate -> ()
+ in
+ try
+ List.iter
+ elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+ with exn ->
+ List.iter remove_single_obj !uris;
+ raise exn
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 (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+ match obj with
+ | Cic.InductiveDefinition (indTypes, _, _, _) ->
+ let counter = ref 0 in
+ List.iter (fun _ -> elim !counter; counter := !counter+1) indTypes;
+ !uris
+ | _ ->
+ failwith (Printf.sprintf "not an inductive definition (%s)"
+ (UriManager.string_of_uri uri))
(* COERCIONS ***********************************************************)
UriManager.UriHashtbl.clear coercion_hashtbl;
CoercDb.remove_coercion (fun (_,_,u1) -> true)
-let add_coercion ~add_composites refinement_toolkit uri =
+let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
let coer_ty,_ =
let coer = CicUtil.term_of_uri uri in
CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph
* should we saturate it with metas in case we insert it?
*
*)
- let extract_last_two_p ty =
+ let spline2list ty =
let rec aux = function
- | Cic.Prod( _, _, ((Cic.Prod _) as t)) ->
- aux t
- | Cic.Prod( _, src, tgt) -> src, tgt
- | _ -> assert false
+ | Cic.Prod( _, src, tgt) -> src::aux tgt
+ | t -> [t]
in
aux ty
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)
+ let src_carr, tgt_carr =
+ let list_remove_from_tail n l =
+ let rec aux n = function
+ | hd::tl when n > 0 -> aux (n-1) tl
+ | l when n = 0 -> l
+ | _ -> assert false
+ in
+ aux n (List.rev l)
+ in
+ let types = spline2list coer_ty in
+ match arity, list_remove_from_tail arity types with
+ | 0,tgt::src::_ ->
+ (* if ~delta is true, it is impossible to define an identity coercion *)
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+ | n,_::src::_ ->
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+ CoercDb.Fun arity
+ | _ -> assert false
+ in
+ let already_in_obj src_carr tgt_carr uri obj =
+ List.exists
+ (fun (s,t,ul) ->
+ List.exists
+ (fun u ->
+ let bo =
+ match obj with
+ | Cic.Constant (_, Some bo, _, _, _) -> bo
+ | _ -> assert false
+ in
+ CoercDb.eq_carr s src_carr &&
+ CoercDb.eq_carr t tgt_carr &&
+ if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
+ CicUniv.oblivion_ugraph)
+ then true else
+ (HLog.warn
+ ("Coercions " ^
+ UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
+ uri^" are not convertible, but are between the same nodes.\n"^
+ "From now on nification can fail randomly.");
+ false))
+ ul)
(CoercDb.to_list ())
- then
- begin
- assert (new_coercions = []);
- []
- end
+ in
+ 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
+ baseuri
+ in
+ let new_coercions =
+ List.filter (fun (s,t,u,obj) -> not(already_in_obj s t u obj))
+ new_coercions
+ 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;
+ 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 (_,tgt,uri,obj) ->
+ add_single_obj uri obj refinement_toolkit;
+ let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+ (uri,arity)::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
+;;
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 *)
let generate_projections refinement_toolkit uri fields =
let uris = ref [] in
- let projections = CicRecord.projections_of uri (List.map fst fields) in
+ let projections =
+ CicRecord.projections_of uri
+ (List.map (fun (x,_,_) -> x) fields)
+ in
try
List.iter2
- (fun (uri, name, bo) (_name, coercion) ->
+ (fun (uri, name, bo) (_name, coercion, arity) ->
try
let ty, ugraph =
CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
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);*)
+ (*CSC: I think there is a bug here. The composite coercions
+ are not remembered in the .moo file. Thus they are re-generated
+ every time. Right? *)
+ let x =
+ add_coercion ~add_composites:true refinement_toolkit uri arity
+ (UriManager.buri_of_uri uri)
+ in
+(*prerr_endline ("are: ");
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
+ prerr_endline "---";
+*)
+ (*CSC: I throw the arity away. See comment above *)
+ List.map fst x
+ end
else
[]
in
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]
+ List.map
+ (fun (ind_uri,ind_obj) ->
+ add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
+ (!build_inversion_principle uri obj)
+
+let
+ generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
+=
+ function
+ Cic.Fix (_,funs) ->
+ snd (
+ List.fold_right
+ (fun (name,idx,ty,bo) (n,uris) ->
+ if name = name_to_avoid then
+ (n+1,uris)
+ else
+ let uri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+ let bo = Cic.Fix (n,funs) in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ add_single_obj uri obj refinement_toolkit;
+ (n+1,uri::uris)
+ ) funs (1,[]))
+ | Cic.CoFix (_,funs) ->
+ snd (
+ List.fold_right
+ (fun (name,ty,bo) (n,uris) ->
+ if name = name_to_avoid then
+ (n+1,uris)
+ else
+ let uri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+ let bo = Cic.CoFix (n,funs) in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ add_single_obj uri obj refinement_toolkit;
+ (n+1,uri::uris)
+ ) funs (1,[]))
+ | _ -> assert false
let add_obj refinement_toolkit uri obj =
add_single_obj uri obj refinement_toolkit;
try
begin
match obj with
+ | Cic.Constant (name,Some bo,_,_,attrs) when
+ List.mem (`Flavour `MutualDefinition) attrs ->
+ uris :=
+ !uris @
+ generate_sibling_mutual_definitions refinement_toolkit uri attrs
+ name bo
| Cic.Constant _ -> ()
| 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