| .bin | ||
| document | ||
| mllex-polyml | ||
| mlyacc-polyml | ||
| .envrc | ||
| .gitignore | ||
| Calc.thy | ||
| CalcExpert.thy | ||
| Datalog.thy | ||
| Examples.thy | ||
| LexYacc.thy | ||
| LICENSE | ||
| 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.
Authors
License
This project is licensed under a 3-clause BSD-style license.
SPDX-License-Identifier: BSD-3-Clause
Upstream Repository
The upstream git repository, i.e., the single source of truth, for this project is hosted by the Software Assurance & Security Research Team at https://git.logicalhacking.com/adbrucker/isabelle_lex-yacc/.