aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst6
-rw-r--r--test-suite/ltac2/compat.v61
-rw-r--r--user-contrib/Ltac2/Ltac1.v6
-rw-r--r--user-contrib/Ltac2/tac2core.ml57
-rw-r--r--user-contrib/Ltac2/tac2env.ml3
-rw-r--r--user-contrib/Ltac2/tac2env.mli4
-rw-r--r--user-contrib/Ltac2/tac2interp.ml2
-rw-r--r--user-contrib/Ltac2/tac2interp.mli3
8 files changed, 127 insertions, 15 deletions
diff --git a/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst b/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst
new file mode 100644
index 0000000000..26b72de2aa
--- /dev/null
+++ b/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst
@@ -0,0 +1,6 @@
+- **Added:**
+ A function Ltac1.lambda allowing to embed Ltac2 functions
+ into Ltac1 runtime values
+ (`#13442 <https://github.com/coq/coq/pull/13442>`_,
+ fixes `#12871 <https://github.com/coq/coq/issues/12871>`_,
+ by Pierre-Marie Pédrot).
diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index 9c11d19c27..b50371386f 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -40,6 +40,67 @@ Fail Ltac1.run (ltac1val:(x |- idtac) 0).
Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))).
Abort.
+(** Check value-returning FFI *)
+
+(* A dummy CPS wrapper in Ltac1 *)
+Ltac arg k :=
+match goal with
+| [ |- ?P ] => k P
+end.
+
+Ltac2 testeval v :=
+ let r := { contents := None } in
+ let k c :=
+ let () := match Ltac1.to_constr c with
+ | None => ()
+ | Some c => r.(contents) := Some c
+ end in
+ (* dummy return value *)
+ ltac1val:(idtac)
+ in
+ let tac := ltac1val:(arg) in
+ let () := Ltac1.apply tac [Ltac1.lambda k] (fun _ => ()) in
+ match r.(contents) with
+ | None => fail
+ | Some c => if Constr.equal v c then () else fail
+ end.
+
+Goal True.
+Proof.
+testeval 'True.
+Abort.
+
+Goal nat.
+Proof.
+testeval 'nat.
+Abort.
+
+(* CPS towers *)
+Ltac2 testeval2 tac :=
+ let fail _ := Control.zero Not_found in
+ let cast c := match Ltac1.to_constr c with
+ | None => fail ()
+ | Some c => c
+ end in
+ let f x y z :=
+ let x := cast x in
+ let y := cast y in
+ let z := cast z in
+ Ltac1.of_constr constr:($x $y $z)
+ in
+ let f := Ltac1.lambda (fun x => Ltac1.lambda (fun y => Ltac1.lambda (fun z => f x y z))) in
+ Ltac1.apply tac [f] Ltac1.run.
+
+Goal False -> True.
+Proof.
+ltac1:(
+let ff := ltac2:(tac |- testeval2 tac) in
+ff ltac:(fun k =>
+ let c := k (fun (n : nat) (i : True) (e : False) => i) O I in
+ exact c)
+).
+Qed.
+
(** Test calls to Ltac2 from Ltac1 *)
Set Default Proof Mode "Classic".
diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v
index 1a69708a7d..fd1555c2fb 100644
--- a/user-contrib/Ltac2/Ltac1.v
+++ b/user-contrib/Ltac2/Ltac1.v
@@ -25,6 +25,12 @@ Ltac2 @ external run : t -> unit := "ltac2" "ltac1_run".
(** Runs an Ltac1 value, assuming it is a 'tactic', i.e. not returning
anything. *)
+Ltac2 @ external lambda : (t -> t) -> t := "ltac2" "ltac1_lambda".
+(** Embed an Ltac2 function into Ltac1 values. Contrarily to the ltac1:(...)
+ quotation, this function allows both to capture an Ltac2 context inside the
+ closure and to return an Ltac1 value. Returning values in Ltac1 is a
+ intrepid endeavour prone to weird runtime semantics. *)
+
Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "ltac2" "ltac1_apply".
(** Applies an Ltac1 value to a list of arguments, and provides the result in
CPS style. It does **not** run the returned value. *)
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 01b1025da1..8663691c0a 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1365,10 +1365,44 @@ let () =
let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (Some "ltac2", in_gen (rawwit wit_ltac2) v) in
Ltac_plugin.Tacentries.create_ltac_quotation "ltac2" inject (e, None)
-(* Ltac1 runtime representation of Ltac2 closure quotations *)
-let typ_ltac2 : (Id.t list * glb_tacexpr) Geninterp.Val.typ =
+(* Ltac1 runtime representation of Ltac2 closures. *)
+let typ_ltac2 : valexpr Geninterp.Val.typ =
Geninterp.Val.create "ltac2:ltac2_eval"
+let cast_typ (type a) (tag : a Geninterp.Val.typ) (v : Geninterp.Val.t) : a =
+ let Geninterp.Val.Dyn (tag', v) = v in
+ match Geninterp.Val.eq tag tag' with
+ | None -> assert false
+ | Some Refl -> v
+
+let () =
+ let open Ltac_plugin in
+ (* This is a hack similar to Tacentries.ml_val_tactic_extend *)
+ let intern_fun _ e = Empty.abort e in
+ let subst_fun s v = v in
+ let () = Genintern.register_intern0 wit_ltac2_val intern_fun in
+ let () = Genintern.register_subst0 wit_ltac2_val subst_fun in
+ (* These are bound names and not relevant *)
+ let tac_id = Id.of_string "F" in
+ let arg_id = Id.of_string "X" in
+ let interp_fun ist () =
+ let tac = cast_typ typ_ltac2 @@ Id.Map.get tac_id ist.Tacinterp.lfun in
+ let arg = Id.Map.get arg_id ist.Tacinterp.lfun in
+ let tac = Tac2ffi.to_closure tac in
+ Tac2ffi.apply tac [of_ltac1 arg] >>= fun ans ->
+ let ans = Tac2ffi.to_ext val_ltac1 ans in
+ Ftactic.return ans
+ in
+ let () = Geninterp.register_interp0 wit_ltac2_val interp_fun in
+ define1 "ltac1_lambda" valexpr begin fun f ->
+ let body = Tacexpr.TacGeneric (Some "ltac2", in_gen (glbwit wit_ltac2_val) ()) in
+ let clos = Tacexpr.TacFun ([Name arg_id], Tacexpr.TacArg (CAst.make body)) in
+ let f = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) f in
+ let lfun = Id.Map.singleton tac_id f in
+ let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun } in
+ Proofview.tclUNIT (of_ltac1 (Tacinterp.Value.of_closure ist clos))
+ end
+
let ltac2_eval =
let open Ltac_plugin in
let ml_name = {
@@ -1380,17 +1414,10 @@ let ltac2_eval =
| tac :: args ->
(* By convention the first argument is the tactic being applied, the rest
being the arguments it should be fed with *)
- let Geninterp.Val.Dyn (tag, tac) = tac in
- let (ids, tac) : Id.t list * glb_tacexpr = match Geninterp.Val.eq tag typ_ltac2 with
- | None -> assert false
- | Some Refl -> tac
- in
- let fold accu id = match Id.Map.find id ist.Geninterp.lfun with
- | v -> Id.Map.add id (Tac2ffi.of_ext val_ltac1 v) accu
- | exception Not_found -> assert false
- in
- let env_ist = List.fold_left fold Id.Map.empty ids in
- Proofview.tclIGNORE (Tac2interp.interp { env_ist } tac)
+ let tac = cast_typ typ_ltac2 tac in
+ let tac = Tac2ffi.to_closure tac in
+ let args = List.map (fun arg -> Tac2ffi.of_ext val_ltac1 arg) args in
+ Proofview.tclIGNORE (Tac2ffi.apply tac args)
in
let () = Tacenv.register_ml_tactic ml_name [|eval_fun|] in
{ Tacexpr.mltac_name = ml_name; mltac_index = 0 }
@@ -1398,7 +1425,7 @@ let ltac2_eval =
let () =
let open Ltac_plugin in
let open Tacinterp in
- let interp ist (ids, tac as self) = match ids with
+ let interp ist (ids, tac) = match ids with
| [] ->
(* Evaluate the Ltac2 quotation eagerly *)
let idtac = Value.of_closure { ist with lfun = Id.Map.empty } (Tacexpr.TacId []) in
@@ -1413,6 +1440,8 @@ let () =
let mk_arg id = Tacexpr.Reference (Locus.ArgVar (CAst.make id)) in
let args = List.map mk_arg ids in
let clos = Tacexpr.TacFun (nas, Tacexpr.TacML (CAst.make (ltac2_eval, mk_arg self_id :: args))) in
+ let self = GTacFun (List.map (fun id -> Name id) ids, tac) in
+ let self = Tac2interp.interp_value { env_ist = Id.Map.empty } self in
let self = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) self in
let ist = { ist with lfun = Id.Map.singleton self_id self } in
Ftactic.return (Value.of_closure ist clos)
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index f6d07e484b..5479ba0d54 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -288,7 +288,8 @@ let ltac1_prefix =
(** Generic arguments *)
-let wit_ltac2 = Genarg.make0 "ltac2:value"
+let wit_ltac2 = Genarg.make0 "ltac2:tactic"
+let wit_ltac2_val = Genarg.make0 "ltac2:value"
let wit_ltac2_constr = Genarg.make0 "ltac2:in-constr"
let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation"
let () = Geninterp.register_val0 wit_ltac2 None
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index af1197c24c..95dcdd7e1b 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -144,6 +144,10 @@ val ltac1_prefix : ModPath.t
val wit_ltac2 : (Id.t CAst.t list * raw_tacexpr, Id.t list * glb_tacexpr, Util.Empty.t) genarg_type
(** Ltac2 quotations in Ltac1 code *)
+val wit_ltac2_val : (Util.Empty.t, unit, Util.Empty.t) genarg_type
+(** Embedding Ltac2 closures of type [Ltac1.t -> Ltac1.t] inside Ltac1. There is
+ no relevant data because arguments are passed by conventional names. *)
+
val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genarg_type
(** Ltac2 quotations in Gallina terms *)
diff --git a/user-contrib/Ltac2/tac2interp.ml b/user-contrib/Ltac2/tac2interp.ml
index ed783afce7..8027a22e01 100644
--- a/user-contrib/Ltac2/tac2interp.ml
+++ b/user-contrib/Ltac2/tac2interp.ml
@@ -223,6 +223,8 @@ and eval_pure_args bnd args =
let map e = eval_pure bnd None e in
Array.map_of_list map args
+let interp_value ist tac =
+ eval_pure ist.env_ist None tac
(** Cross-boundary hacks. *)
diff --git a/user-contrib/Ltac2/tac2interp.mli b/user-contrib/Ltac2/tac2interp.mli
index e466c65224..ae7b2ea86d 100644
--- a/user-contrib/Ltac2/tac2interp.mli
+++ b/user-contrib/Ltac2/tac2interp.mli
@@ -18,6 +18,9 @@ val empty_environment : environment
val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
+val interp_value : environment -> glb_tacexpr -> valexpr
+(** Same as [interp] but assumes that the argument is a syntactic value. *)
+
(* val interp_app : closure -> ml_tactic *)
(** {5 Cross-boundary encodings} *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:55:10 +0000