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
file and
 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 MHonArc.