7.12.4 Advanced macros

Prev Up Next Page 234 of 800 Search internet

Instead of using define macro of x as y end define directly, use Macro define u as v end define. The latter construct is as general as the former but protects its left and right hand sides against macro expansion.

Here is an example of an 'advanced macro' from the Peano page:

Macro define all u : v as \ x . expand-all ( x ) end define

The real work is done by this function:

eager define expand-all ( x ) as newline let << t ,, s ,, c >> = x in newline let << true ,, u ,, v >> = t in newline let u = stateexpand ( u , s , c ) in newline let v = stateexpand ( v , s , c ) in newline expand-all1 ( t , u , v ) end define

The expand-all function expands e.g. all x ,, y ,, z : P into all x : all y : all z : P. The expand-all function is quite typical. Here is what it does:

First it destructures the value x into a term t, a macro state s, and a cache c. The term t is the term to be macro expanded, i.e. the one with the universal quantifier as principal operator. The macro state contains a recipe for macro expanding subterms. The cache is the cache of the page being macro expanded.

Then expand-all destructures the term t into the subterms u and v. Note that this is the only way to recover the subterms u and v. It does not work to refer to u and v in the right hand side of Macro define all u : v as \ x . expand-all ( x ) end define

Then expand-all macro expands the subterms u and v using the recipe s. Note that this has to be done explicitly in advanced macros like the one defined by expand-all. For simple macros defined by macro define x as y end define one does not need to worry about this. For advanced macros, one can choose to macro expand subterms, one can choose not to macro expand them, or one may choose to macro expand them using some other recipe than the one passed down to expand-all.

The macro state has form f :: s prime where f is the recipe itself expressed as a function. s prime is unused and is set to true by all macros described here, but is available for use in case some custom recipes need to include some extra information besides f.

The stateexpand function is essentially defined thus:

eager define stateexpand ( t , s , c ) as ( s head apply << t ,, s ,, c >> maptag ) untag end define

The definition on the base page looks a bit different, but that is because the base page does not use an eager definition eager define x as y end define and tuples for the definition of stateexpand. That is because eager definitions and tuples do not work before stateexpand is in place.

After expanding u and v, expand-all passes t, u, and v on to expand-all1 which finishes the work. The expand-all1 function mainly uses the macro expanded subterms u and v. But it also needs the unexpanded term t for a small detail:

The expand-all1 function returns a parse tree. That parse tree is made up from u and v plus constructs generated by expand-all1. The constructs generated by expand-all1 need to include debugging information so that one can see where they came from. That debugging information is taken from the unexpanded term t.

When writing advanced macros, one has to be very careful in including the right debugging information. When e.g. a proof checker finds an error in a proof, the proof checker must generate a meaningful error and typically calls some error message generator. The generator typically only has access to terms which have undergone macroexpansion and even may have undergone tactic expansion, and for which the context may have been lost. For such error message generators it is essential that the debugging information included in terms tell where the term came from.

Prev Up Next Page 234 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05