Email Gateway (Aug 19 2022 at 12:59): Email Gateway (Aug 19 2022 at 12:59):From: li yongjian <lyj238@gmail.com>
Dear Isabelle experts:
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.
I know that Objcaml has a support for YACC to generate a parse, and I
prefer this Yacc approach. I want to know whther Poly ML supports YACC to
create a parser?
yongjian Li
Email Gateway (Aug 19 2022 at 12:59):From: li yongjian <lyj238@gmail.com>
Dear Isabelle experts:
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.
I know that Objcaml has a support for YACC to generate a parse, and I
prefer this Yacc approach. I want to know whther Poly ML supports YACC to
create a parser?
yongjian Li
Email Gateway (Aug 19 2022 at 12:59):From: Lawrence Paulson <lp15@cam.ac.uk>
The answer is yes.
I believe there all the information that you need can be found on this page:
http://www.tbrk.org/software/poly_smlnj-lib.html
It is not entirely trivial to set up.
Larry Paulson
Email Gateway (Aug 19 2022 at 12:59):From: Michael Norrish <Michael.Norrish@nicta.com.au>
The C Parser that I wrote uses exactly this approach and uses mlyacc and mllex. In fact, the C parser distribution includes code for building those tools.
Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 12:59):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Apr 19 2024 at 12:27 UTC