Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.

Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: kyoDralliam

1 files changed, 71 insertions, 2 deletions

diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v
index e1c20a2059..7b3a460c8c 100644
--- a/test-suite/ltac2/rebind.v
+++ b/test-suite/ltac2/rebind.v
@@ -15,6 +15,39 @@ Fail foo ().
 constructor.
 Qed.
 
+
+(** Bindings are dynamic *)
+
+Ltac2 Type rec nat := [O | S (nat)].
+
+Ltac2 rec nat_eq n m :=
+  match n with
+  | O => match m with | O => true | S _ => false end
+  | S n => match m with | O => false | S m => nat_eq n m end
+  end.
+
+Ltac2 Type exn ::= [ Assertion_failed ].
+
+Ltac2 assert_eq n m :=
+  match nat_eq n m with
+  | true => ()
+  | false => Control.throw Assertion_failed end.
+
+Ltac2 mutable x := O.
+Ltac2 y := x.
+Ltac2 Eval (assert_eq y O).
+Ltac2 Set x := (S O).
+Ltac2 Eval (assert_eq y (S O)).
+
+Ltac2 mutable quw := fun (n : nat) => O.
+Ltac2 Set quw := fun n =>
+  match n with
+  | O => O
+  | S n => S (S (quw n))
+  end.
+
+Ltac2 Eval (quw (S (S O))).
+
 (** Not the right type *)
 Fail Ltac2 Set foo := 0.
 
@@ -25,10 +58,46 @@ Fail Ltac2 Set bar := fun _ => ().
 
 (** Subtype check *)
 
-Ltac2 mutable rec f x := f x.
+Ltac2 rec h x := h x.
 
+Ltac2 mutable f x := h x.
 Fail Ltac2 Set f := fun x => x.
 
 Ltac2 mutable g x := x.
+Ltac2 Set g := h.
+
+(** Rebinding with old values *)
+
+
+
+Ltac2 mutable qux n := S n.
+
+Ltac2 Set qux as self := fun n => self (self n).
+
+Ltac2 Eval assert_eq (qux O) (S (S O)).
+
+Ltac2 mutable quz := O.
+
+Ltac2 Set quz as self := S self.
+
+Ltac2 Eval (assert_eq quz (S O)).
+
+Ltac2 rec addn n :=
+  match n with
+  | O => fun m => m
+  | S n => fun m => S (addn n m)
+
+  end.
+Ltac2 mutable rec quy n :=
+  match n with
+  | O => S O
+  | S n => S (quy n)
+  end.
 
-Ltac2 Set g := f.
+Ltac2 Set quy as self := fun n =>
+                           match n with
+                           | O => O
+                           | S n => addn (self n) (quy n)
+                           end.
+Ltac2 Eval (assert_eq (quy (S (S O))) (S (S (S O)))).
+Ltac2 Eval (assert_eq (quy (S (S (S O)))) (S (S (S (S (S (S O))))))).