Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-02 12:56:43 -0700 (Thu, 02 Sep 2004)
Revision: 6161
Log message:
This is an initial start at an alternate form of parsing.
See theories/mmc/test/mmc_grammar.ml for an example.
This version is resource-based, but I've reached an issue.
If parsing is resource-based, then it has to be delayed until
runtime. That isn't so bad, and it has the advantage of being
able to use runtime values like precedences and conversions.
However, the filter still has to participate a little, by handling
special quotations. Something like:
<:parse< text >> --> Base_parser.parse "text"
This doesn't really work--we need the resource that contains the grammar.
<:parse< text >> --> Base_parser.parse (get_parser_resource ???) "text"
The problem is the ???.
It could be:
let mark = gensym () in
Mp_resource.set_bookmark mark;
get_parser_resource (Mp_resource.find mark)
However, it is obvious that Mp_resource was not designed for
this kind of interaction.
So, we either fix Mp_resource, or push this all back into the filter.
I don't really like the latter option because we add another resource-like
thing that the filter has to manage; we have to design a new syntax for it;
filter_prog.ml gets even larger; and we have to marshal PDAs and such.