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

--- Prabhakar Ragde <plragde at uwaterloo.ca> wrote:

> 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). 

I was referring simply to this:

 - traditional Lex/Yacc is a separate program that takes an
input file written in some custom language and converts it
into a file of C|ML|whatever.

 - the parser-tools is a bunch of macros that takes Scheme
code and converts it into Scheme code

The Haskell guys want to write parsers without creating a
custom language, so they invent parser combinators.  Its
the language integration that macros give us (we write
Scheme to generate Scheme) that makes parser combinators
less interesting in Scheme.  

> It works nicely, but I feel I'm
> transgressing some unwritten law. 

Not really.  I think the parser solution is valid.  You can
embed infix languages in Scheme with macros (every once in
a while somebody does it with arithmetic -- I'm sure there
is an example in the archives) but unless you really want
the embedding it might be more effort than it's worth.

> Danny's solution extends pretty easily to checking a
> whole proof: ... Is that deeply unidiomatic? 

Seems ok to me!

N

Email: noelwelsh <at> yahoo <dot> com   noel <at> untyped <dot> com
AIM: noelhwelsh
Blogs: http://monospaced.blogspot.com/  http://www.untyped.com/untyping/

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com