ltac2val:() quotation in ltac1 to return Ltac1.t values

dev/ci/user-overlays/17575-SkySkimmer-ltac2in1.sh

@@ -0,0 +1 @@
+overlay serapi https://github.com/SkySkimmer/coq-serapi ltac2in1 17575

doc/changelog/06-Ltac2-language/17575-ltac2in1.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  Ltac2 quotations :ref:`ltac2val:(ltac2 tactic) <ltac2in1>` in Ltac1 which produce Ltac1 values
+  (as opposed to `ltac2:()` quotations which are only useful for their side effects)
+  (`#17575 <https://github.com/coq/coq/pull/17575>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proof-engine/ltac2.rst

@@ -1710,6 +1710,8 @@ Debug
 Compatibility layer with Ltac1
 ------------------------------
 
+.. _ltac2in1:
+
 Ltac1 from Ltac2
 ~~~~~~~~~~~~~~~~
 
@@ -1796,10 +1798,37 @@ below will fail immediately and won't print anything.
    Fail mytac ltac2:(fail).
    (* Prints and fails *)
    Fail mytac ltac:(idtac; ltac2:(fail)).
+   Abort.
 
 In any case, the value returned by the fully applied quotation is an
 unspecified dummy Ltac1 closure and should not be further used.
 
+Use the `ltac2val` quotation to return values to Ltac1 from Ltac2.
+
+.. prodn::
+   ltac_expr += ltac2val : ( @ltac2_expr )
+   | ltac2val : ( {+ @ident } |- @ltac2_expr )
+
+It has the same typing rules as `ltac2:()` except the expression must have type `Ltac2.Ltac1.t`.
+
+.. coqtop:: all
+
+   Import Constr.Unsafe.
+
+   Ltac add1 x :=
+     let f := ltac2val:(Ltac1.lambda (fun y =>
+       let y := Option.get (Ltac1.to_constr y) in
+       let y := make (App constr:(S) [|y|]) in
+       Ltac1.of_constr y))
+     in
+     f x.
+
+   Goal True.
+     let z := constr:(0) in
+     let v := add1 z in
+     idtac v.
+   Abort.
+
 Switching between Ltac languages
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 

plugins/ltac2/tac2core.ml

@@ -1957,14 +1957,22 @@ let () =
 (** Ltac2 in Ltac1 *)
 
 let () =
-  let e = Tac2entries.Pltac.tac2expr_in_env in
-  let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (Some "ltac2", in_gen (rawwit wit_ltac2in1) v) in
-  Ltac_plugin.Tacentries.create_ltac_quotation ~plugin:ltac2_plugin "ltac2" inject (e, None)
+  let create name wit =
+    let e = Tac2entries.Pltac.tac2expr_in_env in
+    let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (Some name, in_gen (rawwit wit) v) in
+    Ltac_plugin.Tacentries.create_ltac_quotation ~plugin:ltac2_plugin name inject (e, None)
+  in
+  let () = create "ltac2" wit_ltac2in1 in
+  let () = create "ltac2val" wit_ltac2in1_val in
+  ()
 
 (* Ltac1 runtime representation of Ltac2 closures. *)
 let typ_ltac2 : valexpr Geninterp.Val.typ =
   Geninterp.Val.create "ltac2:ltac2_eval"
 
+let () = Genprint.register_val_print0 typ_ltac2 (fun v ->
+    TopPrinterBasic (fun () -> Pp.str "<ltac2 closure>"))
+
 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
@@ -2027,8 +2035,9 @@ let () =
     let idtac = Value.of_closure { ist with lfun = Id.Map.empty }
         (CAst.make (Tacexpr.TacId [])) in
     let ist = { env_ist = Id.Map.empty } in
-    Tac2interp.interp ist tac >>= fun _ ->
-    Ftactic.return idtac
+    Tac2interp.interp ist tac >>= fun v ->
+    let v = idtac in
+    Ftactic.return v
   | _ :: _ ->
     (* Return a closure [@f := {blob} |- fun ids => ltac2_eval(f, ids) ] *)
     (* This name cannot clash with Ltac2 variables which are all lowercase *)
@@ -2046,6 +2055,15 @@ let () =
   in
   Geninterp.register_interp0 wit_ltac2in1 interp
 
+let () =
+  let interp ist tac =
+    let ist = { env_ist = Id.Map.empty } in
+    Tac2interp.interp ist tac >>= fun v ->
+    let v = repr_to ltac1 v in
+    Ftactic.return v
+  in
+  Geninterp.register_interp0 wit_ltac2in1_val interp
+
 let () =
   let pr_raw _ = Genprint.PrinterBasic (fun _env _sigma -> assert false) in
   let pr_glb (ids, e) =

plugins/ltac2/tac2env.ml

@@ -309,10 +309,13 @@ let ltac1_prefix =
 (** Generic arguments *)
 
 let wit_ltac2in1 = Genarg.make0 "ltac2in1"
-let wit_ltac2_val = Genarg.make0 "ltac2:value"
+let wit_ltac2in1_val = Genarg.make0 "ltac2in1val"
 let wit_ltac2_constr = Genarg.make0 "ltac2:in-constr"
 let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation"
+let wit_ltac2_val = Genarg.make0 "ltac2:value"
+
 let () = Geninterp.register_val0 wit_ltac2in1 None
+let () = Geninterp.register_val0 wit_ltac2in1_val None
 let () = Geninterp.register_val0 wit_ltac2_constr None
 let () = Geninterp.register_val0 wit_ltac2_quotation None
 

plugins/ltac2/tac2env.mli

@@ -158,16 +158,20 @@ val ltac1_prefix : ModPath.t
 val wit_ltac2in1 : (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_ltac2in1_val : (Id.t CAst.t list * raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
+(** Ltac2 quotations in Ltac1 returning Ltac1 values.
+    When ids are bound interning turns them into Ltac1.lambda. *)
 
 val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genarg_type
 (** Ltac2 quotations in Gallina terms *)
 
 val wit_ltac2_quotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type
 (** Ltac2 quotations for variables "$x" in Gallina terms *)
 
+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. *)
+
 (** {5 Helper functions} *)
 
 val is_constructor_id : Id.t -> bool

plugins/ltac2/tac2intern.ml

@@ -23,12 +23,13 @@ open Tac2typing_env
 (** Hardwired types and constants *)
 
 let coq_type n = KerName.make Tac2env.coq_prefix (Label.make n)
-let ltac1_type n = KerName.make Tac2env.ltac1_prefix (Label.make n)
+let ltac1_kn n = KerName.make Tac2env.ltac1_prefix (Label.make n)
 
 let t_int = coq_type "int"
 let t_string = coq_type "string"
 let t_constr = coq_type "constr"
-let t_ltac1 = ltac1_type "t"
+let t_ltac1 = ltac1_kn "t"
+let ltac1_lamdba = ltac1_kn "lambda"
 let t_preterm = coq_type "preterm"
 let t_bool = coq_type "bool"
 
@@ -1850,6 +1851,30 @@ let () =
   in
   Genintern.register_intern0 wit_ltac2in1 intern
 
+let () =
+  let open Genintern in
+  let add_lambda id tac =
+    let pat = CAst.make ?loc:id.CAst.loc (CPatVar (Name id.v)) in
+    let loc = tac.CAst.loc in
+    let mk v = CAst.make ?loc v in
+    let lam = mk @@ CTacFun ([pat], tac) in
+    mk @@ CTacApp (mk @@ CTacRef (AbsKn (TacConstant ltac1_lamdba)), [lam])
+  in
+  let intern ist (bnd,tac) =
+    let env = match Genintern.Store.get ist.extra ltac2_env with
+    | None ->
+      (* Only happens when Ltac2 is called from a toplevel ltac1 quotation *)
+      empty_env ~strict:ist.strict_check ()
+    | Some env -> env
+    in
+    let loc = tac.loc in
+    let tac = List.fold_right add_lambda bnd tac in
+    let (tac, t) = intern_rec env tac in
+    let () = unify ?loc env t (GTypRef (Other t_ltac1, [])) in
+    (ist, tac)
+  in
+  Genintern.register_intern0 wit_ltac2in1_val intern
+
 let () =
   let open Genintern in
   let intern ist tac =
@@ -1876,6 +1901,7 @@ let () =
   Genintern.register_intern0 wit_ltac2_constr intern
 
 let () = Genintern.register_subst0 wit_ltac2in1 (fun s (ids, e) -> ids, subst_expr s e)
+let () = Genintern.register_subst0 wit_ltac2in1_val subst_expr
 let () = Genintern.register_subst0 wit_ltac2_constr (fun s (ids, e) -> ids, subst_expr s e)
 
 let () =

test-suite/ltac2/ltac2in1.v

@@ -0,0 +1,59 @@
+Require Import Ltac2.Ltac2.
+
+Import Constr.Unsafe.
+
+(* manual Ltac1.lambda wrapping *)
+Ltac add1 :=
+  ltac2val:(Ltac1.lambda (fun y =>
+    let y := Option.get (Ltac1.to_constr y) in
+    let y := make (App constr:(S) [|y|]) in
+    Ltac1.of_constr y)).
+
+(* automatic Ltac1.lambda wrapping
+   also check that it's done in the right order *)
+Ltac add1' :=
+  ltac2val:(y z |-
+    let y := Option.get (Ltac1.to_constr y) in
+    let y := make (App constr:(S) [|y|]) in
+    Ltac1.of_constr y).
+
+Set Default Proof Mode "Classic".
+
+Goal True.
+  let z := constr:(0) in
+  let v := add1 z in
+  constr_eq v 1.
+
+  let a := constr:(0) in
+  let v := add1' a 2 in
+  constr_eq v 1.
+
+  (* currying works *)
+  let a := constr:(0) in
+  let v := add1' a in
+  let v' := v 2 in
+  constr_eq v' 1.
+
+  (* check order of arguments *)
+  Fail let a := constr:(0) in
+  let v := add1' 2 a in
+  constr_eq v 1.
+
+  (* printer doesn't anomaly *)
+  let v := add1' in
+  idtac v.
+
+Abort.
+
+(* With ltac2:(x) this would succeed without warning
+   "this expression should have type unit but has type constr"
+   because ltac2:(x) only checks that x has type unifiable with unit.
+   It's not a big problem as the constr gets discarded by ltac2:()
+   so we just get an incomplete warning (maybe fixed in the future).
+
+   With ltac2val such a weak check would produce runtime anomalies.
+ *)
+Fail Ltac2 bad x :=
+  let c1 := constr:(ltac:(ltac2val:(x))) in
+  let c2 := constr:($x) in
+  ().