| document | ||
| mllex-polyml | ||
| mlyacc-polyml | ||
| .gitignore | ||
| Calc.thy | ||
| CalcExpert.thy | ||
| Datalog.thy | ||
| Examples.thy | ||
| LexYacc.thy | ||
| Manual.thy | ||
| Pascal.thy | ||
| README.md | ||
| ROOT | ||
| YaccLib.thy | ||
Lex and Yacc for Isabelle/ML
This repository provides a deep integration of ml-lex and ml-yacc into Isabelle/ML (and, hence, Isabelle/HOL).
ml-lex and ml-yacc
The work is based on the port of ml-lex and ml-yacc of the sml/nj project to Poly/ML:
These tools have been modified in several ways. In particular, they have been modified to work "in memory", i.e., taking the lex and yacc specifications as strings and returning the generated lexer and parser as string. They also have been modified to report errors using the error reporting provided by Isabelle/PIDE.