Lexing-and-parsing
Lexing and parsing of Leo.
We formalize the requirements for lexing and parsing
Unicode character sequences to Leo CSTs.
We formalize these requirements for Leo (code) files,
for Leo input files,
and for Leo putput files.
We plan to extend this to cover Leo configuration files.
The lexing specification is common for
code files, input files, and output files.
The parsing specification differs between them.
We plan to prove that lexing and parsing are unambiguous.
Subtopics
- Lexer
- An executable lexer of Leo.
- Parser
- An executable parser of Leo.
- Token-fringe
- Token fringe.
- Longest-lexp
- Longest lexeme rule.
- Parser-interface
- API functions for parsing Leo programs.
- Grammar-lexp
- Grammatical lexing.
- Identifier-lexp
- Lexing of Identifiers.
- Output-file-parsep
- Parsing of Leo output files.
- Input-file-parsep
- Parsing of Leo input files.
- File-lex-parse-p
- Lexing and parsing of Leo files.
- Filter-tokens
- Token filtering.
- Lexp
- Declarative specification of lexing.
- File-parsep
- Parsing of Leo files.
- Input-parser
- An executable parser of Leo input files.
- Output-file-lex-parse-p
- Lexing and parsing of Leo output files.
- Input-file-lex-parse-p
- Lexing and parsing of Leo input files.
- Parser-abstractor-interface
- API functions for parsing and abstracting Leo programs from CST to AST.
- Identifier-abnf-stringp
- Check if an ABNF string (i.e. a list of natural numbers)
is the fringe of a tree for an identifier.
- Symbol-abnf-stringp
- Check if an ABNF string (i.e. a list of natural numbers)
is the fringe of a tree for a symbol.
- Keyword-abnf-stringp
- Check if an ABNF string (i.e. a list of natural numbers)
is the fringe of a tree for a keyword.
- Output-parser
- An executable parser of Leo output files.
- Tokenizer
- Turn lexemes into tokens.
