Definition of a racket language for parsing expression grammars that generate a parse tree and also provide a type directed semantics for pretty printing them. The library also uses a type inference algorithm which determines if the PEG is complete, i.e. terminates its execution on all inputs.
In order to type check, the tool need a working installation of Z3 SMT Solver. The project is known to work with Z3 version 4.8.14.
Following the racket approach to build small languages, we have build some auxiliar languages to ease the task of use/debug the tool.
#lang typed-peg
: default language, provides a parse and pretty printing function for the specified PEG, after infering types for the input PEG.#lang typed-peg/untyped
: disable the type-inference engine. Use at your own risk!#lang typed-peg/debug/tokenize-only
: outputs the result of the lexical analyser.#lang typed-peg/debug/parse-only
: outputs the result of the parser.#lang typed-peg/debug/constraints-only
: outputs the constraints generated by the algorithm.#lang typed-peg/debug/z3-script-only
: outputs the z3 script that encode the constraints.#lang typed-peg/debug/infer-only
: outputs the infered types for each grammar non-terminal.