blob: 44688ddafcfe9c45e5c037f69ba176bb3549df77 (
plain)
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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(** The type of parsing attribute data *)
type vernac_flags = vernac_flag list
and vernac_flag = string * vernac_flag_value
and vernac_flag_value =
| VernacFlagEmpty
| VernacFlagLeaf of string
| VernacFlagList of vernac_flags
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. *)
type deprecation = { since : string option ; note : string option }
val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
val polymorphic : bool attribute
val program : bool attribute
val template : bool option attribute
val locality : bool option attribute
val deprecation : deprecation option attribute
val canonical : bool 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 = '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 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. *)
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 : 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 : 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 : vernac_flag
val vernac_monomorphic_flag : vernac_flag
(** For the stm, do not use! *)
val polymorphic_nowarn : bool attribute
(** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *)
val universe_polymorphism_option_name : string list
val is_universe_polymorphism : unit -> bool
|
