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.
> 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:
> 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