tla-syntax 0.2.0

Parser, AST and printer for TLA+, with no dependencies
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

//! 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.

pub mod ast;
pub mod error;
mod lexer;
mod parser;
mod print;
pub mod token;

pub use ast::{Bound, Decl, Def, ExceptPath, Expr, LetInstance, Module, Param, QuantKind, Unit};
pub use error::{Error, Result, Stage};
pub use lexer::lex;
pub use parser::{
    DEFAULT_NESTING_LIMIT, parse_expression, parse_expression_bounded, parse_module,
    parse_module_bounded,
};