aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst6
-rw-r--r--doc/sphinx/proof-engine/ltac2.rst4
-rw-r--r--test-suite/ltac2/rebind.v16
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
-rw-r--r--user-contrib/Ltac2/tac2entries.ml29
-rw-r--r--user-contrib/Ltac2/tac2expr.mli2
-rw-r--r--user-contrib/Ltac2/tac2intern.ml10
-rw-r--r--user-contrib/Ltac2/tac2intern.mli4
-rw-r--r--user-contrib/Ltac2/tac2interp.ml31
9 files changed, 83 insertions, 21 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..0eb7ac6bb2 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -226,12 +226,14 @@ Ltac Definitions
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.
Reduction
~~~~~~~~~
diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v
index e1c20a2059..6cec49de1e 100644
--- a/test-suite/ltac2/rebind.v
+++ b/test-suite/ltac2/rebind.v
@@ -32,3 +32,19 @@ Fail Ltac2 Set f := fun x => x.
Ltac2 mutable g x := x.
Ltac2 Set g := f.
+
+(* Rebinding with old values *)
+
+Ltac2 mutable qux () := Message.print (Message.of_string "Hello").
+
+Ltac2 Set qux as self := fun () => self (); self ().
+
+Ltac2 Eval qux ().
+
+Ltac2 Type rec nat := [O | S (nat)].
+
+Ltac2 mutable quz := O.
+
+Ltac2 Set quz as self := S self.
+
+Ltac2 Eval quz.
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..ecea0a9903 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -458,6 +458,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 +1142,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. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:05:38 +0000