diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-09-25 09:49:37 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-25 09:49:37 +0200 |
commit | 00aa9287eb73ce9f3b41444ed23bc370cde828aa (patch) | |
tree | f32a276ba6bcb9fbf8ca560567b44f8d86a7e3bd /tactics | |
parent | 836e0df2ee3cec97adcadd70be218d9c57bbc313 (diff) | |
parent | 9bc2b3d6d0f7d02843180bca5a4d1f908e8a6141 (diff) |
Merge PR #1060: An optimization of tactic constructor
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/tactics.ml | 59 |
1 files changed, 30 insertions, 29 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d0165c555..f1dd61358 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2219,27 +2219,27 @@ let check_number_of_constructors expctdnumopt i nconstr = end; if i > nconstr then error "Not enough constructors." -let constructor_tac with_evars expctdnumopt i lbind = +let constructor_core with_evars cstr lbind = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let (sigma, (cons, u)) = Evd.fresh_constructor_instance env sigma cstr in + let cons = mkConstructU (cons, EInstance.make u) in + let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) apply_tac + end + +let constructor_tac with_evars expctdnumopt i lbind = + Proofview.Goal.enter begin fun gl -> let cl = Tacmach.New.pf_concl gl in - let reduce_to_quantified_ind = - Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl - in - let (mind,redcl) = reduce_to_quantified_ind cl in - let nconstr = - Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in - check_number_of_constructors expctdnumopt i nconstr; - - let (sigma, (cons, u)) = Evd.fresh_constructor_instance - (Proofview.Goal.env gl) sigma (fst mind, i) in - let cons = mkConstructU (cons, EInstance.make u) in - - let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in - Tacticals.New.tclTHENLIST - [ Proofview.Unsafe.tclEVARS sigma; - convert_concl_no_check redcl DEFAULTcast; - intros; apply_tac] + let ((ind,_),redcl) = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl cl in + let nconstr = Array.length (snd (Global.lookup_inductive ind)).mind_consnames in + check_number_of_constructors expctdnumopt i nconstr; + Tacticals.New.tclTHENLIST [ + convert_concl_no_check redcl DEFAULTcast; + intros; + constructor_core with_evars (ind, i) lbind + ] end let one_constructor i lbind = constructor_tac false None i lbind @@ -2251,23 +2251,24 @@ let one_constructor i lbind = constructor_tac false None i lbind let any_constructor with_evars tacopt = let one_constr = - let tac i = constructor_tac with_evars None i NoBindings in + let tac cstr = constructor_core with_evars cstr NoBindings in match tacopt with | None -> tac - | Some t -> fun i -> Tacticals.New.tclTHEN (tac i) t in - let rec any_constr n i () = - if Int.equal i n then one_constr i - else Tacticals.New.tclORD (one_constr i) (any_constr n (i + 1)) in + | Some t -> fun cstr -> Tacticals.New.tclTHEN (tac cstr) t in + let rec any_constr ind n i () = + if Int.equal i n then one_constr (ind,i) + else Tacticals.New.tclORD (one_constr (ind,i)) (any_constr ind n (i + 1)) in Proofview.Goal.enter begin fun gl -> let cl = Tacmach.New.pf_concl gl in - let reduce_to_quantified_ind = - Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl - in - let mind = fst (reduce_to_quantified_ind cl) in + let (ind,_),redcl = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl cl in let nconstr = - Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in + Array.length (snd (Global.lookup_inductive ind)).mind_consnames in if Int.equal nconstr 0 then error "The type has no constructors."; - any_constr nconstr 1 () + Tacticals.New.tclTHENLIST [ + convert_concl_no_check redcl DEFAULTcast; + intros; + any_constr ind nconstr 1 () + ] end let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 |