Logiweb(TM)

7.12.11 Backquoting

Prev Up Next Page 241 of 800 Search internet


The value of

back t quote 2 + x unquote + 3 end quote

equals the value of

quote 2 + x + 3 end quote

except for two things:

As an example, the value of

let x = quote 6 * 7 end quote in back t quote 2 + x unquote + x end quote

equals quote 2 + 6 * 7 + x end quote except for debugging information. In contrast, the value of

let x = quote 6 * 7 end quote in quote 2 + x unquote + x end quote

equals quote 2 + x unquote + x end quote because 'unquoting' (the underlining) does not work inside quotes.

As an example of use, consider again the 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 implements that e.g. all x ,, y ,, z : P macro expands to all x : all y : all z : P. The expand-all function unpacks the argument x and macro expands the subterms u and v of the term t. 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 debugging information is taken from the unexpanded term t.

The term all x ,, y ,, z : P does not really macro expand to all x : all y : all z : P. Rather, it expands to

f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . P

That is so because it was chosen on the Peano page to let universal quantification piggyback lambda abstraction. That allows to re-use functions for variable substitution and computation of the 'free' and 'freefor' side conditions.

The definition of expand-all1 reads:

eager define expand-all1 ( t , u , v ) as newline if .not. u r= quote x ,, y end quote then back t quote f.allfunc \ u unquote . v unquote end quote else newline expand-all1 ( t , u first , expand-all1 ( t , u second , v ) ) end define

The expand-all1 function traverses u as long as the principal operator of u is a comma operator and then uses back t quote f.allfunc \ u unquote . v unquote end quote to construct a universal quantifier with debugging information taken from t. The debugging information is only inserted in the root of the tree, not in the subtrees u and v which retain their own debugging information.

Prev Up Next Page 241 of 800 Search logiweb.eu

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