blob: 3c082b2cebe7647727da31c81ddb72463bcd1771 (
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
|
(***********************************************************************)
(* 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 Rawterm
open Topconstr
open Ppextend
(*i*)
(*s 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 = precedence * precedence list
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 *)
val declare_notation : notation -> scope_name -> aconstr * level -> unit
val interp_notation : notation -> scopes -> aconstr
val find_notation : scope_name -> notation -> scopes ->
(delimiters option * scopes) option
val exists_notation_in_scope :
scope_name -> level -> notation -> aconstr -> 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 *)
val pr_scope : (aconstr -> std_ppcmds) -> scope_name -> std_ppcmds
val pr_scopes : (aconstr -> std_ppcmds) -> std_ppcmds
val declare_printing_rule : notation -> unparsing list * precedence -> unit
val find_notation_printing_rule : notation -> unparsing list * precedence
|
