aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/attributes.ml148
-rw-r--r--vernac/attributes.mli25
-rw-r--r--vernac/comInductive.ml31
-rw-r--r--vernac/comInductive.mli13
-rw-r--r--vernac/g_vernac.mlg45
-rw-r--r--vernac/himsg.ml6
-rw-r--r--vernac/metasyntax.ml74
-rw-r--r--vernac/ppvernac.ml33
-rw-r--r--vernac/record.ml42
-rw-r--r--vernac/record.mli2
-rw-r--r--vernac/vernacentries.ml25
-rw-r--r--vernac/vernacexpr.ml5
12 files changed, 313 insertions, 136 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index efba6d332a..fdaeedef8c 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -11,13 +11,29 @@
open CErrors
(** The type of parsing attribute data *)
+type vernac_flag_type =
+ | FlagIdent of string
+ | FlagString of string
+
type vernac_flags = vernac_flag list
and vernac_flag = string * vernac_flag_value
and vernac_flag_value =
| VernacFlagEmpty
- | VernacFlagLeaf of string
+ | VernacFlagLeaf of vernac_flag_type
| VernacFlagList of vernac_flags
+let pr_vernac_flag_leaf = function
+ | FlagIdent b -> Pp.str b
+ | FlagString s -> Pp.(quote (str s))
+
+let rec pr_vernac_flag_value = let open Pp in function
+ | VernacFlagEmpty -> mt ()
+ | VernacFlagLeaf l -> str "=" ++ pr_vernac_flag_leaf l
+ | VernacFlagList s -> surround (prlist_with_sep pr_comma pr_vernac_flag s)
+and pr_vernac_flag (s, arguments) =
+ let open Pp in
+ str s ++ (pr_vernac_flag_value arguments)
+
let warn_unsupported_attributes =
CWarnings.create ~name:"unsupported-attributes" ~category:"parsing" ~default:CWarnings.AsError
(fun atts ->
@@ -105,16 +121,82 @@ let single_key_parser ~name ~key v prev args =
assert_once ~name prev;
v
-let bool_attribute ~name ~on ~off : bool option attribute =
- attribute_of_list [(on, single_key_parser ~name ~key:on true);
- (off, single_key_parser ~name ~key:off false)]
+let pr_possible_values ~values =
+ Pp.(str "{" ++ prlist_with_sep pr_comma str (List.map fst values) ++ str "}")
+
+(** [key_value_attribute ~key ~default ~values] parses a attribute [key=value]
+ with possible [key] [value] in [values], [default] is for compatibility for users
+ doing [qualif(key)] which is parsed as [qualif(key=default)] *)
+let key_value_attribute ~key ~default ~(values : (string * 'a) list) : 'a option attribute =
+ let parser = function
+ | Some v ->
+ CErrors.user_err Pp.(str "key '" ++ str key ++ str "' has been already set.")
+ | None ->
+ begin function
+ | VernacFlagLeaf (FlagIdent b) ->
+ begin match CList.assoc_f String.equal b values with
+ | exception Not_found ->
+ CErrors.user_err
+ Pp.(str "Invalid value '" ++ str b ++ str "' for key " ++ str key ++ fnl () ++
+ str "use one of " ++ pr_possible_values ~values)
+ | value -> value
+ end
+ | VernacFlagEmpty ->
+ default
+ | err ->
+ CErrors.user_err
+ Pp.(str "Invalid syntax " ++ pr_vernac_flag (key, err) ++ str ", try "
+ ++ str key ++ str "=" ++ pr_possible_values ~values ++ str " instead.")
+ end
+ in
+ attribute_of_list [key, parser]
+
+let bool_attribute ~name : bool option attribute =
+ let values = ["yes", true; "no", false] in
+ key_value_attribute ~key:name ~default:true ~values
+
+let legacy_bool_attribute ~name ~on ~off : bool option attribute =
+ attribute_of_list
+ [(on, single_key_parser ~name ~key:on true);
+ (off, single_key_parser ~name ~key:off false)]
+
+(* important note: we use on as the default for the new bool_attribute ! *)
+let deprecated_bool_attribute_warning =
+ CWarnings.create
+ ~name:"deprecated-attribute-syntax"
+ ~category:"parsing"
+ ~default:CWarnings.Enabled
+ (fun name ->
+ Pp.(str "Syntax for switching off boolean attributes has been updated, use " ++ str name ++ str "=no instead."))
+
+let deprecated_bool_attribute ~name ~on ~off : bool option attribute =
+ bool_attribute ~name:on ++ legacy_bool_attribute ~name ~on ~off |> map (function
+ | None, None ->
+ None
+ | None, Some v ->
+ deprecated_bool_attribute_warning name;
+ Some v
+ | Some v, None -> Some v
+ | Some v1, Some v2 ->
+ CErrors.user_err
+ Pp.(str "attribute " ++ str name ++
+ str ": cannot specify legacy and modern syntax at the same time.")
+ )
(* Variant of the [bool] attribute with only two values (bool has three). *)
let get_bool_value ~key ~default =
function
| VernacFlagEmpty -> default
- | VernacFlagList [ "true", VernacFlagEmpty ] -> true
- | VernacFlagList [ "false", VernacFlagEmpty ] -> false
+ | VernacFlagList [ "true", VernacFlagEmpty ] ->
+ deprecated_bool_attribute_warning key;
+ true
+ | VernacFlagList [ "false", VernacFlagEmpty ] ->
+ deprecated_bool_attribute_warning key;
+ false
+ | VernacFlagLeaf (FlagIdent "yes") ->
+ true
+ | VernacFlagLeaf (FlagIdent "no") ->
+ false
| _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.")
let enable_attribute ~key ~default : bool attribute =
@@ -161,18 +243,37 @@ let () = let open Goptions in
let program =
enable_attribute ~key:"program" ~default:(fun () -> !program_mode)
-let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
-
-let option_locality =
+(* This is a bit complex as the grammar in g_vernac.mlg doesn't
+ distingish between the boolean and ternary case.*)
+let option_locality_parser =
let name = "Locality" in
attribute_of_list [
- ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal);
- ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal);
- ("export", single_key_parser ~name ~key:"export" Goptions.OptExport);
- ] >>= function
+ ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal)
+ ; ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal)
+ ; ("export", single_key_parser ~name ~key:"export" Goptions.OptExport)
+ ]
+
+let option_locality =
+ option_locality_parser >>= function
| None -> return Goptions.OptDefault
| Some l -> return l
+(* locality is supposed to be true when local, false when global *)
+let locality =
+ let locality_to_bool =
+ function
+ | Goptions.OptLocal ->
+ true
+ | Goptions.OptGlobal ->
+ false
+ | Goptions.OptExport ->
+ CErrors.user_err Pp.(str "export attribute not supported here")
+ | Goptions.OptDefault ->
+ CErrors.user_err Pp.(str "default attribute not supported here")
+ in
+ option_locality_parser >>= function l ->
+ return (Option.map locality_to_bool l)
+
let ukey = "universes"
let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
@@ -188,12 +289,17 @@ let is_universe_polymorphism =
fun () -> !b
let polymorphic_base =
- bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" >>= function
+ deprecated_bool_attribute
+ ~name:"Polymorphism"
+ ~on:"polymorphic" ~off:"monomorphic" >>= function
| Some b -> return b
| None -> return (is_universe_polymorphism())
let template =
- qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate")
+ qualify_attribute ukey
+ (deprecated_bool_attribute
+ ~name:"Template"
+ ~on:"template" ~off:"notemplate")
let polymorphic =
qualify_attribute ukey polymorphic_base
@@ -201,12 +307,12 @@ let polymorphic =
let deprecation_parser : Deprecation.t key_parser = fun orig args ->
assert_once ~name:"deprecation" orig;
match args with
- | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
- | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
+ | VernacFlagList [ "since", VernacFlagLeaf (FlagString since) ; "note", VernacFlagLeaf (FlagString note) ]
+ | VernacFlagList [ "note", VernacFlagLeaf (FlagString note) ; "since", VernacFlagLeaf (FlagString since) ] ->
Deprecation.make ~since ~note ()
- | VernacFlagList [ "since", VernacFlagLeaf since ] ->
+ | VernacFlagList [ "since", VernacFlagLeaf (FlagString since) ] ->
Deprecation.make ~since ()
- | VernacFlagList [ "note", VernacFlagLeaf note ] ->
+ | VernacFlagList [ "note", VernacFlagLeaf (FlagString note) ] ->
Deprecation.make ~note ()
| _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
@@ -218,7 +324,7 @@ let only_polymorphism atts = parse polymorphic atts
let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
-let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
+let vernac_monomorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagLeaf (FlagIdent "no")]
let canonical_field =
enable_attribute ~key:"canonical" ~default:(fun () -> true)
@@ -228,7 +334,7 @@ let canonical_instance =
let uses_parser : string key_parser = fun orig args ->
assert_once ~name:"using" orig;
match args with
- | VernacFlagLeaf str -> str
+ | VernacFlagLeaf (FlagString str) -> str
| _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute")
let using = attribute_of_list ["using",uses_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 1969665082..03a14a03ff 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -9,13 +9,19 @@
(************************************************************************)
(** The type of parsing attribute data *)
+type vernac_flag_type =
+ | FlagIdent of string
+ | FlagString of string
+
type vernac_flags = vernac_flag list
and vernac_flag = string * vernac_flag_value
and vernac_flag_value =
| VernacFlagEmpty
- | VernacFlagLeaf of string
+ | VernacFlagLeaf of vernac_flag_type
| VernacFlagList of vernac_flags
+val pr_vernac_flag : vernac_flag -> Pp.t
+
type +'a attribute
(** The type of attributes. When parsing attributes if an ['a
attribute] is present then an ['a] value will be produced.
@@ -82,10 +88,19 @@ val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute
(** Make an attribute from a list of key parsers together with their
associated key. *)
-val bool_attribute : name:string -> on:string -> off:string -> bool option attribute
-(** Define boolean attribute [name] with value [true] when [on] is
- provided and [false] when [off] is provided. The attribute may only
- be set once for a command. *)
+(** Define boolean attribute [name], of the form [name={yes,no}]. The
+ attribute may only be set once for a command. *)
+val bool_attribute : name:string -> bool option attribute
+
+val deprecated_bool_attribute
+ : name:string
+ -> on:string
+ -> off:string
+ -> bool option attribute
+(** Define boolean attribute [name] with will be set when [on] is
+ provided and unset when [off] is provided. The attribute may only
+ be set once for a command; this attribute both accepts the old [on]
+ [off] syntax and new attribute syntax [on=yes] [on=no] *)
val qualify_attribute : string -> 'a attribute -> 'a attribute
(** [qualified_attribute qual att] treats [#[qual(atts)]] like [att]
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index bb26ce652e..597e55a39e 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -367,7 +367,26 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
Evd.restrict_universe_context sigma uvars
-let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
+let check_trivial_variances variances =
+ Array.iter (function
+ | None | Some Univ.Variance.Invariant -> ()
+ | Some _ ->
+ CErrors.user_err
+ Pp.(strbrk "Universe variance was specified but this inductive will not be cumulative."))
+ variances
+
+let variance_of_entry ~cumulative ~variances uctx =
+ match uctx with
+ | Monomorphic_entry _ -> check_trivial_variances variances; None
+ | Polymorphic_entry (nas,_) ->
+ if not cumulative then begin check_trivial_variances variances; None end
+ else
+ let lvs = Array.length variances in
+ let lus = Array.length nas in
+ assert (lvs <= lus);
+ Some (Array.append variances (Array.make (lus - lvs) None))
+
+let interp_mutual_inductive_constr ~sigma ~template ~udecl ~variances ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
(* Compute renewed arities *)
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
@@ -429,13 +448,13 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
mind_entry_private = if private_ind then Some false else None;
mind_entry_universes = uctx;
mind_entry_template = is_template;
- mind_entry_cumulative = poly && cumulative;
+ mind_entry_variance = variance_of_entry ~cumulative ~variances uctx;
}
in
mind_ent, Evd.universe_binders sigma
let interp_params env udecl uparamsl paramsl =
- let sigma, udecl = interp_univ_decl_opt env udecl in
+ let sigma, udecl, variances = interp_cumul_univ_decl_opt env udecl in
let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
interp_context_evars ~program_mode:false env sigma uparamsl in
let sigma, (impls, ((env_params, ctx_params), userimpls)) =
@@ -443,7 +462,7 @@ let interp_params env udecl uparamsl paramsl =
in
(* Names of parameters as arguments of the inductive type (defs removed) *)
sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
- userimpls, useruimpls, impls, udecl)
+ userimpls, useruimpls, impls, udecl, variances)
(* When a hole remains for a param, pretend the param is uniform and
do the unification.
@@ -485,7 +504,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
(* In case of template polymorphism, we need to compute more constraints *)
let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
- let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl) =
+ let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl, variances) =
interp_params env0 udecl uparamsl paramsl
in
@@ -563,7 +582,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
userimpls @ impls) cimpls)
indimpls cimpls
in
- let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
+ let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~variances ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
(mie, pl, impls)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 91e8f609d5..8bce884ba4 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -22,7 +22,7 @@ type uniform_inductive_flag =
val do_mutual_inductive
: template:bool option
- -> universe_decl_expr option
+ -> cumul_univ_decl_expr option
-> (one_inductive_expr * decl_notation list) list
-> cumulative:bool
-> poly:bool
@@ -45,6 +45,7 @@ val interp_mutual_inductive_constr
: sigma:Evd.evar_map
-> template:bool option
-> udecl:UState.universe_decl
+ -> variances:Entries.variance_entry
-> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list
-> indnames:Names.Id.t list
-> arities:EConstr.t list
@@ -86,3 +87,13 @@ val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:
(** [nparams] is the number of parameters which aren't treated as
uniform, ie the length of params (including letins) where the env
is [uniform params, inductives, params, binders]. *)
+
+val variance_of_entry
+ : cumulative:bool
+ -> variances:Entries.variance_entry
+ -> Entries.universes_entry
+ -> Entries.variance_entry option
+(** Will return None if non-cumulative, and resize if there are more
+ universes than originally specified.
+ If monomorphic, [cumulative] is treated as [false].
+*)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1c80d71ea5..116cfc6413 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -119,7 +119,8 @@ GRAMMAR EXTEND Gram
]
;
attr_value:
- [ [ "=" ; v = string -> { VernacFlagLeaf v }
+ [ [ "=" ; v = string -> { VernacFlagLeaf (FlagString v) }
+ | "=" ; v = IDENT -> { VernacFlagLeaf (FlagIdent v) }
| "(" ; a = attribute_list ; ")" -> { VernacFlagList a }
| -> { VernacFlagEmpty } ]
]
@@ -136,7 +137,7 @@ GRAMMAR EXTEND Gram
| IDENT "Cumulative" ->
{ ("universes", VernacFlagList ["cumulative", VernacFlagEmpty]) }
| IDENT "NonCumulative" ->
- { ("universes", VernacFlagList ["noncumulative", VernacFlagEmpty]) }
+ { ("universes", VernacFlagList ["cumulative", VernacFlagLeaf (FlagIdent "no")]) }
| IDENT "Private" ->
{ ("private", VernacFlagList ["matching", VernacFlagEmpty]) }
| IDENT "Program" ->
@@ -194,6 +195,12 @@ let lname_of_lident : lident -> lname =
let name_of_ident_decl : ident_decl -> name_decl =
on_fst lname_of_lident
+let test_variance_ident =
+ let open Pcoq.Lookahead in
+ to_entry "test_variance_ident" begin
+ lk_kws ["=";"+";"*"] >> lk_ident
+ end
+
}
(* Gallina declarations *)
@@ -283,7 +290,7 @@ GRAMMAR EXTEND Gram
[ [ l = universe_name; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ];
r = universe_name -> { (l, ord, r) } ] ]
;
- univ_decl :
+ univ_decl:
[ [ "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) }
@@ -296,10 +303,40 @@ GRAMMAR EXTEND Gram
univdecl_extensible_constraints = snd cs } }
] ]
;
+ variance:
+ [ [ "+" -> { Univ.Variance.Covariant }
+ | "=" -> { Univ.Variance.Invariant }
+ | "*" -> { Univ.Variance.Irrelevant }
+ ] ]
+ ;
+ variance_identref:
+ [ [ id = identref -> { (id, None) }
+ | test_variance_ident; v = variance; id = identref -> { (id, Some v) }
+ (* We need this test to help the parser avoid the conflict
+ between "+" before ident (covariance) and trailing "+" (extra univs allowed) *)
+ ] ]
+ ;
+ cumul_univ_decl:
+ [ [ "@{" ; l = LIST0 variance_identref; ext = [ "+" -> { true } | -> { false } ];
+ cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
+ ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) }
+ | ext = [ "}" -> { true } | bar_cbrace -> { false } ] -> { ([], ext) } ]
+ ->
+ { let open UState in
+ { univdecl_instance = l;
+ univdecl_extensible_instance = ext;
+ univdecl_constraints = fst cs;
+ univdecl_extensible_constraints = snd cs } }
+ ] ]
+ ;
ident_decl:
[ [ i = identref; l = OPT univ_decl -> { (i, l) }
] ]
;
+ cumul_ident_decl:
+ [ [ i = identref; l = OPT cumul_univ_decl -> { (i, l) }
+ ] ]
+ ;
finite_token:
[ [ IDENT "Inductive" -> { Inductive_kw }
| IDENT "CoInductive" -> { CoInductive }
@@ -345,7 +382,7 @@ GRAMMAR EXTEND Gram
| -> { RecordDecl (None, []) } ] ]
;
inductive_definition:
- [ [ oc = opt_coercion; id = ident_decl; indpar = binders;
+ [ [ oc = opt_coercion; id = cumul_ident_decl; indpar = binders;
extrapar = OPT [ "|"; p = binders -> { p } ];
c = OPT [ ":"; c = lconstr -> { c } ];
lc=opt_constructors_or_fields; ntn = decl_notations ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index bef9e29ac2..9d86ea90e6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -744,6 +744,11 @@ let explain_bad_relevance env =
let explain_bad_invert env =
strbrk "Bad case inversion (maybe a bugged tactic)."
+let explain_bad_variance env sigma ~lev ~expected ~actual =
+ str "Incorrect variance for universe " ++ Termops.pr_evd_level sigma lev ++
+ str": expected " ++ Univ.Variance.pr expected ++
+ str " but cannot be less restrictive than " ++ Univ.Variance.pr actual ++ str "."
+
let explain_type_error env sigma err =
let env = make_all_name_different env sigma in
match err with
@@ -788,6 +793,7 @@ let explain_type_error env sigma err =
| DisallowedSProp -> explain_disallowed_sprop ()
| BadRelevance -> explain_bad_relevance env
| BadInvert -> explain_bad_invert env
+ | BadVariance {lev;expected;actual} -> explain_bad_variance env sigma ~lev ~expected ~actual
let pr_position (cl,pos) =
let clpos = match cl with
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8477870cb4..dc2b2e889e 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -194,52 +194,6 @@ let parse_format ({CAst.loc;v=str} : lstring) =
(***********************)
(* Analyzing notations *)
-(* Interpret notations with a recursive component *)
-
-let out_nt = function NonTerminal x -> x | _ -> assert false
-
-let msg_expected_form_of_recursive_notation =
- "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"."
-
-let rec find_pattern nt xl = function
- | Break n as x :: l, Break n' :: l' when Int.equal n n' ->
- find_pattern nt (x::xl) (l,l')
- | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' ->
- find_pattern nt (x::xl) (l,l')
- | [], NonTerminal x' :: l' ->
- (out_nt nt,x',List.rev xl),l'
- | _, Break s :: _ | Break s :: _, _ ->
- user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side."))
- | _, Terminal s :: _ | Terminal s :: _, _ ->
- user_err ~hdr:"Metasyntax.find_pattern"
- (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
- | _, [] ->
- user_err Pp.(str msg_expected_form_of_recursive_notation)
- | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
- anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.")
-
-let rec interp_list_parser hd = function
- | [] -> [], List.rev hd
- | NonTerminal id :: tl when Id.equal id ldots_var ->
- if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation);
- let hd = List.rev hd in
- let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
- let xyl,tl'' = interp_list_parser [] tl' in
- (* We remember each pair of variable denoting a recursive part to *)
- (* remove the second copy of it afterwards *)
- (x,y)::xyl, SProdList (x,sl) :: tl''
- | (Terminal _ | Break _) as s :: tl ->
- if List.is_empty hd then
- let yl,tl' = interp_list_parser [] tl in
- yl, s :: tl'
- else
- interp_list_parser (s::hd) tl
- | NonTerminal _ as x :: tl ->
- let xyl,tl' = interp_list_parser [x] tl in
- xyl, List.rev_append hd tl'
- | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.")
-
-
(* Find non-terminal tokens of notation *)
(* To protect alphabetic tokens and quotes from being seen as variables *)
@@ -256,24 +210,16 @@ let is_numeral_in_constr entry symbs =
| _ ->
false
-let rec get_notation_vars onlyprint = function
- | [] -> []
- | NonTerminal id :: sl ->
- let vars = get_notation_vars onlyprint sl in
- if Id.equal id ldots_var then vars else
- (* don't check for nonlinearity if printing only, see Bug 5526 *)
- if not onlyprint && Id.List.mem id vars then
- user_err ~hdr:"Metasyntax.get_notation_vars"
- (str "Variable " ++ Id.print id ++ str " occurs more than once.")
- else id::vars
- | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl
- | SProdList _ :: _ -> assert false
-
-let analyze_notation_tokens ~onlyprint ntn =
- let l = decompose_raw_notation ntn in
- let vars = get_notation_vars onlyprint l in
- let recvars,l = interp_list_parser [] l in
- recvars, List.subtract Id.equal vars (List.map snd recvars), l
+let analyze_notation_tokens ~onlyprint df =
+ let (recvars,mainvars,symbols as res) = decompose_raw_notation df in
+ (* don't check for nonlinearity if printing only, see Bug 5526 *)
+ (if not onlyprint then
+ match List.duplicates Id.equal (mainvars @ List.map snd recvars) with
+ | id :: _ ->
+ user_err ~hdr:"Metasyntax.get_notation_vars"
+ (str "Variable " ++ Id.print id ++ str " occurs more than once.")
+ | _ -> ());
+ res
let error_not_same_scope x y =
user_err ~hdr:"Metasyntax.error_not_name_scope"
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 0e660bf20c..4cee4f7a47 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -68,10 +68,18 @@ let pr_univ_name_list = function
| Some l ->
str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
+let pr_variance_lident (lid,v) =
+ let v = Option.cata Univ.Variance.pr (mt()) v in
+ v ++ pr_lident lid
+
let pr_univdecl_instance l extensible =
prlist_with_sep spc pr_lident l ++
(if extensible then str"+" else mt ())
+let pr_cumul_univdecl_instance l extensible =
+ prlist_with_sep spc pr_variance_lident l ++
+ (if extensible then str"+" else mt ())
+
let pr_univdecl_constraints l extensible =
if List.is_empty l && extensible then mt ()
else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++
@@ -85,9 +93,20 @@ let pr_universe_decl l =
str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
+let pr_cumul_univ_decl l =
+ let open UState in
+ match l with
+ | None -> mt ()
+ | Some l ->
+ str"@{" ++ pr_cumul_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
+ pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
+
let pr_ident_decl (lid, l) =
pr_lident lid ++ pr_universe_decl l
+let pr_cumul_ident_decl (lid, l) =
+ pr_lident lid ++ pr_cumul_univ_decl l
+
let string_of_fqid fqid =
String.concat "." (List.map Id.to_string fqid)
@@ -848,7 +867,7 @@ let pr_vernac_expr v =
let pr_oneind key (((coe,iddecl),(indupar,indpar),s,lc),ntn) =
hov 0 (
str key ++ spc() ++
- (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
+ (if coe then str"> " else str"") ++ pr_cumul_ident_decl iddecl ++
pr_and_type_binders_arg indupar ++
pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++
pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
@@ -1312,20 +1331,10 @@ let pr_control_flag (p : control_flag) =
let pr_vernac_control flags = Pp.prlist pr_control_flag flags
-let rec pr_vernac_flag (k, v) =
- let k = keyword k in
- let open Attributes in
- match v with
- | VernacFlagEmpty -> k
- | VernacFlagLeaf v -> k ++ str " = " ++ qs v
- | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )"
-and pr_vernac_flags m =
- prlist_with_sep (fun () -> str ", ") pr_vernac_flag m
-
let pr_vernac_attributes =
function
| [] -> mt ()
- | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
+ | flags -> str "#[" ++ prlist_with_sep pr_comma Attributes.pr_vernac_flag flags ++ str "]" ++ cut ()
let pr_vernac ({v = {control; attrs; expr}} as v) =
tag_vernac v
diff --git a/vernac/record.ml b/vernac/record.ml
index 891d7fcebe..583164a524 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -190,11 +190,12 @@ type tc_result =
(* Part relative to closing the definitions *)
* UnivNames.universe_binders
* Entries.universes_entry
+ * Entries.variance_entry
* Constr.rel_context
* DataR.t list
(* ps = parameter list *)
-let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_result =
+let typecheck_params_and_fields def poly udecl ps (records : DataI.t list) : tc_result =
let env0 = Global.env () in
(* Special case elaboration for template-polymorphic inductives,
lower bound on introduced universes is Prop so that we do not miss
@@ -202,7 +203,7 @@ let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_res
let is_template =
List.exists (fun { DataI.arity; _} -> Option.cata check_anonymous_type true arity) records in
let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
- let sigma, decl = Constrintern.interp_univ_decl_opt env0 pl in
+ let sigma, decl, variances = Constrintern.interp_cumul_univ_decl_opt env0 udecl in
let () = List.iter check_parameters_must_be_named ps in
let sigma, (impls_env, ((env1,newps), imps)) =
Constrintern.interp_context_evars ~program_mode:false env0 sigma ps in
@@ -256,7 +257,7 @@ let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_res
let ubinders = Evd.universe_binders sigma in
let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in
let () = List.iter (iter_constr ce) (List.rev newps) in
- template, imps, ubinders, univs, newps, ans
+ template, imps, ubinders, univs, variances, newps, ans
type record_error =
| MissingProj of Id.t * Id.t list
@@ -525,7 +526,7 @@ let declare_structure_entry o =
- prepares and declares the corresponding record projections, mainly taken care of by
[declare_projections]
*)
-let declare_structure ~cumulative finite ~ubind ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
+let declare_structure ~cumulative finite ~ubind ~univs ~variances paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
let nparams = List.length params in
let poly, ctx =
match univs with
@@ -568,7 +569,7 @@ let declare_structure ~cumulative finite ~ubind ~univs paramimpls params templat
mind_entry_private = None;
mind_entry_universes = univs;
mind_entry_template = template;
- mind_entry_cumulative = poly && cumulative;
+ mind_entry_variance = ComInductive.variance_of_entry ~cumulative ~variances univs;
}
in
let impls = List.map (fun _ -> paramimpls, []) record_data in
@@ -633,7 +634,8 @@ let build_class_constant ~univs ~rdata field implfs params paramimpls coers bind
} in
[cref, [m]]
-let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name =
+let build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
+ fields params paramimpls coers id idbuild binder_name =
let record_data =
{ Data.id
; idbuild
@@ -641,7 +643,7 @@ let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields para
; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields
; rdata
} in
- let inds = declare_structure ~cumulative Declarations.BiFinite ~ubind ~univs paramimpls
+ let inds = declare_structure ~cumulative Declarations.BiFinite ~ubind ~univs ~variances paramimpls
params template ~kind:Decls.Method ~name:[|binder_name|] [record_data]
in
let map ind =
@@ -677,7 +679,7 @@ let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields para
2. declare the class, using the information from 1. in the form of [Classes.typeclass]
*)
-let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params
+let declare_class def ~cumulative ~ubind ~univs ~variances id idbuild paramimpls params
rdata template ?(kind=Decls.StructureComponent) coers =
let implfs =
(* Make the class implicit in the projections, and the params if applicable. *)
@@ -694,7 +696,8 @@ let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params
let binder = {binder with binder_name=Name binder_name} in
build_class_constant ~rdata ~univs field implfs params paramimpls coers binder id proj_name
| _ ->
- build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name
+ build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
+ fields params paramimpls coers id idbuild binder_name
in
let univs, params, fields =
match univs with
@@ -852,7 +855,8 @@ let class_struture ~cumulative ~template ~ubind ~impargs ~univs ~params def reco
declare_class def ~cumulative ~ubind ~univs name.CAst.v idbuild
impargs params rdata template coers
-let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data =
+let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~variances ~params ~finite
+ records data =
let adjust_impls impls = impargs @ [CAst.make None] @ impls in
let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in
(* let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = *)
@@ -866,30 +870,36 @@ let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~fini
{ Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers }
in
let data = List.map2 map data records in
- let inds = declare_structure ~cumulative finite ~ubind ~univs impargs params template data in
+ let inds = declare_structure ~cumulative finite ~ubind ~univs ~variances
+ impargs params template data
+ in
List.map (fun ind -> GlobRef.IndRef ind) inds
(** [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances. *)
-let definition_structure udecl kind ~template ~cumulative ~poly finite (records : Ast.t list) =
+let definition_structure udecl kind ~template ~cumulative ~poly
+ finite (records : Ast.t list) : GlobRef.t list =
let () = check_unique_names records in
let () = check_priorities kind records in
let ps, data = extract_record_data records in
- let auto_template, impargs, ubind, univs, params, data =
+ let auto_template, impargs, ubind, univs, variances, params, data =
(* In theory we should be able to use
[Notation.with_notation_protection], due to the call to
Metasyntax.set_notation_for_interpretation, however something
is messing state beyond that.
*)
Vernacstate.System.protect (fun () ->
- typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in
+ typecheck_params_and_fields (kind = Class true) poly udecl ps data) ()
+ in
let template = template, auto_template in
match kind with
| Class def ->
- class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs def records data
+ class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs ~variances
+ def records data
| Inductive_kw | CoInductive | Variant | Record | Structure ->
- regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data
+ regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~variances ~params ~finite
+ records data
module Internal = struct
type nonrec projection_flags = projection_flags = {
diff --git a/vernac/record.mli b/vernac/record.mli
index ffcae2975e..7a40af048c 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -24,7 +24,7 @@ module Ast : sig
end
val definition_structure
- : universe_decl_expr option
+ : cumul_univ_decl_expr option
-> inductive_kind
-> template:bool option
-> cumulative:bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 761f6ef5b7..0f63dfe5ce 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -674,13 +674,19 @@ let is_polymorphic_inductive_cumulativity =
let polymorphic_cumulative =
let error_poly_context () =
user_err
- Pp.(str "The cumulative and noncumulative attributes can only be used in a polymorphic context.");
+ Pp.(str "The cumulative attribute can only be used in a polymorphic context.");
in
let open Attributes in
let open Notations in
+ (* EJGA: this seems redudant with code in attributes.ml *)
qualify_attribute "universes"
- (bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic"
- ++ bool_attribute ~name:"Cumulativity" ~on:"cumulative" ~off:"noncumulative")
+ (deprecated_bool_attribute
+ ~name:"Polymorphism"
+ ~on:"polymorphic" ~off:"monomorphic"
+ ++
+ deprecated_bool_attribute
+ ~name:"Cumulativity"
+ ~on:"cumulative" ~off:"noncumulative")
>>= function
| Some poly, Some cum ->
(* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive
@@ -1314,6 +1320,14 @@ let warn_implicit_core_hint_db =
(fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. "
++ strbrk"Please specify a hint database.")
+let warn_deprecated_hint_without_locality =
+ CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated"
+ (fun () -> strbrk "The default value for hint locality is currently \
+ \"local\" in a section and \"global\" otherwise, but is scheduled to change \
+ in a future release. For the time being, adding hints outside of sections \
+ without specifying an explicit locality is therefore deprecated. It is \
+ recommended to use \"export\" whenever possible.")
+
let check_hint_locality = function
| OptGlobal ->
if Global.sections_are_opened () then
@@ -1323,7 +1337,10 @@ let check_hint_locality = function
if Global.sections_are_opened () then
CErrors.user_err Pp.(str
"This command does not support the export attribute in sections.");
-| OptDefault | OptLocal -> ()
+| OptDefault ->
+ if not @@ Global.sections_are_opened () then
+ warn_deprecated_hint_without_locality ()
+| OptLocal -> ()
let vernac_remove_hints ~atts dbnames ids =
let locality = Attributes.(parse option_locality atts) in
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 6a9a74144f..defb0691c0 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -189,8 +189,9 @@ type inductive_params_expr = local_binder_expr list * local_binder_expr list opt
(** If the option is nonempty the "|" marker was used *)
type inductive_expr =
- ident_decl with_coercion * inductive_params_expr * constr_expr option *
- constructor_list_or_record_decl_expr
+ cumul_ident_decl with_coercion
+ * inductive_params_expr * constr_expr option
+ * constructor_list_or_record_decl_expr
type one_inductive_expr =
lident * inductive_params_expr * constr_expr option * constructor_expr list
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 22:41:03 +0000