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

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

9 files changed, 181 insertions, 28 deletions

diff --git a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst
new file mode 100644
index 0000000000..0dd0fed4e2
--- /dev/null
+++ b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to
+  give a name to the old value so as to be able to reuse it inside the
+  new one
+  (`#11503 <https://github.com/coq/coq/pull/11503>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 35062e0057..1e35160205 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -213,25 +213,63 @@ There is dedicated syntax for list and array literals.
 Ltac Definitions
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term
+.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_value
    :name: Ltac2
 
    This command defines a new global Ltac2 value.
 
-   For semantic reasons, the body of the Ltac2 definition must be a syntactical
-   value, that is, a function, a constant or a pure constructor recursively applied to
-   values.
+   The body of an Ltac2 definition is required to be a syntactical value
+   that is, a function, a constant, a pure constructor recursively applied to
+   values or a (non-recursive) let binding of a value in a value.
+
+   .. productionlist:: coq
+      ltac2_value: fun `ltac2_var` => `ltac2_term`
+                       : `ltac2_qualid`
+                       : `ltac2_constructor` `ltac2_value` ... `ltac2_value`
+                       : `ltac2_var`
+                       : let `ltac2_var` := `ltac2_value` in `ltac2_value`
 
    If ``rec`` is set, the tactic is expanded into a recursive binding.
 
    If ``mutable`` is set, the definition can be redefined at a later stage (see below).
 
-.. cmd:: Ltac2 Set @qualid := @ltac2_term
+.. cmd:: Ltac2 Set @qualid {? as @lident} := @ltac2_term
    :name: Ltac2 Set
 
    This command redefines a previous ``mutable`` definition.
    Mutable definitions act like dynamic binding, i.e. at runtime, the last defined
    value for this entry is chosen. This is useful for global flags and the like.
+   The previous value of the binding can be optionally accessed using the `as`
+   binding syntax.
+
+   .. example:: Dynamic nature of mutable cells
+
+      .. coqtop:: all
+
+         Ltac2 mutable x := true.
+         Ltac2 y := x.
+         Ltac2 Eval y.
+         Ltac2 Set x := false.
+         Ltac2 Eval y.
+
+   .. example:: Interaction with recursive calls
+
+
+      .. coqtop:: all
+
+         Ltac2 mutable rec f b := match b with true => 0 | _ => f true end.
+         Ltac2 Set f := fun b =>
+                  match b with true => 1 | _ => f true end.
+         Ltac2 Eval (f false).
+         Ltac2 Set f as oldf := fun b =>
+                  match b with true => 2 | _ => oldf false end.
+         Ltac2 Eval (f false).
+
+      In the definition, the `f` in the body is resolved statically
+      because the definition is marked recursive. In the first re-definition,
+      the `f` in the body is resolved dynamically. This is witnessed by
+      the second re-definition.
+
 
 Reduction
 ~~~~~~~~~
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))))))).
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 13c4d667a0..8979170026 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -289,7 +289,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   tac2def_mut:
-    [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> { StrMut (qid, e) } ] ]
+    [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = tac2expr -> { StrMut (qid, old, e) } ] ]
   ;
   tac2typ_knd:
     [ [ t = tac2type -> { CTydDef (Some t) }
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 28e877491e..987cd8c1b8 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -336,7 +336,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics =
     if isrec then inline_rec_tactic tactics else tactics
   in
   let map ({loc;v=id}, e) =
-    let (e, t) = intern ~strict:true e in
+    let (e, t) = intern ~strict:true [] e in
     let () =
       if not (is_value e) then
         user_err ?loc (str "Tactic definition must be a syntactical value")
@@ -728,19 +728,26 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with
 type redefinition = {
   redef_kn : ltac_constant;
   redef_body : glb_tacexpr;
+  redef_old : Id.t option;
 }
 
 let perform_redefinition (_, redef) =
   let kn = redef.redef_kn in
   let data = Tac2env.interp_global kn in
-  let data = { data with Tac2env.gdata_expr = redef.redef_body } in
+  let body = match redef.redef_old with
+  | None -> redef.redef_body
+  | Some id ->
+    (* Rebind the old value with a let-binding *)
+    GTacLet (false, [Name id, data.Tac2env.gdata_expr], redef.redef_body)
+  in
+  let data = { data with Tac2env.gdata_expr = body } in
   Tac2env.define_global kn data
 
 let subst_redefinition (subst, redef) =
   let kn = Mod_subst.subst_kn subst redef.redef_kn in
   let body = Tac2intern.subst_expr subst redef.redef_body in
   if kn == redef.redef_kn && body == redef.redef_body then redef
-  else { redef_kn = kn; redef_body = body }
+  else { redef_kn = kn; redef_body = body; redef_old = redef.redef_old }
 
 let classify_redefinition o = Substitute o
 
@@ -751,7 +758,7 @@ let inTac2Redefinition : redefinition -> obj =
      subst_function = subst_redefinition;
      classify_function = classify_redefinition }
 
-let register_redefinition ?(local = false) qid e =
+let register_redefinition ?(local = false) qid old e =
   let kn =
     try Tac2env.locate_ltac qid
     with Not_found -> user_err ?loc:qid.CAst.loc (str "Unknown tactic " ++ pr_qualid qid)
@@ -766,7 +773,11 @@ let register_redefinition ?(local = false) qid e =
     if not (data.Tac2env.gdata_mutable) then
       user_err ?loc:qid.CAst.loc (str "The tactic " ++ pr_qualid qid ++ str " is not declared as mutable")
   in
-  let (e, t) = intern ~strict:true e in
+  let ctx = match old with
+  | None -> []
+  | Some { CAst.v = id } -> [id, data.Tac2env.gdata_type]
+  in
+  let (e, t) = intern ~strict:true ctx e in
   let () =
     if not (is_value e) then
       user_err ?loc:qid.CAst.loc (str "Tactic definition must be a syntactical value")
@@ -777,15 +788,17 @@ let register_redefinition ?(local = false) qid e =
       user_err ?loc:qid.CAst.loc (str "Type " ++ pr_glbtype name (snd t) ++
         str " is not a subtype of " ++ pr_glbtype name (snd data.Tac2env.gdata_type))
   in
+  let old = Option.map (fun { CAst.v = id } -> id) old in
   let def = {
     redef_kn = kn;
     redef_body = e;
+    redef_old = old;
   } in
   Lib.add_anonymous_leaf (inTac2Redefinition def)
 
 let perform_eval ~pstate e =
   let env = Global.env () in
-  let (e, ty) = Tac2intern.intern ~strict:false e in
+  let (e, ty) = Tac2intern.intern ~strict:false [] e in
   let v = Tac2interp.interp Tac2interp.empty_environment e in
   let selector, proof =
     match pstate with
@@ -818,7 +831,7 @@ let register_struct ?local str = match str with
 | StrTyp (isrec, t) -> register_type ?local isrec t
 | StrPrm (id, t, ml) -> register_primitive ?local id t ml
 | StrSyn (tok, lev, e) -> register_notation ?local tok lev e
-| StrMut (qid, e) -> register_redefinition ?local qid e
+| StrMut (qid, old, e) -> register_redefinition ?local qid old e
 
 (** Toplevel exception *)
 
@@ -913,7 +926,7 @@ let solve ~pstate default tac =
 
 let call ~pstate ~default e =
   let loc = e.loc in
-  let (e, t) = intern ~strict:false e in
+  let (e, t) = intern ~strict:false [] e in
   let () = check_unit ?loc t in
   let tac = Tac2interp.interp Tac2interp.empty_environment e in
   solve ~pstate default (Proofview.tclIGNORE tac)
diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli
index a95d8cc49f..548655f561 100644
--- a/user-contrib/Ltac2/tac2expr.mli
+++ b/user-contrib/Ltac2/tac2expr.mli
@@ -168,7 +168,7 @@ type strexpr =
   (** External definition *)
 | StrSyn of sexpr list * int option * raw_tacexpr
   (** Syntactic extensions *)
-| StrMut of qualid * raw_tacexpr
+| StrMut of qualid * Names.lident option * raw_tacexpr
   (** Redefinition of mutable globals *)
 
 (** {5 Dynamic semantics} *)
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index a4f385d432..797f72702d 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -396,11 +396,13 @@ let is_pure_constructor kn =
 
 let rec is_value = function
 | GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true
-| GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false
+| GTacAtm (AtmStr _) | GTacApp _ | GTacLet (true, _, _) -> false
 | GTacCst (Tuple _, _, el) -> List.for_all is_value el
 | GTacCst (_, _, []) -> true
 | GTacOpn (_, el) -> List.for_all is_value el
 | GTacCst (Other kn, _, el) -> is_pure_constructor kn && List.for_all is_value el
+| GTacLet (false, bnd, e) ->
+  is_value e && List.for_all (fun (_, e) -> is_value e) bnd
 | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _
 | GTacWth _ -> false
 
@@ -458,6 +460,10 @@ let monomorphic (t : UF.elt glb_typexpr) : mix_type_scheme =
   let subst id = GTypVar (GVar id) in
   (0, subst_type subst t)
 
+let polymorphic ((n, t) : type_scheme) : mix_type_scheme =
+  let subst id = GTypVar (LVar id) in
+  (n, subst_type subst t)
+
 let warn_not_unit =
   CWarnings.create ~name:"not-unit" ~category:"ltac"
     (fun () -> strbrk "The following expression should have type unit.")
@@ -1138,9 +1144,13 @@ let normalize env (count, vars) (t : UF.elt glb_typexpr) =
   in
   subst_type subst t
 
-let intern ~strict e =
+type context = (Id.t * type_scheme) list
+
+let intern ~strict ctx e =
   let env = empty_env () in
   let env = if strict then env else { env with env_str = false } in
+  let fold accu (id, t) = push_name (Name id) (polymorphic t) accu in
+  let env = List.fold_left fold env ctx in
   let (e, t) = intern_rec env e in
   let count = ref 0 in
   let vars = ref UF.Map.empty in
diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli
index 8b09ecbcf7..ed251d6201 100644
--- a/user-contrib/Ltac2/tac2intern.mli
+++ b/user-contrib/Ltac2/tac2intern.mli
@@ -12,7 +12,9 @@ open Names
 open Mod_subst
 open Tac2expr
 
-val intern : strict:bool -> raw_tacexpr -> glb_tacexpr * type_scheme
+type context = (Id.t * type_scheme) list
+
+val intern : strict:bool -> context -> raw_tacexpr -> glb_tacexpr * type_scheme
 val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef
 val intern_open_type : raw_typexpr -> type_scheme
 
diff --git a/user-contrib/Ltac2/tac2interp.ml b/user-contrib/Ltac2/tac2interp.ml
index 54f2da0621..ed783afce7 100644
--- a/user-contrib/Ltac2/tac2interp.ml
+++ b/user-contrib/Ltac2/tac2interp.ml
@@ -86,7 +86,7 @@ let rec interp (ist : environment) = function
 | GTacVar id -> return (get_var ist id)
 | GTacRef kn ->
   let data = get_ref ist kn in
-  return (eval_pure (Some kn) data)
+  return (eval_pure Id.Map.empty (Some kn) data)
 | GTacFun (ids, e) ->
   let cls = { clos_ref = None; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
   let f = interp_app cls in
@@ -187,26 +187,41 @@ and interp_set ist e p r =
   let () = Valexpr.set_field e p r in
   return (Valexpr.make_int 0)
 
-and eval_pure kn = function
+and eval_pure bnd kn = function
+| GTacVar id -> Id.Map.get id bnd
 | GTacAtm (AtmInt n) -> Valexpr.make_int n
 | GTacRef kn ->
   let { Tac2env.gdata_expr = e } =
     try Tac2env.interp_global kn
     with Not_found -> assert false
   in
-  eval_pure (Some kn) e
+  eval_pure bnd (Some kn) e
 | GTacFun (na, e) ->
-  let cls = { clos_ref = kn; clos_env = Id.Map.empty; clos_var = na; clos_exp = e } in
+  let cls = { clos_ref = kn; clos_env = bnd; clos_var = na; clos_exp = e } in
   let f = interp_app cls in
   Tac2ffi.of_closure f
 | GTacCst (_, n, []) -> Valexpr.make_int n
-| GTacCst (_, n, el) -> Valexpr.make_block n (Array.map_of_list eval_unnamed el)
-| GTacOpn (kn, el) -> Tac2ffi.of_open (kn, Array.map_of_list eval_unnamed el)
-| GTacAtm (AtmStr _) | GTacLet _ | GTacVar _ | GTacSet _
+| GTacCst (_, n, el) -> Valexpr.make_block n (eval_pure_args bnd el)
+| GTacOpn (kn, el) -> Tac2ffi.of_open (kn, eval_pure_args bnd el)
+| GTacLet (isrec, vals, body) ->
+  let () = assert (not isrec) in
+  let fold accu (na, e) = match na with
+  | Anonymous ->
+    (* No need to evaluate, we know this is a value *)
+    accu
+  | Name id ->
+    let v = eval_pure bnd None e in
+    Id.Map.add id v accu
+  in
+  let bnd = List.fold_left fold bnd vals in
+  eval_pure bnd kn body
+| GTacAtm (AtmStr _) | GTacSet _
 | GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ ->
   anomaly (Pp.str "Term is not a syntactical value")
 
-and eval_unnamed e = eval_pure None e
+and eval_pure_args bnd args =
+  let map e = eval_pure bnd None e in
+  Array.map_of_list map args
 
 
 (** Cross-boundary hacks. *)