aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml8
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/declare.ml48
-rw-r--r--interp/declare.mli8
-rw-r--r--interp/deprecation.ml21
-rw-r--r--interp/deprecation.mli16
-rw-r--r--interp/impargs.ml89
-rw-r--r--interp/impargs.mli10
-rw-r--r--interp/implicit_quantifiers.ml27
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/notation.ml30
-rw-r--r--interp/notation.mli3
-rw-r--r--interp/syntax_def.ml78
-rw-r--r--interp/syntax_def.mli4
14 files changed, 170 insertions, 177 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 63c936fa81..ff0c06e705 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2434,10 +2434,8 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
let r = Retyping.relevance_of_type env sigma t in
let d = LocalAssum (make_annot na r,t) in
let impls =
- if k == Implicit then
- let na = match na with Name n -> Some n | Anonymous -> None in
- (ExplByPos (n, na), (true, true, true)) :: impls
- else impls
+ if k == Implicit then CAst.make (Some (na,true)) :: impls
+ else CAst.make None :: impls
in
(push_rel d env, sigma, d::params, succ n, impls)
| Some b ->
@@ -2446,7 +2444,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
let d = LocalDef (make_annot na r, c, t) in
(push_rel d env, sigma, d::params, n, impls))
(env,sigma,[],k+1,[]) (List.rev bl)
- in sigma, ((env, par), impls)
+ in sigma, ((env, par), List.rev impls)
let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
let int_env,bl = intern_context global_level env impl_env params in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 2e4d7479a9..450daea75c 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -61,10 +61,10 @@ type internalization_env = var_internalization_data Id.Map.t
val empty_internalization_env : internalization_env
val compute_internalization_data : env -> evar_map -> var_internalization_type ->
- types -> Impargs.manual_explicitation list -> var_internalization_data
+ types -> Impargs.manual_implicits -> var_internalization_data
val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type ->
- Id.t list -> types list -> Impargs.manual_explicitation list list ->
+ Id.t list -> types list -> Impargs.manual_implicits list ->
internalization_env
type ltac_sign = {
diff --git a/interp/declare.ml b/interp/declare.ml
index 7de92ded59..17de06ed57 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -42,7 +42,7 @@ type constant_obj = {
cst_locl : import_status;
}
-type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
+type constant_declaration = Evd.side_effects constant_entry * logical_kind
(* At load-time, the segment starting from the module name to the discharge *)
(* section (if Remark or Fact) is needed to access a construction *)
@@ -140,12 +140,12 @@ let register_constant kn kind local =
let register_side_effect (c, role) =
let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in
match role with
- | Subproof -> ()
- | Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
+ | None -> ()
+ | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|]
let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
- ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
+ ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
{ const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
const_entry_secctx = None;
const_entry_type = types;
@@ -154,7 +154,14 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
const_entry_feedback = None;
const_entry_inline_code = inline}
-let define_constant ?role ?(export_seff=false) id cd =
+let get_roles export eff =
+ let map c =
+ let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
+ (c, role)
+ in
+ List.map map export
+
+let define_constant ~side_effect ?(export_seff=false) id cd =
(* Logically define the constant and its subproofs, no libobject tampering *)
let is_poly de = match de.const_entry_universes with
| Monomorphic_entry _ -> false
@@ -168,26 +175,39 @@ let define_constant ?role ?(export_seff=false) id cd =
not de.const_entry_opaque ||
is_poly de ->
(* This globally defines the side-effects in the environment. *)
- let body, export = Global.export_private_constants ~in_section (Future.force de.const_entry_body) in
+ let body, eff = Future.force de.const_entry_body in
+ let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in
+ let export = get_roles export eff in
let de = { de with const_entry_body = Future.from_val (body, ()) } in
export, ConstantEntry (PureEntry, DefinitionEntry de)
- | _ -> [], ConstantEntry (EffectEntry, cd)
+ | DefinitionEntry de ->
+ let map (body, eff) = body, eff.Evd.seff_private in
+ let body = Future.chain de.const_entry_body map in
+ let de = { de with const_entry_body = body } in
+ [], ConstantEntry (EffectEntry, DefinitionEntry de)
+ | ParameterEntry _ | PrimitiveEntry _ as cd ->
+ [], ConstantEntry (PureEntry, cd)
in
- let kn, eff = Global.add_constant ?role ~in_section id decl in
+ let kn, eff = Global.add_constant ~side_effect ~in_section id decl in
kn, eff, export
let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) =
let () = check_exists id in
- let kn, _eff, export = define_constant ~export_seff id cd in
+ let kn, (), export = define_constant ~side_effect:PureEntry ~export_seff id cd in
(* Register the libobjects attached to the constants and its subproofs *)
let () = List.iter register_side_effect export in
let () = register_constant kn kind local in
kn
-let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) =
- let kn, eff, export = define_constant ~role id cd in
+let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) =
+ let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in
let () = assert (List.is_empty export) in
let () = register_constant kn kind local in
+ let seff_roles = match role with
+ | None -> Cmap.empty
+ | Some r -> Cmap.singleton kn r
+ in
+ let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
kn, eff
let declare_definition ?(internal=UserIndividualRequest)
@@ -201,7 +221,7 @@ let declare_definition ?(internal=UserIndividualRequest)
(** Declaration of section variables and local definitions *)
type section_variable_entry =
- | SectionLocalDef of Safe_typing.private_constants definition_entry
+ | SectionLocalDef of Evd.side_effects definition_entry
| SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -222,7 +242,9 @@ let cache_variable ((sp,_),o) =
| SectionLocalDef (de) ->
(* The body should already have been forced upstream because it is a
section-local definition, but it's not enforced by typing *)
- let ((body, uctx), eff) = Global.export_private_constants ~in_section:true (Future.force de.const_entry_body) in
+ let (body, eff) = Future.force de.const_entry_body in
+ let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in
+ let eff = get_roles export eff in
let () = List.iter register_side_effect eff in
let poly, univs = match de.const_entry_universes with
| Monomorphic_entry uctx -> false, uctx
diff --git a/interp/declare.mli b/interp/declare.mli
index 4120a82ca0..e2485d7cf0 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -23,7 +23,7 @@ open Decl_kinds
(** Declaration of local constructions (Variable/Hypothesis/Local) *)
type section_variable_entry =
- | SectionLocalDef of Safe_typing.private_constants definition_entry
+ | SectionLocalDef of Evd.side_effects definition_entry
| SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -33,7 +33,7 @@ val declare_variable : variable -> variable_declaration -> Libobject.object_name
(** Declaration of global constructions
i.e. Definition/Theorem/Axiom/Parameter/... *)
-type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
+type constant_declaration = Evd.side_effects constant_entry * logical_kind
type internal_flag =
| UserAutomaticRequest
@@ -44,7 +44,7 @@ type internal_flag =
val definition_entry : ?fix_exn:Future.fix_exn ->
?opaque:bool -> ?inline:bool -> ?types:types ->
?univs:Entries.universes_entry ->
- ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
+ ?eff:Evd.side_effects -> constr -> Evd.side_effects definition_entry
(** [declare_constant id cd] declares a global declaration
(constant/parameter) with name [id] in the current section; it returns
@@ -56,7 +56,7 @@ val declare_constant :
?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
val declare_private_constant :
- role:side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants
+ ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
val declare_definition :
?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
diff --git a/interp/deprecation.ml b/interp/deprecation.ml
new file mode 100644
index 0000000000..b6f0dceb89
--- /dev/null
+++ b/interp/deprecation.ml
@@ -0,0 +1,21 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+type t = { since : string option ; note : string option }
+
+let make ?since ?note () = { since ; note }
+
+let create_warning ~object_name ~warning_name name_printer =
+ let open Pp in
+ CWarnings.create ~name:warning_name ~category:"deprecated"
+ (fun (qid,depr) -> str object_name ++ spc () ++ name_printer qid ++
+ strbrk " is deprecated" ++
+ pr_opt (fun since -> str "since " ++ str since) depr.since ++
+ str "." ++ pr_opt (fun note -> str note) depr.note)
diff --git a/interp/deprecation.mli b/interp/deprecation.mli
new file mode 100644
index 0000000000..aab87c11a2
--- /dev/null
+++ b/interp/deprecation.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+type t = { since : string option ; note : string option }
+
+val make : ?since:string -> ?note:string -> unit -> t
+
+val create_warning : object_name:string -> warning_name:string ->
+ ('b -> Pp.t) -> ?loc:Loc.t -> 'b * t -> unit
diff --git a/interp/impargs.ml b/interp/impargs.ml
index f3cdd64633..112862da18 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,7 +20,6 @@ open Lib
open Libobject
open EConstr
open Reductionops
-open Constrexpr
open Namegen
module NamedDecl = Context.Named.Declaration
@@ -341,77 +340,30 @@ let rec prepare_implicits f = function
Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
| _::imps -> None :: prepare_implicits f imps
-(*
-If found, returns Some (x,(b,fi,fo)) and l with the entry removed,
-otherwise returns None and l unchanged.
- *)
-let assoc_by_pos k l =
- let rec aux = function
- (ExplByPos (k', x), b) :: tl when Int.equal k k' -> Some (x,b), tl
- | hd :: tl -> let (x, tl) = aux tl in x, hd :: tl
- | [] -> raise Not_found
- in try aux l with Not_found -> None, l
-
-let check_correct_manual_implicits autoimps l =
- List.iter (function
- | ExplByName id,(b,fi,forced) ->
- if not forced then
- user_err
- (str "Wrong or non-dependent implicit argument name: " ++ Id.print id ++ str ".")
- | ExplByPos (i,_id),_t ->
- if i<1 || i>List.length autoimps then
- user_err
- (str "Bad implicit argument number: " ++ int i ++ str ".")
- else
- user_err
- (str "Cannot set implicit argument number " ++ int i ++
- str ": it has no name.")) l
-
-(* Take a list l of explicitations, and map them to positions. *)
-let flatten_explicitations l autoimps =
- let rec aux k l = function
- | (Name id,_)::imps ->
- let value, l' =
- try
- let eq = Constrexpr_ops.explicitation_eq in
- let flags = List.assoc_f eq (ExplByName id) l in
- Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l
- with Not_found -> assoc_by_pos k l
- in value :: aux (k+1) l' imps
- | (Anonymous,_)::imps ->
- let value, l' = assoc_by_pos k l
- in value :: aux (k+1) l' imps
- | [] when List.is_empty l -> []
- | [] ->
- check_correct_manual_implicits autoimps l;
- []
- in aux 1 l autoimps
-
let set_manual_implicits flags enriching autoimps l =
- if not (List.distinct l) then
- user_err Pp.(str "Some parameters are referred more than once.");
(* Compare with automatic implicits to recover printing data and names *)
let rec merge k autoimps explimps = match autoimps, explimps with
| autoimp::autoimps, explimp::explimps ->
let imps' = merge (k+1) autoimps explimps in
- begin match autoimp, explimp with
- | (Name id,_), Some (_, (b, fi, _)) ->
- Some (id, Manual, (set_maximality imps' b, fi))
+ begin match autoimp, explimp.CAst.v with
+ | (Name id,_), Some (_,max) ->
+ Some (id, Manual, (set_maximality imps' max, true))
| (Name id,Some exp), None when enriching ->
Some (id, exp, (set_maximality imps' flags.maximal, true))
| (Name _,_), None -> None
- | (Anonymous,_), Some (Some id, (b, fi, true)) ->
- Some (id,Manual,(b,fi))
- | (Anonymous,_), Some (None, (b, fi, true)) ->
+ | (Anonymous,_), Some (Name id,max) ->
+ Some (id,Manual,(max,true))
+ | (Anonymous,_), Some (Anonymous,max) ->
let id = Id.of_string ("arg_" ^ string_of_int k) in
- Some (id,Manual,(b,fi))
- | (Anonymous,_), Some (_, (_, _, false)) -> None
+ Some (id,Manual,(max,true))
| (Anonymous,_), None -> None
end :: imps'
| [], [] -> []
- (* flatten_explicitations returns a list of the same length as autoimps *)
- | _ -> assert false
- in merge 1 autoimps (flatten_explicitations l autoimps)
+ | [], _ -> assert false
+ (* possibly more automatic than manual implicit arguments n
+ when the conclusion is an unfoldable constant *)
+ | autoimps, [] -> merge k autoimps [CAst.make None]
+ in merge 1 autoimps l
let compute_semi_auto_implicits env sigma f t =
if not f.auto then [DefaultImpArgs, []]
@@ -642,9 +594,7 @@ let declare_mib_implicits kn =
(inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
(* Declare manual implicits *)
-type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
-
-type manual_implicits = manual_explicitation list
+type manual_implicits = (Name.t * bool) option CAst.t list
let compute_implicits_with_manual env sigma typ enriching l =
let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
@@ -669,8 +619,6 @@ let projection_implicits env p impls =
CList.skipn_at_least npars impls
let declare_manual_implicits local ref ?enriching l =
- assert (List.for_all (fun (_, (max, fi, fu)) -> fi && fu) l);
- assert (List.for_all (fun (ex, _) -> match ex with ExplByPos (_,_) -> true | _ -> false) l);
let flags = !implicit_args in
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -685,9 +633,8 @@ let declare_manual_implicits local ref ?enriching l =
in add_anonymous_leaf (inImplicits (req,[ref,l]))
let maybe_declare_manual_implicits local ref ?enriching l =
- match l with
- | [] -> ()
- | _ -> declare_manual_implicits local ref ?enriching l
+ if List.exists (fun x -> x.CAst.v <> None) l then
+ declare_manual_implicits local ref ?enriching l
(* TODO: either turn these warnings on and document them, or handle these cases sensibly *)
@@ -750,12 +697,6 @@ let extract_impargs_data impls =
| [] -> [] in
aux 0 impls
-let lift_implicits n =
- List.map (fun x ->
- match fst x with
- ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
- | _ -> x)
-
let make_implicits_list l = [DefaultImpArgs, l]
let rec drop_first_implicits p l =
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 1099074c63..92b6bdd406 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -84,13 +84,7 @@ val force_inference_of : implicit_status -> bool
val positions_of_implicits : implicits_list -> int list
-(** A [manual_explicitation] is a tuple of a positional or named explicitation with
- maximal insertion, force inference and force usage flags. Forcing usage makes
- the argument implicit even if the automatic inference considers it not inferable. *)
-type manual_explicitation = Constrexpr.explicitation *
- (maximal_insertion * force_inference * bool)
-
-type manual_implicits = manual_explicitation list
+type manual_implicits = (Name.t * bool) option CAst.t list
val compute_implicits_with_manual : env -> Evd.evar_map -> types -> bool ->
manual_implicits -> implicit_status list
@@ -131,8 +125,6 @@ val implicits_of_global : GlobRef.t -> implicits_list list
val extract_impargs_data :
implicits_list list -> ((int * int) option * implicit_status list) list
-val lift_implicits : int -> manual_implicits -> manual_implicits
-
val make_implicits_list : implicit_status list -> implicits_list list
val drop_first_implicits : int -> implicits_list -> implicits_list
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 32290f0430..d7bae6b3fd 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -203,32 +203,23 @@ let warn_ignoring_implicit_status =
Name.print na ++ strbrk " and following binders")
let implicits_of_glob_constr ?(with_products=true) l =
- let add_impl i na bk l = match bk with
- | Implicit ->
- let name =
- match na with
- | Name id -> Some id
- | Anonymous -> None
- in
- (ExplByPos (i, name), (true, true, true)) :: l
- | _ -> l
+ let add_impl ?loc na bk l = match bk with
+ | Implicit -> CAst.make ?loc (Some (na,true)) :: l
+ | _ -> CAst.make ?loc None :: l
in
- let rec aux i c =
- let abs na bk b =
- add_impl i na bk (aux (succ i) b)
- in
+ let rec aux c =
match DAst.get c with
| GProd (na, bk, t, b) ->
- if with_products then abs na bk b
+ if with_products then add_impl na bk (aux b)
else
let () = match bk with
| Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
| _ -> ()
in []
- | GLambda (na, bk, t, b) -> abs na bk b
- | GLetIn (na, b, t, c) -> aux i c
+ | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b)
+ | GLetIn (na, b, t, c) -> aux c
| GRec (fix_kind, nas, args, tys, bds) ->
let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
- List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
+ List.fold_right (fun (na,bk,t,_) l -> add_impl ?loc:c.CAst.loc na bk l) args.(nb) (aux bds.(nb))
| _ -> []
- in aux 1 l
+ in aux l
diff --git a/interp/interp.mllib b/interp/interp.mllib
index b65a171ef9..52978a2ab6 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,4 @@
+Deprecation
NumTok
Constrexpr
Tactypes
diff --git a/interp/notation.ml b/interp/notation.ml
index a7bac96d31..cc06d5abfc 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -72,6 +72,7 @@ type notation_location = (DirPath.t * DirPath.t) * string
type notation_data = {
not_interp : interpretation;
not_location : notation_location;
+ not_deprecation : Deprecation.t option;
}
type scope = {
@@ -1095,7 +1096,7 @@ let warn_notation_overridden =
str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
++ strbrk "was already used" ++ which_scope ++ str ".")
-let declare_notation_interpretation ntn scopt pat df ~onlyprint =
+let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation =
let scope = match scopt with Some s -> s | None -> default_scope in
let sc = find_scope scope in
if not onlyprint then begin
@@ -1109,6 +1110,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
let notdata = {
not_interp = pat;
not_location = df;
+ not_deprecation = deprecation;
} in
let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in
scope_map := String.Map.add scope sc !scope_map
@@ -1125,10 +1127,10 @@ let declare_uninterpretation rule (metas,c as pat) =
let rec find_interpretation ntn find = function
| [] -> raise Not_found
| Scope scope :: scopes ->
- (try let (pat,df) = find scope in pat,(df,Some scope)
+ (try let n = find scope in (n,Some scope)
with Not_found -> find_interpretation ntn find scopes)
| SingleNotation ntn'::scopes when notation_eq ntn' ntn ->
- (try let (pat,df) = find default_scope in pat,(df,None)
+ (try let n = find default_scope in (n,None)
with Not_found ->
(* e.g. because single notation only for constr, not cases_pattern *)
find_interpretation ntn find scopes)
@@ -1136,8 +1138,7 @@ let rec find_interpretation ntn find = function
find_interpretation ntn find scopes
let find_notation ntn sc =
- let n = NotationMap.find ntn (find_scope sc).notations in
- (n.not_interp, n.not_location)
+ NotationMap.find ntn (find_scope sc).notations
let notation_of_prim_token = function
| Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n
@@ -1147,7 +1148,9 @@ let notation_of_prim_token = function
let find_prim_token check_allowed ?loc p sc =
(* Try for a user-defined numerical notation *)
try
- let (_,c),df = find_notation (notation_of_prim_token p) sc in
+ let n = find_notation (notation_of_prim_token p) sc in
+ let (_,c) = n.not_interp in
+ let df = n.not_location in
let pat = Notation_ops.glob_constr_of_notation_constr ?loc c in
check_allowed pat;
pat, df
@@ -1167,7 +1170,9 @@ let find_prim_token check_allowed ?loc p sc =
let interp_prim_token_gen ?loc g p local_scopes =
let scopes = make_current_scopes local_scopes in
let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in
- try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes
+ try
+ let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in
+ pat, (loc,sc)
with Not_found ->
user_err ?loc ~hdr:"interp_prim_token"
((match p with
@@ -1192,11 +1197,18 @@ let rec check_allowed_ref_in_pat looked_for = DAst.(with_val (function
let interp_prim_token_cases_pattern_expr ?loc looked_for p =
interp_prim_token_gen ?loc (check_allowed_ref_in_pat looked_for) p
+let warn_deprecated_notation =
+ Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-notation"
+ pr_notation
+
let interp_notation ?loc ntn local_scopes =
let scopes = make_current_scopes local_scopes in
- try find_interpretation ntn (find_notation ntn) scopes
+ try
+ let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in
+ Option.iter (fun d -> warn_deprecated_notation (ntn,d)) n.not_deprecation;
+ n.not_interp, (n.not_location, sc)
with Not_found ->
- user_err ?loc
+ user_err ?loc
(str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
let uninterp_notations c =
diff --git a/interp/notation.mli b/interp/notation.mli
index a67948a778..b32561d908 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -217,7 +217,8 @@ type interp_rule =
| SynDefRule of KerName.t
val declare_notation_interpretation : notation -> scope_name option ->
- interpretation -> notation_location -> onlyprint:bool -> unit
+ interpretation -> notation_location -> onlyprint:bool ->
+ Deprecation.t option -> unit
val declare_uninterpretation : interp_rule -> interpretation -> unit
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a7e1de736c..8df04187f1 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -19,20 +19,24 @@ open Notation_term
(* Syntactic definitions. *)
-type version = Flags.compat_version option
+type syndef =
+ { syndef_pattern : interpretation;
+ syndef_onlyparsing : bool;
+ syndef_deprecation : Deprecation.t option;
+ }
let syntax_table =
- Summary.ref (KNmap.empty : (interpretation*version) KNmap.t)
- ~name:"SYNTAXCONSTANT"
+ Summary.ref (KNmap.empty : syndef KNmap.t)
+ ~name:"SYNDEFS"
-let add_syntax_constant kn c onlyparse =
- syntax_table := KNmap.add kn (c,onlyparse) !syntax_table
+let add_syntax_constant kn syndef =
+ syntax_table := KNmap.add kn syndef !syntax_table
-let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
+let load_syntax_constant i ((sp,kn),(_local,syndef)) =
if Nametab.exists_cci sp then
user_err ~hdr:"cache_syntax_constant"
(Id.print (basename sp) ++ str " already exists");
- add_syntax_constant kn pat onlyparse;
+ add_syntax_constant kn syndef;
Nametab.push_syndef (Nametab.Until i) sp kn
let is_alias_of_already_visible_name sp = function
@@ -42,30 +46,29 @@ let is_alias_of_already_visible_name sp = function
| _ ->
false
-let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
+let open_syntax_constant i ((sp,kn),(_local,syndef)) =
+ let pat = syndef.syndef_pattern in
if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
Nametab.push_syndef (Nametab.Exactly i) sp kn;
- match onlyparse with
- | None ->
+ if not syndef.syndef_onlyparsing then
(* Redeclare it to be used as (short) name in case an other (distfix)
notation was declared in between *)
Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
- | _ -> ()
end
let cache_syntax_constant d =
load_syntax_constant 1 d;
open_syntax_constant 1 d
-let subst_syntax_constant (subst,(local,pat,onlyparse)) =
- (local,Notation_ops.subst_interpretation subst pat,onlyparse)
+let subst_syntax_constant (subst,(local,syndef)) =
+ let syndef_pattern = Notation_ops.subst_interpretation subst syndef.syndef_pattern in
+ (local, { syndef with syndef_pattern })
-let classify_syntax_constant (local,_,_ as o) =
+let classify_syntax_constant (local,_ as o) =
if local then Dispose else Substitute o
-let in_syntax_constant
- : bool * interpretation * Flags.compat_version option -> obj =
- declare_object {(default_object "SYNTAXCONSTANT") with
+let in_syntax_constant : (bool * syndef) -> obj =
+ declare_object {(default_object "SYNDEF") with
cache_function = cache_syntax_constant;
load_function = load_syntax_constant;
open_function = open_syntax_constant;
@@ -79,36 +82,31 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr
let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac)
let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
-let declare_syntactic_definition local id onlyparse pat =
- let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
-
-let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)
-
-let pr_compat_warning (kn, def, v) =
- let pp_def = match def with
- | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r
- | _ -> strbrk " is a compatibility notation"
+let declare_syntactic_definition ~local deprecation id ~onlyparsing pat =
+ let syndef =
+ { syndef_pattern = in_pat pat;
+ syndef_onlyparsing = onlyparsing;
+ syndef_deprecation = deprecation;
+ }
in
- pr_syndef kn ++ pp_def
+ let _ = add_leaf id (in_syntax_constant (local,syndef)) in ()
-let warn_compatibility_notation =
- CWarnings.(create ~name:"compatibility-notation"
- ~category:"deprecated" ~default:Enabled pr_compat_warning)
+let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)
-let verbose_compat ?loc kn def = function
- | Some v when Flags.version_strictly_greater v ->
- warn_compatibility_notation ?loc (kn, def, v)
- | _ -> ()
+let warn_deprecated_syntactic_definition =
+ Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-syntactic-definition"
+ pr_syndef
let search_syntactic_definition ?loc kn =
- let pat,v = KNmap.find kn !syntax_table in
- let def = out_pat pat in
- verbose_compat ?loc kn def v;
+ let syndef = KNmap.find kn !syntax_table in
+ let def = out_pat syndef.syndef_pattern in
+ Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
def
let search_filtered_syntactic_definition ?loc filter kn =
- let pat,v = KNmap.find kn !syntax_table in
- let def = out_pat pat in
+ let syndef = KNmap.find kn !syntax_table in
+ let def = out_pat syndef.syndef_pattern in
let res = filter def in
- (match res with Some _ -> verbose_compat ?loc kn def v | None -> ());
+ if Option.has_some res then
+ Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
res
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 77873f8f67..e6e3b9cffa 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -15,8 +15,8 @@ open Notation_term
type syndef_interpretation = (Id.t * subscopes) list * notation_constr
-val declare_syntactic_definition : bool -> Id.t ->
- Flags.compat_version option -> syndef_interpretation -> unit
+val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t ->
+ onlyparsing:bool -> syndef_interpretation -> unit
val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 13:06:36 +0000