Re: [isabelle] Parser in ML



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

> On 13 Dec 2013, at 4:35, "Lawrence Paulson" <lp15 at cam.ac.uk> wrote:
>
> 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
>
>

________________________________

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.




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