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

Prabhakar Ragde wrote:
> 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. 

See:
http://library.readscheme.org/servlets/cite.ss?pattern=sw2004-owens

...particularly Section 2.2, "The Scheme Way".  (PLT has great propaganda ;)

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

Scheme macros require input in s-expression form, so for anything else, 
you need something to transform the input syntax, even if you just 
transform it into s-expressions and deal with it from there.  A 
yacc-style parser is a reasonable choice if the language you're 
implementing justifies it.

You could, in theory, write a macro named e.g. "formula" that accepts 
input like the following:

   (formula ~(p V ~q) -> (q -> ~p A r))

Note that I got rid of the "/\" and "\/" because those won't parse well 
in most Schemes, including PLT (you could perhaps modify the reader, but 
that way lies ickiness).

But with input such as the above, you'll be essentially writing a parser 
of your own anyway, as part of the implementation of the "formula" 
macro, since the typical macro pattern matchers won't be useful for 
matching a language like that.  PLT's general matcher might be more 
useful, but using that you'll still end up with a kind of recursive 
descent parser.

So, when you're dealing with a language like that, it's of dubious 
benefit to implement it with macros alone.

> 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? 

If you have an s-exp syntax, then macros and ordinary Scheme makes 
sense.  If you need some non-sexp syntax, and you can benefit from the 
scalability of parser-tools, then that's a great solution, particularly 
because of how it's integrated into PLT Scheme.

Anton