From 0e6facc70506d81e765c5a0be241a77bc7b22b85 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 2 Aug 2014 09:30:30 +0200 Subject: Adding a syntax "enough" for the variant of "assert" with the order of subgoals and the role of the "by tac" clause swapped. --- tactics/tacintern.ml | 4 ++-- tactics/tacinterp.ml | 4 ++-- tactics/tacsubst.ml | 4 ++-- tactics/tactics.ml | 16 ++++++++++++---- tactics/tactics.mli | 4 +++- 5 files changed, 21 insertions(+), 11 deletions(-) (limited to 'tactics') diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index c2f85d534..e2f87062e 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -473,8 +473,8 @@ let rec intern_atomic lf ist x = | TacMutualCofix (id,l) -> let f (id,c) = (intern_ident lf ist id,intern_type ist c) in TacMutualCofix (intern_ident lf ist id, List.map f l) - | TacAssert (otac,ipat,c) -> - TacAssert (Option.map (intern_pure_tactic ist) otac, + | TacAssert (b,otac,ipat,c) -> + TacAssert (b,Option.map (intern_pure_tactic ist) otac, Option.map (intern_intro_pattern lf ist) ipat, intern_constr_gen false (not (Option.is_empty otac)) ist c) | TacGeneralize cl -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e0d24e9e1..b52a3e7e9 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1610,7 +1610,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tactics.mutual_cofix (interp_fresh_ident ist env id) l_interp 0) gl end - | TacAssert (t,ipat,c) -> + | TacAssert (b,t,ipat,c) -> Proofview.Goal.raw_enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -1620,7 +1620,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let patt = interp_intro_pattern ist env in Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma) - (Tactics.forward (Option.map (interp_tactic ist) t) + (Tactics.forward b (Option.map (interp_tactic ist) t) (Option.map patt ipat) c) end | TacGeneralize cl -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 30fffed91..428061463 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -146,8 +146,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacCofix idopt as x -> x | TacMutualCofix (id,l) -> TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l) - | TacAssert (b,na,c) -> - TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c) + | TacAssert (b,otac,na,c) -> + TacAssert (b,Option.map (subst_tactic subst) otac,na,subst_glob_constr subst c) | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 442f0a3cb..cb6894fef 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +let a = 1 + open Pp open Errors open Util @@ -1738,6 +1740,7 @@ let assert_as first ipat c = end let assert_tac na = assert_as true (ipat_of_name na) +let enough_tac na = assert_as false (ipat_of_name na) (* apply in as *) @@ -1856,7 +1859,7 @@ let letin_pat_tac with_eq name c occs = letin_tac_gen with_eq (AbstractPattern (name,c,occs,false,tactic_infer_flags)) None (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *) -let forward usetac ipat c = +let forward b usetac ipat c = match usetac with | None -> Proofview.Goal.raw_enter begin fun gl -> @@ -1864,10 +1867,15 @@ let forward usetac ipat c = Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c)) end | Some tac -> - Tacticals.New.tclTHENFIRST (assert_as true ipat c) tac + if b then + Tacticals.New.tclTHENFIRST (assert_as b ipat c) tac + else + Tacticals.New.tclTHENS3PARTS + (assert_as b ipat c) [||] tac [|Tacticals.New.tclIDTAC|] -let pose_proof na c = forward None (ipat_of_name na) c -let assert_by na t tac = forward (Some tac) (ipat_of_name na) t +let pose_proof na c = forward true None (ipat_of_name na) c +let assert_by na t tac = forward true (Some tac) (ipat_of_name na) t +let enough_by na t tac = forward false (Some tac) (ipat_of_name na) t (***************************) (* Generalization tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 20b974a82..c2403d97a 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -334,13 +334,15 @@ val assert_replacing : Id.t -> types -> tactic -> tactic val cut_replacing : Id.t -> types -> tactic -> tactic val assert_as : bool -> intro_pattern_expr located option -> constr -> unit Proofview.tactic -val forward : unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic +val forward : bool -> unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic val letin_tac : (bool * intro_pattern_expr located) option -> Name.t -> constr -> types option -> clause -> unit Proofview.tactic val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t -> evar_map * constr -> clause -> unit Proofview.tactic val assert_tac : Name.t -> types -> unit Proofview.tactic +val enough_tac : Name.t -> types -> unit Proofview.tactic val assert_by : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic +val enough_by : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic val pose_proof : Name.t -> constr -> unit Proofview.tactic val generalize : constr list -> tactic -- cgit v1.2.3