Re: [isabelle] Parser in ML
On Thu, 12 Dec 2013, li yongjian wrote:
Recently I meet a case study where I need:
a parser that accepts a foreign text file and transforms it into a thy
automatically generate some proofs.
I want to know whether poly-ML system that writes Isabelle have some
support for writing a parser.
I have read Larry's ML-book, and after reading the last two chapters, I
think that I can create a parser using suppot from Isabelle system.
The standard way to implement parsers in Isabelle/ML is via parser
combinators, see the ML modules Scan and Parse, and applications of the
same in the sources (e.g. using hypersearch in Isabelle/jEdit).
Note that you normally do not generate theory sources, but produce theory
content directly in ML. You can take $ISABELLE_HOME/src/HOL/SPARK as a
worked example for this approach.
People have also managed to use mllex and mlyacc, although that is rare
these days. E.g. see $ISABELLE_HOME/src/HOL/TPTP.
This archive was generated by a fusion of
Pipermail (Mailman edition) and