blob: ffd82c8084f7b879eb6aea9411a7085455840c58 (
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
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
153
154
155
156
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
(*i*)
open Util
open Pp
open Bignat
open Names
open Nametab
open Libnames
open Rawterm
open Topconstr
open Ppextend
(*i*)
(**********************************************************************)
(* Scopes *)
(*s A scope is a set of interpreters for symbols + optional
interpreter and printers for integers + optional delimiters *)
type level = precedence * tolerability list
type delimiters = string
type scope
type scopes (* = scope_name list*)
val type_scope : scope_name
val declare_scope : scope_name -> unit
(* Open scope *)
val current_scopes : unit -> scopes
val open_close_scope :
(* locality *) bool * (* open *) bool * scope_name -> unit
(* Extend a list of scopes *)
val empty_scope_stack : scopes
val push_scope : scope_name -> scopes -> scopes
(* Declare delimiters for printing *)
val declare_delimiters : scope_name -> delimiters -> unit
val find_delimiters_scope : loc -> delimiters -> scope_name
(*s Declare and uses back and forth a numeral interpretation *)
(* A numeral interpreter is the pair of an interpreter for _integer_
numbers in terms and an optional interpreter in pattern, if
negative numbers are not supported, the interpreter must fail with
an appropriate error message *)
type num_interpreter =
(loc -> bigint -> rawconstr)
* (loc -> bigint -> name -> cases_pattern) option
type num_uninterpreter =
rawconstr list * (rawconstr -> bigint option)
* (cases_pattern -> bigint option) option
type required_module = global_reference * string list
val declare_numeral_interpreter : scope_name -> required_module ->
num_interpreter -> num_uninterpreter -> unit
(* Returns the term/cases_pattern bound to a numeral in a given scope context*)
val interp_numeral : loc -> bigint -> scope_name list -> rawconstr
val interp_numeral_as_pattern : loc -> bigint -> name -> scope_name list ->
cases_pattern
(* Returns the numeral bound to a term/cases_pattern; raises No_match if no *)
(* such numeral *)
val uninterp_numeral : rawconstr -> scope_name * bigint
val uninterp_cases_numeral : cases_pattern -> scope_name * bigint
val availability_of_numeral : scope_name -> scopes -> delimiters option option
(*s Declare and interpret back and forth a notation *)
(* Binds a notation in a given scope to an interpretation *)
type interp_rule =
| NotationRule of scope_name option * notation
| SynDefRule of kernel_name
val declare_notation_interpretation : notation -> scope_name option ->
interpretation -> string -> bool -> unit
val declare_uninterpretation : interp_rule -> interpretation -> unit
(* Returns the interpretation bound to a notation *)
val interp_notation : notation -> scope_name list -> interpretation
(* Returns the possible notations for a given term *)
val uninterp_notations : rawconstr ->
(interp_rule * interpretation * int option) list
val uninterp_cases_pattern_notations : cases_pattern ->
(interp_rule * interpretation * int option) list
(* Test if a notation is available in the scopes *)
(* context [scopes] if available, the result is not None; the first *)
(* argument is itself not None if a delimiters is needed; the second *)
(* argument is a numeral printer if the *)
val availability_of_notation : scope_name option * notation -> scopes ->
(scope_name option * delimiters option) option
(*s Declare and test the level of a (possibly uninterpreted) notation *)
val declare_notation_level : notation -> level option * level -> unit
val level_of_notation : notation -> level option * level (* [Not_found] if no level *)
(*s** Miscellaneous *)
(* Checks for already existing notations *)
val exists_notation_in_scope : scope_name option -> notation ->
interpretation -> bool * bool
(* Declares and looks for scopes associated to arguments of a global ref *)
val declare_arguments_scope: global_reference -> scope_name option list -> unit
val find_arguments_scope : global_reference -> scope_name option list
val declare_class_scope : scope_name -> Classops.cl_typ -> unit
val declare_ref_arguments_scope : global_reference -> unit
(* Building notation key *)
type symbol =
| Terminal of string
| NonTerminal of identifier
| Break of int
val make_notation_key : symbol list -> notation
val decompose_notation_key : notation -> symbol list
(* Prints scopes (expect a pure aconstr printer *)
val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds
val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds
(**********************************************************************)
(*s Printing rules for notations *)
(* Declare and look for the printing rule for symbolic notations *)
type unparsing_rule = unparsing list * precedence
val declare_notation_printing_rule : notation -> unparsing_rule -> unit
val find_notation_printing_rule : notation -> unparsing_rule
(**********************************************************************)
(* Rem: printing rules for numerals are trivial *)
|
