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..c76d3dcd23e1e --- /dev/null +++ b/doc/changelog/06-Ltac2-language/17359-tac2-preterm-antiquot.rst @@ -0,0 +1,5 @@ +- **Added:** + Ltac2 preterm antiquotation `$preterm:` + (`#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..08ff25b7baf21 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -745,10 +745,20 @@ the notation section. .. prodn:: term += $@lident +or equivalently + +.. prodn:: term += $constr:@lident + 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 += $preterm:@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..38e6444886a63 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_dollar_ident_colon_ident = + let open Pcoq.Lookahead in + to_entry "test_dollar_ident_colon_ident" begin + lk_kw "$" >> lk_ident >> lk_kw ":" >> lk_ident >> check_no_space + end + let test_ltac1_env = let open Pcoq.Lookahead in to_entry "test_ltac1_env" begin @@ -939,8 +945,19 @@ let rules = [ Production.make (Rule.stop ++ Symbol.nterm test_dollar_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_quotation) id in + let id = CAst.make ~loc id in + let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_var_quotation) (None, id) in + CAst.make ~loc (CGenarg arg) + end + ); + + Pcoq.( + Production.make + (Rule.stop ++ Symbol.nterm test_dollar_ident_colon_ident ++ + Symbol.token (PKEYWORD "$") ++ Symbol.nterm Prim.identref ++ + Symbol.token (PKEYWORD ":") ++ Symbol.nterm Prim.identref) + begin fun id _ kind _ _ loc -> + let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_var_quotation) (Some kind, id) in CAst.make ~loc (CGenarg arg) end ); diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 9063254d31879..73f659e259a8f 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 @@ -1641,8 +1653,12 @@ let intern_constr self ist c = let (_, (c, _)) = Genintern.intern Stdarg.wit_constr ist c in let v = match DAst.get c with | GGenarg (GenArg (Glbwit tag, v)) -> - begin match genarg_type_eq tag wit_ltac2_quotation with - | Some Refl -> GlbTacexpr (GTacVar v) + begin match genarg_type_eq tag wit_ltac2_var_quotation with + | Some Refl -> + begin match (fst v) with + | ConstrVar -> GlbTacexpr (GTacVar (snd v)) + | _ -> GlbVal c + end | None -> GlbVal c end | _ -> GlbVal c @@ -1904,32 +1920,72 @@ let () = in GlobEnv.register_constr_interp0 wit_ltac2_constr interp +let interp_constr_var_as_constr ?loc env sigma tycon id = + 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 c = Value.to_constr c in + let t = Retyping.get_type_of env sigma c in + let j = { Environ.uj_val = c; uj_type = t } in + match tycon with + | None -> + j, sigma + | Some ty -> + let sigma = + try Evarconv.unify_leq_delay env sigma t ty + with Evarconv.UnableToUnify (sigma,e) -> + Pretype_errors.error_actual_type ?loc env sigma j ty e + in + {j with Environ.uj_type = ty}, sigma + +let interp_preterm_var_as_constr ?loc 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 + let () = - let interp ?loc ~poly env sigma tycon id = - 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 c = Value.to_constr c in - let t = Retyping.get_type_of env sigma c in - let j = { Environ.uj_val = c; uj_type = t } in - match tycon with - | None -> - j, sigma - | Some ty -> - let sigma = - try Evarconv.unify_leq_delay env sigma t ty - with Evarconv.UnableToUnify (sigma,e) -> - Pretype_errors.error_actual_type ?loc env sigma j ty e - in - {j with Environ.uj_type = ty}, sigma + let interp ?loc ~poly env sigma tycon (kind,id) = + let f = match kind with + | ConstrVar -> interp_constr_var_as_constr + | PretermVar -> interp_preterm_var_as_constr + in + f ?loc env sigma tycon id in - GlobEnv.register_constr_interp0 wit_ltac2_quotation interp + GlobEnv.register_constr_interp0 wit_ltac2_var_quotation 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_raw (kind,id) = Genprint.PrinterBasic (fun _env _sigma -> + let ppkind = + match kind with + | None -> mt() + | Some kind -> Id.print kind.CAst.v ++ str ":" + in + str "$" ++ ppkind ++ Id.print id.CAst.v) + in + let pr_glb (kind,id) = Genprint.PrinterBasic (fun _env _sigma -> + let ppkind = match kind with + | ConstrVar -> mt() + | PretermVar -> str "preterm:" + in + str "$" ++ ppkind ++ 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 + Genprint.register_print0 wit_ltac2_var_quotation pr_raw pr_glb pr_top let () = let subs avoid globs (ids, tac) = diff --git a/plugins/ltac2/tac2env.ml b/plugins/ltac2/tac2env.ml index 7f0dec913dc54..3bd9307a1710e 100644 --- a/plugins/ltac2/tac2env.ml +++ b/plugins/ltac2/tac2env.ml @@ -308,16 +308,20 @@ let ltac1_prefix = (** Generic arguments *) +type var_quotation_kind = + | ConstrVar + | PretermVar + let wit_ltac2in1 = Genarg.make0 "ltac2in1" 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_var_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 +let () = Geninterp.register_val0 wit_ltac2_var_quotation 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..f3908cce49363 100644 --- a/plugins/ltac2/tac2env.mli +++ b/plugins/ltac2/tac2env.mli @@ -165,8 +165,13 @@ val wit_ltac2in1_val : (Id.t CAst.t list * raw_tacexpr, glb_tacexpr, Util.Empty. 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 *) +type var_quotation_kind = + | ConstrVar + | PretermVar + +val wit_ltac2_var_quotation : (lident option * lident, var_quotation_kind * Id.t, Util.Empty.t) genarg_type +(** Ltac2 quotations for variables "$x" or "$kind:foo" in Gallina terms. + NB: "$x" means "$constr:x" *) 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 diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index 7926933bec84c..25e292fd189e6 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/plugins/ltac2/tac2intern.ml @@ -1904,30 +1904,42 @@ 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 intern_var_quotation ist (kind, { CAst.v = id; loc }) = let open Genintern in - let intern ist (loc, id) = - let env = match Genintern.Store.get ist.extra ltac2_env with + let kind = match kind with + | None -> ConstrVar + | Some kind -> match Id.to_string kind.CAst.v with + | "constr" -> ConstrVar + | "preterm" -> PretermVar + | _ -> + CErrors.user_err ?loc:kind.loc + Pp.(str "Unknown Ltac2 variable quotation kind" ++ spc() ++ Id.print kind.v) + in + let typ = match kind with + | ConstrVar -> t_constr + | PretermVar -> t_preterm + in + 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, (kind, id)) + +let () = Genintern.register_intern0 wit_ltac2_var_quotation intern_var_quotation -let () = Genintern.register_subst0 wit_ltac2_quotation (fun _ id -> id) +let () = Genintern.register_subst0 wit_ltac2_var_quotation (fun _ v -> v) 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..5a2dbc61ef2ae --- /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 $preterm: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:($preterm: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 *) diff --git a/test-suite/output-coqtop/ltac2_var_quot.out b/test-suite/output-coqtop/ltac2_var_quot.out new file mode 100644 index 0000000000000..3550325ee790a --- /dev/null +++ b/test-suite/output-coqtop/ltac2_var_quot.out @@ -0,0 +1,53 @@ + + +Coq < Coq < Toplevel input, characters 7-9: +> Check $x. +> ^^ +Error: Unbound value x + +Coq < Coq < Toplevel input, characters 16-17: +> Check $preterm:x. +> ^ +Error: Unbound value x + +Coq < Coq < Toplevel input, characters 7-8: +> Check $ x. +> ^ +Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]). + +Coq < Coq < Toplevel input, characters 7-8: +> Check $ preterm:x. +> ^ +Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]). + +Coq < Coq < Toplevel input, characters 7-8: +> Check $ preterm : x. +> ^ +Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]). + +Coq < Coq < Toplevel input, characters 18-19: +> Check $preterm : x. +> ^ +Error: The reference x was not found in the current environment. + +Coq < Coq < Toplevel input, characters 16-24: +> Check fun x => $preterm : x. +> ^^^^^^^^ +Error: Unbound value preterm + +Coq < Coq < Toplevel input, characters 17-18: +> Check $preterm: x. +> ^ +Error: The reference x was not found in the current environment. + +Coq < Coq < Toplevel input, characters 16-24: +> Check fun x => $preterm: x. +> ^^^^^^^^ +Error: Unbound value preterm + +Coq < Coq < Toplevel input, characters 7-8: +> Check $ preterm :x. +> ^ +Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]). + +Coq < diff --git a/test-suite/output-coqtop/ltac2_var_quot.v b/test-suite/output-coqtop/ltac2_var_quot.v new file mode 100644 index 0000000000000..fef38205b4228 --- /dev/null +++ b/test-suite/output-coqtop/ltac2_var_quot.v @@ -0,0 +1,21 @@ +Require Import Ltac2.Ltac2. + +Check $x. + +Check $preterm:x. + +Check $ x. + +Check $ preterm:x. + +Check $ preterm : x. + +Check $preterm : x. + +Check fun x => $preterm : x. + +Check $preterm: x. + +Check fun x => $preterm: x. + +Check $ preterm :x.