]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/pxp/pxp/m2parsergen/README
Initial revision
[helm.git] / helm / DEVEL / pxp / pxp / m2parsergen / README
1 ----------------------------------------------------------------------
2 m2parsergen
3 ----------------------------------------------------------------------
4
5 This is a parser generator for top-down (or recursively descending) parsers.
6 The input file must be structured as follows:
7
8 ---------------------------------------- Begin of file
9
10 <OCAML TEXT ("preamble")>
11
12 %%
13
14 <DECLARATIONS>
15
16 %%
17
18 <RULES>
19
20 %%
21
22 <OCAML TEXT ("postamble")>
23
24 ---------------------------------------- End of file
25
26 The two-character combination %% separates the various sections. The
27 text before the first %% and after the last %% will be copied verbatim
28 to the output file.
29
30 Within the declarations and rules sections you must use /* ... */ as
31 comment braces.
32
33 There are two types of declarations:
34
35 %token Name
36
37 declares that Name is a token without associated value, and
38
39 %token <> Name
40
41 declares that Name is a token with associated value (i.e. Name x).
42
43 In contrast to ocamlyacc, you need not to specify a type. This is a
44 fundamental difference, because m2parsergen will not generate a type
45 declaration for a "token" type; you must do this yourself.
46
47 You need not to declare start symbols; every grammar rule may be used
48 as start symbol.
49
50 The rules look like:
51
52 name_of_rule(arg1, arg2, ...):
53   label1:symbol1 label2:symbol2 ... {{ CODE }}
54 | label1:symbol1 label2:symbol2 ... {{ CODE }}
55 ...
56 | label1:symbol1 label2:symbol2 ... {{ CODE }}
57
58 The rules may have arguments (note that you must write the
59 parantheses, even if the rule does not have arguments). Here, arg1,
60 arg2, ... are the formal names of the arguments; you may refer to them
61 in OCaml code.
62
63 Furthermore, the symbols may have labels (you can leave the labels
64 out). You can refer to the value associated with a symbol by its
65 label, i.e. there is an OCaml variable with the same name as the label
66 prescribes, and this variable contains the value.
67
68 The OCaml code must be embraced by {{ and }}, and these separators
69 must not occur within the code.
70
71 EXAMPLE:
72
73 prefix_term():
74   Plus_symbol Left_paren v1:prefix_term() Comma v2:prefix_term() Right_paren
75     {{ v1 + v2 }}
76 | Times_symbol Left_paren v1:prefix_term() Comma v2:prefix_term() Right_paren
77     {{ v1 * v2 }}
78 | n:Number
79     {{ n }}
80
81 As you can see in the example, you must pass values for the arguments
82 if you call non-terminal symbols (here, the argument list is empty: ()).
83
84 The generated parsers behave as follows:
85
86 - A rule is applicable to a token sequence if the first token is
87   matched by the rule.
88
89   In the example: prefix_term is applicable if the first token of a
90   sequence is either Plus_symbol, Times_symbol, or Number.
91
92 - One branch of the applicable rule is selected: it is the first
93   branch that matches the first token. THE OTHER TOKENS DO NOT HAVE
94   ANY EFFECT ON BRANCH SELECTION!
95
96   For instance, in the following rule the second branch is never
97   selected, because only the A is used to select the branch:
98
99   a():
100     A B {{ ... }}
101   | A C {{ ... }}
102
103 - Once a branch is selected, it is checked whether the branch matches
104   the token sequence. If this check succeeds, the code section of the
105   branch is executed, and the resulting value is returned to the
106   caller.
107   If the check fails, the exception Parsing.Parse_error is raised.
108   Normally, this exception is not caught, and will force the parser
109   to stop.
110
111   The check in detail:
112
113   If the rule demands a terminal, there a must be exactly this
114   terminal at the corresponding location in the token sequence.
115
116   If the rule demands a non-terminal, it is checked whether the rule
117   for to this non-terminal is applicable. If so, the branch
118   is selected, and recursively checked. If the rule is not applicable,
119   the check fails immediately.
120
121 - THERE IS NO BACKTRACKING! 
122
123   Note that the following works (but the construction is resolved at
124   generation time):
125
126   rule1() =
127      rule2() A B ... {{ ... }}
128
129   rule2() =
130      C {{ ... }}
131    | D {{ ... }}
132
133   In this case, the (only) branch of rule1 is selected if the next
134   token is C or D.
135
136 ---
137
138
139
140 *** Options and repetitions ***
141
142 Symbols can be tagged as being optional, or to occur repeatedly:
143
144 rule():
145   Name whitespace()* Question_mark?
146
147 - "*": The symbol matches zero or more occurrences.
148
149 - "?": The symbol matches zero or one occurrence.
150
151 This is done as follows:
152
153 - terminal*: The maximum number of consecutive tokens <terminal> are
154              matched.
155 - non-terminal*: The maximum number of the subsequences matching
156                  <non-terminal> are matched. Before another
157                  subsequence is matched, it is checked whether the
158                  rule for <non-terminal> is applicable. If so, the
159                  rule is invoked and must succeed (otherwise Parsing.
160                  Parse_error). If not, the loop is exited.
161
162 - terminal?: If the next token is <terminal>, it is matched. If not,
163              no token is matched.
164
165 - non-terminal?: It is checked whether the rule for <non-terminal>
166                  is applicable. If so, the rule is invoked, and
167                  matches a sequence of tokens. If not, no token is
168                  matched.
169
170 You may refer to repeated or optional symbols by labels. In this case,
171 the label is associated with lists of values, or optional values, 
172 respectively:
173
174 rule():
175   A  lab:other()*  lab':unlikely()?
176     {{ let n = List.length lab in ... 
177        match lab' with
178          None -> ...
179        | Some v -> ... 
180     }}
181
182 A different scheme is applied if the symbol is a token without
183 associated value (%token Name, and NOT %token <> Name):
184
185 rule():
186   A lab:B* lab':C?
187
188 Here, "lab" becomes an integer variable counting the number of Bs, and
189 "lab'" becomes a boolean variable denoting whether there is a C or not.
190
191
192 *** Early let-binding ***
193
194 You may put some OCaml code directly after the first symbol of a
195 branch:
196
197 rule():
198   A $ {{ let-binding }} C D ... {{ ... }}
199
200 The code brace {{ let-binding }} must be preceded by a dollar
201 sign. You can put "let ... = ... in" statements into this brace:
202
203 rule1():
204   n:A $ {{ let twice = 2 * n in }} rule2(twice) {{ ... }}
205
206 This code is executed once the branch is selected.
207
208
209 *** Very early let-binding ***
210
211 This is also possible:
212
213 rule():
214   $ {{ CODE }}
215   A
216   ...
217
218 The CODE is executed right when the branch is selected, and before any
219 other happens. (Only for hacks!)
220
221
222
223 *** Computed rules ***
224
225 rule():
226   A $ {{ let followup = ... some function ... in }} [ followup ]() 
227     {{ ... }}
228
229 Between [ and ], you can refer to the O'Caml name of *any* function.
230 Here, the function "followup" is bound in the let-binding.
231
232
233 *** Error handling ***
234
235 If a branch is already selected, but the check fails whether the other
236 symbols of the branch match, it is possible to catch the resulting
237 exception and to find out at which position the failure has occurred.
238
239 rule():
240   x:A y:B z:C {{ ... }} ? {{ ERROR-CODE }}
241
242 After a question mark, it is allowed to append another code
243 brace. This code is executed if the branch check fails (but not if the
244 branch is not selected nor if no branches are selected). The string
245 variable !yy_position contains the label of the symbol that caused the
246 failure (or it contains the empty string if the symbol does not have a
247 label). 
248
249 Example:
250
251 rule():
252   x:A y:B z:C {{ print_endline "SUCCESS" }} ? {{ print_endline !yy_position }}
253
254 If the token sequence is A B C, "SUCCESS" will be printed. If the
255 sequence is A C, the second symbol fails, and "y" will be printed. If
256 the sequence is A B D, the third symbol fails, and "z" will be
257 printed. If the sequence is B, the rule will be never selected because
258 it is not applicable.
259
260
261
262 *** Error recovery ***
263
264 You may call the functions yy_current, yy_get_next, or one of the
265 parse_* functions in the error brace to recover from the error
266 (e.g. to move ahead until a certain token is reached). See below.
267
268
269
270 *** How to call the parser ***
271
272 The rules are rewritten into a OCaml let-binding:
273
274 let rec parse_<rule1> ... = ...
275     and parse_<rule2> ... = ...
276     ...
277     and parse_<ruleN> ... = ...
278 in
279
280 i.e. there are lots of functions, and the name of the functions are
281 "parse_" plus the name of the rules. You can call every function.
282
283 The first two arguments of the functions have a special meaning; the
284 other arguments are the arguments coming from the rule description:
285
286 rule(a,b):
287   ...
288
289 ===>
290
291 let rec parse_rule yy_current yy_get_next a b = ...
292
293 The first argument, yy_current, is a function that returns the current
294 token. The second arguments, yy_get_next, is a function that switches
295 to the next token, and returns it.
296
297 If the tokens are stored in a list, this may be a definition:
298
299 let input = ref [ Token1; Token2; ... ] in
300 let yy_current() = List.hd !input in
301 let yy_get_next () =
302   input := List.tl !input;
303   List.hd !input
304
305 When you call one of the parser functions, the current token must
306 already be loaded, i.e. yy_current returns the first token to match by
307 the function.
308
309 After the functions has returned, the current token is the token
310 following the sequence of tokens that have been matched by the
311 function.
312
313 The function returns the value computed by the OCaml code brace of the
314 rule (or the value of the error brace).
315
316 If the rule is not applicable, the exception Not_found is raised.
317
318 If the rule is applicable, but it does not match, the exception
319 Parsing.Parse_error is raised.