1 \section{Data structures}
3 \subsection{Algebraic Datatypes (ADT)}
5 (ADT is also the usual accronym for Abstract DataType. However, I'll
6 never talk about abstract datatypes in this manual, so there's no
7 reason to get confused about it. ADT always refers to algebraic
10 Metalua's distinctive feature is its ability to easily work on program
11 source codes as trees, and this include a proper syntax for tree
12 manipulation. The generic table structure offered by Lua is
13 definitely good enough to represent trees, but since we're going to
14 manipulate them a lot, we give them a specific syntax which makes them
15 easier to read and write.
17 So, a tree is basically a node, with:
19 \item a tag (a string, stored in the table field named ``{\tt tag}'')
20 \item some children, which are either sub-trees, or atomic values
21 (generally strings, numbers or booleans). These children are stored
22 in the array-part\footnote{Tables in Lua can be indexed by integers,
23 as regular arrays, or by any other Lua data. Moreover, their
24 internal representation is able to optimize both array-style and
25 hashtable-style usage, and both kinds of keys can be used in the
26 same table. In this manual, I'll refer to the integer-indexed part
27 of a table as its array-part, and the other one as its hash-part.}
28 of the table, i.e. with consecutive integers as keys.
33 The most canonical example of ADT is probably the inductive list. Such
34 a list is described either as the empty list \verb+Nil+, or a pair
35 (called a \verb+cons+ in Lisp) of the first element on one side
36 (\verb+car+ in Lisp), and the list of remaining elements on the other
37 side (\verb+cdr+ in Lisp). These will be represented in Lua as
38 \verb+{ tag = "Nil" }+ and {\tt\{ tag = "Cons", car, cdr \}}. The list
39 (1, 2, 3) will be represented as:
50 Here is a more programming language oriented example: imagine that we
51 are working on a symbolic calculator. We will have to work this:
53 \item literal numbers, represented as integers;
54 \item symbolic variables, represented by the string of their
56 \item formulae, i.e. numbers, variables an/or sub-formulae
57 combined by operators. Such a formula is represented by the symbol
58 of its operator, and the sub-formulae / numbers / variables it
61 Most operations, e.g. evaluation or simplification, will do different
62 things depending on whether it is applied on a number, a variable or a
63 formula. Moreover, the meaning of the fields in data structures depends
64 on that data type. The datatype is given by the name put in the
65 \verb+tag+ field. In this example, \verb+tag+ can be one of
66 \verb+Number+, \verb+Var+ or \verb+Formula+. The formula $e^{i\pi}+1$
69 { tag="Formula", "Addition",
70 { tag="Formula", "Exponent",
71 { tag="Variable", "e" },
72 { tag="Formula", "Multiplication",
73 { tag="Variable", "i" },
74 { tag="Variable", "pi" } } },
80 The simple data above already has a quite ugly representation, so here
81 are the syntax extensions we provide to represent trees in a more
85 \item The tag can be put in front of the table, prefixed with a
86 backquote. For instance, {\tt\{ tag = "Cons", car, cdr \}} can be
87 abbreviated as {\tt`Cons\{ car, cdr \}}.
88 \item If the table contains nothing but a tag, the braces can be
89 omitted. Therefore, \verb+{ tag = "Nil" }+ can be abbreviated as
90 \verb+`Nil+ (although \verb|`Nil{ }| is also legal).
91 \item If there is only one element in the table besides the tag, and
92 this element is a literal number or a literal string, braces can be
93 omitted. Therefore {\tt\{ tag = "Foo", "Bar" \}} can be abbreviated
97 With this syntax sugar, the $e^{i\pi}+1$ example above would read:
100 `Formula"{ "Exponent",
102 `Formula{ "Multiplication",
108 Notice that this is a valid description of some tree structure in metalua, but
109 it's not a representation of metalua code: metalua code is represented as tree
110 structures indeed, but a structure different from this example's one. In other
111 words, this is an ADT, but not an AST.
113 For the record, the metalua (AST) representation of the code {\tt"1+e\^\ (i*pi)"}
116 `Op{ "add", `Number 1,
118 `Op{ "mul", `Id "i", `Id "pi" } } }
121 After reading more about AST definition and manipulation tools, you'll hopefully
122 be convinced that the latter representation is more powerful.
124 \subsection{Abstract Syntax Trees (AST)}
126 An AST is an Abstract Syntax Tree, a data representation of source
127 code suitable for easy manipulation. AST are just a particular usage
128 of ADT, and we will represent them with the ADT syntax described
131 \paragraph{Example} this is the tree representing the source code
132 \verb+print(foo, "bar")+:
134 \verb+`Call{ `Id "print", `Id "foo", `String "bar" }+
136 Metalua tries, as much as possible, to shield users from direct AST
137 manipulation, and a thorough knowledge of them is generally not
138 needed. Metaprogrammers should know their general form, but it is
139 reasonnable to rely on a cheat-sheet to remember the exact details of
140 AST structures. Such a summary is provided
141 in an appendix of this tutorial, as a reference when dealing with them.
143 In the rest of this section, we will present the translation from Lua
144 source to their corresponding AST.
146 \subsection{AST $\Longleftrightarrow$ Lua source translation}
148 This subsection explains how to translate a piece of lua source code
149 into the corresponding AST, and conversely. Most of time, users will
150 rely on a mechanism called quasi-quotes to produce the AST they will
151 work with, but it is sometimes necessary to directly deal with AST,
152 and therefore to have at least a superficial knowledge of their
155 \subsubsection{Expressions}
157 The expressions are pieces of Lua code which can be evaluated to give a
158 value. This includes constants, variable identifiers, table
159 constructors, expressions based on unary or binary operators, function
160 definitions, function calls, method invocations, and index selection
163 Expressions should not be confused with statements: an expression has
164 a value with can be returned through evaluation, whereas statements
165 just execute themselves and change the computer state (mainly memory
166 and IO). For instance, \verb|2+2| is an expression which evaluates to
167 4, but \verb|four=2+2| is a statement, which sets the value of
168 variable \verb|four| but has no value itself.
170 \paragraph{Number constants}
171 A number is represented by an AST with tag \verb+Number+ and the
172 number value as its sole child. For instance, \verb+6+ is represented
173 by \verb+`Number 6+\footnote{As explained in the section about ADT,
174 {\tt `Number 6} is exactly the same as {\tt `Number\{ 6 \}}, or
175 plain Lua {\tt\{ tag="Number", 6\}} }.
177 \paragraph{String constants}
178 A string is represented by an AST with tag \verb+String+ and the
179 string as its sole child. For instance, \verb+"foobar"+ is
181 \verb+`String "foobar"+.
183 \paragraph{Variable names}
184 A variable identifier is represented by an AST with tag \verb+Id+ and the
185 number value as its sole child. For instance, variable \verb+foobar+ is
186 represented by \verb+`Id "foobar"+.
188 \paragraph{Other atomic values}
189 Here are the translations of other keyword-based atomic values:
191 \item \verb+nil+ is encoded as \verb+`Nil+\footnote{which is a
192 short-hand for {\tt`Nil\{ \}}, or {\tt\{ tag="Nil" \}} in plain Lua.};
193 \item \verb+false+ is encoded as \verb+`False+;
194 \item \verb+true+ is encoded as \verb+`True+;
195 \item \verb+...+ is encoded as \verb+`Dots+.
198 \paragraph{Table constructors}
199 A table constructor is encoded as:
201 \verb+`Table{ ( `Pair{ expr expr } | expr )* }+
203 This is a list, tagged with \verb+Table+, whose elements are either:
205 \item the AST of an expression, for array-part entries without an
206 explicit associated key;
207 \item a pair of expression AST, tagged with \verb+Pair+: the first
208 expression AST represents a key, and the second represents the value
209 associated to this key.
212 \subparagraph{Examples}
215 \item The empty table \verb+{ }+ is represented as \verb+`Table{ }+;
217 \item \verb+{1, 2, "a"}+ is represented as:\\
218 \verb+`Table{ `Number 1, `Number 2, `String "a" }+;
220 \item \verb+{x=1, y=2}+ is syntax sugar for \verb+{["x"]=1, ["y"]=2}+,
221 and is represented by {\tt`Table\{ `Pair\{ `String "x", `Number 1
222 \}, `Pair\{ `String "y", `Number 2\} \}};
224 \item indexed and non-indexed entries can be mixed:
225 \verb+{ 1, [100]="foo", 3}+ is represented as {\tt`Table\{ `Number
226 1, `Pair\{ `Number 100, `String "foo"\}, `Number 3 \}};
230 \paragraph{Binary Operators}
231 Binary operations are represented by {\tt`Op\{ operator, left,
232 right\}}, where \verb+operator+ is a the operator's name as one of
233 the strings below, \verb+left+ is the AST of the left operand, and
234 \verb+right+ the AST of the right operand.
236 The following table associates a Lua operator to its AST name:
239 \begin{tabular}{|c|c||c|c||c|c||c|c|}
246 \hline\hline %%%%%%%%%%%%%%%%%
247 \verb|+| & \verb+"add"+ &
248 \verb+-+ & \verb+"sub"+ &
249 \verb+*+ & \verb+"mul"+ &
250 \verb+/+ & \verb+"div"+ \\
251 \hline %%%%%%%%%%%%%%%%%%%%%%%
252 \verb+%+ & \verb+"mod"+ &
253 \verb+^+ & \verb+"pow"+ &
254 \verb+..+ & \verb+"concat"+ &
255 \verb+==+ & \verb+"eq"+ \\
256 \hline %%%%%%%%%%%%%%%%%%%%%%%
257 \verb+<+ & \verb+"lt"+ &
258 \verb+<=+ & \verb+"le"+ &
259 \verb+and+ & \verb+"and"+ &
260 \verb+or+ & \verb+"or"+ \\
261 \hline %%%%%%%%%%%%%%%%%%%%%%%
265 Operator names are the same as the corresponding Lua metatable entry,
266 without the prefix {\tt"\_\,\_"}. There are no operators for
267 \verb+~=+, \verb+>=+ and \verb+>+: they can be simulated by swapping
268 the arguments of \verb+<=+ and \verb+<+, or adding a \verb+not+ to
271 \subparagraph{Examples}
273 \item \verb|2+2| is represented as
274 \verb|`Op{ 'add', `Number 2, `Number 2 }|;
275 \item \verb|1+2*3| is represented as:\\[-2em]
277 `Op{ 'add', `Number 1,
278 `Op{ 'mul', `Number 2, `Number 3 } }
280 \item \verb|(1+2)*3| is represented as:\\[-2em]
282 `Op{ 'mul, `Op{ 'add', `Number 1, `Number 2 },
286 \verb|`Op{ 'mul', `Op{ 'add', `Number 1, `Number 2 }, `Number 3 }|
287 \item \verb|x>=1 and x<42 | is represented as:\\[-2em]
289 `Op{ 'and', `Op{ 'le', `Number 1, `Id "x" },
290 `Op{ 'lt', `Id "x", `Number 42 } }
295 \paragraph{Unary Operators}
296 Unary operations are similar to binary operators, except that they
297 only take the AST of one subexression. The following table associates
298 a Lua unary operator to its AST:
301 \begin{tabular}{|c|c||c|c||c|c|}
307 \hline\hline %%%%%%%%%%%%%%
308 \verb+-+ & \verb+"unm"+ &
309 \verb+#+ & \verb+"len"+ &
310 \verb+not+ & \verb+"not"+ \\
311 \hline %%%%%%%%%%%%%%%%%%%%
315 \subparagraph{Examples}
317 \item \verb|-x| is represented as \verb|`Op{ 'unm', `Id "x" }|;
318 \item \verb|-(1+2)| is represented as:\\
319 \verb|`Op{ 'unm', `Op{ 'add', `Number 1, `Number 2 } }|
320 \item \verb|#x| is represented as
321 \verb|`Op{ 'len', `Id "x" }|
324 \paragraph{Indexed accesses}
325 They are represented by an AST with tag \verb+Index+, the table's AST
326 as first child, and the key's AST as second child.
328 \subparagraph{Examples}
330 \item \verb+x[3]+ is represented as \verb+`Index{ `Id "x", `Number 3 }+;
331 \item \verb+x[3][5]+ is represented as:\\
332 \verb+`Index{ `Index{ `Id "x", `Number 3 }, `Number 5 }+
333 \item \verb+x.y+ is syntax sugar for \verb+x["y"]+, and is represented as:\\
334 \verb+`Index{ `Id "x", `String "y" }+
337 Notice that an index AST can also appear as the left-hand side of
338 an assignment, as shall be shown in the subsection dedicated to
341 \paragraph{Function calls}
342 A function call AST has the tag \verb+Call+, the called function's AST
343 as the first child, and its arguments as the remaining children.
345 \subparagraph{Examples}
347 \item \verb+f()+ is represented as \verb+`Call{ `Id "f" }+;
348 \item \verb+f(x, 1)+ is represented as
349 \verb+`Call{ `Id "f", `Id "x", `Number 1 }+;
350 \item \verb+f(x, ...)+ is represented as
351 \verb+`Call{ `Id "f", `Id "x", `Dots }+.
354 Notice that function calls can be used as expressions, but also as statements.
356 \paragraph{Method invocations}
357 A method invocation AST has the tag \verb+Invoke+, the object's AST as
358 the first child, the string name of the method as the second child, and
359 the arguments as remaining children.
361 \subparagraph{Examples}
363 \item \verb+o:f()+ is represented as \verb+`Invoke{ `Id "o", String "f" }+;
364 \item \verb+o:f(x, 1)+ is represented as:\\
365 \verb+`Invoke{ `Id "o", `String "f", `Id "x", `Number 1 }+;
366 \item \verb+o:f(x, ...)+ is represented as:\\
367 \verb+`Invoke{ `Id "o", `String "f", `Id "x", `Dots }+;
370 Notice that method invocations can be used as expressions, but also as
371 statements. Notice also that ``{\tt function o:m (x) return x end}'' is
372 not a method invocation, but syntax sugar for the statement ``{\tt
373 o["f"] = function (self, x) return x end}''. See the paragraph about
374 assignment in the statements subsection for its AST representation.
377 \paragraph{Function definitions}
378 A function definition consists of a list of parameters and a block of
379 statements. The parameter list, which can be empty, contains only
380 variable names, represented by their \verb+`Id{...}+ AST, except for
381 the last element of the list, which can also be a dots AST \verb+`Dots+
382 (to indicate that the function is a vararg function).
384 The block is a list of statement AST, optionally terminated with a
385 \verb+`Return{...}+ or \verb+`Break+ pseudo-statement. These
386 pseudo-statements will be described in the statements subsection.
388 FIXME: finally, return and break will be considered as regular
389 statements: it's useful for many macros.
391 The function definition is encoded as
392 \verb+`Function{ parameters block }+
394 \subparagraph{Examples}
397 \item \verb+function (x) return x end+ is represented as:\\
398 \verb+`Function{ { `Id x } { `Return{ `Id "x" } } }+;
400 \item \verb+function (x, y) foo(x); bar(y) end+ is represented as:
402 `Function{ { `Id x, `Id y }
403 { `Call{ `Id "foo", `Id "x" },
404 `Call{ `Id "bar", `Id "y" } } }
407 \item \verb+function (fmt, ...) print (string.format (fmt, ...)) end+
410 `Function{ { `Id "fmt", `Dots }
411 { `Call{ `Id "print",
412 `Call{ `Index{ `Id "string",
418 \item \verb+function f (x) return x end+ is not an expression, but a
419 statement: it is actually syntax sugar for the assignment {\tt f =
420 function (x) return x end}, and as such, is represented as:
423 { `Function{ {`Id 'x'} {`Return{`Id 'x'} } } } }
425 (see assignment in the statements subsection for more details);
429 \paragraph{Parentheses}
431 In Lua, parentheses are sometimes semantically meaningful: when the
432 parenthesised expression returns multiple values, putting it between
433 parentheses forces it to return only one value. For instance, ``{\tt
434 local function f() return 1, 2, 3 end; return \{ f() \}}'' will
435 return ``{\tt\{1, 2, 3\}}'', whereas ``{\tt local function f() return
436 1, 2, 3 end; return \{ (f()) \}}'' will return ``{\tt\{ 1 \}}''
437 (notice the parentheses around the function call).
439 Parentheses are represented in the AST as a node ``{\tt`Paren\{
440 \}}''. The second example above has the following AST:
443 { `Localrec{ { `Id "f" },
448 `Return{ `Table{ `Paren{ `Call{ `Id "f" } } } } }
451 \subsubsection{Statements}
453 Statements are instructions which modify the state of the
454 computer. There are simple statements, such as variable assignments,
455 local variable declarations, function calls and method invocations;
456 there are also control structure statements, which take simpler
457 statements and modify their action: these are if/then/else,
458 repeat/until, while/do/end, for/do/end and do/end statements.
460 \paragraph{Assignments}
461 A variable assignment \verb+a, b, c = foo, bar+ is represented by the
462 AST \verb+`Set{ lhs, rhs }+, with {\tt lhs} being a list of variables or
463 table indexes, and {\tt rhs} the list of values assigned to them.
465 \subparagraph{Examples}
468 \item \verb+x[1]=2+ is represented as:\\
469 \verb+`Set{ { `Index{ `Id "x", `Number 1 } }, { `Number 2 } }+;
471 \item \verb+a, b = 1, 2+ is represented as:\\
472 \verb+`Set{ { `Id "a",`Id "b" }, { `Number 1, `Number 2 } }+;
474 \item \verb+a = 1, 2, 3+ is represented as:\\
475 \verb+`Set{ { `Id "a" }, { `Number 1, `Number 2, `Number 3 } }+;
477 \item \verb+function f(x) return x end+ is syntactic sugar for:\\
478 \verb+f = function (x) return x end+. As such, it is represented as:\\[-2em]
481 { `Function{ {`Id 'x'} {`Return{ `Id "x" } } } } }
484 \item \verb+function o:m(x) return x end+ is syntactic sugar for:\\
485 \verb+o["f"] = function (self, x) return x end+, and as such, is
486 represented as:\\[-2em]
488 `Set{ { `Index{ `Id "o", `String "f" } },
489 { `Function{ { `Id "self, "`Id x }
490 { `Return{ `Id "x" } } } } }
495 \paragraph{Local declarations}
496 A local declaration \verb+local a, b, c = foo, bar+ works just as an
497 assignment, except that the tag is \verb+Local+, and it is allowed to
498 have an empty list as values.
500 \subparagraph{Examples}
503 \item \verb+local x=2+ is represented as:\\
504 \verb+`Local{ { `Id "x" }, { `Number 2 } }+;
506 \item \verb+local a, b+ is represented as:\\
507 \verb+`Local{ { `Id "a",`Id "b" }, { } }+;
511 \paragraph{Recursive local declarations}
512 In a local declaration, the scope of local variables starts {\em
513 after} the statement. Therefore, it is not possible to refer to a
514 variable inside the value it receives, and
515 ``{\tt local function f(x) f(x) end}'' is not equivalent to
516 ``{\tt local f = function (x) f(x) end}'': in the latter, the \verb|f|
517 call inside the function definition probably refers to some global
518 variable, whereas in the former, it refers to the local variable
519 currently being defined (f is therefore a function looping forever).
521 To handle this, the AST syntax defines a special \verb|`Localrec|
522 local declaration statement, in which the variables enter into scope
523 {\em before} their content is evaluated. Therefore, the AST
524 corresponding to {\tt local function f(x) f(x) end} is:
526 `Localrec{ { `Id "f" },
527 { `Function{ { `Id x }
528 { `Call{ `Id "f", `Id "x" } } } } }
531 \caveat{In the current implementation, both variable name lists and
532 value lists have to be of lenght 1. This is enough to represent
533 {\tt local function ... end}, but should be generalized in the
534 final version of Metalua.}
537 \paragraph{Function calls and method invocations}
538 They are represented the same way as their expression counterparts,
539 see the subsection above for details.
541 \paragraph{Blocks and pseudo-statements}
542 Control statements generally take a block of instructions as
543 parameters, e.g. as the body of a \verb|for| loop. Such statement
544 blocks are represented as the list of the instructions they
545 contain. As a list, the block itself has no \verb|tag| field.
547 \subparagraph{Example}
548 \verb|foo(x); bar(y); return x,y| is represented as:
550 { `Call{ `Id "foo", `Id "x" },
551 `Call{ `Id "bar", `Id "y" },
552 `Return{ `Id "x", `Id "y" } }
555 \paragraph{Do statements}
556 These represent \verb|do ... end| statements, which limit the scope of
557 local variables. They are represented as blocks with a \verb|Do| tag.
559 \subparagraph{Example}
560 \verb|do foo(x); bar(y); return x,y end| is represented as:
562 `Do{ `Call{ `Id "foo", `Id "x" },
563 `Call{ `Id "bar", `Id "y" },
564 `Return{ `Id "x", `Id "y" } }
567 \paragraph{While statements}
568 \verb|while <foo> do <bar1>; <bar2>; ... end| is represented as \\
569 \verb|`While{ <foo>, { <bar1>, <bar2>, ... } }|.
571 \paragraph{Repeat statements}
572 \verb|repeat <bar1>; <bar2>; ... until <foo>| is represented as \\
573 \verb|`Repeat{ { <bar1>, <bar2>, ... }, <foo> }|.
575 \paragraph{For statements}
577 {\tt for x=<first>,<last>,<step> do <foo>; <bar>; ... end} is
578 represented as {\tt `Fornum\{ `Id "x", <first>, <last>, <step>, \{
579 <foo>, <bar>, ... \} \}}.
581 The \verb|step| parameter can be omitted if it is equal to 1.
584 for x1, x2... in e1, e2... do
591 {\tt `Forin\{ \{`Id "x1",`Id "x2",...\}, \{ <e1>, <e2>,... \} \{
592 <foo>, <bar>, ... \} \}}.
594 \paragraph{If statements}
595 ``If'' statements are composed of a series of (condition, block)
596 pairs, and optionally of a last default ``else'' block. The conditions
597 and blocks are simply listed in an \verb|`If{ ... }| ADT. Notice that
598 an ``if'' statement without a final ``else'' block will have an even
599 number of children, whereas a statement with a final ``else'' block
600 will have an odd number of children.
602 \subparagraph{Examples}
605 \item \verb+if <foo> then <bar>; <baz> end+ is represented as:\\
606 \verb+`If{ <foo>, { <bar>, <baz> } }+;
608 \item \verb+if <foo> then <bar1> else <bar2>; <baz2> end+
610 \verb+`If{ <foo>, { <bar1> }, { <bar2>, <baz2> } }+;
613 \verb+if <foo1> then <bar1>; <baz1> elseif <foo2> then <bar2>; <baz2> end+
614 \\ is represented as: \\
615 \verb+`If{ <foo1>, { <bar1>, <baz1> }, <foo2>,{ <bar2>, <baz2> } }+;
619 if <foo1> then <bar1>; <baz1>
620 elseif <foo2> then <bar2>; <baz2>
621 else <bar3>; <baz3> end+
625 `If{ <foo1>, { <bar1>, <baz1> },
626 <foo2>, { <bar2>, <baz2> },
632 \paragraph{Breaks and returns}
633 Breaks are represented by the childless \verb|`Break| AST. Returns are
634 retpresented by the (possibly empty) list of returned values.
636 \subparagraph{Example}
637 {\tt return 1, 2, 3} is represented as:\\
638 {\tt`Return\{ `Number 1, `Number 2, `Number 3 \}}.
640 \subsubsection{Extensions with no syntax}
642 A couple of AST nodes do not exist in Lua, nor in Metalua native
643 syntax, but are provided because they are particularly useful for
644 writing macros. They are presented here.
646 \paragraph{Goto and Labels}
648 Labels can be string AST, identifier AST, or simply string; they
649 indicate a target for goto statements. A very common idiom is ``{\tt
650 local x = mlp.gensym(); ... `Label\{ x \} }''. You just jump to that
651 label with ``{\tt `Goto\{ x \} }''.
653 Identifiers, string AST or plain strings are equivalent:
654 ``{\tt`Label\{ `Id "foo"\}}'' is synonymous for ``{\tt`Label\{ `String
655 "foo"\}}'' and ``{\tt`Label "foo"}''. The same equivalences apply
658 Labels are local to a function; you can safely jump out of a block,
659 but if you jump {\em into} a block, you're likely to get into unspecified
660 trouble, as local variables will be in a random state.
662 \paragraph{Statements in expressions}
663 A common need when writing a macro is to insert a statement in the
664 middle of an expression. It can be done by using an anonymous function
665 closure, but that would be expensive, so Metalua offers a better
666 solution. The \verb|`Stat| node evaluates a statement block in the
667 middle of an expression, then returns an arbitrary expression as its
668 result. Notice one important point: the expression is evaluated in
669 the block's context, i.e. if there are some local variables declared
670 in the block, the expression can use them.
672 For instance, {\tt `Stat\{ +\{local x=3\}, +\{x\}\}} evaluates to 3.
674 %\subsubsection{Formal translation defintion}
676 %\caveat{FIXME: here should go a formal, inductive definition of
677 % AST/syntax translation, to serve as a reference}