From 29a5127dac6d4fbc317e38452cf0fe05916adc56 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 26 Oct 2014 14:23:00 +0100 Subject: Fixing destruct/induction with a using clause on a non-inductive type, that was broken by commit bf01856940 + use types from induction scheme to restrict selection of pattern + accept matching from partially applied term when using "using". --- tactics/tactics.ml | 58 ++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 45 insertions(+), 13 deletions(-) (limited to 'tactics/tactics.ml') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2f64fd351..009a1d2ac 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2254,7 +2254,8 @@ let letin_pat_tac with_eq id c occs = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.concl gl in - let abs = AbstractPattern (false,id,c,AtOccs occs,false) in + let check t = true in + let abs = AbstractPattern (false,check,id,c,AtOccs occs,false) in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in let sigma,c = match res with | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c @@ -3789,8 +3790,9 @@ let clear_induction_arg_if_hyp is_arg_pure_hyp c env = else env -let make_body env sigma is_arg_pure_hyp c lbind t = - let mind,typ = reduce_to_quantified_ind env sigma t in +let make_body env sigma (is_arg_pure_hyp,_) c lbind t = + let decls,t = splay_prod env sigma t in + let typ = it_mkProd t decls in let indclause = make_clenv_binding env sigma (c,typ) lbind in let env = clear_induction_arg_if_hyp is_arg_pure_hyp c env in let evdref = ref indclause.evd in @@ -3811,7 +3813,37 @@ let make_body env sigma is_arg_pure_hyp c lbind t = (* side-effect *) (!evdref, c) -let pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim +let check_expected_type env sigma (elimc,bl) t = + (* Compute the expected template type of the term in case a using + clause is given *) + let elimt = typ_of env sigma elimc in + let sign,_ = splay_prod env sigma elimt in + let n = List.length sign in + if n == 0 then error "Scheme cannot be applied."; + let sigma,cl = make_evar_clause env sigma (Some (n-1)) elimt in + let sigma = solve_evar_clause env sigma true cl bl in + let (_,u,_) = destProd cl.cl_concl in + Evarconv.e_cumul env (ref sigma) t u + +let check_enough_applied env sigma elim = + (* A heuristic to decide whether the induction arg is enough applied *) + match elim with + | None -> + (* No eliminator given *) + fun u -> + let t,_ = decompose_app (whd_betadeltaiota env sigma u) in isInd t + | Some elimc -> + let elimt = typ_of env sigma (fst elimc) in + let scheme = compute_elim_sig ~elimc elimt in + fun u -> match scheme.indref with + | None -> + (* in the absence of information, do not assume it may be + partially applied *) + true + | Some gr -> + check_expected_type env sigma elimc u + +let pose_induction_arg clear_flag isrec with_evars info_arg elim id ((pending,(c0,lbind)),(eqname,names)) t inhyps cls = Proofview.Goal.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -3819,16 +3851,17 @@ let pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim Proofview.Refine.refine ~unsafe:true begin fun sigma -> let (sigma',c') = use_bindings env sigma (c0,lbind) t in let occs = match cls with None -> LikeFirst | Some occs -> AtOccs occs in - let abs = AbstractPattern (true,Name id,(pending,c'),occs,false) in + let check = check_enough_applied env sigma elim in + let abs = AbstractPattern (snd info_arg,check,Name id,(pending,c'),occs,false) in let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in match res with | None -> (* pattern not found *) let (sigma,c0) = finish_evar_resolution ~flags:(tactic_infer_flags with_evars) env sigma (pending,c0) in - let (sigma,c) = make_body env sigma is_arg_pure_hyp c0 lbind t in + let (sigma,c) = make_body env sigma info_arg c0 lbind t in let t = Retyping.get_type_of env sigma c in let with_eq = Option.map (fun eq -> (false,eq)) eqname in - let env = clear_induction_arg_if_hyp is_arg_pure_hyp c0 env in + let env = clear_induction_arg_if_hyp (fst info_arg) c0 env in mkletin_goal env sigma with_eq false (id,lastlhyp,ccl,c) (Some t) | Some (sigma',c) -> @@ -3840,9 +3873,6 @@ let pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim end end -let isIndType env sigma t = - try let _ = find_mrectype env sigma t in true with Not_found -> false - let induction_gen clear_flag isrec with_evars elim ((_pending,(c,lbind)),(eqname,names) as arg) cls = let inhyps = match cls with @@ -3856,7 +3886,8 @@ let induction_gen clear_flag isrec with_evars elim isVar c && not (mem_named_context (destVar c) (Global.named_context())) && lbind == NoBindings && not with_evars && Option.is_empty eqname && not (has_selected_occurrences cls) in - if is_arg_pure_hyp && isIndType env sigma t then + let enough_applied = check_enough_applied env sigma elim t in + if is_arg_pure_hyp && enough_applied then (* First case: induction on a variable already in an inductive type and with maximal abstraction over the variable. This is a situation where the induction argument is a @@ -3874,11 +3905,12 @@ let induction_gen clear_flag isrec with_evars elim (* Type not the right one if partially applied but anyway for internal use*) let x = id_of_name_using_hdchar (Global.env()) t Anonymous in new_fresh_id [] x gl in + let info_arg = (is_arg_pure_hyp, not enough_applied) in if isrec then (* Historically, induction has side conditions last *) Tacticals.New.tclTHENFIRST (Tacticals.New.tclTHENLIST [ - pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim id arg t inhyps cls; + pose_induction_arg clear_flag isrec with_evars info_arg elim id arg t inhyps cls; if with_evars (* do not give a success semantics to edestruct on an open term yet *) @@ -3893,7 +3925,7 @@ let induction_gen clear_flag isrec with_evars elim (* Historically, destruct has side conditions first *) Tacticals.New.tclTHENLAST (Tacticals.New.tclTHENLIST [ - pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim id arg t inhyps cls; + pose_induction_arg clear_flag isrec with_evars info_arg elim id arg t inhyps cls; if with_evars (* do not give a success semantics to edestruct on an open term yet *) -- cgit v1.2.3