Crate tla_syntax 

Lexer, parser and AST for the fragment of TLA+ that specifications are written in: modules, declarations, definitions and expressions.

Temporal formulas are parsed into the AST but carry no meaning here — the evaluator that consumes this crate answers questions about concrete states, not about behaviours.

Re-exports

pub use ast::Bound;

pub use ast::Decl;

pub use ast::Def;

pub use ast::ExceptPath;

pub use ast::Expr;

pub use ast::LetInstance;

pub use ast::Module;

pub use ast::Param;

pub use ast::QuantKind;

pub use ast::Unit;

pub use error::Error;

pub use error::Result;

pub use error::Stage;

Modules

ast

error

token

Constants

DEFAULT_NESTING_LIMIT

How deeply expressions may nest before the parser gives up on them.

Functions

lex

parse_expression

Parse a bare expression, with no surrounding module. Task definitions carry predicates as strings, and they have nowhere else to live.

parse_expression_bounded

As parse_expression, with a nesting limit of your own.

parse_module

parse_module_bounded

Parse with a nesting limit of your own, for a caller whose stack is smaller than DEFAULT_NESTING_LIMIT assumes.