X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion_principle.ml;h=3229a261b46f82640d05a52a78ece4ecc4dabd3b;hb=7f9e313fe5ae4200f080f481a6b8b795a0618093;hp=ae0a481862797155d34e48db7d3ebdc5608b0581;hpb=84e6cbe962c9a534be48542c098d7bb0d90be9a1;p=helm.git diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml index ae0a48186..3229a261b 100644 --- a/helm/software/components/tactics/inversion_principle.ml +++ b/helm/software/components/tactics/inversion_principle.ml @@ -129,93 +129,116 @@ let rec build_theorem rightparam_tys arity_l (*arity_l only to name p's*) [(Cic.Rel 1)] uri typeno ) ;; +let build_one typeno inversor_uri indty_uri nleft arity cons_list selections = + (*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 indty_uri typeno in + debug_print + (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem))); + let (ref_theorem,_,metasenv,_) = + CicRefine.type_of_aux' [] [] theorem CicUniv.oblivion_ugraph in + (*DEBUG*) debug_print + (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem))); + let goal = CicMkImplicit.new_meta metasenv [] in + let metasenv' = (goal,[],ref_theorem)::metasenv in + let attrs = [`Class (`InversionPrinciple); `Generated] in + let _subst = [] in + let proof= + Some inversor_uri,metasenv',_subst, + lazy (Cic.Meta(goal,[])),ref_theorem, attrs 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 = + ProofEngineTypes.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) selections + | 1 -> + Tacticals.then_ + ~start:(Inversion.private_inversion_tac (Cic.Rel 1) selections) + ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) + | _ -> + Tacticals.thens + ~start:(Inversion.private_inversion_tac (Cic.Rel 1) selections) + ~continuations:applies)) + (proof,goal) in + let _,metasenv,_subst,bo,ty, attrs = proof1 in + assert (metasenv = []); + Some + (inversor_uri, + Cic.Constant + (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[])) + with + Inversion.EqualityNotDefinedYet -> + HLog.warn "No default equality, no inversion principle"; + None + | CicRefine.RefineFailure ls -> + HLog.warn + ("CicRefine.RefineFailure during generation of inversion principle: " ^ + Lazy.force ls) ; + None + | CicRefine.Uncertain ls -> + HLog.warn + ("CicRefine.Uncertain during generation of inversion principle: " ^ + Lazy.force ls) ; + None + | CicRefine.AssertFailure ls -> + HLog.warn + ("CicRefine.AssertFailure during generation of inversion principle: " ^ + Lazy.force ls) ; + None +;; + +let build_inverter ~add_obj status u indty_uri params = + let indty_uri, indty_no, _ = UriManager.ind_uri_split indty_uri in + let indty_no = match indty_no with None -> raise (Invalid_argument "not an inductive type")| Some n -> n in + let indty, univ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph indty_uri + in + match indty with + | Cic.InductiveDefinition (tys,_,nleft,attrs) -> + let _,inductive,_,_ = List.hd tys in + if not inductive then raise (Invalid_argument "not an inductive type") + else + let name,_,arity,cons_list = List.nth tys (indty_no-1) in + (match build_one (indty_no-1) u indty_uri nleft arity cons_list params with + | None -> status,[] + | Some (uri, obj) -> + let status, added = add_obj uri obj status in + status, uri::added) + | _ -> assert false +;; + let build_inversion ~add_obj ~add_coercion uri obj = match obj with | Cic.InductiveDefinition (tys,_,nleft,attrs) -> let _,inductive,_,_ = List.hd tys in if not inductive then [] else - 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.oblivion_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 attrs = [`Class (`InversionPrinciple); `Generated] in - let _subst = [] in - let proof= - Some inversor_uri,metasenv',_subst, - lazy (Cic.Meta(goal,[])),ref_theorem, attrs 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 = - ProofEngineTypes.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,_subst,bo,ty, attrs = proof1 in - assert (metasenv = []); - Some - (inversor_uri, - Cic.Constant - (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[])) - with - Inversion.EqualityNotDefinedYet -> - HLog.warn "No default equality, no inversion principle"; - None - | CicRefine.RefineFailure ls -> - HLog.warn - ("CicRefine.RefineFailure during generation of inversion principle: " ^ - Lazy.force ls) ; - None - | CicRefine.Uncertain ls -> - HLog.warn - ("CicRefine.Uncertain during generation of inversion principle: " ^ - Lazy.force ls) ; - None - | CicRefine.AssertFailure ls -> - HLog.warn - ("CicRefine.AssertFailure during generation of inversion principle: " ^ - Lazy.force ls) ; - None - in let counter = ref (List.length tys) in let all_inverters = List.fold_right (fun (name,_,arity,cons_list) res -> + let arity_l = cut_last (list_of_prod arity) in + let rightparam_tys = cut_first nleft arity_l in + let params = HExtlib.mk_list true (List.length rightparam_tys) in + let buri = UriManager.buri_of_uri uri in + let inversor_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in counter := !counter-1; - match build_one !counter name nleft arity cons_list with + match build_one !counter inversor_uri uri nleft arity cons_list params with None -> res | Some inv -> inv::res ) tys [] @@ -226,6 +249,5 @@ let build_inversion ~add_obj ~add_coercion uri obj = | _ -> [] ;; - let init () = LibrarySync.add_object_declaration_hook build_inversion;;