From f6263eadaa2b8d0bc0c2a5a944e0d4641c356fe9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 13 Sep 2006 17:22:21 +0000 Subject: [PATCH] Bug fixed in injection: injection can now work on inductive types that have right parameters. It is still bugged on inductive types with left parameters. --- components/tactics/discriminationTactics.ml | 116 +++++++++++++------- 1 file changed, 78 insertions(+), 38 deletions(-) diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml index 9c9998907..97e9597c6 100644 --- a/components/tactics/discriminationTactics.ml +++ b/components/tactics/discriminationTactics.ml @@ -115,35 +115,72 @@ and injection1_tac ~term ~i = let tty',_ = CicTypeChecker.type_of_aux' metasenv context t1' CicUniv.empty_ugraph in - let pattern = - match fst(CicEnvironment.get_obj - CicUniv.empty_ugraph turi ) with - C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx,_) -> - let _,_,_,constructor_list = (List.nth ind_type_list typeno) in - let i_constr_id,_ = List.nth constructor_list (consno - 1) in - List.map - (function (id,cty) -> - let reduced_cty = CicReduction.whd context cty in - let rec aux t k = - match t with - C.Prod (_,_,target) when (k <= nr_ind_params_dx) -> - aux target (k+1) - | C.Prod (binder,source,target) when (k > nr_ind_params_dx) -> - let binder' = - match binder with - C.Name b -> C.Name b - | C.Anonymous -> C.Name "y" - in - C.Lambda (binder',source,(aux target (k+1))) - | _ -> - let nr_param_constr = k - 1 - nr_ind_params_dx in - if (id = i_constr_id) - then C.Rel (nr_param_constr - i + 1) - else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda agguinto esternamente al case *) - in aux reduced_cty 1 - ) - constructor_list - | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible")) + let patterns,outtype = + match + fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) + with + C.InductiveDefinition (ind_type_list,_,paramsno,_)-> + let _,_,_,constructor_list = + List.nth ind_type_list typeno in + let i_constr_id,_ = + List.nth constructor_list (consno - 1) in + let patterns = + List.map + (function (id,cty) -> + let reduced_cty = CicReduction.whd context cty in + let rec aux t k = + match t with + C.Prod (_,_,target) when k <= paramsno -> + aux target (k+1) + | C.Prod (binder,source,target) when k > paramsno -> + let binder' = + match binder with + C.Name b -> C.Name b + | C.Anonymous -> C.Name "y" + in + C.Lambda (binder',source,(aux target (k+1))) + | _ -> + let nr_param_constr = k - 1 - paramsno in + if id = i_constr_id + then C.Rel (nr_param_constr - i + 1) + else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda aggiunto esternamente al case *) + in aux reduced_cty 1 + ) constructor_list in + let outtype = + let rec to_lambdas te head = + match CicReduction.whd context te with + | C.Prod (name,so,ta) -> + C.Lambda (name,so,to_lambdas ta head) + | _ -> head in + let rec skip_prods n te = + match n, CicReduction.whd context te with + 0, _ -> te + | n, C.Prod (_,_,ta) -> skip_prods (n - 1) ta + | _, _ -> assert false + in + let abstracted_tty = + match CicSubstitution.lift (paramsno + 1) tty with + C.MutInd _ as tty' -> tty' + | C.Appl l -> + let keep,abstract = + HExtlib.split_nth (paramsno +1) l in + let rec mk_rels = + function + 0 -> [] + | n -> C.Rel n :: (mk_rels (n - 1)) + in + C.Appl (keep@mk_rels (List.length abstract)) + | _ -> assert false + in + match ind_type_list with + [] -> assert false + | (_,_,ty,_)::_ -> + to_lambdas (skip_prods paramsno ty) + (C.Lambda (C.Name "x", abstracted_tty, + S.lift (2+paramsno) tty')) + in + patterns,outtype + | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible")) in ProofEngineTypes.apply_tactic (T.thens @@ -170,15 +207,18 @@ and injection1_tac ~term ~i = ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1')) (fun _ m u -> - C.Appl [ C.Lambda (C.Name "x", tty, - C.MutCase (turi, typeno, - (C.Lambda ((C.Name "x"), - (S.lift 1 tty), - (S.lift 2 tty'))), - (C.Rel 1), pattern - ) - ); - t1], m, u)) +let xxx = + C.Appl [ + C.Lambda + (C.Name "x", + tty, + C.MutCase + (turi,typeno,outtype,C.Rel 1,patterns)) ; + t1] +in +(*prerr_endline ("XXX: " ^ CicPp.ppterm xxx);*) +xxx, + m, u)) status )) ~continuation: -- 2.39.2