From bde36d4b00185065628324d8ca71994f84eae244 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Apr 2016 22:25:26 +0200 Subject: In the short term, stronger invariant on the syntax of TacAssert, what allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause. --- intf/tacexpr.mli | 2 +- ltac/tacintern.ml | 2 +- ltac/tacinterp.ml | 4 ++-- ltac/tacsubst.ml | 3 ++- ltac/tauto.ml | 2 +- parsing/g_tactic.ml4 | 8 ++------ printing/pptactic.ml | 15 ++++++--------- tactics/tactics.ml | 7 +++++-- tactics/tactics.mli | 2 +- 9 files changed, 21 insertions(+), 24 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index e06436d8a..f6b60b2d5 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -148,7 +148,7 @@ type 'a gen_atomic_tactic_expr = | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list | TacMutualCofix of Id.t * (Id.t * 'trm) list | TacAssert of - bool * 'tacexpr option * + bool * 'tacexpr option option * 'dtrm intro_pattern_expr located option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 15589d5c4..4917c3bb5 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -502,7 +502,7 @@ let rec intern_atomic lf ist x = 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 (b,otac,ipat,c) -> - TacAssert (b,Option.map (intern_pure_tactic ist) otac, + TacAssert (b,Option.map (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/ltac/tacinterp.ml b/ltac/tacinterp.ml index 9b41a276b..b875fb26f 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1765,10 +1765,10 @@ and interp_atomic ist tac : unit Proofview.tactic = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in - let tac = Option.map (interp_tactic ist) t in + let tac = Option.map (Option.map (interp_tactic ist)) t in Tacticals.New.tclWITHHOLES false (name_atomic ~env - (TacAssert(b,Option.map ignore t,ipat,c)) + (TacAssert(b,Option.map (Option.map ignore) t,ipat,c)) (Tactics.forward b tac ipat' c)) sigma end } | TacGeneralize cl -> diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 438219f5a..22660aa83 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -151,7 +151,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacMutualCofix (id,l) -> TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l) | TacAssert (b,otac,na,c) -> - TacAssert (b,Option.map (subst_tactic subst) otac,na,subst_glob_constr subst c) + TacAssert (b,Option.map (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) | TacLetTac (id,c,clp,b,eqpat) -> diff --git a/ltac/tauto.ml b/ltac/tauto.ml index a86fdb98a..fa65a02b4 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -99,7 +99,7 @@ let intro = Tactics.intro let assert_ ?by c = let tac = match by with | None -> None - | Some tac -> Some (tclCOMPLETE tac) + | Some tac -> Some (Some tac) in Proofview.tclINDEPENDENT (Tactics.forward true tac None c) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 0c90a8bca..d36399c0d 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -483,10 +483,6 @@ GEXTEND Gram [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ] ; by_tactic: - [ [ "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac - | -> TacId [] ] ] - ; - opt_by_tactic: [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac | -> None ] ] ; @@ -621,9 +617,9 @@ GEXTEND Gram (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t)) + cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t)) | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t)) + cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t)) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7949bafcb..5dbf9a42a 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -507,8 +507,9 @@ module Make | ipat -> spc() ++ prc c ++ pr_as_ipat prdc ipat - let pr_by_tactic prt tac = - spc() ++ keyword "by" ++ spc () ++ prt tac + let pr_by_tactic prt = function + | Some tac -> keyword "by" ++ spc () ++ prt tac + | None -> mt() let pr_hyp_location pr_id = function | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs @@ -821,7 +822,7 @@ module Make hov 1 ( primitive (if b then "assert" else "enough") ++ pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++ - pr_by_tactic (pr.pr_tactic ltop) tac + pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac ) | TacAssert (_,None,ipat,c) -> hov 1 ( @@ -904,7 +905,7 @@ module Make ) (* Equality and inversion *) - | TacRewrite (ev,l,cl,by) -> + | TacRewrite (ev,l,cl,tac) -> hov 1 ( primitive (with_evars ev "rewrite") ++ spc () ++ prlist_with_sep @@ -914,11 +915,7 @@ module Make pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c) l ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl - ++ ( - match by with - | Some by -> pr_by_tactic (pr.pr_tactic ltop) by - | None -> mt() - ) + ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac ) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 ( diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a626092dd..4c47dc67e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2551,6 +2551,9 @@ let forward b usetac ipat c = (Proofview.V82.tactic (exact_no_check c)) end } | Some tac -> + let tac = match tac with + | None -> Tacticals.New.tclIDTAC + | Some tac -> Tacticals.New.tclCOMPLETE tac in if b then Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac else @@ -2558,8 +2561,8 @@ let forward b usetac ipat c = (assert_as b None ipat c) [||] tac [|Tacticals.New.tclIDTAC|] 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 +let assert_by na t tac = forward true (Some (Some tac)) (ipat_of_name na) t +let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t (***************************) (* Generalization tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 4c4a96ec0..0919fb28e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -365,7 +365,7 @@ val pose_proof : Name.t -> constr -> (** Common entry point for user-level "assert", "enough" and "pose proof" *) -val forward : bool -> unit Proofview.tactic option -> +val forward : bool -> unit Proofview.tactic option option -> intro_pattern option -> constr -> unit Proofview.tactic (** Implements the tactic cut, actually a modus ponens rule *) -- cgit v1.2.3