Parser-abstractor-interface
API functions for parsing and abstracting Leo programs from CST to AST.
This section defines convenient functions
(whose names start with ast-from-)
for parsing and abstracting Leo programs and fragments.
By "parsing", we mean lexing, tokenization, and parsing, with
the result being a CST (concrete syntax tree) for a Leo file.
By "abstracting", we mean simplifying the CST into an abstract syntax
tree (AST).
A list of specific Leo constructs is supported:
file, statement, expression, and token.
For token, we only support identifiers and atomic-literals.
Subtopics
- Ast-from-fragment
- Parse and abstract to AST.
- Ast-from-string
- Parse UTF-8 ACL2 string and abstract to a Leo file AST.
- Ast-from-file-at-path
- Parse and abstract a Leo file at a path into an AST.