blob: f5b26b877058af0b8db517c3831907062d05b88c (
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
|
open Names
open Util
open Nametab
open Rawterm
open Bignat
(* 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 numeral_interpreter_name = string
type numeral_interpreter =
(loc -> bigint -> rawconstr)
* (loc -> bigint -> name -> cases_pattern) option
(* A scope is a set of interpreters for symbols + optional
interpreter and printers for integers + optional delimiters *)
type level = Extend.precedence * Extend.precedence list
type scope_name = string
type delimiters = string * string
type scope
type scopes = scope_name list
val default_scope : scope_name
val current_scopes : unit -> scopes
val open_scope : scope_name -> unit
val declare_scope : scope_name -> unit
(* Declare delimiters for printing *)
val declare_delimiters : scope_name -> delimiters -> unit
(* Declare, interpret, and look for a printer for numeral *)
val declare_numeral_interpreter :
numeral_interpreter_name -> numeral_interpreter -> unit
val interp_numeral : loc -> bigint -> scopes -> rawconstr
val interp_numeral_as_pattern: loc -> bigint -> name -> scopes -> cases_pattern
val find_numeral_printer : string -> scopes ->
(delimiters option * scopes) option
(* Declare, interpret, and look for a printer for symbolic notations *)
type notation = string
val declare_notation : level -> notation -> rawconstr -> scope_name -> unit
val interp_notation : notation -> scopes -> rawconstr list -> rawconstr
val find_notation : scope_name -> notation -> scopes ->
(delimiters option * scopes) option
val exists_notation_in_scope :
scope_name -> level -> notation -> rawconstr -> bool
val exists_notation : level -> notation -> bool
(* Declare and look for scopes associated to arguments of a global ref *)
open Libnames
val declare_arguments_scope: global_reference -> scope_name option list -> unit
val find_arguments_scope : global_reference -> scope_name option list
(* Printing scopes *)
open Pp
val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
|
