Filter
Top Products
Chapter 7
Parsing and printing
We have already used the automatic quotation parsers quite extensively, and it’s
time we looked at the relationship between the underlying representations and the
surface syntax in more detail. Many convenient constructs are representing using
some special constants inside HOL, and the parser and printer transform such inter-
nal representations into more palatable surface syntax. For example the conditional
expression
if b then e1 else e2
is represented inside the logic using a constant COND:
CONS b e1 e2
Various other handy syntactic constructs are also dealt with in this way, e.g.
abstractions over non-variables, and let-terms. For example
\(x,y,z). x + y + z
is represented by:
GABS (\f. !x y z. GEQ (f (x,y,z)) (x + y + z))
and
let x = 1 and y = 2 in x + y
is represented by:
LET (\x y. LET_END (x + y)) 1 2
Apart from special case like these, the parser-printer transformations are pretty
straightforward. Identifiers may be declared infix, and given a precedence and
associativity (right or left) using parse as infix. Here are a few genuine examples
from the source code:
parse_as_infix("<",(12,"right"));;
parse_as_infix("+",(16,"right"));;
parse_as_infix("-",(18,"left"));;
parse_as_infix("IN",(11,"right"));;
parse_as_infix("UNION",(16,"right"));;
65