From be16471f978380deb789b3b70c92d998addbb350 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 4 Sep 2006 11:27:49 +0000 Subject: [PATCH] Generation of inductive and inversion principles for mutual inductive types (before only single types were allowed). --- components/library/cicElim.ml | 3 +- components/library/librarySync.ml | 44 ++++--- components/library/librarySync.mli | 2 +- components/tactics/inversion.ml | 11 +- components/tactics/inversion_principle.ml | 137 ++++++++++++---------- 5 files changed, 111 insertions(+), 86 deletions(-) diff --git a/components/library/cicElim.ml b/components/library/cicElim.ml index fb3c0655c..f919d2875 100644 --- a/components/library/cicElim.ml +++ b/components/library/cicElim.ml @@ -409,7 +409,8 @@ debug_print (lazy (CicPp.ppterm eliminator_body)); | Cic.Type _ -> "_rect" | _ -> assert false in - let name = UriManager.name_of_uri uri ^ suffix in + (* let name = UriManager.name_of_uri uri ^ suffix in *) + let name = name ^ suffix in let buri = UriManager.buri_of_uri uri in let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in let obj_attrs = [`Class (`Elim sort); `Generated] in diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index e1b73821b..1db8f0cfc 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -178,19 +178,30 @@ let remove_single_obj uri = 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 ***********************************************************) @@ -350,11 +361,10 @@ let generate_projections refinement_toolkit uri fields = 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; diff --git a/components/library/librarySync.mli b/components/library/librarySync.mli index b29a0aa03..61e2b2515 100644 --- a/components/library/librarySync.mli +++ b/components/library/librarySync.mli @@ -26,7 +26,7 @@ exception AlreadyDefined of UriManager.uri (* this is a pointer to the function which builds the inversion principle *) -val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) option) ref +val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) list) ref (* adds an object to the library together with all auxiliary lemmas on it *) (* (e.g. elimination principles, projections, etc.) *) diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml index 74117f710..e381b3003 100644 --- a/components/tactics/inversion.ml +++ b/components/tactics/inversion.ml @@ -306,14 +306,17 @@ let inversion_tac ~term = let (_,metasenv,_,_) = proof in let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in - let uri = baseuri_of_term termty in + let uri, typeno = + match termty with + | Cic.MutInd (uri,typeno,_) + | Cic.Appl(Cic.MutInd (uri,typeno,_)::_) -> uri,typeno + | _ -> assert false + in + (* let uri = baseuri_of_term termty in *) let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in let name,nleft,arity,cons_list = match obj with Cic.InductiveDefinition (tys,_,nleft,_) -> - (*we suppose there is only one inductiveType in the definition, - so typeno=0 identically *) - let typeno = 0 in let (name,_,arity,cons_list) = List.nth tys typeno in (name,nleft,arity,cons_list) |_ -> assert false diff --git a/components/tactics/inversion_principle.ml b/components/tactics/inversion_principle.ml index 8031e7bbd..1d56cab72 100644 --- a/components/tactics/inversion_principle.ml +++ b/components/tactics/inversion_principle.ml @@ -132,70 +132,81 @@ let rec build_theorem rightparam_tys arity_l (*arity_l only to name p's*) let build_inversion uri obj = (*uri e obj of InductiveDefinition *) let module PET = ProofEngineTypes in - let typeno = 0 in - let name,nleft,arity,cons_list = - match obj with - Cic.InductiveDefinition (tys,_,nleft,_) -> - let (name,_,arity,cons_list) = List.nth tys typeno in - (*we suppose there is only one inductiveType, so typeno=0 identically *) - (name,nleft,arity,cons_list) - |_ -> assert false + let build_one typeno name nleft arity cons_list = + (*check if there are right parameters, else return void*) + if List.length (list_of_prod arity) = (nleft + 1) then + None + else + try + let arity_l = cut_last (list_of_prod arity) in + let rightparam_tys = cut_first nleft arity_l in + let theorem = build_theorem rightparam_tys arity_l arity cons_list + [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in + debug_print + (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem))); + let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem + CicUniv.empty_ugraph in + (*DEBUG*) debug_print + (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem))); + let buri = UriManager.buri_of_uri uri in + let inversor_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in + let goal = CicMkImplicit.new_meta metasenv [] in + let metasenv' = (goal,[],ref_theorem)::metasenv in + let proof= + (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem) in + let _,applies = + List.fold_right + (fun _ (i,applies) -> + i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies) + cons_list (2,[]) + in + let proof1,gl1 = + PET.apply_tactic + (Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ()) + (*if the number of applies is 1, we cannot use + thens, but then_*) + ~continuation: + (match (List.length applies) with + 0 -> (Inversion.private_inversion_tac (Cic.Rel 1)) + | 1 -> (Tacticals.then_ + ~start:(Inversion.private_inversion_tac + (Cic.Rel 1)) + ~continuation:(PrimitiveTactics.apply_tac + (Cic.Rel 2)) + ) + | _ -> (Tacticals.thens + ~start:(Inversion.private_inversion_tac + (Cic.Rel 1)) + ~continuations:applies + ) + )) + (proof,goal) + in + let metasenv,bo,ty = + match proof1 with (_,metasenv,bo,ty) -> metasenv,bo,ty + in + assert (metasenv = []); + Some + (inversor_uri, + Cic.Constant + (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[])) + with + Inversion.EqualityNotDefinedYet -> None in - (*check if there are right parameters, else return void*) - if List.length (list_of_prod arity) = (nleft + 1) then - None - else - try - let arity_l = cut_last (list_of_prod arity) in - let rightparam_tys = cut_first nleft arity_l in - let theorem = build_theorem rightparam_tys arity_l arity cons_list - [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in - (*DEBUG*) debug_print (lazy ("theorem prima di refine: " ^ (CicPp.ppterm - theorem))); - let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem - CicUniv.empty_ugraph in - (*DEBUG*) debug_print (lazy ("theorem dopo refine: " ^ (CicPp.ppterm - ref_theorem))); - let buri = UriManager.buri_of_uri uri in - let inversor_uri = - UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in - let goal = CicMkImplicit.new_meta metasenv [] in - let metasenv' = (goal,[],ref_theorem)::metasenv in - let proof= (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem) in - let _,applies = - List.fold_right - (fun _ (i,applies) -> - i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies) - cons_list (2,[]) - in - let proof1,gl1 = - PET.apply_tactic - (Tacticals.then_ - ~start:(PrimitiveTactics.intros_tac ()) - (*if the number of applies is 1, we cannot use thens, but then_*) - ~continuation: - (match (List.length applies) with - 0 -> (Inversion.private_inversion_tac (Cic.Rel 1)) - | 1 -> (Tacticals.then_ - ~start:(Inversion.private_inversion_tac (Cic.Rel 1)) - ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) - ) - | _ -> (Tacticals.thens - ~start:(Inversion.private_inversion_tac (Cic.Rel 1)) - ~continuations:applies - ) - )) - (proof,goal) - in - let metasenv,bo,ty = - match proof1 with (_,metasenv,bo,ty) -> metasenv,bo,ty - in - assert (metasenv = []); - Some - (inversor_uri, - Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[])) - with - Inversion.EqualityNotDefinedYet -> None + match obj with + | Cic.InductiveDefinition (tys,_,nleft,_) -> + let counter = ref (List.length tys) in + List.fold_right + (fun (name,_,arity,cons_list) res -> + counter := !counter-1; + match build_one !counter name nleft arity cons_list with + | None -> res + | Some inv -> inv::res) + tys [] + |_ -> assert false + ;; let init () = ();; -- 2.39.2