blob: 8734e34525308dc82d78c7be12e3dc4702b723df (
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
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(*i $Id$ i*)
(*i*)
open Pp
open Ast
open Coqast
type nonterm_prod =
| ProdList0 of nonterm_prod
| ProdList1 of nonterm_prod
| ProdOpt of nonterm_prod
| ProdPrimitive of (string * string)
type prod_item =
| Term of Token.pattern
| NonTerm of nonterm_prod * (string * ast_action_type) option
type grammar_rule = {
gr_name : string;
gr_production : prod_item list;
gr_action : Ast.act }
type grammar_entry = {
ge_name : string;
ge_type : ast_action_type;
gl_assoc : Gramext.g_assoc option;
gl_rules : grammar_rule list }
type grammar_command = {
gc_univ : string;
gc_entries : grammar_entry list }
type grammar_associativity = Gramext.g_assoc option
type nonterm =
| NtShort of string
| NtQual of string * string
type grammar_production =
| VTerm of string
| VNonTerm of loc * nonterm * string option
type raw_grammar_rule = string * grammar_production list * grammar_action
type raw_grammar_entry =
string * ast_action_type * grammar_associativity * raw_grammar_rule list
val terminal : string -> string * string
val rename_command : string -> string
val subst_grammar_command :
Names.substitution -> grammar_command -> grammar_command
(*s Pretty-print. *)
(* Dealing with precedences *)
type precedence = int * int * int
type parenRelation = L | E | Any | Prec of precedence
type ppbox =
| PpHB of int
| PpHOVB of int
| PpHVB of int
| PpVB of int
| PpTB
(* unparsing objects *)
type 'pat unparsing_hunk =
| PH of 'pat * string option * parenRelation
| RO of string
| UNP_BOX of ppbox * 'pat unparsing_hunk list
| UNP_BRK of int * int
| UNP_TBRK of int * int
| UNP_TAB
| UNP_FNL
| UNP_INFIX of Libnames.extended_global_reference * string * string *
(parenRelation * parenRelation)
(*val subst_unparsing_hunk :
Names.substitution -> (Names.substitution -> 'pat -> 'pat) ->
'pat unparsing_hunk -> 'pat unparsing_hunk
*)
(* 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
val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
type 'pat syntax_entry = {
syn_id : string;
syn_prec: precedence;
syn_astpat : 'pat;
syn_hunks : 'pat unparsing_hunk list }
val subst_syntax_entry :
(Names.substitution -> 'pat -> 'pat) ->
Names.substitution -> 'pat syntax_entry -> 'pat syntax_entry
type 'pat syntax_command = {
sc_univ : string;
sc_entries : 'pat syntax_entry list }
val subst_syntax_command :
(Names.substitution -> 'pat -> 'pat) ->
Names.substitution -> 'pat syntax_command -> 'pat syntax_command
type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list
type syntax_entry_ast = precedence * syntax_rule list
val interp_grammar_command :
string -> (string * string -> entry_type) ->
raw_grammar_entry list -> grammar_command
val interp_syntax_entry :
string -> syntax_entry_ast list -> Ast.astpat syntax_command
|
