aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/g_ltac2.ml440
-rw-r--r--src/tac2core.ml1
-rw-r--r--src/tac2entries.ml1
-rw-r--r--src/tac2entries.mli1
-rw-r--r--src/tac2qexpr.mli6
-rw-r--r--src/tac2quote.ml11
-rw-r--r--src/tac2quote.mli2
-rw-r--r--src/tac2stdlib.ml20
-rw-r--r--src/tac2tactics.ml16
-rw-r--r--src/tac2tactics.mli6
-rw-r--r--tests/example2.v25
-rw-r--r--theories/Notations.v7
-rw-r--r--theories/Std.v7
13 files changed, 129 insertions, 14 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index e6921e2f6c..c92a242637 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -53,15 +53,21 @@ let test_lpar_idnum_coloneq =
lk_kw "(" >> (lk_ident_or_anti <+> lk_int) >> lk_kw ":="
end
+(* lookahead for (x:t), (?x:t) *)
+let test_lpar_id_colon =
+ entry_of_lookahead "test_lpar_id_colon" begin
+ lk_kw "(" >> lk_ident_or_anti >> lk_kw ":"
+ end
+
(* Hack to recognize "(x := t)" and "($x := t)" *)
-let test_lpar_coloneq =
- entry_of_lookahead "test_coloneq" begin
+let test_lpar_id_coloneq =
+ entry_of_lookahead "test_lpar_id_coloneq" begin
lk_kw "(" >> lk_ident_or_anti >> lk_kw ":="
end
(* Hack to recognize "(x)" *)
let test_lpar_id_rpar =
- entry_of_lookahead "test_lpar_id_coloneq" begin
+ entry_of_lookahead "test_lpar_id_rpar" begin
lk_kw "(" >> lk_ident >> lk_kw ")"
end
@@ -370,7 +376,7 @@ GEXTEND Gram
GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
q_destruction_arg q_reference q_with_bindings q_constr_matching
- q_hintdb q_move_location q_pose;
+ q_hintdb q_move_location q_pose q_assert;
anti:
[ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
;
@@ -709,7 +715,7 @@ GEXTEND Gram
] ]
;
pose:
- [ [ test_lpar_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
+ [ [ test_lpar_id_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
Loc.tag ~loc:!@loc (Some id, c)
| c = Constr.constr; na = as_name -> Loc.tag ~loc:!@loc (na, c)
] ]
@@ -717,6 +723,30 @@ GEXTEND Gram
q_pose:
[ [ p = pose -> p ] ]
;
+ as_ipat:
+ [ [ "as"; ipat = simple_intropattern -> Some ipat
+ | -> None
+ ] ]
+ ;
+ by_tactic:
+ [ [ "by"; tac = tac2expr -> Some tac
+ | -> None
+ ] ]
+ ;
+ assertion:
+ [ [ test_lpar_id_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
+ Loc.tag ~loc:!@loc (QAssertValue (id, c))
+ | test_lpar_id_colon; "("; id = ident_or_anti; ":"; c = Constr.lconstr; ")"; tac = by_tactic ->
+ let loc = !@loc in
+ let ipat = Loc.tag ~loc @@ QIntroNaming (Loc.tag ~loc @@ QIntroIdentifier id) in
+ Loc.tag ~loc (QAssertType (Some ipat, c, tac))
+ | c = Constr.constr; ipat = as_ipat; tac = by_tactic ->
+ Loc.tag ~loc:!@loc (QAssertType (ipat, c, tac))
+ ] ]
+ ;
+ q_assert:
+ [ [ a = assertion -> a ] ]
+ ;
END
(** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 9e65111c0d..1917fa5f66 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1114,6 +1114,7 @@ let () = add_expr_scope "strategy" q_strategy_flag Tac2quote.of_strategy_flag
let () = add_expr_scope "reference" q_reference Tac2quote.of_reference
let () = add_expr_scope "move_location" q_move_location Tac2quote.of_move_location
let () = add_expr_scope "pose" q_pose Tac2quote.of_pose
+let () = add_expr_scope "assert" q_assert Tac2quote.of_assertion
let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching
let () = add_generic_scope "constr" Pcoq.Constr.constr Tac2quote.wit_constr
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 78fe7b5bd9..24db19d02a 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -41,6 +41,7 @@ let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching"
let q_hintdb = Pcoq.Gram.entry_create "tactic:q_hintdb"
let q_move_location = Pcoq.Gram.entry_create "tactic:q_move_location"
let q_pose = Pcoq.Gram.entry_create "tactic:q_pose"
+let q_assert = Pcoq.Gram.entry_create "tactic:q_assert"
end
(** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 55e658884b..7bd512651c 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -80,6 +80,7 @@ val q_constr_matching : constr_matching Pcoq.Gram.entry
val q_hintdb : hintdb Pcoq.Gram.entry
val q_move_location : move_location Pcoq.Gram.entry
val q_pose : pose Pcoq.Gram.entry
+val q_assert : assertion Pcoq.Gram.entry
end
(** {5 Hooks} *)
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 580039afe5..cb43a980de 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -141,3 +141,9 @@ type move_location_r =
type move_location = move_location_r located
type pose = (Id.t located or_anti option * Constrexpr.constr_expr) located
+
+type assertion_r =
+| QAssertType of intro_pattern option * Constrexpr.constr_expr * raw_tacexpr option
+| QAssertValue of Id.t located or_anti * Constrexpr.constr_expr
+
+type assertion = assertion_r located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 466c1f5094..e89f37f2ba 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -373,3 +373,14 @@ let of_move_location (loc, mv) = match mv with
let of_pose p =
of_pair (fun id -> of_option (fun id -> of_anti of_ident id) id) of_open_constr p
+
+let of_assertion (loc, ast) = match ast with
+| QAssertType (ipat, c, tac) ->
+ let ipat = of_option of_intro_pattern ipat in
+ let c = of_constr c in
+ let tac = of_option thunk tac in
+ std_constructor ?loc "AssertType" [ipat; c; tac]
+| QAssertValue (id, c) ->
+ let id = of_anti of_ident id in
+ let c = of_constr c in
+ std_constructor ?loc "AssertValue" [id; c]
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index ccb832535a..b9cae23e63 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -77,6 +77,8 @@ val of_strategy_flag : strategy_flag -> raw_tacexpr
val of_pose : pose -> raw_tacexpr
+val of_assertion : assertion -> raw_tacexpr
+
val of_constr_matching : constr_matching -> raw_tacexpr
(** {5 Generic arguments} *)
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 07b01b1174..5f61081a76 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -144,6 +144,17 @@ let to_induction_clause = function
| _ ->
assert false
+let to_assertion = function
+| ValBlk (0, [| ipat; t; tac |]) ->
+ let to_tac t = Proofview.tclIGNORE (thaw t) in
+ let ipat = Value.to_option to_intro_pattern ipat in
+ let t = Value.to_constr t in
+ let tac = Value.to_option to_tac tac in
+ AssertType (ipat, t, tac)
+| ValBlk (1, [| id; c |]) ->
+ AssertValue (Value.to_ident id, Value.to_constr c)
+| _ -> assert false
+
let to_multi = function
| ValBlk (0, [| n |]) -> Precisely (Value.to_int n)
| ValBlk (1, [| n |]) -> UpTo (Value.to_int n)
@@ -256,12 +267,9 @@ let () = define_prim1 "tac_generalize" begin fun cl ->
Tactics.new_generalize_gen cl
end
-let () = define_prim3 "tac_assert" begin fun c tac ipat ->
- let c = Value.to_constr c in
- let of_tac t = Proofview.tclIGNORE (thaw t) in
- let tac = Value.to_option (fun t -> Value.to_option of_tac t) tac in
- let ipat = Value.to_option to_intro_pattern ipat in
- Tac2tactics.forward true tac ipat c
+let () = define_prim1 "tac_assert" begin fun ast ->
+ let ast = to_assertion ast in
+ Tac2tactics.assert_ ast
end
let () = define_prim3 "tac_enough" begin fun c tac ipat ->
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 083ec9e9d4..a6dd4e3a9f 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -170,6 +170,10 @@ type rewriting =
multi *
constr_with_bindings tactic
+type assertion =
+| AssertType of intro_pattern option * EConstr.t * unit tactic option
+| AssertValue of Id.t * EConstr.t
+
let rewrite ev rw cl by =
let map_rw (orient, repeat, c) =
let c = c >>= fun c -> return (mk_with_bindings c) in
@@ -179,9 +183,17 @@ let rewrite ev rw cl by =
let by = Option.map (fun tac -> Tacticals.New.tclCOMPLETE tac, Equality.Naive) by in
Equality.general_multi_rewrite ev rw cl by
-let forward ev tac ipat c =
+let forward fst tac ipat c =
+ let ipat = Option.map mk_intro_pattern ipat in
+ Tactics.forward fst tac ipat c
+
+let assert_ = function
+| AssertValue (id, c) ->
+ let ipat = Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id) in
+ Tactics.forward true None (Some ipat) c
+| AssertType (ipat, c, tac) ->
let ipat = Option.map mk_intro_pattern ipat in
- Tactics.forward ev tac ipat c
+ Tactics.forward true (Some tac) ipat c
let letin_pat_tac ev ipat na c cl =
let ipat = Option.map (fun (b, ipat) -> (b, Loc.tag @@ mk_intro_pattern_naming ipat)) ipat in
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 5fdd1c39bc..8e15fb1392 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -63,6 +63,10 @@ type rewriting =
multi *
constr_with_bindings tactic
+type assertion =
+| AssertType of intro_pattern option * constr * unit tactic option
+| AssertValue of Id.t * constr
+
(** Local reimplementations of tactics variants from Coq *)
val intros_patterns : evars_flag -> intro_pattern list -> unit tactic
@@ -91,6 +95,8 @@ val rewrite :
val forward : bool -> unit tactic option option ->
intro_pattern option -> constr -> unit tactic
+val assert_ : assertion -> unit tactic
+
val letin_pat_tac : evars_flag -> (bool * intro_pattern_naming) option ->
Name.t -> (Evd.evar_map * constr) -> clause -> unit tactic
diff --git a/tests/example2.v b/tests/example2.v
index 378abb86a8..20819606db 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -224,6 +224,12 @@ Qed.
Goal True.
Proof.
+pose True as X.
+constructor.
+Qed.
+
+Goal True.
+Proof.
let x := @foo in
set ($x := True) in * |-.
constructor.
@@ -235,3 +241,22 @@ remember 0 as n eqn: foo at 1.
rewrite foo.
reflexivity.
Qed.
+
+Goal True.
+Proof.
+assert (H := 0 + 0).
+constructor.
+Qed.
+
+Goal True.
+Proof.
+assert (exists n, n = 0) as [n Hn].
++ exists 0; reflexivity.
++ exact I.
+Qed.
+
+Goal True -> True.
+Proof.
+assert (H : 0 + 0 = 0) by reflexivity.
+intros x; exact x.
+Qed.
diff --git a/theories/Notations.v b/theories/Notations.v
index d4520dbdfd..91025ea964 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -279,6 +279,13 @@ Ltac2 Notation "set" p(thunk(pose)) cl(opt(clause)) :=
Ltac2 Notation "eset" p(thunk(pose)) cl(opt(clause)) :=
Std.set true p (default_on_concl cl).
+Ltac2 assert0 ev ast :=
+ enter_h ev (fun _ ast => Std.assert ast) ast.
+
+Ltac2 Notation "assert" ast(thunk(assert)) := assert0 false ast.
+
+Ltac2 Notation "eassert" ast(thunk(assert)) := assert0 true ast.
+
Ltac2 default_everywhere cl :=
match cl with
| None => { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }
diff --git a/theories/Std.v b/theories/Std.v
index 2eab172432..7831baf046 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -88,6 +88,11 @@ Ltac2 Type induction_clause := {
indcl_in : clause option;
}.
+Ltac2 Type assertion := [
+| AssertType (intro_pattern option, constr, (unit -> unit) option)
+| AssertValue (ident, constr)
+].
+
Ltac2 Type repeat := [
| Precisely (int)
| UpTo (int)
@@ -131,7 +136,7 @@ Ltac2 @ external case : evar_flag -> constr_with_bindings -> unit := "ltac2" "ta
Ltac2 @ external generalize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_generalize".
-Ltac2 @ external assert : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_assert".
+Ltac2 @ external assert : assertion -> unit := "ltac2" "tac_assert".
Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_enough".
Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose".
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 04:07:27 +0000