Parsing style [Was: [plt-scheme] proof checking: a, subproblem]

Noel wrote:
> Parsing is not such an interesting problem when
> you have sexps and read, and macros let you integrate a
> traditional YACC style parser into the language.

But Danny's solution isn't integrated in that fashion; it uses an 
implementation of lex/Bison in Scheme (which may use macros down below, 
but I can't see them). It works nicely, but I feel I'm transgressing 
some unwritten law. You (Noel) taught me how to apply macros to 
something in an input file, but I still don't know enough about macros 
to see how to transform something that is quite distant from s-exps.

Danny's solution extends pretty easily to checking a whole proof: I can 
extend the grammar to match whole lines and then sets of lines, and the 
action on recognizing a line is to throw the AST into a hash table (idea 
stolen from calc.ss example), after first retrieving the ASTs for the 
cited lines from the hash table and checking that the cited rule 
constructs the line just recognized (straightforward application of 
"equal?"). Is that deeply unidiomatic? When last I used yacc, my only 
exposure to functional programming was through reading John Backus's 
Turing Award lecture (recent at the time). --PR