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 _ -> ());
+ ) files_to_remove ;
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 ->
+ ignore (LibraryDb.remove_uri uri);
+ (*CoercGraph.remove_coercion uri;*)
+ CicEnvironment.remove_obj uri
+ ) uris_to_remove
(*** 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 =
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 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 =
List.exists
- (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+ (fun (s,t,ul) ->
+ List.exists
+ (fun u ->
+ UriManager.eq u uri &&
+ CoercDb.eq_carr s src_carr &&
+ CoercDb.eq_carr t tgt_carr)
+ 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
if not add_composites then
(CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
else
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
if coercion then
begin
(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
- let x = add_coercion ~add_composites:true refinement_toolkit uri
+ let x =
+ add_coercion ~add_composites:true refinement_toolkit uri arity
in
(*prerr_endline ("are: ");
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
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 add_obj refinement_toolkit uri obj =
add_single_obj uri obj refinement_toolkit;
projects / helm.git / blobdiff