From 33a209a259d02824d115ba2e16f88988b452a2fc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 6 Feb 2023 17:51:39 +0100 Subject: [PATCH] ltac2 preterm antiquotation --- .../17359-tac2-preterm-antiquot.rst | 5 ++ doc/sphinx/proof-engine/ltac2.rst | 6 ++ plugins/ltac2/g_ltac2.mlg | 16 +++++ plugins/ltac2/tac2core.ml | 42 +++++++++++++ plugins/ltac2/tac2env.ml | 2 + plugins/ltac2/tac2env.mli | 3 + plugins/ltac2/tac2intern.ml | 40 ++++++------ pretyping/pretyping.ml | 3 + pretyping/pretyping.mli | 4 ++ test-suite/ltac2/preterm_antiquot.v | 61 +++++++++++++++++++ 10 files changed, 162 insertions(+), 20 deletions(-) create mode 100644 doc/changelog/06-Ltac2-language/17359-tac2-preterm-antiquot.rst create mode 100644 test-suite/ltac2/preterm_antiquot.v diff --git a/doc/changelog/06-Ltac2-language/17359-tac2-preterm-antiquot.rst b/doc/changelog/06-Ltac2-language/17359-tac2-preterm-antiquot.rst new file mode 100644 index 0000000000000..3abba8136d59f --- /dev/null +++ b/doc/changelog/06-Ltac2-language/17359-tac2-preterm-antiquot.rst @@ -0,0 +1,5 @@ +- **Added:** + Ltac2 preterm antiquotation `$$` + (`#17359 `_, + fixes `#13977 `_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 1889b61df807d..0129f9c91d4a8 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -749,6 +749,12 @@ In a Coq term, writing :g:`$x` is semantically equivalent to :g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term. +Similarly variables of type `preterm` have an antiquotation + +.. prodn:: term += $$@lident + +It is equivalent to pretyping the preterm with the appropriate typing constraint. + Match over terms ~~~~~~~~~~~~~~~~ diff --git a/plugins/ltac2/g_ltac2.mlg b/plugins/ltac2/g_ltac2.mlg index c14815d43fea9..1abc060d55604 100644 --- a/plugins/ltac2/g_ltac2.mlg +++ b/plugins/ltac2/g_ltac2.mlg @@ -65,6 +65,12 @@ let test_dollar_ident = lk_kw "$" >> lk_ident >> check_no_space end +let test_2dollar_ident = + let open Pcoq.Lookahead in + to_entry "test_2dollar_ident" begin + lk_kw "$$" >> lk_ident >> check_no_space + end + let test_ltac1_env = let open Pcoq.Lookahead in to_entry "test_ltac1_env" begin @@ -945,6 +951,16 @@ let rules = [ end ); + Pcoq.( + Production.make + (Rule.stop ++ Symbol.nterm test_2dollar_ident ++ Symbol.token (PKEYWORD "$$") ++ Symbol.nterm Prim.ident) + begin fun id _ _ loc -> + let id = Loc.tag ~loc id in + let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_prequotation) id in + CAst.make ~loc (CGenarg arg) + end + ); + Pcoq.( Production.make (Rule.stop ++ Symbol.nterm test_ampersand_ident ++ Symbol.token (PKEYWORD "&") ++ Symbol.nterm Prim.ident) diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 9063254d31879..9c52083eb63fa 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -43,6 +43,18 @@ let open_constr_no_classes_flags = polymorphic = false; } +let preterm_flags = + let open Pretyping in + { + use_coercions = true; + use_typeclasses = Pretyping.NoUseTC; + solve_unification_constraints = true; + fail_evar = false; + expand_evars = false; + program_mode = false; + polymorphic = false; + } + (** Standard values *) module Value = Tac2ffi @@ -1925,12 +1937,42 @@ let () = in GlobEnv.register_constr_interp0 wit_ltac2_quotation interp +let () = + let interp ?loc ~poly env sigma tycon id = + let open Ltac_pretype in + let ist = Tac2interp.get_env @@ GlobEnv.lfun env in + let env = GlobEnv.renamed_env env in + let c = Id.Map.find id ist.env_ist in + let {closure; term} = Value.to_ext Value.val_preterm c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = closure.genargs; + } + in + let flags = preterm_flags in + let tycon = let open Pretyping in match tycon with + | Some ty -> OfType ty + | None -> WithoutTypeConstraint + in + let sigma, t, ty = Pretyping.understand_ltac_ty flags env sigma vars tycon term in + Environ.make_judge t ty, sigma + in + GlobEnv.register_constr_interp0 wit_ltac2_prequotation interp + let () = let pr_raw id = Genprint.PrinterBasic (fun _env _sigma -> assert false) in let pr_glb id = Genprint.PrinterBasic (fun _env _sigma -> str "$" ++ Id.print id) in let pr_top x = Util.Empty.abort x in Genprint.register_print0 wit_ltac2_quotation pr_raw pr_glb pr_top +let () = + let pr_raw id = Genprint.PrinterBasic (fun _env _sigma -> assert false) in + let pr_glb id = Genprint.PrinterBasic (fun _env _sigma -> str "$$" ++ Id.print id) in + let pr_top e = Util.Empty.abort e in + Genprint.register_print0 wit_ltac2_prequotation pr_raw pr_glb pr_top + let () = let subs avoid globs (ids, tac) = (* Let-bind the notation terms inside the tactic *) diff --git a/plugins/ltac2/tac2env.ml b/plugins/ltac2/tac2env.ml index 7f0dec913dc54..d217c649e59c0 100644 --- a/plugins/ltac2/tac2env.ml +++ b/plugins/ltac2/tac2env.ml @@ -313,11 +313,13 @@ 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 wit_ltac2_prequotation = Genarg.make0 "ltac2:prequotation" 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 +let () = Geninterp.register_val0 wit_ltac2_prequotation None let is_constructor_id id = let id = Id.to_string id in diff --git a/plugins/ltac2/tac2env.mli b/plugins/ltac2/tac2env.mli index c33cbc886bac4..f6885f4c490b7 100644 --- a/plugins/ltac2/tac2env.mli +++ b/plugins/ltac2/tac2env.mli @@ -172,6 +172,9 @@ 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_prequotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type +(** Ltac2 quotations for preterm variables "$$x" in Gallina terms *) + (** {5 Helper functions} *) val is_constructor_id : Id.t -> bool diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index 7926933bec84c..152bca35b188f 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/plugins/ltac2/tac2intern.ml @@ -1904,30 +1904,30 @@ let () = Genintern.register_subst0 wit_ltac2in1 (fun s (ids, e) -> ids, subst_ex 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 () = - let open Genintern in - let intern ist (loc, id) = - let env = match Genintern.Store.get ist.extra ltac2_env with +let intern_quotation typ = let open Genintern in + fun ist (loc, id) -> + let env = match Genintern.Store.get ist.extra ltac2_env with | None -> (* Only happens when Ltac2 is called from a constr or ltac1 quotation *) empty_env ~strict:ist.strict_check () | Some env -> env - in - (* Special handling of notation variables *) - let () = - if Id.Map.mem id ist.intern_sign.notation_variable_status then - (* Always fail *) - unify ?loc env (GTypRef (Other t_preterm, [])) (GTypRef (Other t_constr, [])) - in - let t = - try find_var id env - with Not_found -> - CErrors.user_err ?loc (str "Unbound value " ++ Id.print id) - in - let t = fresh_mix_type_scheme env t in - let () = unify ?loc env t (GTypRef (Other t_constr, [])) in - (ist, id) in - Genintern.register_intern0 wit_ltac2_quotation intern + (* Special handling of notation variables *) + let () = + if Id.Map.mem id ist.intern_sign.notation_variable_status then + (* Always fail for constr, never for preterm *) + unify ?loc env (GTypRef (Other t_preterm, [])) (GTypRef (Other typ, [])) + in + let t = + try find_var id env + with Not_found -> + CErrors.user_err ?loc (str "Unbound value " ++ Id.print id) + in + let t = fresh_mix_type_scheme env t in + let () = unify ?loc env t (GTypRef (Other typ, [])) in + (ist, id) + +let () = Genintern.register_intern0 wit_ltac2_quotation (intern_quotation t_constr) +let () = Genintern.register_intern0 wit_ltac2_prequotation (intern_quotation t_preterm) let () = Genintern.register_subst0 wit_ltac2_quotation (fun _ id -> id) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9031631b46a9b..ae50604ca2777 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1452,6 +1452,9 @@ let understand_ltac flags env sigma lvar kind c = let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) +let understand_ltac_ty flags env sigma lvar kind c = + ise_pretype_gen flags env sigma lvar kind c + (* Fully evaluate an untyped constr *) let understand_uconstr ?(flags = all_and_fail_flags) ?(expected_type = WithoutTypeConstraint) env sigma c = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index c03eedd70e259..d34472af26f4d 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -98,6 +98,10 @@ val understand_ltac : inference_flags -> env -> evar_map -> ltac_var_map -> typing_constraint -> glob_constr -> evar_map * EConstr.t +val understand_ltac_ty : inference_flags -> + env -> evar_map -> ltac_var_map -> + typing_constraint -> glob_constr -> evar_map * EConstr.t * EConstr.types + (** Standard call to get a constr from a glob_constr, resolving implicit arguments and coercions, and compiling pattern-matching; the default inference_flags tells to use type classes and diff --git a/test-suite/ltac2/preterm_antiquot.v b/test-suite/ltac2/preterm_antiquot.v new file mode 100644 index 0000000000000..81d8e9ea5b7d0 --- /dev/null +++ b/test-suite/ltac2/preterm_antiquot.v @@ -0,0 +1,61 @@ +Require Import ZArith. +Open Scope Z_scope. + +Require Import Ltac2.Ltac2. + +Ltac2 rec z2nat_preterm x := + let b := eval cbv in (Z.leb $x 0) in + lazy_match! b with + | true => preterm:(O) + | false => + let pred := eval cbv in (Z.pred $x) in + let r := z2nat_preterm pred in + preterm:(S $$r) + end. + + +Ltac2 rec z2nat_constr x := + let b := eval cbv in (Z.leb $x 0) in + lazy_match! b with + | true => constr:(O) + | false => let pred := eval cbv in (Z.pred $x) in + let r := z2nat_constr pred in + constr:(S $r) + end. + +Ltac2 mk_app(a: constr)(b: constr) := + Constr.Unsafe.make (Constr.Unsafe.App a [| b |]). + +Ltac2 rec z2nat_mk_app x := + let b := eval cbv in (Z.leb $x 0) in + lazy_match! b with + | true => Env.instantiate reference:(O) + | false => let pred := eval cbv in (Z.pred $x) in + mk_app (Env.instantiate reference:(S)) (z2nat_mk_app pred) + end. + +(* Time Ltac2 Eval *) +(* let c := z2nat_constr constr:(10000) in *) +(* Message.print (Message.of_constr c). (* 9 secs *) *) + +(* Time Ltac2 Eval *) +(* let c := z2nat_mk_app constr:(10000) in *) +(* Message.print (Message.of_constr c). (* <1 secs *) *) + +Time Ltac2 Eval + let c := z2nat_preterm constr:(10000) in + let c := constr:($$c) in + Message.print (Message.of_constr c). (* 6 secs *) + +(* Time Ltac2 Eval *) +(* let c := z2nat_constr constr:(20000) in *) +(* Message.print (Message.of_constr c). (* 22 secs *) *) + +(* Time Ltac2 Eval *) +(* let c := z2nat_mk_app constr:(20000) in *) +(* Message.print (Message.of_constr c). (* 1.6 secs *) *) + +Time Ltac2 Eval + let c := z2nat_preterm constr:(20000) in + let c := Constr.pretype c in + Message.print (Message.of_constr c). (* 32 secs *)