From f38799d6488cacad2aba9829788185d5256853ba Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Fri, 26 Sep 2025 10:30:26 +0200 Subject: [PATCH 01/12] Add and use helper for predicates producing diagnostics --- src/rocq_elpi_builtins.ml | 60 ++++++++++++--------------------------- src/rocq_elpi_utils.ml | 23 +++++++++++++++ src/rocq_elpi_utils.mli | 6 ++++ 3 files changed, 47 insertions(+), 42 deletions(-) diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index b09a73757..839382876 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -3545,13 +3545,9 @@ Universe constraints are put in the constraint store.|})))), let state, assignments = set_current_sigma ~depth state sigma in state, r, assignments with Pretype_errors.PretypeError (env, sigma, err) -> - match diag with - | Data B.OK -> - (* optimization: don't print the error if caller wants OK *) - raise No_clause - | _ -> - let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in - state, ?: None +! B.mkERROR error, [])), + diag_error_lazy diag @@ fun () -> + let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in + state, ?: None +! B.mkERROR error, [])), DocAbove); MLCode(Pred("coq.typecheck-ty", @@ -3579,13 +3575,9 @@ Universe constraints are put in the constraint store.|})))), let state, assignments = set_current_sigma ~depth state sigma in state, r, assignments with Pretype_errors.PretypeError (env, sigma, err) -> - match diag with - | Data B.OK -> - (* optimization: don't print the error if caller wants OK *) - raise No_clause - | _ -> - let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in - state, ?: None +! B.mkERROR error, [])), + diag_error_lazy diag @@ fun () -> + let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in + state, ?: None +! B.mkERROR error, [])), DocAbove); MLCode(Pred("coq.unify-eq", @@ -3600,13 +3592,9 @@ Universe constraints are put in the constraint store.|})))), let state, assignments = set_current_sigma ~depth state sigma in state, !: B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> - match diag with - | Data B.OK -> - (* optimization: don't print the error if caller wants OK *) - raise No_clause - | _ -> - let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in - state, !: (B.mkERROR error), [])), + diag_error_lazy diag @@ fun () -> + let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in + state, !: (B.mkERROR error), [])), DocAbove); MLCode(Pred("coq.unify-leq", @@ -3621,13 +3609,9 @@ Universe constraints are put in the constraint store.|})))), let state, assignments = set_current_sigma ~depth state sigma in state, !: B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> - match diag with - | Data B.OK -> - (* optimization: don't print the error if caller wants OK *) - raise No_clause - | _ -> - let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in - state, !: (B.mkERROR error), [])), + diag_error_lazy diag @@ fun () -> + let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in + state, !: (B.mkERROR error), [])), DocAbove); MLCode(Pred("coq.elaborate-skeleton", @@ -3670,13 +3654,9 @@ Supported attributes: let state, assignments = set_current_sigma ~depth state sigma in state, ?: None +! uj_val +! B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> - match diag with - | Data B.OK -> - (* optimization: don't print the error if caller wants OK *) - raise No_clause - | _ -> - let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in - state, ?: None +? None +! B.mkERROR error, [])), + diag_error_lazy diag @@ fun () -> + let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in + state, ?: None +? None +! B.mkERROR error, [])), DocAbove); MLCode(Pred("coq.elaborate-ty-skeleton", @@ -3704,13 +3684,9 @@ Supported attributes: let state, assignments = set_current_sigma ~depth state sigma in state, !: sort +! uj_val +! B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> - match diag with - | Data B.OK -> - (* optimization: don't print the error if caller wants OK *) - raise No_clause - | _ -> - let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in - state, ?: None +? None +! B.mkERROR error, [])), + diag_error_lazy diag @@ fun () -> + let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in + state, ?: None +? None +! B.mkERROR error, [])), DocAbove); LPDoc "-- Coq's reduction flags ------------------------------------"; diff --git a/src/rocq_elpi_utils.ml b/src/rocq_elpi_utils.ml index b9938916d..bcd103323 100644 --- a/src/rocq_elpi_utils.ml +++ b/src/rocq_elpi_utils.ml @@ -873,3 +873,26 @@ let eta_contract env sigma t = in (*Printf.eprintf "------------- %s\n" Pp.(string_of_ppcmds @@ Printer.pr_econstr_env env sigma t);*) map env t + +(* Command argument specifiers *) +type arg_kind = + | Elaborated + | Unelaborated + | Syntactic +let arg_kind_merge ?loc (old : arg_kind option) (k : arg_kind) = + match old with + | None -> k + | Some old when old = k -> k + | _ -> CErrors.user_err ?loc Pp.(str "Syntax error, incompatible values for attribute \"arguments\"") + +(* Helper for predicates that produce diagnostics *) +let diag_error_lazy + ?(on_ok=fun () -> raise API.BuiltInPredicate.No_clause) + diag_arg + (on_other : unit -> 'a) : 'a = + let open API.BuiltInPredicate in + (* optimization: don't print the error if caller wants OK *) + match diag_arg with + | Data Elpi.Builtin.OK -> on_ok () + | _ -> on_other () + diff --git a/src/rocq_elpi_utils.mli b/src/rocq_elpi_utils.mli index f0e0aeba1..1eb51536b 100644 --- a/src/rocq_elpi_utils.mli +++ b/src/rocq_elpi_utils.mli @@ -89,3 +89,9 @@ val mp2path: Names.ModPath.t -> string list val gr2path: Names.GlobRef.t -> string list val eta_contract : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t + +(* Diagnostics *) +val diag_error_lazy : ?on_ok:(unit -> 'a) -> (* defaults to [raise No_clause] *) + Elpi.Builtin.diagnostic Elpi.API.BuiltInPredicate.ioarg -> + (unit -> 'a) -> + 'a From 20c57dac04f831f465c256ff9032d6653bc7146f Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Wed, 24 Sep 2025 17:15:26 +0200 Subject: [PATCH 02/12] Add @no-coercion! option and macro --- builtin-doc/coq-builtin.elpi | 1 + elpi/coq-HOAS.elpi | 1 + src/rocq_elpi_HOAS.ml | 9 ++++++--- src/rocq_elpi_HOAS.mli | 1 + src/rocq_elpi_builtins.ml | 8 ++++++-- 5 files changed, 15 insertions(+), 5 deletions(-) diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index f142b6b5b..e505dfe22 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/builtin-doc/coq-builtin.elpi @@ -480,6 +480,7 @@ macro @keep-alg-univs! :- get-option "coq:keepalgunivs" tt. macro @primitive! :- get-option "coq:primitive" tt. % primitive records macro @reversible! :- get-option "coq:reversible" tt. % coercions macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference +macro @no-coercion! :- get-option "coq:no_coercion" tt. % ignore coercions during pretyping macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index 3c16f2399..951e0c427 100644 --- a/elpi/coq-HOAS.elpi +++ b/elpi/coq-HOAS.elpi @@ -308,6 +308,7 @@ macro @keep-alg-univs! :- get-option "coq:keepalgunivs" tt. macro @primitive! :- get-option "coq:primitive" tt. % primitive records macro @reversible! :- get-option "coq:reversible" tt. % coercions macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference +macro @no-coercion! :- get-option "coq:no_coercion" tt. % ignore coercions during pretyping macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance diff --git a/src/rocq_elpi_HOAS.ml b/src/rocq_elpi_HOAS.ml index 196704c80..bf9029c78 100644 --- a/src/rocq_elpi_HOAS.ml +++ b/src/rocq_elpi_HOAS.ml @@ -311,6 +311,7 @@ type options = { keepunivs : bool option; redflags : RedFlags.reds option; no_tc: bool option; + no_coercion: bool option; algunivs : bool option; } let default_options () = { @@ -330,15 +331,16 @@ let default_options () = { keepunivs = None; redflags = None; no_tc = None; + no_coercion = None; algunivs = None; } let make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs - ~redflags ~no_tc ~algunivs = + ~redflags ~no_tc ~no_coercion ~algunivs = let user_warns = Some UserWarn.{ depr; warn } in { hoas_holes; local; user_warns; primitive; failsafe; ppwidth; pp; pplevel; using; inline; uinstance; universe_decl; reversible; keepunivs; - redflags; no_tc; algunivs; } + redflags; no_tc; no_coercion; algunivs; } let make_warn = UserWarn.make_warn type 'a coq_context = { @@ -1314,12 +1316,13 @@ let get_options ~depth hyps state = let universe_decl = get_universe_decl () in let reversible = get_bool_option "coq:reversible" in let no_tc = get_bool_option "coq:no_tc" in + let no_coercion = get_bool_option "coq:no_coercion" in let keepunivs = get_bool_option "coq:keepunivs" in let redflags = get_redflags_option () in let algunivs = get_bool_option "coq:keepalgunivs" in make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs - ~redflags ~no_tc ~algunivs + ~redflags ~no_tc ~no_coercion ~algunivs let mk_coq_context ~options state = let env = get_global_env state in let section = section_ids env in diff --git a/src/rocq_elpi_HOAS.mli b/src/rocq_elpi_HOAS.mli index 1cbdf4701..ed9233dc6 100644 --- a/src/rocq_elpi_HOAS.mli +++ b/src/rocq_elpi_HOAS.mli @@ -48,6 +48,7 @@ type options = { keepunivs : bool option; redflags : RedFlags.reds option; no_tc: bool option; + no_coercion: bool option; algunivs : bool option; } diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 839382876..6a4f43301 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -3627,7 +3627,9 @@ Supported attributes: - @keepunivs! (default false, do not disregard universe levels) - @no-tc! (default false, do not infer typeclasses) |}))))), (fun gt ety _ diag ~depth proof_context _ state -> - let flags = if proof_context.options.no_tc = Some true then {(Pretyping.default_inference_flags false) with use_typeclasses = NoUseTC} else Pretyping.default_inference_flags false in + let flags = Pretyping.default_inference_flags false in + let flags = if proof_context.options.no_tc = Some true then {flags with use_typeclasses = NoUseTC} else flags in + let flags = if proof_context.options.no_coercion = Some true then {flags with use_coercions = false} else flags in try let sigma = get_sigma state in let ety_given, expected_type = @@ -3674,7 +3676,9 @@ Supported attributes: (fun gt es _ diag ~depth proof_context _ state -> try let sigma = get_sigma state in - let flags = if proof_context.options.no_tc = Some true then {(Pretyping.default_inference_flags false) with use_typeclasses = NoUseTC} else Pretyping.default_inference_flags false in + let flags = Pretyping.default_inference_flags false in + let flags = if proof_context.options.no_tc = Some true then {flags with use_typeclasses = NoUseTC} else flags in + let flags = if proof_context.options.no_coercion = Some true then {flags with use_coercions = false} else flags in let expected_type = Pretyping.IsType in let sigma = Evd.push_future_goals sigma in let sigma, uj_val, uj_type = From 914f603bf2161870e2b29d06e617d36e007e9366 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Wed, 24 Sep 2025 17:15:26 +0200 Subject: [PATCH 03/12] Add support for syntactic command arguments --- elpi/coq-arg-HOAS.elpi | 2 + src/rocq_elpi_arg_HOAS.ml | 333 ++++++++++++++++++++++++------ src/rocq_elpi_arg_HOAS.mli | 87 +++++++- src/rocq_elpi_arg_syntax.mlg | 16 +- src/rocq_elpi_builtins.ml | 121 +++++++++++ src/rocq_elpi_builtins_synterp.ml | 3 +- src/rocq_elpi_programs.ml | 12 +- src/rocq_elpi_programs.mli | 4 +- src/rocq_elpi_utils.mli | 7 + src/rocq_elpi_vernacular.ml | 22 +- src/rocq_elpi_vernacular.mli | 6 +- tests/test_API_elaborate.v | 194 +++++++++++++++-- 12 files changed, 697 insertions(+), 110 deletions(-) diff --git a/elpi/coq-arg-HOAS.elpi b/elpi/coq-arg-HOAS.elpi index 25f96d79b..65a59b0ea 100644 --- a/elpi/coq-arg-HOAS.elpi +++ b/elpi/coq-arg-HOAS.elpi @@ -54,6 +54,8 @@ external symbol str : string -> argument. % Eg. x "y" z.w. or any Coq keywo external symbol trm : term -> argument. % Eg. (t). external symbol open-trm : int -> term -> argument. +external symbol syntax.arg : syntax.argument -> argument. + % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context] % take precedence over the [str] argument above (when not "quoted"). % diff --git a/src/rocq_elpi_arg_HOAS.ml b/src/rocq_elpi_arg_HOAS.ml index 53272ed61..f64293064 100644 --- a/src/rocq_elpi_arg_HOAS.ml +++ b/src/rocq_elpi_arg_HOAS.ml @@ -4,7 +4,12 @@ module API = Elpi.API module E = API.RawData +module CC = API.ContextualConversion +module C = API.Conversion +module D = API.OpaqueData module CD = API.RawOpaqueData +module Alg = API.AlgebraicData +module P = API.RawPp open Rocq_elpi_utils open Rocq_elpi_HOAS @@ -59,20 +64,39 @@ let drop_relevance (a,_,c,d,e) = (a,c,d,e) let intern_global_context_synterp (ctx : Constrexpr.local_binder_expr list) : Glob_term.glob_decl list = CList.concat_map intern_one ctx |> List.rev +module GS = struct + type 'a t = { + gs : Genintern.glob_sign; + vl : 'a + } + let get {vl;_} = vl + let mk gs vl = {gs; vl} +end + +module IS = struct + type 'a t = { + is : Geninterp.interp_sign; + gs : Genintern.glob_sign; + vl : 'a + } + let get {vl;_} = vl + let mk is gs vl = {is; gs; vl} + let of_gs is GS.{gs; vl} = {is; gs; vl} +end + module Cmd = struct type raw_term = Constrexpr.constr_expr -type glob_term = Genintern.glob_constr_and_expr -type top_term = - Ltac_plugin.Tacinterp.interp_sign * Genintern.glob_constr_and_expr +type glob_term = raw_term GS.t +type top_term = raw_term IS.t type raw_record_decl = Vernacentries.Preprocessed_Mind_decl.record -type glob_record_decl = Genintern.glob_sign * raw_record_decl -type top_record_decl = Geninterp.interp_sign * glob_record_decl +type glob_record_decl = raw_record_decl GS.t +type top_record_decl = raw_record_decl IS.t type raw_indt_decl = Vernacentries.Preprocessed_Mind_decl.inductive -type glob_indt_decl = Genintern.glob_sign * raw_indt_decl -type top_indt_decl = Geninterp.interp_sign * glob_indt_decl +type glob_indt_decl = raw_indt_decl GS.t +type top_indt_decl = raw_indt_decl IS.t type univpoly = Mono | Poly | CumulPoly @@ -147,8 +171,8 @@ type glob_constant_decl_elpi = { typ : Glob_term.glob_constr; body : Glob_term.glob_constr option; } -type glob_constant_decl = Genintern.glob_sign * raw_constant_decl -type top_constant_decl = Geninterp.interp_sign * glob_constant_decl +type glob_constant_decl = raw_constant_decl GS.t +type top_constant_decl = raw_constant_decl IS.t let pr_raw_constant_decl _ _ _ = Pp.str "TODO: pr_raw_constant_decl" let pr_glob_constant_decl _ _ _ = Pp.str "TODO: pr_glob_constant_decl" @@ -156,8 +180,8 @@ let pr_top_constant_decl _ _ _ = Pp.str "TODO: pr_top_constant_decl" type raw_context_decl = Constrexpr.local_binder_expr list -type glob_context_decl = Genintern.glob_sign * raw_context_decl -type top_context_decl = Geninterp.interp_sign * glob_context_decl +type glob_context_decl = raw_context_decl GS.t +type top_context_decl = raw_context_decl IS.t let pr_raw_context_decl _ _ _ = Pp.str "TODO: pr_raw_context_decl" let pr_glob_context_decl _ _ _ = Pp.str "TODO: pr_glob_context_decl" @@ -172,10 +196,24 @@ type ('a,'b,'c,'d,'e) t = | ConstantDecl : 'd -> ('a,'b,'c,'d,'e) t | Context : 'e -> ('a,'b,'c,'d,'e) t +let map (type a b c d e v w x y z) : + (a -> v) -> (b -> w) -> (c -> x) -> (d -> y) -> (e -> z) -> + (a,b,c,d,e) t -> (v,w,x,y,z) t = fun f g h i j -> function + | Int _ as x -> x + | String _ as x -> x + | Term s -> Term (f s) + | RecordDecl s -> RecordDecl (g s) + | IndtDecl s -> IndtDecl (h s) + | ConstantDecl s -> ConstantDecl (i s) + | Context c -> Context (j c) + type raw = (raw_term, raw_record_decl, raw_indt_decl, raw_constant_decl, raw_context_decl) t type glob = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl, glob_context_decl) t type top = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl) t +let raw_of_glob : glob -> raw = map GS.get GS.get GS.get GS.get GS.get +let raw_of_top : top -> raw = map IS.get IS.get IS.get IS.get IS.get + let pr_arg f g h i j x = match x with | Int n -> Pp.int n | String s -> Pp.qstring s @@ -200,21 +238,11 @@ let pr_glob_constr_and_expr env sigma = function Printer.pr_glob_constr_env env sigma c let pp_glob env sigma : glob -> Pp.t = - pr_arg - (pr_glob_constr_and_expr env sigma) - (pr_glob_record_decl env sigma) - (pr_glob_indt_decl env sigma) - (pr_glob_constant_decl env sigma) - (pr_glob_context_decl env sigma) - + fun g -> g |> raw_of_glob |> pp_raw env sigma + let pp_top env sigma : top -> Pp.t = - pr_arg - (fun (_,x) -> pr_glob_constr_and_expr env sigma x) - (pr_top_record_decl env sigma) - (pr_top_indt_decl env sigma) - (pr_top_constant_decl env sigma) - (pr_top_context_decl env sigma) - + fun g -> g |> raw_of_top |> pp_raw env sigma + let sep_last_qualid = function | [] -> "_", [] | l -> CList.sep_last l @@ -326,7 +354,7 @@ let of_coq_record_definition id = univpoly = univpoly_of ~poly ~cumulative } [%%endif] -let intern_record_decl glob_sign (it : raw_record_decl) = glob_sign, it +let intern_record_decl glob_sign (it : raw_record_decl) = it let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,None,y,z) let dest_entry (_,_,_,_,x) = x @@ -477,7 +505,7 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform List.map (fun (id,ty) -> id.CAst.v, intern_global_constr_ty ~expty:(Pretyping.OfType indty) glob_sign_params_self ~intern_env ty) constructors in { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly } -let intern_indt_decl glob_sign (it : raw_indt_decl) = glob_sign, it +let intern_indt_decl glob_sign (it : raw_indt_decl) = it let expr_hole = CAst.make @@ Constrexpr.CHole(None) @@ -488,7 +516,7 @@ let raw_context_decl_to_glob_synterp fields = let raw_context_decl_to_glob glob_sign fields = let _intern_env, fields = intern_global_context ~intern_env:Constrintern.empty_internalization_env glob_sign fields in List.rev fields -let intern_context_decl glob_sign (it : raw_context_decl) = glob_sign, it +let intern_context_decl glob_sign (it : raw_context_decl) = it let raw_decl_name_to_glob name = let name, space = sep_last_qualid name in @@ -570,28 +598,15 @@ let raw_constant_decl_to_glob glob_sign ({ name; atts; udecl; typ = (params,typ) let state = merge_universe_context state ustate in state, NonCumulative ((univdecl_instance,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) in state, { name = raw_decl_name_to_glob name; params; typ; udecl; body } -let intern_constant_decl glob_sign (it : raw_constant_decl) = glob_sign, it +let intern_constant_decl glob_sign (it : raw_constant_decl) = it -let glob glob_sign : raw -> glob = function - | Int _ as x -> x - | String _ as x -> x - | Term t -> Term (intern_tactic_constr glob_sign t) - | RecordDecl t -> RecordDecl (intern_record_decl glob_sign t) - | IndtDecl t -> IndtDecl (intern_indt_decl glob_sign t) - | ConstantDecl t -> ConstantDecl (intern_constant_decl glob_sign t) - | Context c -> Context (intern_context_decl glob_sign c) +let glob glob_sign raw = glob_sign, raw +let glob glob_sign : raw -> glob = map (GS.mk glob_sign) (GS.mk glob_sign) (GS.mk glob_sign) (GS.mk glob_sign) (GS.mk glob_sign) let subst _mod_subst _x = CErrors.anomaly Pp.(str "command arguments should not be substituted") -let interp ist env evd : glob -> top = function - | Int _ as x -> x - | String _ as x -> x - | Term t -> Term(ist,t) - | RecordDecl t -> (RecordDecl(ist,t)) - | IndtDecl t -> (IndtDecl(ist,t)) - | ConstantDecl t -> (ConstantDecl(ist,t)) - | Context c -> (Context(ist,c)) +let interp ist env evd : glob -> top = map (IS.of_gs ist) (IS.of_gs ist) (IS.of_gs ist) (IS.of_gs ist) (IS.of_gs ist) end @@ -945,6 +960,15 @@ let tacc = E.Constants.declare_global_symbol "tac" let intc = E.Constants.declare_global_symbol "int" let ctxc = E.Constants.declare_global_symbol "ctx-decl" +(* HACK: We just want to be able to mention this in other places. *) +let arg_type = API.Conversion.{ + ty = TyName "argument"; + pp_doc = (fun fmt _ -> Format.fprintf fmt ""); + pp = (fun fmt _ -> Format.fprintf fmt ""); + embed = (fun ~depth state s -> state, s, []); + readback = (fun ~depth state s -> state, s, []); + } + let my_cast_to_string v = let open Ltac_plugin in try Taccoerce.Value.cast (Genarg.topwit Stdarg.wit_string) v @@ -1191,30 +1215,31 @@ let interp_mutual_inductive ~flags ~env ~uniform ~private_ind ?typing_flags ~ude [%%endif] -let in_elpi_cmd ~loc ~depth ~base ?calldepth coq_ctx state ~raw (x : Cmd.top) = +let in_elpi_cmd_interpreted ~loc ~depth ~base ?calldepth ~kind coq_ctx state (x : Cmd.top) = let open Cmd in let hyps = [] in - match x with - | RecordDecl (_ist,(glob_sign,raw_rdecl)) when raw -> + match x, kind with + | _, Syntactic -> assert false + | RecordDecl IS.{is=_ist; gs=glob_sign; vl=raw_rdecl}, Unelaborated -> let raw_rdecl = of_coq_record_definition raw_rdecl in let glob_rdecl = raw_record_decl_to_glob glob_sign raw_rdecl in let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in let state, t = grecord2lp ~loc ~base ~depth state glob_rdecl in state, t, [] - | RecordDecl (_ist,(glob_sign,raw_rdecl)) -> + | RecordDecl IS.{is=_ist; gs=glob_sign; vl=raw_rdecl}, Elaborated -> let flags, udecl, primitive_proj, kind, records = dest_rdecl raw_rdecl in let flags = handle_template_polymorphism flags in (* Definitional type classes cannot be interpreted using this function (why?) *) let kind = if kind = Vernacexpr.Class true then Vernacexpr.Class false else kind in let e = interp_structure ~flags udecl kind ~primitive_proj records in record_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e - | IndtDecl (_ist,(glob_sign,raw_indt)) when raw -> + | IndtDecl IS.{is=_ist; gs=glob_sign; vl=raw_indt}, Unelaborated -> let raw_indt = of_coq_inductive_definition raw_indt in let glob_indt = raw_indt_decl_to_glob glob_sign raw_indt in let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in let state, t = ginductive2lp ~loc ~depth ~base state glob_indt in state, t, [] - | IndtDecl (_ist,(glob_sign,raw_indt)) -> + | IndtDecl IS.{is=_ist; gs=glob_sign; vl=raw_indt}, Elaborated -> let flags, udecl, typing_flags, uniform, private_ind, inductives = dest_idecl raw_indt in let flags = handle_template_polymorphism flags in let e = @@ -1224,11 +1249,11 @@ let in_elpi_cmd ~loc ~depth ~base ?calldepth coq_ctx state ~raw (x : Cmd.top) = | _ -> nYI "(HOAS) mutual inductives" in inductive_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e - | ConstantDecl (_ist,(glob_sign,raw_cdecl)) when raw -> + | ConstantDecl IS.{is=_ist; gs=glob_sign; vl=raw_cdecl}, Unelaborated -> let state, glob_cdecl = raw_constant_decl_to_glob glob_sign raw_cdecl state in let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in cdecl2lp ~loc ~depth ~base state glob_cdecl - | ConstantDecl (_ist,(glob_sign,({ name; typ = (bl,_) } as raw_cdecl))) -> + | ConstantDecl IS.{is=_ist; gs=glob_sign; vl=({ name; typ = (bl,_) } as raw_cdecl)}, Elaborated -> let state, udecl, typ, body, gls0 = raw_constant_decl_to_constr ~depth coq_ctx state raw_cdecl in let state, typ, gls1 = constr2lp_closed ~depth ?calldepth coq_ctx E.no_constraints state typ in @@ -1244,25 +1269,215 @@ let in_elpi_cmd ~loc ~depth ~base ?calldepth coq_ctx state ~raw (x : Cmd.top) = let state, ud, gls3 = universe_decl.API.Conversion.embed ~depth state (NonCumul udecl) in state, E.mkApp ucdeclc c [body;typ;ud], gls0 @ gls1 @ gls2 @ gls3 end - | Context (_ist,(glob_sign,raw_ctx)) when raw -> + | Context IS.{is=_ist; gs=glob_sign; vl=raw_ctx}, Unelaborated -> let glob_ctx = raw_context_decl_to_glob glob_sign raw_ctx in let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in let state, t = do_context_glob ~loc glob_ctx ~depth ~base state in state, E.mkApp ctxc t [], [] - | Context (_ist,(glob_sign,raw_ctx)) -> + | Context IS.{is=_ist; gs=glob_sign; vl=raw_ctx}, Elaborated -> let sigma, ctx = ComAssumption.interp_context coq_ctx.env (get_sigma state) raw_ctx in let state, gls0 = set_current_sigma ~depth state sigma in let state, t, gls1 = do_context_constr (upcast coq_ctx) E.no_constraints ctx ~depth state in state, E.mkApp ctxc t [], gls0 @ gls1 - | Int x -> in_elpi_int_arg ~depth state x - | String x -> in_elpi_string_arg ~depth state x - | Term (ist,glob_or_expr) when raw -> + | Int x, _ -> in_elpi_int_arg ~depth state x + | String x, _ -> in_elpi_string_arg ~depth state x + | Term IS.{is=ist; gs=glob_sign; vl=constexpr}, Unelaborated -> let sigma = get_sigma state in + let glob_or_expr = intern_tactic_constr glob_sign constexpr in in_elpi_term_arg ~loc ~depth ~base state coq_ctx hyps sigma ist glob_or_expr - | Term (ist,glob_or_expr) -> + | Term IS.{is=ist; gs=glob_sign; vl=constexpr}, Elaborated -> let sigma = get_sigma state in + let glob_or_expr = intern_tactic_constr glob_sign constexpr in in_elpi_elab_term_arg ~depth ?calldepth state coq_ctx hyps sigma ist glob_or_expr + +module Syntactic = struct + open Cmd + + module Tag = struct + (* The Non-trivial syntactic types do not have comparison functions. We + augment the data with a tag to use for sorting. + *) + type 'a t = { + is : Geninterp.interp_sign; + gs : Genintern.glob_sign; + vl : 'a; + tag : int; + } + let compare_tag {tag=n1;_} {tag=n2;_} = Int.compare n1 n2 + + let counter = ref 0 + + let fresh IS.{is;gs;vl} = + incr counter; + let tag = !counter in + {is;gs;vl;tag} + + let drop_tag (type a) : a t -> a IS.t = fun {is;gs;vl;tag=_} -> IS.{is;gs;vl} + end + + type res_term = raw_term Tag.t + type res_record_decl = raw_record_decl Tag.t + type res_indt_decl = raw_indt_decl Tag.t + type res_constant_decl = raw_constant_decl Tag.t + type res_context_decl = raw_context_decl Tag.t + type res = (res_term, res_record_decl, res_indt_decl, res_constant_decl, res_context_decl) t + + let pp_res env sigma : res -> Pp.t = fun r -> + Cmd.map Tag.drop_tag Tag.drop_tag Tag.drop_tag Tag.drop_tag Tag.drop_tag r |> pp_top env sigma + + (* We need an order on syntactic terms but Rocq offers nothing of the sort. So + we equip each term with a unique integer to decide what to return when the + glob constrs are not equal. *) + let trm, trm_type = CD.declare { + name = "syntax.trm"; + doc = "Unprocessed term argument"; + pp = (fun fmt (t : res_term) -> + Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.Term t)))); + compare = (fun (Tag.{tag=n1; vl=ce1} as t1) (Tag.{tag=n2; vl=ce2} as t2) -> + if Constrexpr_ops.constr_expr_eq ce1 ce2 + then 0 + else Tag.compare_tag t1 t2 + ); + hash = (fun _ -> 0); + hconsed = false; + constants = []; + } + + let constant_decl, constant_decl_type = CD.declare { + name = "syntax.const-decl"; + doc = "Unprocessed term argument"; + pp = (fun fmt (t : res_constant_decl) -> + Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.ConstantDecl t)))); + compare = Tag.compare_tag; (* we do not even try to compare these based on contents *) + hash = (fun _ -> 0); + hconsed = false; + constants = []; + } + + let indt_decl, indt_decl_type = CD.declare { + name = "syntax.indt-decl"; + doc = "Unprocessed term argument"; + pp = (fun fmt (t : res_indt_decl) -> + Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.IndtDecl t)))); + compare = Tag.compare_tag; (* we do not even try to compare these based on contents *) + hash = (fun _ -> 0); + hconsed = false; + constants = []; + } + + let record_decl, record_decl_type = CD.declare { + name = "syntax.record-decl"; + doc = "Unprocessed term argument"; + pp = (fun fmt (t : res_record_decl) -> + Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.RecordDecl t)))); + compare = Tag.compare_tag; (* we do not even try to compare these based on contents *) + hash = (fun _ -> 0); + hconsed = false; + constants = []; + } + + let context, context_type = CD.declare { + name = "syntax.context-decl"; + doc = "Unprocessed term argument"; + pp = (fun fmt (t : res_context_decl) -> + Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.Context t)))); + compare = Tag.compare_tag; (* we do not even try to compare these based on contents *) + hash = (fun _ -> 0); + hconsed = false; + constants = []; + } + + let arg_type = Alg.declare { + ty = TyName "syntax.argument"; + doc = "Unprocessed command argument"; + pp = (fun fmt t -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty t))); + constructors = [ + K("syntax.str", "", A(API.BuiltInData.string, N), + B (fun s -> Cmd.String s), + M (fun ~ok ~ko -> function Cmd.String s -> ok s | _ -> ko ()) + ); + K("syntax.int", "", A(API.BuiltInData.int, N), + B (fun s -> Cmd.Int s), + M (fun ~ok ~ko -> function Cmd.Int s -> ok s | _ -> ko ()) + ); + K("syntax.trm", "", A(trm_type, N), + B (fun s -> Cmd.Term s), + M (fun ~ok ~ko -> function Cmd.Term s -> ok s | _ -> ko ()) + ); + K("syntax.const-decl", "", A(constant_decl_type, N), + B (fun s -> Cmd.ConstantDecl s), + M (fun ~ok ~ko -> function Cmd.ConstantDecl s -> ok s | _ -> ko ()) + ); + K("syntax.indt-decl", "", A(indt_decl_type, N), + B (fun s -> Cmd.IndtDecl s), + M (fun ~ok ~ko -> function Cmd.IndtDecl s -> ok s | _ -> ko ()) + ); + K("syntax.record-decl", "", A(record_decl_type, N), + B (fun s -> Cmd.RecordDecl s), + M (fun ~ok ~ko -> function Cmd.RecordDecl s -> ok s | _ -> ko ()) + ); + K("syntax.ctx-decl", "", A(context_type, N), + B (fun s -> Cmd.Context s), + M (fun ~ok ~ko -> function Cmd.Context s -> ok s | _ -> ko ()) + ); + ]; + } |> CC.(!<) + + let as_normal_arg = E.Constants.declare_global_symbol "syntax.arg" + + let delimiter_depth = API.OpaqueData.declare { + name = "delimiter_depth"; + doc = "Syntax scope delimiter depth"; + pp = Constrexpr.(fun fmt -> function + | DelimOnlyTmpScope -> Format.fprintf fmt "DelimOnlyTmpScope" + | DelimUnboundedScope -> Format.fprintf fmt "DelimUnboundedScope"); + compare = Stdlib.compare; + hash = Hashtbl.hash; + hconsed = true; + constants = [ + ("delimit-only-tmp-scope", DelimOnlyTmpScope); + ("delimit-unbounded-scope", DelimUnboundedScope); + ]; + } + + let ml_data = + let open API.BuiltIn in + [MLData arg_type; + MLData trm_type; + MLData constant_decl_type; + MLData indt_decl_type; + MLData record_decl_type; + MLData context_type; + MLData delimiter_depth; + ] + + let res_of_top : top -> res = + Cmd.map + Tag.fresh + Tag.fresh + Tag.fresh + Tag.fresh + Tag.fresh + + let top_of_res : res -> top = + Cmd.map + Tag.drop_tag + Tag.drop_tag + Tag.drop_tag + Tag.drop_tag + Tag.drop_tag +end + +let in_elpi_cmd ~loc ~depth ~base ?calldepth ~kind coq_ctx state(x : Cmd.top) : API.State.t * E.term * _ = + match kind with + | Syntactic -> + let state, res, extra_goals = + Syntactic.arg_type.embed ~depth state (Syntactic.res_of_top x) + in + state, E.mkApp Syntactic.as_normal_arg res [], extra_goals + | _ -> in_elpi_cmd_interpreted ~loc ~depth ~base ?calldepth ~kind coq_ctx state x + type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t | CLtac1 of Geninterp.Val.t let in_coq_arg ~depth proof_context constraints state t = diff --git a/src/rocq_elpi_arg_HOAS.mli b/src/rocq_elpi_arg_HOAS.mli index 5dc033260..96aa13a8d 100644 --- a/src/rocq_elpi_arg_HOAS.mli +++ b/src/rocq_elpi_arg_HOAS.mli @@ -5,24 +5,47 @@ open Elpi.API.RawData open Rocq_elpi_utils +module API = Elpi.API +module CD = Elpi.API.RawOpaqueData + type phase = Interp | Synterp | Both type proof = | Begin of string option (* None = always, Some x only if #[x] present*) | End +module GS : sig + type 'a t = { + gs : Genintern.glob_sign; + vl : 'a + } + val get : 'a t -> 'a + val mk : Genintern.glob_sign -> 'a -> 'a t +end + +module IS : sig + type 'a t = { + is : Geninterp.interp_sign; + gs : Genintern.glob_sign; + vl : 'a + } + val get : 'a t -> 'a + val mk : Geninterp.interp_sign -> Genintern.glob_sign -> 'a -> 'a t + val of_gs : Geninterp.interp_sign -> 'a GS.t -> 'a t +end + module Cmd : sig type raw_term = Constrexpr.constr_expr -type glob_term = Genintern.glob_constr_and_expr -type top_term = Ltac_plugin.Tacinterp.interp_sign * Genintern.glob_constr_and_expr +type glob_term = raw_term GS.t +type top_term = raw_term IS.t type raw_record_decl = Vernacentries.Preprocessed_Mind_decl.record -type glob_record_decl = Genintern.glob_sign * raw_record_decl -type top_record_decl = Geninterp.interp_sign * glob_record_decl +type glob_record_decl = raw_record_decl GS.t +type top_record_decl = raw_record_decl IS.t type raw_indt_decl = Vernacentries.Preprocessed_Mind_decl.inductive -type glob_indt_decl = Genintern.glob_sign * raw_indt_decl -type top_indt_decl = Geninterp.interp_sign * glob_indt_decl +type glob_indt_decl = raw_indt_decl GS.t +type top_indt_decl = raw_indt_decl IS.t type raw_constant_decl = { name : qualified_name; @@ -33,12 +56,12 @@ type raw_constant_decl = { red : Genredexpr.raw_red_expr option; } val pr_raw_constant_decl : Environ.env -> Evd.evar_map -> raw_constant_decl -> Pp.t -type glob_constant_decl = Genintern.glob_sign * raw_constant_decl -type top_constant_decl = Geninterp.interp_sign * glob_constant_decl +type glob_constant_decl = raw_constant_decl GS.t +type top_constant_decl = raw_constant_decl IS.t type raw_context_decl = Constrexpr.local_binder_expr list -type glob_context_decl = Genintern.glob_sign * raw_context_decl -type top_context_decl = Geninterp.interp_sign * glob_context_decl +type glob_context_decl = raw_context_decl GS.t +type top_context_decl = raw_context_decl IS.t type ('a,'b,'c,'d,'e) t = | Int : int -> ('a,'b,'c,'d,'e) t @@ -125,14 +148,56 @@ val in_elpi_tac_econstr : Elpi.API.State.t * term list * Elpi.API.Conversion.extra_goals (* for commands *) +val arg_type : API.Data.term API.Conversion.t +module Syntactic : sig + module Tag : + sig + type 'a t = { + is : Geninterp.interp_sign; + gs : Genintern.glob_sign; + vl : 'a; + tag : int; + } + val compare_tag : 'a t -> 'b t -> int + val counter : int ref + val fresh : 'a IS.t -> 'a t + val drop_tag : 'a t -> 'a IS.t + end + type res_term = Cmd.raw_term Tag.t + type res_record_decl = Cmd.raw_record_decl Tag.t + type res_indt_decl = Cmd.raw_indt_decl Tag.t + type res_constant_decl = Cmd.raw_constant_decl Tag.t + type res_context_decl = Cmd.raw_context_decl Tag.t + type res = + (res_term, res_record_decl, res_indt_decl, res_constant_decl, + res_context_decl) + Cmd.t + val pp_res : Environ.env -> Evd.evar_map -> res -> Pp.t + val trm : res_term CD.cdata + val trm_type : res_term API.Conversion.t + val constant_decl : res_constant_decl CD.cdata + val constant_decl_type : res_constant_decl API.Conversion.t + val indt_decl : res_indt_decl CD.cdata + val indt_decl_type : res_indt_decl API.Conversion.t + val record_decl : res_record_decl CD.cdata + val record_decl_type : res_record_decl API.Conversion.t + val context : res_context_decl CD.cdata + val context_type : res_context_decl API.Conversion.t + val arg_type : res API.Conversion.t + val delimiter_depth : Constrexpr.delimiter_depth API.Conversion.t + val as_normal_arg : API.RawData.constant + val res_of_top : Cmd.top -> res + val top_of_res : res -> Cmd.top + val ml_data : API.BuiltIn.declaration list +end val in_elpi_cmd : loc:Loc.t -> depth:int -> base:Elpi.API.Compile.program -> ?calldepth:int -> + kind:arg_kind -> Rocq_elpi_HOAS.empty Rocq_elpi_HOAS.coq_context -> Elpi.API.State.t -> - raw:bool -> Cmd.top -> Elpi.API.State.t * term * Elpi.API.Conversion.extra_goals val in_elpi_cmd_synterp : diff --git a/src/rocq_elpi_arg_syntax.mlg b/src/rocq_elpi_arg_syntax.mlg index c53267780..8b4bede0b 100644 --- a/src/rocq_elpi_arg_syntax.mlg +++ b/src/rocq_elpi_arg_syntax.mlg @@ -195,7 +195,21 @@ let skip_and_synterp_attributes = Attributes.Notations.(skip_attribute ++ synter let scope_and_skip_and_synterp_attributes = Attributes.Notations.(scope_attribute ++ skip_attribute ++ synterp_attribute) let raw_args_attributes = - Attributes.(qualify_attribute "arguments" (bool_attribute ~name:"raw")) + Attributes.qualify_attribute "arguments" + (Attributes.attribute_of_list + ["elaborated", (fun ?loc old -> function + | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Elaborated + | _ -> CErrors.user_err ?loc Pp.(str "Argument \"elaborated\" does not expect a value")); + "unelaborated", (fun ?loc old -> function + | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Unelaborated + | _ -> CErrors.user_err ?loc Pp.(str "Argument \"unelaborated\" does not expect a value")); + "raw", (fun ?loc old -> function + | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Unelaborated + | _ -> CErrors.user_err ?loc Pp.(str "Argument \"raw\" does not expect a value")); + "syntactic", (fun ?loc old -> function + | VernacFlagEmpty -> U.arg_kind_merge ?loc old U.Syntactic + | _ -> CErrors.user_err ?loc Pp.(str "Argument \"syntactic\" does not expect a value")); + ]) let validate_attributes a flags = let extra, raw_args = Attributes.parse_with_extra a flags in diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 6a4f43301..47f6e1793 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -27,6 +27,7 @@ open Names open Rocq_elpi_utils open Rocq_elpi_HOAS +open Rocq_elpi_arg_HOAS let string_of_ppcmds options pp = let b = Buffer.create 512 in @@ -252,6 +253,27 @@ let term_skeleton = { embed = (fun ~depth _ _ _ _ -> assert false); } +let type_constraint = + API.AlgebraicData.declare { + ty = TyName "type-constraint"; + doc = "The expected type for elaborating syntactic terms"; + pp = (fun fmt _ -> Format.fprintf fmt ""); + constructors = Pretyping.[ + K("without-type-constraint", "Pretype without type constraint", N, + B (WithoutTypeConstraint), + M (fun ~ok ~ko -> function WithoutTypeConstraint -> ok | _ -> ko ()) + ); + K("of-type", "Pretype with a specific expected type", CA(term, N), + B (fun t -> OfType t), + M (fun ~ok ~ko -> function OfType t -> ok t | _ -> ko ()) + ); + K("is-type", "Pretype as a type", N, + B (IsType), + M (fun ~ok ~ko -> function IsType -> ok | _ -> ko ()) + ); + ]; + } + let sealed_goal = { Conv.ty = Conv.TyName "sealed-goal"; pp_doc = (fun fmt () -> ()); @@ -4390,5 +4412,104 @@ Supported attributes: DocAbove) ] + @ Syntactic.ml_data @ + [MLDataC(type_constraint); + MLCode(Pred("syntax.default-elab", + In(Syntactic.arg_type, "SyntaxArg", + Out(Rocq_elpi_arg_HOAS.arg_type, "Arg", + InOut(B.ioarg B.diagnostic, "Diagnostic", + Full(global, "Elaborates the syntactic argument with the settings of #[arguments(elaborated)]")))), + fun sarg _ diag ~depth coq_ctx _csts state -> + let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in + let base = Option.get (State.get base state) in + try + let state, res, extra_goals = + Syntactic.top_of_res sarg |> + Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base ~kind:Elaborated coq_ctx state + in + state, (!: res +! B.mkOK), extra_goals + with e -> + diag_error_lazy diag @@ fun () -> + let error = + string_of_ppcmds coq_ctx.options @@ + try CErrors.print_no_report e with | _ -> raise No_clause + in + state, ?: None +! B.mkERROR error, [] + ), + DocAbove); + MLCode(Pred("syntax.default-unelab", + In(Syntactic.arg_type, "SyntaxArg", + Out(Rocq_elpi_arg_HOAS.arg_type, "Arg", + InOut(B.ioarg B.diagnostic, "Diagnostic", + Full(global, "Elaborates the syntactic argument with the settings of #[arguments(unelaborated)]")))), + fun sarg _ diag ~depth coq_ctx _csts state -> + let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in + let base = Option.get (State.get base state) in + try + let state, res, extra_goals = + Syntactic.top_of_res sarg |> + Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base ~kind:Unelaborated coq_ctx state + in + state, (!: res +! B.mkOK), extra_goals + with e -> + diag_error_lazy diag @@ fun () -> + let error = + string_of_ppcmds coq_ctx.options @@ + try CErrors.print_no_report e with | _ -> raise No_clause + in + state, ?: None +! B.mkERROR error, [] + ), + DocAbove); + MLCode(Pred("syntax.push-scope", + In(Syntactic.trm_type, "SyntaxTerm", + In(Syntactic.delimiter_depth, "DelimiterDepth", + In(B.string, "ScopeName", + Out(Syntactic.trm_type, "ScopedSyntaxTerm", + Full(global, "Pushes the scope ScopeName on top of SyntaxTerm."))))), + fun t delim_depth scope _ ~depth coq_context _csts state -> + let open Syntactic in + let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in + let Tag.{vl; _} = t in + let vl = CAst.make ~loc (Constrexpr.CDelimiters (delim_depth, scope, vl)) in + let ot = Tag.{t with vl} in + state, (!: ot), [] + ), + DocAbove); + MLCode(Pred("syntax.elaborate", + In(Syntactic.trm_type, "SyntaxTerm", + CIn(type_constraint, "TypeConstraint", + COut(term, "Term", + InOut(B.ioarg B.diagnostic, "Diagnostic", + Full(proof_context, "Elaborates SyntaxTerm using TypeConstraint. Respects @no-tc! and @no-coercion!"))))), + fun t expected_type _ diag ~depth coq_ctx csts state -> + let open Syntactic in + let Tag.{is;gs;vl} = t in + let vl = Ltac_plugin.Tacintern.intern_constr gs vl in + let sigma = get_sigma state in + let flags = + let open Pretyping in + let flags = all_no_fail_flags in + let options = coq_ctx.options in + let use_typeclasses = if Option.default false options.no_tc then NoUseTC else UseTC in + let use_coercions = not @@ Option.default false options.no_coercion in + { flags with use_typeclasses; use_coercions } + in + try + let sigma, vl = + Ltac_plugin.Tacinterp.interp_open_constr ~flags ~expected_type is coq_ctx.env sigma vl + in + let state, extra_goals = set_current_sigma ~depth state sigma in + state, (!: vl +! B.mkOK), extra_goals + with e -> + diag_error_lazy diag @@ fun () -> + let error = + string_of_ppcmds coq_ctx.options @@ + try CErrors.print_no_report e with | _ -> raise No_clause + in + state, ?: None +! B.mkERROR error, [] + ), + DocAbove); + ] + ;; diff --git a/src/rocq_elpi_builtins_synterp.ml b/src/rocq_elpi_builtins_synterp.ml index 0f8366bc6..68f1e29a6 100644 --- a/src/rocq_elpi_builtins_synterp.ml +++ b/src/rocq_elpi_builtins_synterp.ml @@ -19,6 +19,7 @@ open Names open Rocq_elpi_utils open Rocq_elpi_HOAS +open Rocq_elpi_arg_HOAS let prop = { B.any with Conv.ty = Conv.TyName "prop" } @@ -1229,7 +1230,7 @@ Supported attributes: ] @ SynterpAction.get_parsing_actions_synterp @ [ MLData attribute_value; MLData attribute; - ] + ] @ Syntactic.ml_data let synterp_api_doc = ". bla bla" diff --git a/src/rocq_elpi_programs.ml b/src/rocq_elpi_programs.ml index 0e10f9f6f..e761f8ea8 100644 --- a/src/rocq_elpi_programs.ml +++ b/src/rocq_elpi_programs.ml @@ -163,7 +163,7 @@ type db = { units : Names.KNset.t; } -type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool } +type nature = Command of { args : arg_kind } | Tactic | Program of { args : arg_kind } type program = { sources_rev : qualified_name Code.t; @@ -242,7 +242,7 @@ module type Programs = sig val db_inspect : qualified_name -> int val get_and_compile_existing_db : loc:Loc.t -> qualified_name -> EC.program - val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (EC.program * bool) option + val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (EC.program * arg_kind) option end @@ -804,7 +804,7 @@ let compile ~loc src = in compile_code src -let get_and_compile ~loc ?even_if_empty name : (EC.program * bool) option = +let get_and_compile ~loc ?even_if_empty name : (EC.program * arg_kind) option = let t = Unix.gettimeofday () in let res = code ?even_if_empty name |> Option.map (fun src -> (* Format.eprintf "compile %a = %a" pp_qualified_name name (Code.pp Chunk.pp) src; *) @@ -815,9 +815,9 @@ let get_and_compile ~loc ?even_if_empty name : (EC.program * bool) option = let prog = recache_code 0 old_hash new_hash prog src in let raw_args = match get_nature name with - | Command { raw_args } -> raw_args - | Program { raw_args } -> raw_args - | Tactic -> true in + | Command { args } -> args + | Program { args } -> args + | Tactic -> Elaborated in (prog, raw_args)) in Rocq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: get_and_compile %1.4f" (Unix.gettimeofday () -. t)))); res diff --git a/src/rocq_elpi_programs.mli b/src/rocq_elpi_programs.mli index 3b6382e71..49cf0511c 100644 --- a/src/rocq_elpi_programs.mli +++ b/src/rocq_elpi_programs.mli @@ -24,7 +24,7 @@ and src_db_header = { dast : cunit; } -type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool } +type nature = Command of { args : arg_kind } | Tactic | Program of { args : arg_kind } module Chunk : sig @@ -120,7 +120,7 @@ module type Programs = sig val db_inspect : qualified_name -> int val get_and_compile_existing_db : loc:Loc.t -> qualified_name -> Compile.program - val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (Compile.program * bool) option + val get_and_compile : loc:Loc.t -> ?even_if_empty:bool -> qualified_name -> (Compile.program * arg_kind) option end diff --git a/src/rocq_elpi_utils.mli b/src/rocq_elpi_utils.mli index 1eb51536b..103d5929a 100644 --- a/src/rocq_elpi_utils.mli +++ b/src/rocq_elpi_utils.mli @@ -90,6 +90,13 @@ val gr2path: Names.GlobRef.t -> string list val eta_contract : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t +(* Command argument specifiers *) +type arg_kind = + | Elaborated + | Unelaborated + | Syntactic +val arg_kind_merge : ?loc:Loc.t -> arg_kind option -> arg_kind -> arg_kind + (* Diagnostics *) val diag_error_lazy : ?on_ok:(unit -> 'a) -> (* defaults to [raise No_clause] *) Elpi.Builtin.diagnostic Elpi.API.BuiltInPredicate.ioarg -> diff --git a/src/rocq_elpi_vernacular.ml b/src/rocq_elpi_vernacular.ml index f2d9b756c..b620fa8a8 100644 --- a/src/rocq_elpi_vernacular.ml +++ b/src/rocq_elpi_vernacular.ml @@ -399,10 +399,10 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x) let print ~atts ~loc ~name ~args output = skip ~ph:atts (print ~loc ~name ~args) output - let create_command ~atts:(raw_args) ~loc n = - let raw_args = Option.default false raw_args in + let create_command ~atts:(args) ~loc n = + let args = Option.default Elaborated args in let _ = P.ensure_initialized () in - P.declare_program n (Command { raw_args }); + P.declare_program n (Command { args }); P.init_program n ~loc [P.command_init()]; set_current_program (snd n) @@ -412,10 +412,10 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x) if P.stage = Summary.Stage.Interp then P.init_program n ~loc [P.command_init();P.tactic_init ()]; set_current_program (snd n) - let create_program ~atts:(raw_args) ~loc n ~init:(sloc,s) = - let raw_args = Option.default false raw_args in + let create_program ~atts:(args) ~loc n ~init:(sloc,s) = + let args = Option.default Elaborated args in let elpi = P.ensure_initialized () in - P.declare_program n (Program { raw_args }); + P.declare_program n (Program { args }); if P.stage = Summary.Stage.Interp then begin let unit = P.unit_from_string ~elpi ~base:(EC.empty_base ~elpi) ~loc sloc s in let init = EmbeddedString { sast = unit} in @@ -454,7 +454,7 @@ end module type Common = sig val get_and_compile : - loc:Loc.t -> qualified_name -> (Elpi.API.Compile.program * bool) option + loc:Loc.t -> qualified_name -> (Elpi.API.Compile.program * arg_kind) option val run : loc:Loc.t -> Elpi.API.Compile.program -> query -> @@ -475,8 +475,8 @@ module type Common = sig val bound_steps : atts:phase option -> int -> unit val print : atts:phase option -> loc:Loc.t -> name:qualified_name -> args:string list -> string -> unit - val create_program : atts:bool option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit - val create_command : atts:bool option -> loc:Loc.t -> program_name -> unit + val create_program : atts:arg_kind option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit + val create_command : atts:arg_kind option -> loc:Loc.t -> program_name -> unit val create_tactic : loc:Loc.t -> program_name -> unit val create_db : atts:phase option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit val create_file : atts:phase option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit @@ -538,7 +538,7 @@ module Interp = struct strbrk "The command lacks code for the synterp phase. In order to add code to this phase use '#[synterp] Elpi Accumulate'. See also https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_command.html#parsing-and-execution" let run_program ~loc name ~main ~atts ~syndata args more_args = - get_and_compile ~loc name |> Option.map (fun (program, raw_args) -> + get_and_compile ~loc name |> Option.map (fun (program, kind) -> let env = Global.env () in let sigma = Evd.from_env env in let args = args @@ -555,7 +555,7 @@ module Interp = struct let query state = let depth = 0 in let state, args, gls = EU.map_acc - (Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base:program ~raw:raw_args Rocq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state)) + (Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base:program ~kind:kind Rocq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state)) state args in let loc = Rocq_elpi_utils.of_coq_loc loc in diff --git a/src/rocq_elpi_vernacular.mli b/src/rocq_elpi_vernacular.mli index 60ec6bdfc..b77532f39 100644 --- a/src/rocq_elpi_vernacular.mli +++ b/src/rocq_elpi_vernacular.mli @@ -20,7 +20,7 @@ type what = Code | Signature module type Common = sig val get_and_compile : - loc:Loc.t -> qualified_name -> (Elpi.API.Compile.program * bool) option + loc:Loc.t -> qualified_name -> (Elpi.API.Compile.program * arg_kind) option val run : loc:Loc.t -> Elpi.API.Compile.program -> query -> Elpi.API.Execute.outcome @@ -42,8 +42,8 @@ module type Common = sig val bound_steps : atts:phase option -> int -> unit val print : atts:phase option -> loc:Loc.t -> name:qualified_name -> args:string list -> string -> unit - val create_program : atts:bool option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit - val create_command : atts:bool option -> loc:Loc.t -> program_name -> unit + val create_program : atts:arg_kind option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit + val create_command : atts:arg_kind option -> loc:Loc.t -> program_name -> unit val create_tactic : loc:Loc.t -> program_name -> unit val create_db : atts:phase option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit val create_file : atts:phase option -> loc:Loc.t -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v index d4e2fefb8..5c28d497a 100644 --- a/tests/test_API_elaborate.v +++ b/tests/test_API_elaborate.v @@ -21,38 +21,38 @@ Coercion g1 : T1 >-> Funclass. Coercion g3 : T3 >-> Funclass. Coercion h : T2 >-> T3. -Elpi Query lp:{{ +Elpi Query lp:{{/*(*/ std.assert-ok! (coq.elaborate-skeleton {{ fun n (t : T2 n) (x : t) => t 3 }} TY E) "that was easy", coq.env.add-const "elab_1" E TY tt _ -}}. +/*)*/}}. Class foo (n : nat). Definition bar n {f : foo n} := n = n. #[local] Instance xxx : foo 3. Defined. -Elpi Query lp:{{ +Elpi Query lp:{{/*(*/ std.assert-ok! (coq.elaborate-ty-skeleton {{ bar _ }} TY E) "that was easy", coq.env.add-const "elab_2" E (sort TY) tt _ -}}. +/*)*/}}. Structure s := { field : Type; #[canonical=no] op : field -> field; }. Canonical c := {| field := nat; op := (fun x => x) |}. -Elpi Query lp:{{ +Elpi Query lp:{{/*(*/ std.assert-ok! (coq.elaborate-skeleton {{ op _ 3 }} TY E) "that was easy", coq.env.add-const "elab_3" E TY tt _ -}}. +/*)*/}}. (* #[arguments(raw)] *) Elpi Command test.API2. -Elpi Accumulate lp:{{ +Elpi Accumulate lp:{{/*(*/ main [indt-decl D] :- coq.say "raw:" D, std.assert-ok! (coq.elaborate-indt-decl-skeleton D D1) "illtyped", coq.say "elab1:" D1, @@ -65,7 +65,7 @@ Elpi Accumulate lp:{{ std.assert-ok! (coq.elaborate-skeleton BO TY1 BO1) "illtyped", coq.env.add-const N BO1 TY1 @transparent! _, ]. -}}. +/*)*/}}. Elpi test.API2 Inductive ind1 (A : T1) | (B : Type) := @@ -145,43 +145,205 @@ Check (forall x : ind3, x -> Prop). Elpi test.API2 Definition def1 A := fun x : A => x. -Elpi Query lp:{{ +Elpi Query lp:{{/*(*/ std.assert-ok! (coq.elaborate-skeleton {{ op lib:elpi.hole 3 }} TY E) "that was easy 2", coq.env.add-const "elab_4" E TY tt _ -}}. +/*)*/}}. Elpi Tactic test. -Elpi Accumulate lp:{{ +Elpi Accumulate lp:{{/*(*/ solve _ _ :- coq.term->string X S, X = global (indc Y), coq.say S. -}}. +/*)*/}}. Goal True. Fail elpi test. Abort. Elpi Tactic test2. -Elpi Accumulate lp:{{ +Elpi Accumulate lp:{{/*(*/ solve _ _ :- coq.term->string (global (indc Y)) S, coq.say S. -}}. +/*)*/}}. Goal True. elpi test2. Abort. #[arguments(raw)] Elpi Command detype. -Elpi Accumulate lp:{{ +Elpi Accumulate lp:{{/*(*/ main [upoly-const-decl _ _ (parameter _ _ (sort (typ U)) _ as A) (upoly-decl [UL] _ _ _)] :- std.assert! (coq.univ.variable U UL) "wtf", (@keepunivs! => std.assert-ok! (coq.elaborate-arity-skeleton A _ (parameter _ _ (sort (typ V)) _)) "wtf"), std.assert! (U = V) "elaboration refreshes", coq.say U V. -}}. +/*)*/}}. Elpi detype #[universes(polymorphic)] Definition f@{u|Set < u} (x : Type@{u}) := x. +(** Parser tests *) +Succeed #[arguments(raw)] Elpi Command argtest. +Succeed #[arguments(unelaborated)] Elpi Command argtest. +Succeed #[arguments(elaborated)] Elpi Command argtest. +Succeed #[arguments(syntactic)] Elpi Command argtest. +(* The test below should fail but does not for some reason. + Also, the error message is terribly. See https://github.com/rocq-prover/rocq/issues/17041 *) +#[local] Set Warnings "+unsupported-attributes". +Succeed #[arguments(something_else)] Elpi Command argtest. + +(* Arguments do not allow any specified values, not even booleans *) +Fail #[arguments(raw="test")] Elpi Command detype. +Fail #[arguments(raw=false)] Elpi Command detype. + +(* Syntactic tests *) +#[arguments(syntactic)] Elpi Command syntax_test1. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg (syntax.int 1)]. +/*)*/}}. +Elpi syntax_test1 1. +Fail Elpi syntax_test1 2. + +#[arguments(syntactic)] Elpi Command syntax_test2. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg (syntax.str "test")]. +/*)*/}}. +Elpi syntax_test2 "test". +Fail Elpi syntax_test2 "foo". + +#[arguments(syntactic)] Elpi Command syntax_test3. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg Arg] :- + syntax.default-elab Arg (int 1) ok. +/*)*/}}. +Elpi syntax_test3 1. +Fail Elpi syntax_test3 2. + +#[arguments(syntactic)] Elpi Command syntax_test4. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg Arg] :- + syntax.default-elab Arg (trm {{(1 + 1)}}) ok. +/*)*/}}. +Elpi syntax_test4 (1 + 1). +Fail Elpi syntax_test4 (2 + 1). + + +(* Test evar dependencies *) +#[arguments(elaborated)] Elpi Command evar_deps. +Elpi Accumulate lp:{{/*(*/ + main [trm T1, trm T2] :- + pattern_match T1 {{ 1 + 1 }}, + pattern_match T2 {{ 1 }}. +/*)*/}}. +(* Evars are elaborated/interpreted before they are unified during the execution of [main]. *) +Elpi evar_deps (?[x] + ?x) (?x). +(* Rocq is perhaps a bit too eager to throw away instantiated evars: https://github.com/rocq-prover/rocq/issues/21116 *) +Fail Elpi evar_deps (eq_refl : (?[x] = 1)) (?x). + +#[arguments(syntactic)] Elpi Command syntax_test_evars. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg Arg1, syntax.arg Arg2] :- + syntax.default-elab Arg1 (trm {{ 1 + 1 }}) ok, + syntax.default-elab Arg2 (trm {{(1)}}) ok. +/*)*/}}. +Elpi syntax_test_evars (1 + 1) (1). +Elpi syntax_test_evars (?[x] + 1) (1). +Elpi syntax_test_evars (1 + 1) (?[x]). +(* Our program interpretes and then unifies the evars in the first argument +before it interpretes the second argument. The named evar disappears after the +first step and thus the second argument cannot be interpreted any more. *) +Fail Elpi syntax_test_evars (?[x] + ?x) (?x). + +(* We can fix this by taking these steps more slowly. *) +#[arguments(syntactic)] Elpi Command syntax_test_evars_staged. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg Arg1, syntax.arg Arg2] :- + syntax.default-elab Arg1 (trm T1) ok, + syntax.default-elab Arg2 (trm T2) ok, + T1 = {{ 1 + 1 }}, + T2 = {{ 1 }}. +/*)*/}}. +Elpi syntax_test_evars_staged (1 + 1) (1). +Elpi syntax_test_evars_staged (?[x] + 1) (1). +Elpi syntax_test_evars_staged (1 + 1) (?[x]). +(* Now we interprete both terms first and only then start unifying them. *) +Elpi syntax_test_evars_staged (?[x] + ?x) (?x). + + +(* Adding scopes to syntactic terms. *) +Declare Scope test_scope. +Delimit Scope test_scope with test. +Notation "'[test_notation' ]" := (tt) : test_scope. + +#[arguments(syntactic)] Elpi Command syntax_test6. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg (syntax.str Scope), syntax.arg (syntax.trm Arg1)] :- + syntax.push-scope Arg1 delimit-only-tmp-scope Scope ScopedArg, + syntax.default-elab (syntax.trm ScopedArg) (trm {{ tt }}) ok. +/*)*/}}. +Fail Check [test_notation]. +Fail Elpi syntax_test6 "core" ([test_notation ]). +Succeed Check [test_notation]%test. +Elpi syntax_test6 "test" ([test_notation ]). + +(* Manual Elaboration *) + +#[arguments(syntactic)] Elpi Command elaborate_test. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg (syntax.trm T)] :- + syntax.elaborate T without-type-constraint T' ok, + T' = {{ _ + _ }}. +/*)*/}}. +Elpi elaborate_test (1 + 1). +Elpi elaborate_test (1 + ?[x]). +Elpi elaborate_test (?[x] + ?x). + +Definition f : unit -> nat := fun _ => 0. +Coercion f : unit >-> nat. + +Class Cls := { proj : nat }. +Instance : Cls := {| proj := 1 |}. + +Elpi elaborate_test (1 + tt). (* coercions *) +Elpi elaborate_test (tt + 1). +Elpi elaborate_test (tt + proj). (* and typeclasses *) +Elpi elaborate_test (proj + tt). + +#[arguments(syntactic)] Elpi Command elaborate_test_ty. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg (syntax.trm Ty), syntax.arg (syntax.trm T)] :- + syntax.elaborate Ty is-type Ty' ok, + syntax.elaborate T (of-type Ty') T' ok, + ground_term T'. +/*)*/}}. +Elpi elaborate_test_ty (nat) (1 + 1). +Fail Elpi elaborate_test_ty (False) (I). +Elpi elaborate_test_ty (nat) (tt). (* uses coercion *) +Elpi elaborate_test_ty (nat) (proj). (* typeclasses *) +Elpi elaborate_test_ty (Cls -> nat) (@proj). + +#[arguments(syntactic)] Elpi Command elaborate_test_ty2. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg (syntax.trm Ty), syntax.arg (syntax.trm T)] :- + syntax.elaborate Ty is-type Ty' ok, + (@no-tc! => @no-coercion! => syntax.elaborate T (of-type Ty') T' ok), + ground_term T'. +/*)*/}}. +Elpi elaborate_test_ty2 (nat) (1 + 1). +Fail Elpi elaborate_test_ty (False) (I). +Fail Elpi elaborate_test_ty2 (nat) (tt). (* requires coercions *) +Fail Elpi elaborate_test_ty2 (nat) (proj). (* requires TC *) +Elpi elaborate_test_ty2 (Cls -> nat) (@proj). + +(* Error messages *) +#[arguments(syntactic)] Elpi Command error_msgs. +Elpi Accumulate lp:{{/*(*/ + main [syntax.arg (syntax.str RegExp), syntax.arg (syntax.trm T)] :- + syntax.elaborate T without-type-constraint _ (error E), + rex.match RegExp E. +/*)*/}}. +Elpi error_msgs ".*has type.*True.*" (I + 1). +Elpi error_msgs ".*exhaust.*false.*" (match true with | true => I end). From 0373e4e1856d7c326da6172513e923aa03645552 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Tue, 30 Sep 2025 18:51:03 +0200 Subject: [PATCH 04/12] WIP Address feedback --- elpi/coq-arg-HOAS.elpi | 5 ++-- src/rocq_elpi_arg_HOAS.ml | 36 +++++++++++++-------------- src/rocq_elpi_builtins.ml | 21 ++++++++++------ tests/test_API_elaborate.v | 50 +++++++++++++++++++------------------- 4 files changed, 60 insertions(+), 52 deletions(-) diff --git a/elpi/coq-arg-HOAS.elpi b/elpi/coq-arg-HOAS.elpi index 65a59b0ea..439d79712 100644 --- a/elpi/coq-arg-HOAS.elpi +++ b/elpi/coq-arg-HOAS.elpi @@ -48,13 +48,14 @@ external func attributes -> list attribute. external pred get-option o:string, o:A. % The data type of arguments (for commands or tactics) -kind argument type. +kind elaborated.argument type. +typeabbrev argument elaborated.argument. external symbol int : int -> argument. % Eg. 1 -2. external symbol str : string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol external symbol trm : term -> argument. % Eg. (t). external symbol open-trm : int -> term -> argument. -external symbol syntax.arg : syntax.argument -> argument. +external symbol syntactic.arg : syntactic.argument -> argument. % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context] % take precedence over the [str] argument above (when not "quoted"). diff --git a/src/rocq_elpi_arg_HOAS.ml b/src/rocq_elpi_arg_HOAS.ml index f64293064..522b11e27 100644 --- a/src/rocq_elpi_arg_HOAS.ml +++ b/src/rocq_elpi_arg_HOAS.ml @@ -1330,7 +1330,7 @@ module Syntactic = struct we equip each term with a unique integer to decide what to return when the glob constrs are not equal. *) let trm, trm_type = CD.declare { - name = "syntax.trm"; + name = "syntactic.trm"; doc = "Unprocessed term argument"; pp = (fun fmt (t : res_term) -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.Term t)))); @@ -1345,7 +1345,7 @@ module Syntactic = struct } let constant_decl, constant_decl_type = CD.declare { - name = "syntax.const-decl"; + name = "syntactic.const-decl"; doc = "Unprocessed term argument"; pp = (fun fmt (t : res_constant_decl) -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.ConstantDecl t)))); @@ -1356,7 +1356,7 @@ module Syntactic = struct } let indt_decl, indt_decl_type = CD.declare { - name = "syntax.indt-decl"; + name = "syntactic.indt-decl"; doc = "Unprocessed term argument"; pp = (fun fmt (t : res_indt_decl) -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.IndtDecl t)))); @@ -1367,7 +1367,7 @@ module Syntactic = struct } let record_decl, record_decl_type = CD.declare { - name = "syntax.record-decl"; + name = "syntactic.record-decl"; doc = "Unprocessed term argument"; pp = (fun fmt (t : res_record_decl) -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.RecordDecl t)))); @@ -1378,7 +1378,7 @@ module Syntactic = struct } let context, context_type = CD.declare { - name = "syntax.context-decl"; + name = "syntactic.context-decl"; doc = "Unprocessed term argument"; pp = (fun fmt (t : res_context_decl) -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty (Cmd.Context t)))); @@ -1389,46 +1389,46 @@ module Syntactic = struct } let arg_type = Alg.declare { - ty = TyName "syntax.argument"; + ty = TyName "syntactic.argument"; doc = "Unprocessed command argument"; pp = (fun fmt t -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((pp_res (Global.env()) Evd.empty t))); constructors = [ - K("syntax.str", "", A(API.BuiltInData.string, N), + K("syntactic.str", "", A(API.BuiltInData.string, N), B (fun s -> Cmd.String s), M (fun ~ok ~ko -> function Cmd.String s -> ok s | _ -> ko ()) ); - K("syntax.int", "", A(API.BuiltInData.int, N), + K("syntactic.int", "", A(API.BuiltInData.int, N), B (fun s -> Cmd.Int s), M (fun ~ok ~ko -> function Cmd.Int s -> ok s | _ -> ko ()) ); - K("syntax.trm", "", A(trm_type, N), + K("syntactic.trm", "", A(trm_type, N), B (fun s -> Cmd.Term s), M (fun ~ok ~ko -> function Cmd.Term s -> ok s | _ -> ko ()) ); - K("syntax.const-decl", "", A(constant_decl_type, N), + K("syntactic.const-decl", "", A(constant_decl_type, N), B (fun s -> Cmd.ConstantDecl s), M (fun ~ok ~ko -> function Cmd.ConstantDecl s -> ok s | _ -> ko ()) ); - K("syntax.indt-decl", "", A(indt_decl_type, N), + K("syntactic.indt-decl", "", A(indt_decl_type, N), B (fun s -> Cmd.IndtDecl s), M (fun ~ok ~ko -> function Cmd.IndtDecl s -> ok s | _ -> ko ()) ); - K("syntax.record-decl", "", A(record_decl_type, N), + K("syntactic.record-decl", "", A(record_decl_type, N), B (fun s -> Cmd.RecordDecl s), M (fun ~ok ~ko -> function Cmd.RecordDecl s -> ok s | _ -> ko ()) ); - K("syntax.ctx-decl", "", A(context_type, N), + K("syntactic.ctx-decl", "", A(context_type, N), B (fun s -> Cmd.Context s), M (fun ~ok ~ko -> function Cmd.Context s -> ok s | _ -> ko ()) ); ]; } |> CC.(!<) - let as_normal_arg = E.Constants.declare_global_symbol "syntax.arg" + let as_normal_arg = E.Constants.declare_global_symbol "syntactic.arg" let delimiter_depth = API.OpaqueData.declare { - name = "delimiter_depth"; - doc = "Syntax scope delimiter depth"; + name = "syntactic.delimiter_depth"; + doc = "Syntactic scope delimiter depth"; pp = Constrexpr.(fun fmt -> function | DelimOnlyTmpScope -> Format.fprintf fmt "DelimOnlyTmpScope" | DelimUnboundedScope -> Format.fprintf fmt "DelimUnboundedScope"); @@ -1436,8 +1436,8 @@ module Syntactic = struct hash = Hashtbl.hash; hconsed = true; constants = [ - ("delimit-only-tmp-scope", DelimOnlyTmpScope); - ("delimit-unbounded-scope", DelimUnboundedScope); + ("syntactic.delimit-only-tmp-scope", DelimOnlyTmpScope); + ("syntactic.delimit-unbounded-scope", DelimUnboundedScope); ]; } diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 47f6e1793..5e91d6a8a 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -3647,7 +3647,9 @@ not assigned even if the elaborated term has a term in place of the hole. Similarly universe levels present in T are disregarded. Supported attributes: - @keepunivs! (default false, do not disregard universe levels) -- @no-tc! (default false, do not infer typeclasses) |}))))), +- @no-tc! (default false, do not infer typeclasses) +- @no-coercion! (default: false, do not insert coercions) +|}))))), (fun gt ety _ diag ~depth proof_context _ state -> let flags = Pretyping.default_inference_flags false in let flags = if proof_context.options.no_tc = Some true then {flags with use_typeclasses = NoUseTC} else flags in @@ -4414,7 +4416,7 @@ Supported attributes: ] @ Syntactic.ml_data @ [MLDataC(type_constraint); - MLCode(Pred("syntax.default-elab", + MLCode(Pred("syntactic.default-elab", In(Syntactic.arg_type, "SyntaxArg", Out(Rocq_elpi_arg_HOAS.arg_type, "Arg", InOut(B.ioarg B.diagnostic, "Diagnostic", @@ -4437,7 +4439,7 @@ Supported attributes: state, ?: None +! B.mkERROR error, [] ), DocAbove); - MLCode(Pred("syntax.default-unelab", + MLCode(Pred("syntactic.default-unelab", In(Syntactic.arg_type, "SyntaxArg", Out(Rocq_elpi_arg_HOAS.arg_type, "Arg", InOut(B.ioarg B.diagnostic, "Diagnostic", @@ -4460,7 +4462,7 @@ Supported attributes: state, ?: None +! B.mkERROR error, [] ), DocAbove); - MLCode(Pred("syntax.push-scope", + MLCode(Pred("syntactic.push-scope", In(Syntactic.trm_type, "SyntaxTerm", In(Syntactic.delimiter_depth, "DelimiterDepth", In(B.string, "ScopeName", @@ -4475,12 +4477,17 @@ Supported attributes: state, (!: ot), [] ), DocAbove); - MLCode(Pred("syntax.elaborate", - In(Syntactic.trm_type, "SyntaxTerm", + MLCode(Pred("syntactic.elaborate", + In(Syntactic.trm_type, "SyntacticTerm", CIn(type_constraint, "TypeConstraint", COut(term, "Term", InOut(B.ioarg B.diagnostic, "Diagnostic", - Full(proof_context, "Elaborates SyntaxTerm using TypeConstraint. Respects @no-tc! and @no-coercion!"))))), + Full(proof_context, {| +Elaborates SyntaxTerm using TypeConstraint. +Supported attributes: +- @no-tc! (default false, do not infer typeclasses) +- @no-coercion! (default: false, do not insert coercions) +|}))))), fun t expected_type _ diag ~depth coq_ctx csts state -> let open Syntactic in let Tag.{is;gs;vl} = t in diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v index 5c28d497a..859c49a32 100644 --- a/tests/test_API_elaborate.v +++ b/tests/test_API_elaborate.v @@ -202,30 +202,30 @@ Fail #[arguments(raw=false)] Elpi Command detype. (* Syntactic tests *) #[arguments(syntactic)] Elpi Command syntax_test1. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg (syntax.int 1)]. + main [syntactic.arg (syntactic.int 1)]. /*)*/}}. Elpi syntax_test1 1. Fail Elpi syntax_test1 2. #[arguments(syntactic)] Elpi Command syntax_test2. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg (syntax.str "test")]. + main [syntactic.arg (syntactic.str "test")]. /*)*/}}. Elpi syntax_test2 "test". Fail Elpi syntax_test2 "foo". #[arguments(syntactic)] Elpi Command syntax_test3. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg Arg] :- - syntax.default-elab Arg (int 1) ok. + main [syntactic.arg Arg] :- + syntactic.default-elab Arg (int 1) ok. /*)*/}}. Elpi syntax_test3 1. Fail Elpi syntax_test3 2. #[arguments(syntactic)] Elpi Command syntax_test4. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg Arg] :- - syntax.default-elab Arg (trm {{(1 + 1)}}) ok. + main [syntactic.arg Arg] :- + syntactic.default-elab Arg (trm {{(1 + 1)}}) ok. /*)*/}}. Elpi syntax_test4 (1 + 1). Fail Elpi syntax_test4 (2 + 1). @@ -245,9 +245,9 @@ Fail Elpi evar_deps (eq_refl : (?[x] = 1)) (?x). #[arguments(syntactic)] Elpi Command syntax_test_evars. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg Arg1, syntax.arg Arg2] :- - syntax.default-elab Arg1 (trm {{ 1 + 1 }}) ok, - syntax.default-elab Arg2 (trm {{(1)}}) ok. + main [syntactic.arg Arg1, syntactic.arg Arg2] :- + syntactic.default-elab Arg1 (trm {{ 1 + 1 }}) ok, + syntactic.default-elab Arg2 (trm {{(1)}}) ok. /*)*/}}. Elpi syntax_test_evars (1 + 1) (1). Elpi syntax_test_evars (?[x] + 1) (1). @@ -260,9 +260,9 @@ Fail Elpi syntax_test_evars (?[x] + ?x) (?x). (* We can fix this by taking these steps more slowly. *) #[arguments(syntactic)] Elpi Command syntax_test_evars_staged. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg Arg1, syntax.arg Arg2] :- - syntax.default-elab Arg1 (trm T1) ok, - syntax.default-elab Arg2 (trm T2) ok, + main [syntactic.arg Arg1, syntactic.arg Arg2] :- + syntactic.default-elab Arg1 (trm T1) ok, + syntactic.default-elab Arg2 (trm T2) ok, T1 = {{ 1 + 1 }}, T2 = {{ 1 }}. /*)*/}}. @@ -280,9 +280,9 @@ Notation "'[test_notation' ]" := (tt) : test_scope. #[arguments(syntactic)] Elpi Command syntax_test6. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg (syntax.str Scope), syntax.arg (syntax.trm Arg1)] :- - syntax.push-scope Arg1 delimit-only-tmp-scope Scope ScopedArg, - syntax.default-elab (syntax.trm ScopedArg) (trm {{ tt }}) ok. + main [syntactic.arg (syntactic.str Scope), syntactic.arg (syntactic.trm Arg1)] :- + syntactic.push-scope Arg1 syntactic.delimit-only-tmp-scope Scope ScopedArg, + syntactic.default-elab (syntactic.trm ScopedArg) (trm {{ tt }}) ok. /*)*/}}. Fail Check [test_notation]. Fail Elpi syntax_test6 "core" ([test_notation ]). @@ -293,8 +293,8 @@ Elpi syntax_test6 "test" ([test_notation ]). #[arguments(syntactic)] Elpi Command elaborate_test. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg (syntax.trm T)] :- - syntax.elaborate T without-type-constraint T' ok, + main [syntactic.arg (syntactic.trm T)] :- + syntactic.elaborate T without-type-constraint T' ok, T' = {{ _ + _ }}. /*)*/}}. Elpi elaborate_test (1 + 1). @@ -314,9 +314,9 @@ Elpi elaborate_test (proj + tt). #[arguments(syntactic)] Elpi Command elaborate_test_ty. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg (syntax.trm Ty), syntax.arg (syntax.trm T)] :- - syntax.elaborate Ty is-type Ty' ok, - syntax.elaborate T (of-type Ty') T' ok, + main [syntactic.arg (syntactic.trm Ty), syntactic.arg (syntactic.trm T)] :- + syntactic.elaborate Ty is-type Ty' ok, + syntactic.elaborate T (of-type Ty') T' ok, ground_term T'. /*)*/}}. Elpi elaborate_test_ty (nat) (1 + 1). @@ -327,9 +327,9 @@ Elpi elaborate_test_ty (Cls -> nat) (@proj). #[arguments(syntactic)] Elpi Command elaborate_test_ty2. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg (syntax.trm Ty), syntax.arg (syntax.trm T)] :- - syntax.elaborate Ty is-type Ty' ok, - (@no-tc! => @no-coercion! => syntax.elaborate T (of-type Ty') T' ok), + main [syntactic.arg (syntactic.trm Ty), syntactic.arg (syntactic.trm T)] :- + syntactic.elaborate Ty is-type Ty' ok, + (@no-tc! => @no-coercion! => syntactic.elaborate T (of-type Ty') T' ok), ground_term T'. /*)*/}}. Elpi elaborate_test_ty2 (nat) (1 + 1). @@ -341,8 +341,8 @@ Elpi elaborate_test_ty2 (Cls -> nat) (@proj). (* Error messages *) #[arguments(syntactic)] Elpi Command error_msgs. Elpi Accumulate lp:{{/*(*/ - main [syntax.arg (syntax.str RegExp), syntax.arg (syntax.trm T)] :- - syntax.elaborate T without-type-constraint _ (error E), + main [syntactic.arg (syntactic.str RegExp), syntactic.arg (syntactic.trm T)] :- + syntactic.elaborate T without-type-constraint _ (error E), rex.match RegExp E. /*)*/}}. Elpi error_msgs ".*has type.*True.*" (I + 1). From b33ccf2fedb90fcb8c77d6144eb90ed875d5a9a7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 3 Oct 2025 14:40:12 +0200 Subject: [PATCH 05/12] regenerate builtins --- builtin-doc/coq-builtin-synterp.elpi | 45 +++++++++++++++- builtin-doc/coq-builtin.elpi | 80 +++++++++++++++++++++++++++- 2 files changed, 122 insertions(+), 3 deletions(-) diff --git a/builtin-doc/coq-builtin-synterp.elpi b/builtin-doc/coq-builtin-synterp.elpi index 49d420f9a..ebeeec3c7 100644 --- a/builtin-doc/coq-builtin-synterp.elpi +++ b/builtin-doc/coq-builtin-synterp.elpi @@ -90,12 +90,15 @@ external func attributes -> list attribute. external pred get-option o:string, o:A. % The data type of arguments (for commands or tactics) -kind argument type. +kind elaborated.argument type. +typeabbrev argument elaborated.argument. external symbol int : int -> argument. % Eg. 1 -2. external symbol str : string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol external symbol trm : term -> argument. % Eg. (t). external symbol open-trm : int -> term -> argument. +external symbol syntactic.arg : syntactic.argument -> argument. + % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context] % take precedence over the [str] argument above (when not "quoted"). % @@ -423,6 +426,46 @@ external symbol node : list attribute -> attribute-value = "1". kind attribute type. external symbol attribute : string -> attribute-value -> attribute = "1". +% Unprocessed command argument +kind syntactic.argument type. +external symbol syntactic.str : string -> syntactic.argument = "1". +external symbol syntactic.int : int -> syntactic.argument = "1". +external symbol syntactic.trm : syntactic.trm -> syntactic.argument = "1". +external symbol syntactic.const-decl : syntactic.const-decl -> + syntactic.argument = "1". +external symbol syntactic.indt-decl : syntactic.indt-decl -> + syntactic.argument = "1". +external symbol syntactic.record-decl : syntactic.record-decl -> + syntactic.argument = "1". +external symbol syntactic.ctx-decl : syntactic.context-decl -> + syntactic.argument = "1". + +% Unprocessed term argument +kind syntactic.trm type. + + +% Unprocessed term argument +kind syntactic.const-decl type. + + +% Unprocessed term argument +kind syntactic.indt-decl type. + + +% Unprocessed term argument +kind syntactic.record-decl type. + + +% Unprocessed term argument +kind syntactic.context-decl type. + + +% Syntactic scope delimiter depth +kind syntactic.delimiter_depth type. + +external symbol syntactic.delimit-unbounded-scope : syntactic.delimiter_depth = "1". +external symbol syntactic.delimit-only-tmp-scope : syntactic.delimiter_depth = "1". + diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index e505dfe22..5f186c617 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/builtin-doc/coq-builtin.elpi @@ -63,12 +63,15 @@ external func attributes -> list attribute. external pred get-option o:string, o:A. % The data type of arguments (for commands or tactics) -kind argument type. +kind elaborated.argument type. +typeabbrev argument elaborated.argument. external symbol int : int -> argument. % Eg. 1 -2. external symbol str : string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol external symbol trm : term -> argument. % Eg. (t). external symbol open-trm : int -> term -> argument. +external symbol syntactic.arg : syntactic.argument -> argument. + % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context] % take precedence over the [str] argument above (when not "quoted"). % @@ -1481,7 +1484,9 @@ external func coq.unify-leq term, term -> diagnostic. % hole. Similarly universe levels present in T are disregarded. % Supported attributes: % - @keepunivs! (default false, do not disregard universe levels) -% - @no-tc! (default false, do not infer typeclasses) +% - @no-tc! (default false, do not infer typeclasses) +% - @no-coercion! (default: false, do not insert coercions) +% external func coq.elaborate-skeleton term -> term, term, diagnostic. % [coq.elaborate-ty-skeleton T U E Diagnostic] elabotares T expecting it to @@ -2291,6 +2296,77 @@ external symbol coq.pp.nl : coq.pp = "1". % - @ppwidth! N (default 80, max line length) external func coq.pp->string coq.pp -> string. +% Unprocessed command argument +kind syntactic.argument type. +external symbol syntactic.str : string -> syntactic.argument = "1". +external symbol syntactic.int : int -> syntactic.argument = "1". +external symbol syntactic.trm : syntactic.trm -> syntactic.argument = "1". +external symbol syntactic.const-decl : syntactic.const-decl -> + syntactic.argument = "1". +external symbol syntactic.indt-decl : syntactic.indt-decl -> + syntactic.argument = "1". +external symbol syntactic.record-decl : syntactic.record-decl -> + syntactic.argument = "1". +external symbol syntactic.ctx-decl : syntactic.context-decl -> + syntactic.argument = "1". + +% Unprocessed term argument +kind syntactic.trm type. + + +% Unprocessed term argument +kind syntactic.const-decl type. + + +% Unprocessed term argument +kind syntactic.indt-decl type. + + +% Unprocessed term argument +kind syntactic.record-decl type. + + +% Unprocessed term argument +kind syntactic.context-decl type. + + +% Syntactic scope delimiter depth +kind syntactic.delimiter_depth type. + +external symbol syntactic.delimit-unbounded-scope : syntactic.delimiter_depth = "1". +external symbol syntactic.delimit-only-tmp-scope : syntactic.delimiter_depth = "1". + +% The expected type for elaborating syntactic terms +kind type-constraint type. +external symbol of-type : term -> type-constraint = "1". % Pretype with a specific expected type +external symbol is-type : type-constraint = "1". % Pretype as a type + +% [syntactic.default-elab SyntaxArg Arg Diagnostic] Elaborates the syntactic +% argument with the settings of #[arguments(elaborated)] +external func syntactic.default-elab syntactic.argument -> argument, + diagnostic. + +% [syntactic.default-unelab SyntaxArg Arg Diagnostic] Elaborates the +% syntactic argument with the settings of #[arguments(unelaborated)] +external func syntactic.default-unelab syntactic.argument -> argument, + diagnostic. + +% [syntactic.push-scope SyntaxTerm DelimiterDepth ScopeName +% ScopedSyntaxTerm] Pushes the scope ScopeName on top of SyntaxTerm. +external func syntactic.push-scope syntactic.trm, + syntactic.delimiter_depth, + string -> syntactic.trm. + +% [syntactic.elaborate SyntacticTerm TypeConstraint Term Diagnostic] +% +% Elaborates SyntaxTerm using TypeConstraint (if provided). +% Supported attributes: +% - @no-tc! (default false, do not infer typeclasses) +% - @no-coercion! (default: false, do not insert coercions) +% +external func syntactic.elaborate syntactic.trm, type-constraint -> term, + diagnostic. + From 7588c7cb302e6b5a7b5be915d934b072b551275b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 3 Oct 2025 14:40:37 +0200 Subject: [PATCH 06/12] keep loc if any --- src/rocq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 5e91d6a8a..e23cd7620 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -4472,7 +4472,7 @@ Supported attributes: let open Syntactic in let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in let Tag.{vl; _} = t in - let vl = CAst.make ~loc (Constrexpr.CDelimiters (delim_depth, scope, vl)) in + let vl = CAst.make ~loc:(Option.default loc vl.CAst.loc) (Constrexpr.CDelimiters (delim_depth, scope, vl)) in let ot = Tag.{t with vl} in state, (!: ot), [] ), From 786ad932a82f6e24658e43fe3f30828a8f7cc4b6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 3 Oct 2025 14:41:03 +0200 Subject: [PATCH 07/12] give error, do not backtrack --- src/rocq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index e23cd7620..750da77e9 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -4511,7 +4511,7 @@ Supported attributes: diag_error_lazy diag @@ fun () -> let error = string_of_ppcmds coq_ctx.options @@ - try CErrors.print_no_report e with | _ -> raise No_clause + try CErrors.print_no_report e with | _ -> Pp.str "syntactic.elaborate: anomaly printing error" in state, ?: None +! B.mkERROR error, [] ), From bfad5cd4ad57dee275b460db58542860977e7942 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 3 Oct 2025 14:41:22 +0200 Subject: [PATCH 08/12] rm without-type-constraint --- src/rocq_elpi_builtins.ml | 12 ++++++------ tests/test_API_elaborate.v | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 750da77e9..15563239b 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -259,10 +259,6 @@ let type_constraint = doc = "The expected type for elaborating syntactic terms"; pp = (fun fmt _ -> Format.fprintf fmt ""); constructors = Pretyping.[ - K("without-type-constraint", "Pretype without type constraint", N, - B (WithoutTypeConstraint), - M (fun ~ok ~ko -> function WithoutTypeConstraint -> ok | _ -> ko ()) - ); K("of-type", "Pretype with a specific expected type", CA(term, N), B (fun t -> OfType t), M (fun ~ok ~ko -> function OfType t -> ok t | _ -> ko ()) @@ -4479,11 +4475,11 @@ Supported attributes: DocAbove); MLCode(Pred("syntactic.elaborate", In(Syntactic.trm_type, "SyntacticTerm", - CIn(type_constraint, "TypeConstraint", + CIn(B.unspecC type_constraint, "TypeConstraint", COut(term, "Term", InOut(B.ioarg B.diagnostic, "Diagnostic", Full(proof_context, {| -Elaborates SyntaxTerm using TypeConstraint. +Elaborates SyntaxTerm using TypeConstraint (if provided). Supported attributes: - @no-tc! (default false, do not infer typeclasses) - @no-coercion! (default: false, do not insert coercions) @@ -4501,6 +4497,10 @@ Supported attributes: let use_coercions = not @@ Option.default false options.no_coercion in { flags with use_typeclasses; use_coercions } in + let expected_type = + match expected_type with + | B.Unspec -> Pretyping.WithoutTypeConstraint + | B.Given x -> x in try let sigma, vl = Ltac_plugin.Tacinterp.interp_open_constr ~flags ~expected_type is coq_ctx.env sigma vl diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v index 859c49a32..c5ac8a550 100644 --- a/tests/test_API_elaborate.v +++ b/tests/test_API_elaborate.v @@ -294,7 +294,7 @@ Elpi syntax_test6 "test" ([test_notation ]). #[arguments(syntactic)] Elpi Command elaborate_test. Elpi Accumulate lp:{{/*(*/ main [syntactic.arg (syntactic.trm T)] :- - syntactic.elaborate T without-type-constraint T' ok, + syntactic.elaborate T _ T' ok, T' = {{ _ + _ }}. /*)*/}}. Elpi elaborate_test (1 + 1). @@ -342,7 +342,7 @@ Elpi elaborate_test_ty2 (Cls -> nat) (@proj). #[arguments(syntactic)] Elpi Command error_msgs. Elpi Accumulate lp:{{/*(*/ main [syntactic.arg (syntactic.str RegExp), syntactic.arg (syntactic.trm T)] :- - syntactic.elaborate T without-type-constraint _ (error E), + syntactic.elaborate T _ _ (error E), rex.match RegExp E. /*)*/}}. Elpi error_msgs ".*has type.*True.*" (I + 1). From e7dedbaf42795d19664ec16ea5565559ce9b9318 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 3 Oct 2025 15:19:32 +0200 Subject: [PATCH 09/12] refactor/rename --- builtin-doc/coq-builtin.elpi | 36 ++++---- src/rocq_elpi_builtins.ml | 155 +++++++++++++++++------------------ tests/test_API_elaborate.v | 22 ++--- 3 files changed, 106 insertions(+), 107 deletions(-) diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index 5f186c617..01d275458 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/builtin-doc/coq-builtin.elpi @@ -2336,20 +2336,17 @@ kind syntactic.delimiter_depth type. external symbol syntactic.delimit-unbounded-scope : syntactic.delimiter_depth = "1". external symbol syntactic.delimit-only-tmp-scope : syntactic.delimiter_depth = "1". -% The expected type for elaborating syntactic terms -kind type-constraint type. -external symbol of-type : term -> type-constraint = "1". % Pretype with a specific expected type -external symbol is-type : type-constraint = "1". % Pretype as a type - -% [syntactic.default-elab SyntaxArg Arg Diagnostic] Elaborates the syntactic -% argument with the settings of #[arguments(elaborated)] -external func syntactic.default-elab syntactic.argument -> argument, - diagnostic. - -% [syntactic.default-unelab SyntaxArg Arg Diagnostic] Elaborates the -% syntactic argument with the settings of #[arguments(unelaborated)] -external func syntactic.default-unelab syntactic.argument -> argument, - diagnostic. +% [syntactic.argument->elaborated.argument SyntaxArg Arg Diagnostic] +% Elaborates the syntactic argument with the settings of +% #[arguments(elaborated)] +external func syntactic.argument->elaborated.argument syntactic.argument -> argument, + diagnostic. + +% [syntactic.argument->unelaborated.argument SyntaxArg Arg Diagnostic] +% Elaborates the syntactic argument with the settings of +% #[arguments(unelaborated)] +external func syntactic.argument->unelaborated.argument syntactic.argument -> argument, + diagnostic. % [syntactic.push-scope SyntaxTerm DelimiterDepth ScopeName % ScopedSyntaxTerm] Pushes the scope ScopeName on top of SyntaxTerm. @@ -2364,8 +2361,15 @@ external func syntactic.push-scope syntactic.trm, % - @no-tc! (default false, do not infer typeclasses) % - @no-coercion! (default: false, do not insert coercions) % -external func syntactic.elaborate syntactic.trm, type-constraint -> term, - diagnostic. +external func syntactic.elaborate syntactic.trm, term -> term, diagnostic. + +% [syntactic.elaborate-ty SyntacticTerm Term Diagnostic] +% Elaborates SyntaxTerm as a Type. +% Supported attributes: +% - @no-tc! (default false, do not infer typeclasses) +% - @no-coercion! (default: false, do not insert coercions) +% +external func syntactic.elaborate-ty syntactic.trm -> term, diagnostic. diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 15563239b..1f42c1428 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -253,23 +253,6 @@ let term_skeleton = { embed = (fun ~depth _ _ _ _ -> assert false); } -let type_constraint = - API.AlgebraicData.declare { - ty = TyName "type-constraint"; - doc = "The expected type for elaborating syntactic terms"; - pp = (fun fmt _ -> Format.fprintf fmt ""); - constructors = Pretyping.[ - K("of-type", "Pretype with a specific expected type", CA(term, N), - B (fun t -> OfType t), - M (fun ~ok ~ko -> function OfType t -> ok t | _ -> ko ()) - ); - K("is-type", "Pretype as a type", N, - B (IsType), - M (fun ~ok ~ko -> function IsType -> ok | _ -> ko ()) - ); - ]; - } - let sealed_goal = { Conv.ty = Conv.TyName "sealed-goal"; pp_doc = (fun fmt () -> ()); @@ -1520,9 +1503,58 @@ let apply_proof ~name ~poly env tac pf = pv [%%endif] +let syntactic_arg_to_arg api ~kind sarg diag ~depth coq_ctx _csts state = + let open API.BuiltIn in + let open Pred in + let open Notation in + let open CConv in + let open Syntactic in + let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in + let base = Option.get (State.get base state) in + try + let state, res, extra_goals = + Syntactic.top_of_res sarg |> + Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base ~kind coq_ctx state + in + state, (!: res +! B.mkOK), extra_goals + with e -> + diag_error_lazy diag @@ fun () -> + let error = + string_of_ppcmds coq_ctx.options @@ + try CErrors.print_no_report e with | _ -> Pp.(str api ++ str ": anomaly printing error") + in + state, ?: None +! B.mkERROR error, [] - - +let syntactic_arg_elaborate api t expected_type diag ~depth coq_ctx csts state = + let open API.BuiltIn in + let open Pred in + let open Notation in + let open CConv in + let open Syntactic in + let Tag.{is;gs;vl} = t in + let vl = Ltac_plugin.Tacintern.intern_constr gs vl in + let sigma = get_sigma state in + let flags = + let open Pretyping in + let flags = all_no_fail_flags in + let options = coq_ctx.options in + let use_typeclasses = if Option.default false options.no_tc then NoUseTC else UseTC in + let use_coercions = not @@ Option.default false options.no_coercion in + { flags with use_typeclasses; use_coercions } + in + try + let sigma, vl = + Ltac_plugin.Tacinterp.interp_open_constr ~flags ~expected_type is coq_ctx.env sigma vl + in + let state, extra_goals = set_current_sigma ~depth state sigma in + state, (!: vl +! B.mkOK), extra_goals + with e -> + diag_error_lazy diag @@ fun () -> + let error = + string_of_ppcmds coq_ctx.options @@ + try CErrors.print_no_report e with | _ -> Pp.(str api ++ str ": anomaly printing error") + in + state, ?: None +! B.mkERROR error, [] let coq_misc_builtins = let open API.BuiltIn in @@ -4411,52 +4443,23 @@ Supported attributes: ] @ Syntactic.ml_data @ - [MLDataC(type_constraint); - MLCode(Pred("syntactic.default-elab", + [MLCode(Pred("syntactic.argument->elaborated.argument", In(Syntactic.arg_type, "SyntaxArg", Out(Rocq_elpi_arg_HOAS.arg_type, "Arg", InOut(B.ioarg B.diagnostic, "Diagnostic", Full(global, "Elaborates the syntactic argument with the settings of #[arguments(elaborated)]")))), fun sarg _ diag ~depth coq_ctx _csts state -> - let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in - let base = Option.get (State.get base state) in - try - let state, res, extra_goals = - Syntactic.top_of_res sarg |> - Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base ~kind:Elaborated coq_ctx state - in - state, (!: res +! B.mkOK), extra_goals - with e -> - diag_error_lazy diag @@ fun () -> - let error = - string_of_ppcmds coq_ctx.options @@ - try CErrors.print_no_report e with | _ -> raise No_clause - in - state, ?: None +! B.mkERROR error, [] + syntactic_arg_to_arg "syntactic.argument->elaborated.argument" ~kind:Elaborated sarg diag ~depth coq_ctx _csts state ), DocAbove); - MLCode(Pred("syntactic.default-unelab", + MLCode(Pred("syntactic.argument->unelaborated.argument", In(Syntactic.arg_type, "SyntaxArg", Out(Rocq_elpi_arg_HOAS.arg_type, "Arg", InOut(B.ioarg B.diagnostic, "Diagnostic", Full(global, "Elaborates the syntactic argument with the settings of #[arguments(unelaborated)]")))), fun sarg _ diag ~depth coq_ctx _csts state -> - let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in - let base = Option.get (State.get base state) in - try - let state, res, extra_goals = - Syntactic.top_of_res sarg |> - Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base ~kind:Unelaborated coq_ctx state - in - state, (!: res +! B.mkOK), extra_goals - with e -> - diag_error_lazy diag @@ fun () -> - let error = - string_of_ppcmds coq_ctx.options @@ - try CErrors.print_no_report e with | _ -> raise No_clause - in - state, ?: None +! B.mkERROR error, [] - ), + syntactic_arg_to_arg "syntactic.argument->unelaborated.argument" ~kind:Unelaborated sarg diag ~depth coq_ctx _csts state + ), DocAbove); MLCode(Pred("syntactic.push-scope", In(Syntactic.trm_type, "SyntaxTerm", @@ -4475,7 +4478,7 @@ Supported attributes: DocAbove); MLCode(Pred("syntactic.elaborate", In(Syntactic.trm_type, "SyntacticTerm", - CIn(B.unspecC type_constraint, "TypeConstraint", + CIn(B.unspecC term, "TypeConstraint", COut(term, "Term", InOut(B.ioarg B.diagnostic, "Diagnostic", Full(proof_context, {| @@ -4485,37 +4488,29 @@ Supported attributes: - @no-coercion! (default: false, do not insert coercions) |}))))), fun t expected_type _ diag ~depth coq_ctx csts state -> - let open Syntactic in - let Tag.{is;gs;vl} = t in - let vl = Ltac_plugin.Tacintern.intern_constr gs vl in - let sigma = get_sigma state in - let flags = - let open Pretyping in - let flags = all_no_fail_flags in - let options = coq_ctx.options in - let use_typeclasses = if Option.default false options.no_tc then NoUseTC else UseTC in - let use_coercions = not @@ Option.default false options.no_coercion in - { flags with use_typeclasses; use_coercions } - in let expected_type = match expected_type with | B.Unspec -> Pretyping.WithoutTypeConstraint - | B.Given x -> x in - try - let sigma, vl = - Ltac_plugin.Tacinterp.interp_open_constr ~flags ~expected_type is coq_ctx.env sigma vl - in - let state, extra_goals = set_current_sigma ~depth state sigma in - state, (!: vl +! B.mkOK), extra_goals - with e -> - diag_error_lazy diag @@ fun () -> - let error = - string_of_ppcmds coq_ctx.options @@ - try CErrors.print_no_report e with | _ -> Pp.str "syntactic.elaborate: anomaly printing error" - in - state, ?: None +! B.mkERROR error, [] + | B.Given x -> Pretyping.OfType x in + syntactic_arg_elaborate "syntactic.elaborate" t expected_type diag ~depth coq_ctx csts state ), DocAbove); + MLCode(Pred("syntactic.elaborate-ty", + In(Syntactic.trm_type, "SyntacticTerm", + COut(term, "Term", + InOut(B.ioarg B.diagnostic, "Diagnostic", + Full(proof_context, {| +Elaborates SyntaxTerm as a Type. +Supported attributes: +- @no-tc! (default false, do not infer typeclasses) +- @no-coercion! (default: false, do not insert coercions) +|})))), + fun t _ diag ~depth coq_ctx csts state -> + let expected_type = Pretyping.IsType in + syntactic_arg_elaborate "syntactic.elaborate-ty" t expected_type diag ~depth coq_ctx csts state + ), + DocAbove); + ] diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v index c5ac8a550..49e50c06e 100644 --- a/tests/test_API_elaborate.v +++ b/tests/test_API_elaborate.v @@ -217,7 +217,7 @@ Fail Elpi syntax_test2 "foo". #[arguments(syntactic)] Elpi Command syntax_test3. Elpi Accumulate lp:{{/*(*/ main [syntactic.arg Arg] :- - syntactic.default-elab Arg (int 1) ok. + syntactic.argument->elaborated.argument Arg (int 1) ok. /*)*/}}. Elpi syntax_test3 1. Fail Elpi syntax_test3 2. @@ -225,7 +225,7 @@ Fail Elpi syntax_test3 2. #[arguments(syntactic)] Elpi Command syntax_test4. Elpi Accumulate lp:{{/*(*/ main [syntactic.arg Arg] :- - syntactic.default-elab Arg (trm {{(1 + 1)}}) ok. + syntactic.argument->elaborated.argument Arg (trm {{(1 + 1)}}) ok. /*)*/}}. Elpi syntax_test4 (1 + 1). Fail Elpi syntax_test4 (2 + 1). @@ -246,8 +246,8 @@ Fail Elpi evar_deps (eq_refl : (?[x] = 1)) (?x). #[arguments(syntactic)] Elpi Command syntax_test_evars. Elpi Accumulate lp:{{/*(*/ main [syntactic.arg Arg1, syntactic.arg Arg2] :- - syntactic.default-elab Arg1 (trm {{ 1 + 1 }}) ok, - syntactic.default-elab Arg2 (trm {{(1)}}) ok. + syntactic.argument->elaborated.argument Arg1 (trm {{ 1 + 1 }}) ok, + syntactic.argument->elaborated.argument Arg2 (trm {{(1)}}) ok. /*)*/}}. Elpi syntax_test_evars (1 + 1) (1). Elpi syntax_test_evars (?[x] + 1) (1). @@ -261,8 +261,8 @@ Fail Elpi syntax_test_evars (?[x] + ?x) (?x). #[arguments(syntactic)] Elpi Command syntax_test_evars_staged. Elpi Accumulate lp:{{/*(*/ main [syntactic.arg Arg1, syntactic.arg Arg2] :- - syntactic.default-elab Arg1 (trm T1) ok, - syntactic.default-elab Arg2 (trm T2) ok, + syntactic.argument->elaborated.argument Arg1 (trm T1) ok, + syntactic.argument->elaborated.argument Arg2 (trm T2) ok, T1 = {{ 1 + 1 }}, T2 = {{ 1 }}. /*)*/}}. @@ -282,7 +282,7 @@ Notation "'[test_notation' ]" := (tt) : test_scope. Elpi Accumulate lp:{{/*(*/ main [syntactic.arg (syntactic.str Scope), syntactic.arg (syntactic.trm Arg1)] :- syntactic.push-scope Arg1 syntactic.delimit-only-tmp-scope Scope ScopedArg, - syntactic.default-elab (syntactic.trm ScopedArg) (trm {{ tt }}) ok. + syntactic.argument->elaborated.argument (syntactic.trm ScopedArg) (trm {{ tt }}) ok. /*)*/}}. Fail Check [test_notation]. Fail Elpi syntax_test6 "core" ([test_notation ]). @@ -315,8 +315,8 @@ Elpi elaborate_test (proj + tt). #[arguments(syntactic)] Elpi Command elaborate_test_ty. Elpi Accumulate lp:{{/*(*/ main [syntactic.arg (syntactic.trm Ty), syntactic.arg (syntactic.trm T)] :- - syntactic.elaborate Ty is-type Ty' ok, - syntactic.elaborate T (of-type Ty') T' ok, + syntactic.elaborate-ty Ty Ty' ok, + syntactic.elaborate T Ty' T' ok, ground_term T'. /*)*/}}. Elpi elaborate_test_ty (nat) (1 + 1). @@ -328,8 +328,8 @@ Elpi elaborate_test_ty (Cls -> nat) (@proj). #[arguments(syntactic)] Elpi Command elaborate_test_ty2. Elpi Accumulate lp:{{/*(*/ main [syntactic.arg (syntactic.trm Ty), syntactic.arg (syntactic.trm T)] :- - syntactic.elaborate Ty is-type Ty' ok, - (@no-tc! => @no-coercion! => syntactic.elaborate T (of-type Ty') T' ok), + syntactic.elaborate-ty Ty Ty' ok, + (@no-tc! => @no-coercion! => syntactic.elaborate T Ty' T' ok), ground_term T'. /*)*/}}. Elpi elaborate_test_ty2 (nat) (1 + 1). From 91cc77c75ba1efa8ec6b31dad3b717987ea5d750 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 3 Oct 2025 15:19:41 +0200 Subject: [PATCH 10/12] util --- src/rocq_elpi_arg_HOAS.ml | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/src/rocq_elpi_arg_HOAS.ml b/src/rocq_elpi_arg_HOAS.ml index 522b11e27..dc6198a53 100644 --- a/src/rocq_elpi_arg_HOAS.ml +++ b/src/rocq_elpi_arg_HOAS.ml @@ -206,6 +206,18 @@ let map (type a b c d e v w x y z) : | IndtDecl s -> IndtDecl (h s) | ConstantDecl s -> ConstantDecl (i s) | Context c -> Context (j c) +let inj (type a b c d e v) : + (int -> v) -> + (string -> v) -> + (a -> v) -> (b -> v) -> (c -> v) -> (d -> v) -> (e -> v) -> + (a,b,c,d,e) t -> v = fun f0 f1 f g h i j -> function + | Int x -> f0 x + | String x -> f1 x + | Term s -> (f s) + | RecordDecl s -> (g s) + | IndtDecl s -> (h s) + | ConstantDecl s -> (i s) + | Context c -> (j c) type raw = (raw_term, raw_record_decl, raw_indt_decl, raw_constant_decl, raw_context_decl) t type glob = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl, glob_context_decl) t @@ -214,15 +226,7 @@ type top = (top_term, top_record_decl, top_indt_decl, top_constant_decl, to let raw_of_glob : glob -> raw = map GS.get GS.get GS.get GS.get GS.get let raw_of_top : top -> raw = map IS.get IS.get IS.get IS.get IS.get -let pr_arg f g h i j x = match x with -| Int n -> Pp.int n -| String s -> Pp.qstring s -| Term s -> f s -| RecordDecl s -> g s -| IndtDecl s -> h s -| ConstantDecl s -> i s -| Context c -> j c - +let pr_arg f g h i j x = inj Pp.int Pp.qstring f g h i j x let pp_raw env sigma : raw -> Pp.t = pr_arg (Ppconstr.pr_constr_expr env sigma) @@ -1314,6 +1318,7 @@ module Syntactic = struct {is;gs;vl;tag} let drop_tag (type a) : a t -> a IS.t = fun {is;gs;vl;tag=_} -> IS.{is;gs;vl} + end type res_term = raw_term Tag.t From 88635fc2e66131285ae04e8bae9c946854bcd655 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 3 Oct 2025 15:22:28 +0200 Subject: [PATCH 11/12] fix test --- tests/test_API_elaborate.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v index 49e50c06e..6e25c63d8 100644 --- a/tests/test_API_elaborate.v +++ b/tests/test_API_elaborate.v @@ -343,7 +343,7 @@ Elpi elaborate_test_ty2 (Cls -> nat) (@proj). Elpi Accumulate lp:{{/*(*/ main [syntactic.arg (syntactic.str RegExp), syntactic.arg (syntactic.trm T)] :- syntactic.elaborate T _ _ (error E), - rex.match RegExp E. + std.assert! (rex.match RegExp E) "bad message". /*)*/}}. Elpi error_msgs ".*has type.*True.*" (I + 1). -Elpi error_msgs ".*exhaust.*false.*" (match true with | true => I end). +Elpi error_msgs ".*Non exhaust.*" (match true with | true => I end). From f9746b04fa52d6c3b15cbeef5eb1bf3edde4d5f7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 3 Oct 2025 15:26:32 +0200 Subject: [PATCH 12/12] syntactic.arg -> syntactic --- builtin-doc/coq-builtin-synterp.elpi | 2 +- builtin-doc/coq-builtin.elpi | 2 +- elpi/coq-arg-HOAS.elpi | 2 +- src/rocq_elpi_arg_HOAS.ml | 2 +- tests/test_API_elaborate.v | 22 +++++++++++----------- 5 files changed, 15 insertions(+), 15 deletions(-) diff --git a/builtin-doc/coq-builtin-synterp.elpi b/builtin-doc/coq-builtin-synterp.elpi index ebeeec3c7..ac3e63422 100644 --- a/builtin-doc/coq-builtin-synterp.elpi +++ b/builtin-doc/coq-builtin-synterp.elpi @@ -97,7 +97,7 @@ external symbol str : string -> argument. % Eg. x "y" z.w. or any Coq keywo external symbol trm : term -> argument. % Eg. (t). external symbol open-trm : int -> term -> argument. -external symbol syntactic.arg : syntactic.argument -> argument. +external symbol syntactic : syntactic.argument -> argument. % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context] % take precedence over the [str] argument above (when not "quoted"). diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index 01d275458..ea1dd0f20 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/builtin-doc/coq-builtin.elpi @@ -70,7 +70,7 @@ external symbol str : string -> argument. % Eg. x "y" z.w. or any Coq keywo external symbol trm : term -> argument. % Eg. (t). external symbol open-trm : int -> term -> argument. -external symbol syntactic.arg : syntactic.argument -> argument. +external symbol syntactic : syntactic.argument -> argument. % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context] % take precedence over the [str] argument above (when not "quoted"). diff --git a/elpi/coq-arg-HOAS.elpi b/elpi/coq-arg-HOAS.elpi index 439d79712..8376e00bd 100644 --- a/elpi/coq-arg-HOAS.elpi +++ b/elpi/coq-arg-HOAS.elpi @@ -55,7 +55,7 @@ external symbol str : string -> argument. % Eg. x "y" z.w. or any Coq keywo external symbol trm : term -> argument. % Eg. (t). external symbol open-trm : int -> term -> argument. -external symbol syntactic.arg : syntactic.argument -> argument. +external symbol syntactic : syntactic.argument -> argument. % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context] % take precedence over the [str] argument above (when not "quoted"). diff --git a/src/rocq_elpi_arg_HOAS.ml b/src/rocq_elpi_arg_HOAS.ml index dc6198a53..55ddeabab 100644 --- a/src/rocq_elpi_arg_HOAS.ml +++ b/src/rocq_elpi_arg_HOAS.ml @@ -1429,7 +1429,7 @@ module Syntactic = struct ]; } |> CC.(!<) - let as_normal_arg = E.Constants.declare_global_symbol "syntactic.arg" + let as_normal_arg = E.Constants.declare_global_symbol "syntactic" let delimiter_depth = API.OpaqueData.declare { name = "syntactic.delimiter_depth"; diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v index 6e25c63d8..cbe06c16d 100644 --- a/tests/test_API_elaborate.v +++ b/tests/test_API_elaborate.v @@ -202,21 +202,21 @@ Fail #[arguments(raw=false)] Elpi Command detype. (* Syntactic tests *) #[arguments(syntactic)] Elpi Command syntax_test1. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg (syntactic.int 1)]. + main [syntactic (syntactic.int 1)]. /*)*/}}. Elpi syntax_test1 1. Fail Elpi syntax_test1 2. #[arguments(syntactic)] Elpi Command syntax_test2. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg (syntactic.str "test")]. + main [syntactic (syntactic.str "test")]. /*)*/}}. Elpi syntax_test2 "test". Fail Elpi syntax_test2 "foo". #[arguments(syntactic)] Elpi Command syntax_test3. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg Arg] :- + main [syntactic Arg] :- syntactic.argument->elaborated.argument Arg (int 1) ok. /*)*/}}. Elpi syntax_test3 1. @@ -224,7 +224,7 @@ Fail Elpi syntax_test3 2. #[arguments(syntactic)] Elpi Command syntax_test4. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg Arg] :- + main [syntactic Arg] :- syntactic.argument->elaborated.argument Arg (trm {{(1 + 1)}}) ok. /*)*/}}. Elpi syntax_test4 (1 + 1). @@ -245,7 +245,7 @@ Fail Elpi evar_deps (eq_refl : (?[x] = 1)) (?x). #[arguments(syntactic)] Elpi Command syntax_test_evars. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg Arg1, syntactic.arg Arg2] :- + main [syntactic Arg1, syntactic Arg2] :- syntactic.argument->elaborated.argument Arg1 (trm {{ 1 + 1 }}) ok, syntactic.argument->elaborated.argument Arg2 (trm {{(1)}}) ok. /*)*/}}. @@ -260,7 +260,7 @@ Fail Elpi syntax_test_evars (?[x] + ?x) (?x). (* We can fix this by taking these steps more slowly. *) #[arguments(syntactic)] Elpi Command syntax_test_evars_staged. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg Arg1, syntactic.arg Arg2] :- + main [syntactic Arg1, syntactic Arg2] :- syntactic.argument->elaborated.argument Arg1 (trm T1) ok, syntactic.argument->elaborated.argument Arg2 (trm T2) ok, T1 = {{ 1 + 1 }}, @@ -280,7 +280,7 @@ Notation "'[test_notation' ]" := (tt) : test_scope. #[arguments(syntactic)] Elpi Command syntax_test6. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg (syntactic.str Scope), syntactic.arg (syntactic.trm Arg1)] :- + main [syntactic (syntactic.str Scope), syntactic (syntactic.trm Arg1)] :- syntactic.push-scope Arg1 syntactic.delimit-only-tmp-scope Scope ScopedArg, syntactic.argument->elaborated.argument (syntactic.trm ScopedArg) (trm {{ tt }}) ok. /*)*/}}. @@ -293,7 +293,7 @@ Elpi syntax_test6 "test" ([test_notation ]). #[arguments(syntactic)] Elpi Command elaborate_test. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg (syntactic.trm T)] :- + main [syntactic (syntactic.trm T)] :- syntactic.elaborate T _ T' ok, T' = {{ _ + _ }}. /*)*/}}. @@ -314,7 +314,7 @@ Elpi elaborate_test (proj + tt). #[arguments(syntactic)] Elpi Command elaborate_test_ty. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg (syntactic.trm Ty), syntactic.arg (syntactic.trm T)] :- + main [syntactic (syntactic.trm Ty), syntactic (syntactic.trm T)] :- syntactic.elaborate-ty Ty Ty' ok, syntactic.elaborate T Ty' T' ok, ground_term T'. @@ -327,7 +327,7 @@ Elpi elaborate_test_ty (Cls -> nat) (@proj). #[arguments(syntactic)] Elpi Command elaborate_test_ty2. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg (syntactic.trm Ty), syntactic.arg (syntactic.trm T)] :- + main [syntactic (syntactic.trm Ty), syntactic (syntactic.trm T)] :- syntactic.elaborate-ty Ty Ty' ok, (@no-tc! => @no-coercion! => syntactic.elaborate T Ty' T' ok), ground_term T'. @@ -341,7 +341,7 @@ Elpi elaborate_test_ty2 (Cls -> nat) (@proj). (* Error messages *) #[arguments(syntactic)] Elpi Command error_msgs. Elpi Accumulate lp:{{/*(*/ - main [syntactic.arg (syntactic.str RegExp), syntactic.arg (syntactic.trm T)] :- + main [syntactic (syntactic.str RegExp), syntactic (syntactic.trm T)] :- syntactic.elaborate T _ _ (error E), std.assert! (rex.match RegExp E) "bad message". /*)*/}}.