diff --git a/Changelog.md b/Changelog.md index 4a6edf70d..03aab48b9 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,13 @@ # Changelog +## Unreleased + +- New option `@warn! Cats Message`. + In order to pass a warn directive one has to do something like + `@warn! "cata, catb, catc" "Beware of foo." => coq.add-something` + Deprecation is understood by: + - `coq.notation.add-abbreviation` + ## [2.0.1] - 24/12/2023 Requires Elpi 1.18.1 and Coq 8.19. diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 3ab751e67..43b4ad4a4 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -490,6 +490,10 @@ macro @redflags! F :- get-option "coq:redflags" F. % for whd & co macro @deprecated! Since Msg :- get-option "coq:deprecated" (pr Since Msg). +% both arguments are strings eg "cata, catb, catc" "Beware of foo." +macro @warn! Cats Msg :- + get-option "coq:warn" (pr Cats Msg). + macro @ltacfail! N :- get-option "ltac:fail" N. % retrocompatibility macro for Coq v8.10 @@ -1346,6 +1350,7 @@ typeabbrev abbreviation (ctype "abbreviation"). % ignored, eg (fun _ _ x\ fun _ _ y\ app[global "add",x,y]). % Supported attributes: % - @deprecated! (default: not deprecated) +% - @warn! (default: no warning) % - @global! (default: false) external pred coq.notation.add-abbreviation i:id, i:int, i:term, i:bool, o:abbreviation. diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index bd7d8ebb0..0c0c43f0d 100644 --- a/elpi/coq-HOAS.elpi +++ b/elpi/coq-HOAS.elpi @@ -339,6 +339,10 @@ macro @redflags! F :- get-option "coq:redflags" F. % for whd & co macro @deprecated! Since Msg :- get-option "coq:deprecated" (pr Since Msg). +% both arguments are strings eg "cata, catb, catc" "Beware of foo." +macro @warn! Cats Msg :- + get-option "coq:warn" (pr Cats Msg). + macro @ltacfail! N :- get-option "ltac:fail" N. % retrocompatibility macro for Coq v8.10 diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 661b9720b..6f1ce60c2 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -333,7 +333,7 @@ type universe_decl_option = type options = { hoas_holes : hole_mapping option; local : bool option; - deprecation : Deprecation.t option; + user_warns : UserWarn.t option; primitive : bool option; failsafe : bool; (* don't fail, e.g. we are trying to print a term *) ppwidth : int; @@ -352,7 +352,7 @@ type options = { let default_options () = { hoas_holes = Some Verbatim; local = None; - deprecation = None; + user_warns = None; primitive = None; failsafe = false; ppwidth = Option.default 80 (Topfmt.get_margin ()); @@ -1127,6 +1127,12 @@ let get_options ~depth hyps state = let since = unspec2opt since |> empty2none in let note = unspec2opt note |> empty2none in Some { Deprecation.since; note } in + let warn = function + | None -> [] + | Some(cats,note) -> + let cats = unspec2opt cats |> empty2none in + let note = unspec2opt note |> empty2none in + Option.cata (fun note -> [UserWarn.make_warn ~note ?cats ()]) [] note in let get_universe_decl () = match API.Data.StrMap.find_opt "coq:udecl-cumul" map, API.Data.StrMap.find_opt "coq:udecl" map with | None, None -> NotUniversePolymorphic @@ -1154,7 +1160,12 @@ let get_options ~depth hyps state = | Some true -> Some Heuristic | Some false -> Some Verbatim end; local = locality @@ get_string_option "coq:locality"; - deprecation = deprecation @@ get_pair_option API.BuiltInData.string API.BuiltInData.string "coq:deprecation"; + user_warns = + begin + let depr = deprecation @@ get_pair_option API.BuiltInData.string API.BuiltInData.string "coq:deprecated" in + let warn = warn @@ get_pair_option API.BuiltInData.string API.BuiltInData.string "coq:warn" in + Some UserWarn.{ depr; warn } + end; primitive = get_bool_option "coq:primitive"; failsafe = false; ppwidth = ppwidth @@ get_int_option "coq:ppwidth"; diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index b96405847..afafe8a20 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -33,7 +33,7 @@ type universe_decl_option = type options = { hoas_holes : hole_mapping option; local : bool option; - deprecation : Deprecation.t option; + user_warns : UserWarn.t option; primitive : bool option; failsafe : bool; (* readback is resilient to illformed terms *) ppwidth : int; diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 044364107..83b61daf5 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2994,6 +2994,7 @@ Supported attributes: The term must begin with at least Nargs "fun" nodes whose domain is ignored, eg (fun _ _ x\ fun _ _ y\ app[global "add",x,y]). Supported attributes: - @deprecated! (default: not deprecated) +- @warn! (default: no warning) - @global! (default: false)|})))))), (fun name nargs term onlyparsing _ ~depth { env; options } _ -> grab_global_env "coq.notation.add-abbreviation" (fun state -> let sigma = get_sigma state in @@ -3036,7 +3037,7 @@ Supported attributes: let vars, nenv, env, body = strip_n_lambas nargs env term in let gbody = Coq_elpi_utils.detype env sigma body in let pat, _ = Notation_ops.notation_constr_of_glob_constr nenv gbody in - Abbreviation.declare_abbreviation ~local ~onlyparsing options.deprecation name (vars,pat); + Abbreviation.declare_abbreviation ~local ~onlyparsing options.user_warns name (vars,pat); let qname = Libnames.qualid_of_string (Id.to_string name) in match Nametab.locate_extended qname with | Globnames.TrueGlobal _ -> assert false