From 4aaeb5d429227505adfde9fe04c3c0fb69f2d37f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 24 May 2018 04:38:30 +0200 Subject: [api] Misctypes removal: tactic flags. We move the "flag types" to its use place, and mark some arguments with named parameters better. --- tactics/auto.ml | 2 +- tactics/class_tactics.ml | 2 +- tactics/elim.mli | 3 +-- tactics/equality.ml | 4 ++-- tactics/equality.mli | 2 +- tactics/tacticals.ml | 10 +++++----- tactics/tacticals.mli | 3 +-- tactics/tactics.ml | 12 ++++++++---- tactics/tactics.mli | 6 +++++- 9 files changed, 25 insertions(+), 19 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 77fe31415..d7de6c4fb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -99,7 +99,7 @@ let unify_resolve poly flags ((c : raw_hint), clenv) = Proofview.Goal.enter begin fun gl -> let clenv, c = connect_hint_clenv poly c clenv gl in let clenv = clenv_unique_resolver ~flags clenv gl in - Clenvtac.clenv_refine false clenv + Clenvtac.clenv_refine clenv end let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 4beeaaae0..773fc1520 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -207,7 +207,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' = try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls) with e -> Proofview.tclZERO e in resolve >>= fun clenv' -> - Clenvtac.clenv_refine with_evars ~with_classes:false clenv' + Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv' end let unify_e_resolve poly flags = begin fun gls (c,_,clenv) -> diff --git a/tactics/elim.mli b/tactics/elim.mli index d6b67e5ba..ddfac3f2c 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -11,12 +11,11 @@ open Names open EConstr open Tacticals -open Misctypes open Tactypes (** Eliminations tactics. *) -val introCaseAssumsThen : evars_flag -> +val introCaseAssumsThen : Tactics.evars_flag -> (intro_patterns -> branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index 1033c56c9..671e765e0 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -155,7 +155,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = - Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'} + Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} in let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = @@ -1044,7 +1044,7 @@ let onEquality with_evars tac (c,lbindc) = let t = type_of c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in - let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in + let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in tclTHEN diff --git a/tactics/equality.mli b/tactics/equality.mli index 9395cf4a8..6f3e08ea0 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -15,8 +15,8 @@ open EConstr open Environ open Ind_tables open Locus -open Misctypes open Tactypes +open Tactics (*i*) type dep_proof_flag = bool (* true = support rewriting dependent proofs *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 53a02f89b..f34c83ae7 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -223,7 +223,7 @@ let compute_induction_names_gen check_and branchletsigns = function let compute_induction_names = compute_induction_names_gen true (* Compute the let-in signature of case analysis or standard induction scheme *) -let compute_constructor_signatures isrec ((_,k as ity),u) = +let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = match Constr.kind c, recargs with | Prod (_,_,c), recarg::rest -> @@ -231,7 +231,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) = begin match Declareops.dest_recarg recarg with | Norec | Imbr _ -> true :: rest | Mrec (_,j) -> - if isrec && Int.equal j k then true :: true :: rest + if rec_flag && Int.equal j k then true :: true :: rest else true :: rest end | LetIn (_,_,_,c), rest -> false :: analrec c rest @@ -634,7 +634,7 @@ module New = struct (* Find the right elimination suffix corresponding to the sort of the goal *) (* 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) = + rec_flag allnames tac predicate ind (c, t) = Proofview.Goal.enter begin fun gl -> let sigma, elim = mk_elim ind gl in let ind = on_snd (fun u -> EInstance.kind sigma u) ind in @@ -663,7 +663,7 @@ module New = struct (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in - let branchsigns = compute_constructor_signatures isrec ind in + let branchsigns = compute_constructor_signatures ~rec_flag ind in let brnames = compute_induction_names_gen false branchsigns allnames in let flags = Unification.elim_flags () in let elimclause' = @@ -686,7 +686,7 @@ module New = struct in let branchtacs = List.init (Array.length branchsigns) after_tac in Proofview.tclTHEN - (Clenvtac.clenv_refine false clenv') + (Clenvtac.clenv_refine clenv') (Proofview.tclEXTEND [] tclIDTAC branchtacs) end) end diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index cbaf691f1..1e66c2b0b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -14,7 +14,6 @@ open EConstr open Evd open Proof_type open Locus -open Misctypes open Tactypes (** Tacticals i.e. functions from tactics to tactics. *) @@ -124,7 +123,7 @@ val fix_empty_or_and_pattern : int -> delayed_open_constr or_and_intro_pattern_expr -> delayed_open_constr or_and_intro_pattern_expr -val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array +val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool list array (** Useful for [as intro_pattern] modifier *) val compute_induction_names : diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cf07532c0..67170d2cf 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -43,7 +43,6 @@ open Pretype_errors open Unification open Locus open Locusops -open Misctypes open Tactypes open Proofview.Notations open Context.Named.Declaration @@ -1154,6 +1153,11 @@ let tactic_infer_flags with_evar = { Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + type 'a core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident @@ -1282,7 +1286,7 @@ let do_replace id = function let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) targetid id sigma0 clenv tac = - let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in + let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in let clenv = if with_classes then { clenv with evd = Typeclasses.resolve_typeclasses @@ -2259,7 +2263,7 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in - let branchsigns = compute_constructor_signatures false ind in + let branchsigns = compute_constructor_signatures ~rec_flag:false ind in let nv_with_let = Array.map List.length branchsigns in let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in let ll = get_and_check_or_and_pattern ?loc ll branchsigns in @@ -4197,7 +4201,7 @@ let induction_tac with_evars params indvars elim = let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - Clenvtac.clenv_refine with_evars resolved + Clenvtac.clenv_refine ~with_evars resolved end (* Apply induction "in place" taking into account dependent diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 086442e42..8d4302450 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -18,7 +18,6 @@ open Clenv open Redexpr open Pattern open Unification -open Misctypes open Tactypes open Locus open Ltac_pretype @@ -91,6 +90,11 @@ val intros_clearing : bool list -> unit Proofview.tactic val try_intros_until : (Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + (** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) -- cgit v1.2.3