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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
|
(***********************************************************************)
(* 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*)
open Util
open Pp
open Gramext
open Names
open Ast
open Ppextend
open Topconstr
open Genarg
type entry_type = argument_type
type constr_entry_type = ETConstr | ETIdent | ETReference
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 * (Names.identifier * constr_entry_type) option
type grammar_rule = {
gr_name : string;
gr_production : prod_item list;
gr_action : aconstr }
type grammar_entry = {
ge_name : string;
ge_type : constr_entry_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
(**********************************************************************)
(* Globalisation and type-checking of Grammar actions *)
type entry_context = (identifier * constr_entry_type) list
let ast_to_rawconstr = ref (fun _ _ -> AVar (id_of_string "Z"))
let set_ast_to_rawconstr f = ast_to_rawconstr := f
let act_of_ast vars = function
| SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr vars a
| SimpleAction (loc,CasesPatternNode a) -> failwith "TODO:act_of_ast: cases_pattern"
| CaseAction _ -> failwith "case/let not supported"
let to_act_check_vars = act_of_ast
type syntax_modifier =
| SetItemLevel of string * int
| SetLevel of int
| SetAssoc of Gramext.g_assoc
| SetEntryType of string * constr_entry_type
type nonterm =
| NtShort of string
| NtQual of string * string
type grammar_production =
| VTerm of string
| VNonTerm of loc * nonterm * Names.identifier option
type raw_grammar_rule = string * grammar_production list * grammar_action
type raw_grammar_entry =
string * constr_entry_type * grammar_associativity * raw_grammar_rule list
let subst_grammar_rule subst gr =
{ gr with gr_action = subst_aconstr subst gr.gr_action }
let subst_grammar_entry subst ge =
{ ge with gl_rules = List.map (subst_grammar_rule subst) ge.gl_rules }
let subst_grammar_command subst gc =
{ gc with gc_entries = List.map (subst_grammar_entry subst) gc.gc_entries }
(*s Terminal symbols interpretation *)
let is_ident_not_keyword s =
match s.[0] with
| 'a'..'z' | 'A'..'Z' | '_' -> not (Lexer.is_keyword s)
| _ -> false
let is_number s =
match s.[0] with
| '0'..'9' -> true
| _ -> false
let strip s =
let len =
let rec loop i len =
if i = String.length s then len
else if s.[i] == ' ' then loop (i + 1) len
else loop (i + 1) (len + 1)
in
loop 0 0
in
if len == String.length s then s
else
let s' = String.create len in
let rec loop i i' =
if i == String.length s then s'
else if s.[i] == ' ' then loop (i + 1) i'
else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end
in
loop 0 0
let terminal s =
let s = strip s in
if s = "" then failwith "empty token";
if is_ident_not_keyword s then ("IDENT", s)
else if is_number s then ("INT", s)
else ("", s)
(*s Non-terminal symbols interpretation *)
(* For compatibility *)
let warn nt nt' =
warning ("'"^nt^"' grammar entry is obsolete; use name '"^nt'^"' instead");
nt'
let rename_command nt =
if String.length nt >= 7 & String.sub nt 0 7 = "command"
then warn nt ("constr"^(String.sub nt 7 (String.length nt - 7)))
else if nt = "lcommand" then warn nt "lconstr"
else if nt = "lassoc_command4" then warn nt "lassoc_constr4"
else nt
let qualified_nterm current_univ = function
| NtQual (univ, en) -> (rename_command univ, rename_command en)
| NtShort en -> (current_univ, rename_command en)
let entry_type_of_constr_entry_type = function
| ETConstr -> ConstrArgType
| ETIdent -> IdentArgType
| ETReference -> RefArgType
let constr_entry_of_entry = function
| ConstrArgType -> ETConstr
| IdentArgType -> ETIdent
| RefArgType -> ETReference
| _ -> error "Cannot arbitrarily extend non constr/ident/ref entries"
let nterm loc (get_entry_type,univ) nont =
let nt = qualified_nterm univ nont in
try (nt,constr_entry_of_entry (get_entry_type nt))
with Not_found ->
let (s,n) = nt in
user_err_loc(loc,"Externd.nterm",str("unknown grammar entry: "^s^":"^n))
let prod_item univ env = function
| VTerm s -> env, Term (terminal s)
| VNonTerm (loc, nt, Some p) ->
let (nont, etyp) = nterm loc univ nt in
((p, etyp) :: env, NonTerm (ProdPrimitive nont, Some (p,etyp)))
| VNonTerm (loc, nt, None) ->
let (nont, etyp) = nterm loc univ nt in
env, NonTerm (ProdPrimitive nont, None)
let rec prod_item_list univ penv pil =
match pil with
| [] -> [], penv
| pi :: pitl ->
let (env, pic) = prod_item univ penv pi in
let (pictl, act_env) = prod_item_list univ env pitl in
(pic :: pictl, act_env)
let gram_rule univ etyp (name,pil,act) =
let (pilc, act_env) = prod_item_list univ [] pil in
let a = to_act_check_vars act_env act in
{ gr_name = name; gr_production = pilc; gr_action = a }
let gram_entry univ (nt, etyp, ass, rl) =
{ ge_name = rename_command nt;
ge_type = etyp;
gl_assoc = ass;
gl_rules = List.map (gram_rule univ etyp) rl }
let interp_grammar_command univ ge entryl =
let univ = rename_command univ in
{ gc_univ = univ;
gc_entries = List.map (gram_entry (ge,univ)) entryl }
(* 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_SYMBOLIC of string * string * 'pat unparsing_hunk
let rec subst_hunk subst_pat subst hunk = match hunk with
| PH (pat,so,pr) ->
let pat' = subst_pat subst pat in
if pat'==pat then hunk else
PH (pat',so,pr)
| RO _ -> hunk
| UNP_BOX (ppbox, hunkl) ->
let hunkl' = list_smartmap (subst_hunk subst_pat subst) hunkl in
if hunkl' == hunkl then hunk else
UNP_BOX (ppbox, hunkl')
| UNP_BRK _
| UNP_TBRK _
| UNP_TAB
| UNP_FNL -> hunk
| UNP_SYMBOLIC (s1, s2, pat) ->
let pat' = subst_hunk subst_pat subst pat in
if pat' == pat then hunk else
UNP_SYMBOLIC (s1, s2, pat')
(* Checks if the precedence of the parent printer (None means the
highest precedence), and the child's one, follow the given
relation. *)
(*
let compare_prec (a1,b1,c1) (a2,b2,c2) =
match (a1=a2),(b1=b2),(c1=c2) with
| true,true,true -> 0
| true,true,false -> c1-c2
| true,false,_ -> b1-b2
| false,_,_ -> a1-a2
*)
let compare_prec a1 a2 = a1-a2
let tolerable_prec oparent_prec_reln child_prec =
match oparent_prec_reln with
| Some (pprec, L) -> (compare_prec child_prec pprec) < 0
| Some (pprec, E) -> (compare_prec child_prec pprec) <= 0
| Some (_, Prec level) -> (compare_prec child_prec level) <= 0
| _ -> true
type 'pat syntax_entry = {
syn_id : string;
syn_prec: precedence;
syn_astpat : 'pat;
syn_hunks : 'pat unparsing_hunk list }
let subst_syntax_entry subst_pat subst sentry =
let syn_astpat' = subst_pat subst sentry.syn_astpat in
let syn_hunks' = list_smartmap (subst_hunk subst_pat subst) sentry.syn_hunks
in
if syn_astpat' == sentry.syn_astpat
&& syn_hunks' == sentry.syn_hunks then sentry
else
{ sentry with
syn_astpat = syn_astpat' ;
syn_hunks = syn_hunks' ;
}
type 'pat syntax_command = {
sc_univ : string;
sc_entries : 'pat syntax_entry list }
let subst_syntax_command subst_pat subst scomm =
let sc_entries' =
list_smartmap (subst_syntax_entry subst_pat subst) scomm.sc_entries
in
if sc_entries' == scomm.sc_entries then scomm else
{ scomm with sc_entries = sc_entries' }
type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list
type raw_syntax_entry = precedence * syntax_rule list
let rec interp_unparsing env = function
| PH (ast,ext,pr) -> PH (Ast.val_of_ast env ast,ext,pr)
| UNP_BOX (b,ul) -> UNP_BOX (b,List.map (interp_unparsing env) ul)
| UNP_BRK _ | RO _ | UNP_TBRK _ | UNP_TAB | UNP_FNL as x -> x
| UNP_SYMBOLIC (x,y,u) -> UNP_SYMBOLIC (x,y,interp_unparsing env u)
let rule_of_ast univ prec (s,spat,unp) =
let (astpat,meta_env) = Ast.to_pat [] spat in
let hunks = List.map (interp_unparsing meta_env) unp in
{ syn_id = s;
syn_prec = prec;
syn_astpat = astpat;
syn_hunks = hunks }
let level_of_ast univ (prec,rl) = List.map (rule_of_ast univ prec) rl
let interp_syntax_entry univ sel =
{ sc_univ = univ;
sc_entries = List.flatten (List.map (level_of_ast univ) sel)}
|