blob: 086d1b2ebcbb75e6ea3a7a7dc0790ab373353e54 (
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
|
(*i $Id$ i*)
(*i*)
open Pp
open Pcoq
(*i*)
(* Parsing. *)
type nonterm =
| NtShort of string
| NtQual of string * string
val qualified_nterm : (string * gram_universe) -> nonterm ->
(string * gram_universe) * string
type prod_item =
| Term of Token.pattern
| NonTerm of nonterm * entry_type * string option
type grammar_rule = {
gr_name : string;
gr_production : prod_item list;
gr_action : Ast.act }
type grammar_entry = {
ge_name : string;
ge_type : entry_type;
gl_assoc : Gramext.g_assoc option;
gl_rules : grammar_rule list }
type grammar_command = {
gc_univ : string;
gc_entries : grammar_entry list }
val gram_assoc : Coqast.t -> Gramext.g_assoc option
val interp_grammar_command : string -> Coqast.t list -> grammar_command
(*s Pretty-print. *)
(* Dealing with precedences *)
type precedence = int * int * int
type parenRelation = L | E | Any
(* Checks if the precedence of the parent printer (None means the
highest precedence), and the child's one, follow the given
relation. *)
type tolerability = (string * precedence) * parenRelation
val tolerable_prec : tolerability option -> (string * precedence) -> bool
(* unparsing objects *)
type ppbox =
| PpHB of int
| PpHOVB of int
| PpHVB of int
| PpVB of int
| PpTB
type unparsing_hunk =
| PH of Ast.pat * (string * tolerability option) option * parenRelation
| RO of string
| UNP_BOX of ppbox * unparsing_hunk list
| UNP_BRK of int * int
| UNP_TBRK of int * int
| UNP_TAB
| UNP_FNL
val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
val unparsing_of_ast : Ast.entry_env -> Coqast.t -> unparsing_hunk list
type syntax_entry = {
syn_id : string;
syn_prec: precedence;
syn_astpat : Ast.pat;
syn_hunks : unparsing_hunk list }
type syntax_command = {
sc_univ : string;
sc_entries : syntax_entry list }
val interp_syntax_entry : string -> Coqast.t list -> syntax_command
|
