Re: [isabelle] Parser in ML



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


On 12 Dec 2013, at 14:56, li yongjian <lyj238 at gmail.com> wrote:

> 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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.