From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Dec 2016 10:45:19 +0100 Subject: Removing most nf_enter in tactics. Now they are useless because all of the primitives are (should?) be evar-insensitive. --- tactics/tacticals.ml | 140 +++++++++++++++++++++++++-------------------------- 1 file changed, 68 insertions(+), 72 deletions(-) (limited to 'tactics/tacticals.ml') diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 94f22f903..27c1987a0 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -267,40 +267,6 @@ let pf_with_evars glsev k gls = let pf_constr_of_global gr k = pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k -(* computing the case/elim combinators *) - -let gl_make_elim ind gl = - let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in - let (sigma, c) = pf_apply Evd.fresh_global gl gr in - (sigma, EConstr.of_constr c) - -let gl_make_case_dep ind gl = - let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in - let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true - (elimination_sort_of_goal gl) - in - (Sigma.to_evar_map sigma, EConstr.of_constr r) - -let gl_make_case_nodep ind gl = - let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in - let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false - (elimination_sort_of_goal gl) - in - (Sigma.to_evar_map sigma, EConstr.of_constr r) - -let make_elim_branch_assumptions ba gl = - let assums = - try List.rev (List.firstn ba.nassums (pf_hyps gl)) - with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in - { ba = ba; assums = assums } - -let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl - -let make_case_branch_assumptions = make_elim_branch_assumptions - -let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl - - (** Tacticals of Ltac defined directly in term of Proofview *) module New = struct open Proofview @@ -534,7 +500,7 @@ module New = struct Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if let tclDELAYEDWITHHOLES check x tac = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let Sigma (x, sigma, _) = x.delayed env sigma in @@ -578,13 +544,13 @@ module New = struct let onLastHyp = onNthHyp 1 let onNthDecl m tac = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> Proofview.tclUNIT (nthDecl m gl) >>= tac end } let onLastDecl = onNthDecl 1 let ifOnHyp pred tac1 tac2 id = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let typ = Tacmach.New.pf_get_hyp_typ id gl in if pred (id,typ) then tac1 id @@ -592,7 +558,7 @@ module New = struct tac2 id end } - let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end } + let onHyps find tac = Proofview.Goal.enter { enter = begin fun gl -> tac (find.enter gl) end } let afterHyp id tac = Proofview.Goal.enter { enter = begin fun gl -> @@ -625,13 +591,13 @@ module New = struct (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim isrec allnames tac predicate ind (c, t) = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma, elim = (mk_elim ind).enter gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Proofview.Goal.nf_enter { enter = begin fun gl -> - let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in + (Proofview.Goal.enter { enter = begin fun gl -> + let indclause = mk_clenv_from gl (c, t) in (* applying elimination_scheme just a little modified *) - let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in + let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim) in let indmv = match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with | Meta mv -> mv @@ -660,7 +626,7 @@ module New = struct | None -> elimclause' | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' in - let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in + let clenv' = clenv_unique_resolver ~flags elimclause' gl in let after_tac i = let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in let ba = { branchsign = branchsigns.(i); @@ -679,8 +645,64 @@ module New = struct (Proofview.tclEXTEND [] tclIDTAC branchtacs) end }) end } + let elimination_sort_of_goal gl = + (** Retyping will expand evars anyway. *) + let c = Proofview.Goal.concl (Goal.assume gl) in + pf_apply Retyping.get_sort_family_of gl c + + let elimination_sort_of_hyp id gl = + (** Retyping will expand evars anyway. *) + let c = pf_get_hyp_typ id (Goal.assume gl) in + pf_apply Retyping.get_sort_family_of gl c + + let elimination_sort_of_clause id gl = match id with + | None -> elimination_sort_of_goal gl + | Some id -> elimination_sort_of_hyp id gl + + (* computing the case/elim combinators *) + + let gl_make_elim ind = { enter = begin fun gl -> + let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in + let (sigma, c) = pf_apply Evd.fresh_global gl gr in + (sigma, EConstr.of_constr c) + end } + + let gl_make_case_dep ind = { enter = begin fun gl -> + let sigma = Sigma.Unsafe.of_evar_map (project gl) in + let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true + (elimination_sort_of_goal gl) + in + (Sigma.to_evar_map sigma, EConstr.of_constr r) + end } + + let gl_make_case_nodep ind = { enter = begin fun gl -> + let sigma = Sigma.Unsafe.of_evar_map (project gl) in + let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false + (elimination_sort_of_goal gl) + in + (Sigma.to_evar_map sigma, EConstr.of_constr r) + end } + + let make_elim_branch_assumptions ba hyps = + let assums = + try List.rev (List.firstn ba.nassums hyps) + with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in + { ba = ba; assums = assums } + + let elim_on_ba tac ba = + Proofview.Goal.enter { enter = begin fun gl -> + let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in + tac branches + end } + + let case_on_ba tac ba = + Proofview.Goal.enter { enter = begin fun gl -> + let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in + tac branches + end } + let elimination_then tac c = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with @@ -696,34 +718,8 @@ module New = struct let case_nodep_then_using = general_elim_then_using gl_make_case_nodep false - let elim_on_ba tac ba = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in - tac branches - end } - - let case_on_ba tac ba = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in - tac branches - end } - - let elimination_sort_of_goal gl = - (** Retyping will expand evars anyway. *) - let c = Proofview.Goal.concl (Goal.assume gl) in - pf_apply Retyping.get_sort_family_of gl c - - let elimination_sort_of_hyp id gl = - (** Retyping will expand evars anyway. *) - let c = pf_get_hyp_typ id (Goal.assume gl) in - pf_apply Retyping.get_sort_family_of gl c - - let elimination_sort_of_clause id gl = match id with - | None -> elimination_sort_of_goal gl - | Some id -> elimination_sort_of_hyp id gl - let pf_constr_of_global ref tac = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (sigma, c) = Evd.fresh_global env sigma ref in -- cgit v1.2.3