1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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) *)
(************************************************************************)
(** 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) CAst.t
and vernac_flag_value =
| VernacFlagEmpty
| 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.
In the most general case, an attribute transforms the raw flags
along with its value. *)
val parse : 'a attribute -> vernac_flags -> 'a
(** Errors on unsupported attributes. *)
val unsupported_attributes : vernac_flags -> unit
(** Errors if the list of flags is nonempty. *)
module Notations : sig
(** Notations to combine attributes. *)
include Monad.Def with type 'a t = 'a attribute
(** Attributes form a monad. [a1 >>= f] means [f] will be run on the
flags transformed by [a1] and using the value produced by [a1].
The trivial attribute [return x] does no action on the flags. *)
val (++) : 'a attribute -> 'b attribute -> ('a * 'b) attribute
(** Combine 2 attributes. If any keys are in common an error will be raised. *)
end
(** Definitions for some standard attributes. *)
val raw_attributes : vernac_flags attribute
val polymorphic : bool attribute
val program : bool attribute
val template : bool option attribute
val unfold_fix : bool attribute
val locality : bool option attribute
val option_locality : Goptions.option_locality attribute
val deprecation : Deprecation.t option attribute
val user_warn_warn : UserWarn.warn list attribute
val user_warns : UserWarn.t option attribute
val reversible : bool option attribute
val canonical_field : bool attribute
val canonical_instance : bool attribute
val using : string option attribute
val explicit_hint_locality : Hints.hint_locality option attribute
val bind_scope_where : Notation.add_scope_where option attribute
(** Default: if sections are opened then Local otherwise Export.
Although this is named and uses the type [hint_locality]
it may be used as the standard 3-valued locality attribute.
*)
val hint_locality : Hints.hint_locality attribute
(** Enable/Disable universe checking *)
val typing_flags : Declarations.typing_flags option attribute
val program_mode_option_name : string list
(** For internal use when messing with the global option. *)
val only_locality : vernac_flags -> bool option
(** Parse attributes allowing only locality. *)
val only_polymorphism : vernac_flags -> bool
(** Parse attributes allowing only polymorphism.
Uses the global flag for the default value. *)
val parse_drop_extra : 'a attribute -> vernac_flags -> 'a
(** Ignores unsupported attributes. *)
val parse_with_extra : 'a attribute -> vernac_flags -> vernac_flags * 'a
(** Returns unsupported attributes. *)
(** * Defining attributes. *)
type 'a key_parser = ?loc:Loc.t -> 'a option -> vernac_flag_value -> 'a
(** A parser for some key in an attribute. It is given a nonempty ['a
option] when the attribute is multiply set for some command.
eg in [#[polymorphic] Monomorphic Definition foo := ...], when
parsing [Monomorphic] it will be given [Some true]. *)
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 payload_parser : ?cat:(string -> string -> string) -> name:string -> string key_parser
(** [payload_parser ?cat ~name] parses attributes like [#[name="payload"]].
If the attribute is used multiple times and [cat] is non-None,
the payloads are concatenated using it.
If [cat] is None, having multiple occurences of the attribute is forbidden. *)
val payload_attribute : ?cat:(string -> string -> string) -> name:string -> string option attribute
(** This is just [attribute_of_list] for a single [payload_parser]. *)
(** 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 qualify_attribute : string -> 'a attribute -> 'a attribute
(** [qualified_attribute qual att] treats [#[qual(atts)]] like [att]
treats [atts]. *)
(** Combinators to help define your own parsers. See the
implementation of [bool_attribute] for practical use. *)
val assert_empty : ?loc:Loc.t -> string -> vernac_flag_value -> unit
(** [assert_empty key v] errors if [v] is not empty. [key] is used in
the error message as the name of the attribute. *)
val assert_once : ?loc:Loc.t -> name:string -> 'a option -> unit
(** [assert_once ~name v] errors if [v] is not empty. [name] is used
in the error message as the name of the attribute. Used to ensure
that a given attribute is not reapeated. *)
val single_key_parser : name:string -> key:string -> 'a -> 'a key_parser
(** [single_key_parser ~name ~key v] makes a parser for attribute
[name] giving the constant value [v] for key [key] taking no
arguments. [name] may only be given once. *)
val make_attribute : (vernac_flags -> vernac_flags * 'a) -> 'a attribute
(** Make an attribute using the internal representation, thus with
access to the full power of attributes. Unstable. *)
(** Compatibility values for parsing [Polymorphic]. *)
val vernac_polymorphic_flag : Loc.t option -> vernac_flag
val vernac_monomorphic_flag : Loc.t option -> vernac_flag
(** For internal use. *)
val universe_polymorphism_option_name : string list
val is_universe_polymorphism : unit -> bool
|
