Ltac2: add notations for eval cbv in ... and other in place reductions

5 files changed, 108 insertions, 0 deletions

diff --git a/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst b/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst
new file mode 100644
index 0000000000..2f8d92fae5
--- /dev/null
+++ b/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Ltac2 notations for reductions in terms: :n:`eval @red_expr in @ltac2_term`
+  (`#11981 <https://github.com/coq/coq/pull/11981>`_,
+  by Michael Soegtrop).
diff --git a/test-suite/ltac2/notations.v b/test-suite/ltac2/notations.v
index 3d2a875e38..32c8a7cbe7 100644
--- a/test-suite/ltac2/notations.v
+++ b/test-suite/ltac2/notations.v
@@ -1,6 +1,8 @@
 From Ltac2 Require Import Ltac2.
 From Coq Require Import ZArith String List.
 
+(** * Test cases for the notation system itself *)
+
 Open Scope Z_scope.
 
 Check 1 + 1 : Z.
@@ -22,3 +24,9 @@ Lemma maybe : list bool.
 Proof.
   refine (sl ["left" =? "right"]).
 Qed.
+
+(** * Test cases for specific notations with special contexts *)
+
+(** ** Test eval ... in / reduction tactics *)
+
+(** Moved to test-suite/output/ltac2_notations_eval_in.v so that the output can be checked s*)
diff --git a/test-suite/output/ltac2_notations_eval_in.out b/test-suite/output/ltac2_notations_eval_in.out
new file mode 100644
index 0000000000..15e43b7fb9
--- /dev/null
+++ b/test-suite/output/ltac2_notations_eval_in.out
@@ -0,0 +1,21 @@
+- : constr =
+constr:((fix add (n m : nat) {struct n} : nat :=
+           match n with
+           | 0 => m
+           | S p => S (add p m)
+           end) (1 + 2) 3)
+- : constr = constr:(S (0 + 2 + 3))
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(1 + 2 + 3)
+- : constr list = [constr:(0 <> 0); constr:(0 = 0 -> False);
+constr:((fun P : Prop => P -> False) (0 = 0)); constr:(
+0 <> 0)]
diff --git a/test-suite/output/ltac2_notations_eval_in.v b/test-suite/output/ltac2_notations_eval_in.v
new file mode 100644
index 0000000000..4a11e7cae0
--- /dev/null
+++ b/test-suite/output/ltac2_notations_eval_in.v
@@ -0,0 +1,42 @@
+From Ltac2 Require Import Ltac2.
+From Coq Require Import ZArith.
+
+(** * Test eval ... in / reduction tactics *)
+
+(** The below test cases test if the notation syntax works - not the tactics as such *)
+
+Ltac2 Eval (eval red in (1+2+3)).
+
+Ltac2 Eval (eval hnf in (1+2+3)).
+
+Ltac2 Eval (eval simpl in (1+2+3)).
+
+Ltac2 Eval (eval simpl Z.add in (1+2+3)).
+
+Ltac2 Eval (eval cbv in (1+2+3)).
+
+Ltac2 Eval (eval cbv delta [Z.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval cbv delta [Z.add Pos.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval cbn in (1+2+3)).
+
+Ltac2 Eval (eval cbn delta [Z.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval cbn delta [Z.add Pos.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval lazy in (1+2+3)).
+
+Ltac2 Eval (eval lazy delta [Z.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval lazy delta [Z.add Pos.add] beta iota in (1+2+3)).
+
+(* The example for [fold] in the reference manual *)
+
+Ltac2 Eval (
+  let t1 := '(~0=0) in
+  let t2 := eval unfold not in $t1 in
+  let t3 := eval pattern (0=0) in $t2 in
+  let t4 := eval fold not in $t3 in
+  [t1; t2; t3; t4]
+).
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v
index 390b39bab1..931d753521 100644
--- a/user-contrib/Ltac2/Notations.v
+++ b/user-contrib/Ltac2/Notations.v
@@ -396,6 +396,39 @@ Ltac2 Notation "native_compute" pl(opt(seq(pattern, occurrences))) cl(opt(clause
   Std.native pl (default_on_concl cl).
 Ltac2 Notation native_compute := native_compute.
 
+Ltac2 Notation "eval" "red" "in" c(constr) :=
+  Std.eval_red c.
+
+Ltac2 Notation "eval" "hnf" "in" c(constr) :=
+  Std.eval_hnf c.
+
+Ltac2 Notation "eval" "simpl" s(strategy) pl(opt(seq(pattern, occurrences))) "in" c(constr) :=
+  Std.eval_simpl s pl c.
+
+Ltac2 Notation "eval" "cbv" s(strategy) "in" c(constr) :=
+  Std.eval_cbv s c.
+
+Ltac2 Notation "eval" "cbn" s(strategy) "in" c(constr) :=
+  Std.eval_cbn s c.
+
+Ltac2 Notation "eval" "lazy" s(strategy) "in" c(constr) :=
+  Std.eval_lazy s c.
+
+Ltac2 Notation "eval" "unfold" pl(list1(seq(reference, occurrences), ",")) "in" c(constr) :=
+  Std.eval_unfold pl c.
+
+Ltac2 Notation "eval" "fold" pl(thunk(list1(open_constr))) "in" c(constr) :=
+  Std.eval_fold (pl ()) c.
+
+Ltac2 Notation "eval" "pattern" pl(list1(seq(constr, occurrences), ",")) "in" c(constr) :=
+  Std.eval_pattern pl c.
+
+Ltac2 Notation "eval" "vm_compute" pl(opt(seq(pattern, occurrences))) "in" c(constr) :=
+  Std.eval_vm pl c.
+
+Ltac2 Notation "eval" "native_compute" pl(opt(seq(pattern, occurrences))) "in" c(constr) :=
+  Std.eval_native pl c.
+
 Ltac2 change0 p cl :=
   let (pat, c) := p in
   Std.change pat c (default_on_concl cl).