Parser-interface
API functions for parsing Leo programs.
This section defines convenient functions
(whose names start with parse-from-)
for parsing Leo programs from:
- a list of Unicode code points
- a list of UTF-8 bytes
- an ACL2 string (in UTF-8)
- a file
By "parsing", we mean lexing, tokenization, and parsing, with
the result being a CST (concrete syntax tree) for a Leo file,
and optionally the sequence of lexeme CSTs (see below).
Additionally, we define functions for parsing specific Leo constructs
from strings: file, statement, expression, and token.
These can be used for the <leo>/tests/parser namespaces
Parse, ParseExpression, ParseStatement, and Token,
where <leo> is the GitHub repo of the Leo compiler.
See parse-fragment-to-CST. For simply checking if a given
string can be fully parsed, we define predicates xxx-parses? for
the same set of supported rulenames.
The API functions whose names end in + also return the full sequence
of lexemes from the lexer. This can be valuable for checking correctness,
for proving theorems, and for locating specific tokens within the
input.
Subtopics
- Parse-from-file-at-path+
- Parse a Leo file at a path.
- Tokens-to-cst
- Parse list of tokens for a supported grammar rule name.
- Parse-fragment-to-cst+
- Parse source string for a supported grammar rule name.
- Lexemes-to-cst+
- Tokenize and parse list of lexemes for a supported grammar rule name.
- Parse-from-string+
- Parse UTF-8 ACL2 string into a CST.
- Parse-from-codepoints+
- Parse Unicode code points into a CST.
- Parse-fragment-to-cst
- Parse source string for a supported grammar rule name.
- Parse-from-bytes+
- Parse UTF-8 bytes into a CST.
- Parse-from-string
- Parse UTF-8 ACL2 string into a CST.
- Parse-from-file-at-path
- Parse a Leo file at a path.
- Token-parses?
- Checks if the given string can be parsed to a Leo token CST.
- Statement-parses?
- Checks if the given string can be parsed to a Leo statement CST.
- Expression-parses?
- Checks if the given string can be parsed to a Leo expression CST.
- File-parses?
- Checks if the given string can be parsed to a Leo file CST.
- Token-parses-same-fringe?
- Checks if the given string can be parsed to a Leo token CST.
- Expression-parses-same-fringe?
- Checks if the given string can be parsed to a Leo expression CST.
- Statement-parses-same-fringe?
- Checks if the given string can be parsed to a Leo statement CST.
- Parse-from-codepoints
- Parse Unicode code points into a CST.
- File-parses-same-fringe?
- Checks if the given string can be parsed to a Leo file CST.
- Parse-from-bytes
- Parse UTF-8 bytes into a CST.
