From 08920fc79601e03c8a3cf99cc95f46e23ef38b77 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 5 May 2023 15:45:19 +0200 Subject: [PATCH 1/2] Rename wit_ltac2 -> wit_ltac2in1 --- plugins/ltac2/tac2core.ml | 6 +++--- plugins/ltac2/tac2env.ml | 4 ++-- plugins/ltac2/tac2env.mli | 2 +- plugins/ltac2/tac2intern.ml | 4 ++-- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index d47d0debdfeb..8a6d326d354b 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -1958,7 +1958,7 @@ let () = let () = let e = Tac2entries.Pltac.tac2expr_in_env in - let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (Some "ltac2", in_gen (rawwit wit_ltac2) v) 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) (* Ltac1 runtime representation of Ltac2 closures. *) @@ -2044,7 +2044,7 @@ let () = let ist = { ist with lfun = Id.Map.singleton self_id self } in Ftactic.return (Value.of_closure ist clos) in - Geninterp.register_interp0 wit_ltac2 interp + Geninterp.register_interp0 wit_ltac2in1 interp let () = let pr_raw _ = Genprint.PrinterBasic (fun _env _sigma -> assert false) in @@ -2056,7 +2056,7 @@ let () = Genprint.PrinterBasic Pp.(fun _env _sigma -> ids ++ Tac2print.pr_glbexpr e) in let pr_top x = Util.Empty.abort x in - Genprint.register_print0 wit_ltac2 pr_raw pr_glb pr_top + Genprint.register_print0 wit_ltac2in1 pr_raw pr_glb pr_top let () = let pr_raw _ = Genprint.PrinterBasic (fun _env _sigma -> assert false) in diff --git a/plugins/ltac2/tac2env.ml b/plugins/ltac2/tac2env.ml index bda30589a4d1..9e110845741a 100644 --- a/plugins/ltac2/tac2env.ml +++ b/plugins/ltac2/tac2env.ml @@ -308,11 +308,11 @@ let ltac1_prefix = (** Generic arguments *) -let wit_ltac2 = Genarg.make0 "ltac2:tactic" +let wit_ltac2in1 = Genarg.make0 "ltac2in1" 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 +let () = Geninterp.register_val0 wit_ltac2in1 None let () = Geninterp.register_val0 wit_ltac2_constr None let () = Geninterp.register_val0 wit_ltac2_quotation None diff --git a/plugins/ltac2/tac2env.mli b/plugins/ltac2/tac2env.mli index 0f0f96090be1..02265961c341 100644 --- a/plugins/ltac2/tac2env.mli +++ b/plugins/ltac2/tac2env.mli @@ -155,7 +155,7 @@ val ltac1_prefix : ModPath.t (** {5 Generic arguments} *) -val wit_ltac2 : (Id.t CAst.t list * raw_tacexpr, Id.t list * glb_tacexpr, Util.Empty.t) genarg_type +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 diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index bca9a9364f38..9bb0cb4c4bd6 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/plugins/ltac2/tac2intern.ml @@ -1848,7 +1848,7 @@ let () = let () = check_elt_unit loc env t in (ist, (ids, tac)) in - Genintern.register_intern0 wit_ltac2 intern + Genintern.register_intern0 wit_ltac2in1 intern let () = let open Genintern in @@ -1875,7 +1875,7 @@ let () = in Genintern.register_intern0 wit_ltac2_constr intern -let () = Genintern.register_subst0 wit_ltac2 (fun s (ids, e) -> ids, subst_expr s e) +let () = Genintern.register_subst0 wit_ltac2in1 (fun s (ids, e) -> ids, subst_expr s e) let () = Genintern.register_subst0 wit_ltac2_constr (fun s (ids, e) -> ids, subst_expr s e) let () = From 9dbf1b7d29b36094b5aae441d2830bfa51656de1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 9 May 2023 17:34:52 +0200 Subject: [PATCH 2/2] ltac2val:() quotation in ltac1 to return Ltac1.t values --- .../17575-SkySkimmer-ltac2in1.sh | 1 + .../06-Ltac2-language/17575-ltac2in1.rst | 5 ++ doc/sphinx/proof-engine/ltac2.rst | 29 +++++++++ plugins/ltac2/tac2core.ml | 28 +++++++-- plugins/ltac2/tac2env.ml | 5 +- plugins/ltac2/tac2env.mli | 10 +++- plugins/ltac2/tac2intern.ml | 30 +++++++++- test-suite/ltac2/ltac2in1.v | 59 +++++++++++++++++++ 8 files changed, 156 insertions(+), 11 deletions(-) create mode 100644 dev/ci/user-overlays/17575-SkySkimmer-ltac2in1.sh create mode 100644 doc/changelog/06-Ltac2-language/17575-ltac2in1.rst create mode 100644 test-suite/ltac2/ltac2in1.v diff --git a/dev/ci/user-overlays/17575-SkySkimmer-ltac2in1.sh b/dev/ci/user-overlays/17575-SkySkimmer-ltac2in1.sh new file mode 100644 index 000000000000..98383701b589 --- /dev/null +++ b/dev/ci/user-overlays/17575-SkySkimmer-ltac2in1.sh @@ -0,0 +1 @@ +overlay serapi https://github.com/SkySkimmer/coq-serapi ltac2in1 17575 diff --git a/doc/changelog/06-Ltac2-language/17575-ltac2in1.rst b/doc/changelog/06-Ltac2-language/17575-ltac2in1.rst new file mode 100644 index 000000000000..828f3e044ebb --- /dev/null +++ b/doc/changelog/06-Ltac2-language/17575-ltac2in1.rst @@ -0,0 +1,5 @@ +- **Added:** + Ltac2 quotations :ref:`ltac2val:(ltac2 tactic) ` in Ltac1 which produce Ltac1 values + (as opposed to `ltac2:()` quotations which are only useful for their side effects) + (`#17575 `_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index c332dd46d94a..1889b61df807 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 8a6d326d354b..9063254d3187 100644 --- a/plugins/ltac2/tac2core.ml +++ b/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 "")) + 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) = diff --git a/plugins/ltac2/tac2env.ml b/plugins/ltac2/tac2env.ml index 9e110845741a..7f0dec913dc5 100644 --- a/plugins/ltac2/tac2env.ml +++ b/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 diff --git a/plugins/ltac2/tac2env.mli b/plugins/ltac2/tac2env.mli index 02265961c341..c33cbc886bac 100644 --- a/plugins/ltac2/tac2env.mli +++ b/plugins/ltac2/tac2env.mli @@ -158,9 +158,9 @@ 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 *) @@ -168,6 +168,10 @@ val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genar 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 diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index 9bb0cb4c4bd6..7c7089ef6202 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/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 () = diff --git a/test-suite/ltac2/ltac2in1.v b/test-suite/ltac2/ltac2in1.v new file mode 100644 index 000000000000..1bf8d2b712bf --- /dev/null +++ b/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 + ().