tla_eval/
error.rs

1use std::fmt;
2
3pub type Result<T> = std::result::Result<T, Error>;
4
5#[derive(Debug, Clone, PartialEq, Eq)]
6pub enum Error {
7    /// A name the specification never declares or defines.
8    Undefined(String),
9    /// A value used where its type makes no sense — `Len` of an integer, a
10    /// non-boolean conjunct, arithmetic on a string.
11    Type(String),
12    /// `x'` with no successor state supplied: the expression is an action but
13    /// was evaluated as a state predicate.
14    NoNextState(String),
15    /// A construct that cannot be decided by looking at one state or one step:
16    /// `[]P`, `<>P`, `WF_v(A)`, `ENABLED A`.
17    NotGround(String),
18    /// Enumeration of something that cannot be enumerated, or that is larger
19    /// than the evaluator will materialize.
20    Unbounded(String),
21    /// A specification error the language itself forbids: `@` outside EXCEPT,
22    /// wrong operator arity, a recursive definition that does not terminate.
23    Malformed(String),
24    Syntax(tla_syntax::Error),
25}
26
27impl fmt::Display for Error {
28    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
29        match self {
30            Error::Undefined(name) => write!(f, "`{name}` is not defined"),
31            Error::Type(m)
32            | Error::NoNextState(m)
33            | Error::NotGround(m)
34            | Error::Unbounded(m)
35            | Error::Malformed(m) => f.write_str(m),
36            Error::Syntax(e) => write!(f, "{e}"),
37        }
38    }
39}
40
41impl std::error::Error for Error {}
42
43impl From<tla_syntax::Error> for Error {
44    fn from(e: tla_syntax::Error) -> Self {
45        Error::Syntax(e)
46    }
47}
48
49pub(crate) fn type_error<T>(msg: impl Into<String>) -> Result<T> {
50    Err(Error::Type(msg.into()))
51}
tla_eval/error.rs

tla_eval/
error.rs
