tla_syntax/
token.rs

1#[derive(Debug, Clone, Copy, PartialEq, Eq)]
2pub enum Kw {
3    Module,
4    Extends,
5    Constant,
6    Variable,
7    Let,
8    In,
9    If,
10    Then,
11    Else,
12    Choose,
13    Case,
14    Other,
15    Assume,
16    Theorem,
17    Instance,
18    With,
19    Local,
20    Recursive,
21    Lambda,
22    /// A keyword that only appears inside a TLAPS proof.
23    Proof,
24    Except,
25    True,
26    False,
27    Domain,
28    Subset,
29    Union,
30    Enabled,
31    Unchanged,
32}
33
34impl Kw {
35    /// How the keyword is spelled, for the rare specification that defines
36    /// something by that name. `Proof` stands for a dozen words at once and so
37    /// has none.
38    pub fn text(self) -> Option<&'static str> {
39        Some(match self {
40            Self::Module => "MODULE",
41            Self::Extends => "EXTENDS",
42            Self::Constant => "CONSTANT",
43            Self::Variable => "VARIABLE",
44            Self::Let => "LET",
45            Self::In => "IN",
46            Self::If => "IF",
47            Self::Then => "THEN",
48            Self::Else => "ELSE",
49            Self::Choose => "CHOOSE",
50            Self::Case => "CASE",
51            Self::Other => "OTHER",
52            Self::Assume => "ASSUME",
53            Self::Theorem => "THEOREM",
54            Self::Instance => "INSTANCE",
55            Self::With => "WITH",
56            Self::Local => "LOCAL",
57            Self::Recursive => "RECURSIVE",
58            Self::Lambda => "LAMBDA",
59            Self::Except => "EXCEPT",
60            Self::True => "TRUE",
61            Self::False => "FALSE",
62            Self::Domain => "DOMAIN",
63            Self::Subset => "SUBSET",
64            Self::Union => "UNION",
65            Self::Enabled => "ENABLED",
66            Self::Unchanged => "UNCHANGED",
67            Self::Proof => return None,
68        })
69    }
70
71    pub fn lookup(word: &str) -> Option<Self> {
72        Some(match word {
73            "MODULE" => Self::Module,
74            "EXTENDS" => Self::Extends,
75            "CONSTANT" | "CONSTANTS" => Self::Constant,
76            "VARIABLE" | "VARIABLES" => Self::Variable,
77            "LET" => Self::Let,
78            "IN" => Self::In,
79            "IF" => Self::If,
80            "THEN" => Self::Then,
81            "ELSE" => Self::Else,
82            "CHOOSE" => Self::Choose,
83            "CASE" => Self::Case,
84            "OTHER" => Self::Other,
85            "ASSUME" | "ASSUMPTION" => Self::Assume,
86            "INSTANCE" => Self::Instance,
87            "WITH" => Self::With,
88            "LOCAL" => Self::Local,
89            "RECURSIVE" => Self::Recursive,
90            "LAMBDA" => Self::Lambda,
91            "THEOREM" | "LEMMA" | "COROLLARY" | "PROPOSITION" | "AXIOM" => Self::Theorem,
92            "PROOF" | "BY" | "OBVIOUS" | "OMITTED" | "QED" | "DEF" | "DEFS" | "DEFINE"
93            | "SUFFICES" | "PICK" | "WITNESS" | "HAVE" | "TAKE" | "USE" | "HIDE" | "PROVE"
94            | "NEW" | "ONLY" => Self::Proof,
95            "EXCEPT" => Self::Except,
96            "TRUE" => Self::True,
97            "FALSE" => Self::False,
98            "DOMAIN" => Self::Domain,
99            "SUBSET" => Self::Subset,
100            "UNION" => Self::Union,
101            "ENABLED" => Self::Enabled,
102            "UNCHANGED" => Self::Unchanged,
103            _ => return None,
104        })
105    }
106}
107
108#[derive(Debug, Clone, Copy, PartialEq, Eq)]
109pub enum Op {
110    Implies,
111    Equiv,
112    Or,
113    And,
114    Eq,
115    Neq,
116    Lt,
117    Gt,
118    Le,
119    Ge,
120    In,
121    NotIn,
122    Subseteq,
123    Supseteq,
124    AtAt,
125    OneTo,
126    Cup,
127    Cap,
128    SetMinus,
129    DotDot,
130    Plus,
131    Minus,
132    Times,
133    Div,
134    Mod,
135    Cartesian,
136    Concat,
137    Pow,
138    Not,
139    Always,
140    Eventually,
141    Forall,
142    Exists,
143    Domain,
144    Subset,
145    BigUnion,
146    Enabled,
147    Unchanged,
148    /// `P ~> Q`: temporal leads-to.
149    LeadsTo,
150    /// `\AA x : F` and `\EE x : F`: quantification over a hidden variable.
151    TemporalForall,
152    TemporalExists,
153    /// An operator the language reserves a symbol and a precedence for but
154    /// gives no meaning to. Every one of these exists to be defined by a
155    /// specification; `\prec`, `\oplus` and `&` are all of them.
156    User(&'static str),
157}
158
159/// The symbols TLA+ sets aside for specifications to define, with the
160/// precedence the language fixes for each. Taken from the operator table in
161/// *Specifying Systems*; the left binding power is used, which is what matters
162/// for reading an expression back the way it was written.
163pub(crate) const USER_OPERATORS: &[(&str, u8)] = &[
164    ("\\prec", 5),
165    ("\\preceq", 5),
166    ("\\succ", 5),
167    ("\\succeq", 5),
168    ("\\sqsubset", 5),
169    ("\\sqsubseteq", 5),
170    ("\\sqsupset", 5),
171    ("\\sqsupseteq", 5),
172    ("\\subset", 5),
173    ("\\supset", 5),
174    ("\\ll", 5),
175    ("\\gg", 5),
176    ("\\sim", 5),
177    ("\\simeq", 5),
178    ("\\approx", 5),
179    ("\\asymp", 5),
180    ("\\cong", 5),
181    ("\\doteq", 5),
182    ("\\propto", 5),
183    ("\\cdot", 5),
184    ("\\mod", 11),
185    ("...", 9),
186    ("--", 11),
187    ("\\times", 11),
188    ("|-", 5),
189    ("-|", 5),
190    ("|=", 5),
191    ("=|", 5),
192    ("::=", 5),
193    ("<:", 7),
194    (":=", 5),
195    ("\\sqcap", 9),
196    ("\\sqcup", 9),
197    ("\\uplus", 9),
198    ("\\oplus", 10),
199    ("\\ominus", 11),
200    ("(+)", 10),
201    ("(-)", 11),
202    ("(.)", 13),
203    ("(/)", 13),
204    ("(\\X)", 13),
205    ("\\odot", 13),
206    ("\\oslash", 13),
207    ("\\otimes", 13),
208    ("\\star", 13),
209    ("\\bullet", 13),
210    ("\\bigcirc", 13),
211    ("\\wr", 14),
212    ("&", 13),
213    ("&&", 13),
214    ("|", 10),
215    ("||", 10),
216    ("$", 9),
217    ("$$", 9),
218    ("??", 9),
219    ("%%", 11),
220    ("##", 9),
221    ("!!", 9),
222    ("^^", 14),
223    ("++", 10),
224    ("**", 13),
225    ("//", 13),
226    ("/", 13),
227    ("^+", 15),
228    ("^*", 15),
229    ("^#", 15),
230    ("-+->", 2),
231];
232
233pub(crate) fn user_operator(symbol: &str) -> Option<Op> {
234    USER_OPERATORS
235        .iter()
236        .find(|(name, _)| *name == symbol)
237        .map(|(name, _)| Op::User(name))
238}
239
240impl Op {
241    /// Binding power as an infix operator; `None` for prefix-only operators.
242    ///
243    /// Ordering follows TLA+'s table where it matters for these specs: `\cup`
244    /// binds tighter than `=`, and `:>` tighter than `@@`, so `a \cup {b} = c`
245    /// and `("k" :> v) @@ rest` parse without parentheses.
246    pub fn infix_prec(self) -> Option<u8> {
247        Some(match self {
248            Self::Implies => 1,
249            Self::Equiv | Self::LeadsTo => 2,
250            Self::Or => 3,
251            Self::And => 4,
252            Self::Eq
253            | Self::Neq
254            | Self::Lt
255            | Self::Gt
256            | Self::Le
257            | Self::Ge
258            | Self::In
259            | Self::NotIn
260            | Self::Subseteq
261            | Self::Supseteq => 5,
262            Self::AtAt => 6,
263            Self::OneTo => 7,
264            Self::Cup | Self::Cap | Self::SetMinus => 8,
265            Self::DotDot => 9,
266            Self::Plus | Self::Minus => 10,
267            Self::Times | Self::Div | Self::Mod | Self::Cartesian => 11,
268            Self::Concat => 12,
269            Self::Pow => 13,
270            Self::User(_) if self.is_postfix() => return None,
271            Self::User(symbol) => {
272                return USER_OPERATORS
273                    .iter()
274                    .find(|(name, _)| *name == symbol)
275                    .map(|(_, prec)| *prec);
276            }
277            _ => return None,
278        })
279    }
280
281    /// `s^+`, `s^*` and `s^#` follow their operand rather than sitting
282    /// between two, so they are never infix.
283    pub fn is_postfix(self) -> bool {
284        matches!(self, Self::User("^+" | "^*" | "^#"))
285    }
286
287    pub fn is_right_assoc(self) -> bool {
288        matches!(self, Self::Implies | Self::Pow)
289    }
290
291    /// How the operator is written. Where TLA+ offers several spellings the
292    /// ASCII one is chosen, so printed output can be re-read by the parser.
293    pub fn symbol(self) -> &'static str {
294        match self {
295            Self::Implies => "=>",
296            Self::Equiv => "<=>",
297            Self::Or => "\\/",
298            Self::And => "/\\",
299            Self::Eq => "=",
300            Self::Neq => "#",
301            Self::Lt => "<",
302            Self::Gt => ">",
303            Self::Le => "<=",
304            Self::Ge => ">=",
305            Self::In => "\\in",
306            Self::NotIn => "\\notin",
307            Self::Subseteq => "\\subseteq",
308            Self::Supseteq => "\\supseteq",
309            Self::AtAt => "@@",
310            Self::OneTo => ":>",
311            Self::Cup => "\\cup",
312            Self::Cap => "\\cap",
313            Self::SetMinus => "\\",
314            Self::DotDot => "..",
315            Self::Plus => "+",
316            Self::Minus => "-",
317            Self::Times => "*",
318            Self::Div => "\\div",
319            Self::Mod => "%",
320            Self::Cartesian => "\\X",
321            Self::Concat => "\\o",
322            Self::Pow => "^",
323            Self::Not => "~",
324            Self::Always => "[]",
325            Self::Eventually => "<>",
326            Self::Forall => "\\A",
327            Self::Exists => "\\E",
328            Self::Domain => "DOMAIN",
329            Self::Subset => "SUBSET",
330            Self::BigUnion => "UNION",
331            Self::Enabled => "ENABLED",
332            Self::Unchanged => "UNCHANGED",
333            Self::LeadsTo => "~>",
334            Self::TemporalForall => "\\AA",
335            Self::TemporalExists => "\\EE",
336            Self::User(symbol) => symbol,
337        }
338    }
339
340    /// How tightly the operator holds its operand when used as a prefix, and
341    /// so how tightly it binds as a node in printed output.
342    pub fn prefix_prec(self) -> u8 {
343        match self {
344            Self::Minus => 11,
345            Self::Domain | Self::Subset | Self::BigUnion => 9,
346            _ => 5,
347        }
348    }
349
350    /// True for the word-shaped prefix operators, which need a space before
351    /// their operand where the symbolic ones do not.
352    pub fn is_word(self) -> bool {
353        matches!(
354            self,
355            Self::Domain | Self::Subset | Self::BigUnion | Self::Enabled | Self::Unchanged
356        )
357    }
358}
359
360#[derive(Debug, Clone, PartialEq, Eq)]
361pub enum Tok {
362    Ident(String),
363    Num(i64),
364    /// `123.456`, kept as written: TLA+ decimals are exact, and no binary
365    /// floating-point type could hold one faithfully.
366    Decimal(String),
367    Str(String),
368    Kw(Kw),
369    Op(Op),
370    /// `WF_vars` / `SF_vars`, which lex as one word but mean an operator
371    /// applied to a subscript.
372    Fair {
373        strong: bool,
374        subscript: String,
375    },
376    ModuleEnd,
377    Separator,
378    DefEq,
379    LParen,
380    RParen,
381    LBrack,
382    RBrack,
383    LBrace,
384    RBrace,
385    LTup,
386    RTup,
387    Comma,
388    Colon,
389    /// The `::` of a labelled expression.
390    ColonColon,
391    Dot,
392    Bang,
393    /// The `@` of an `EXCEPT` update, standing for the value being replaced.
394    At,
395    Underscore,
396    Prime,
397    MapsTo,
398    Arrow,
399    Gets,
400    Eof,
401}
402
403#[derive(Debug, Clone, PartialEq, Eq)]
404pub struct Token {
405    pub tok: Tok,
406    pub line: u32,
407    pub col: u32,
408}
tla_syntax/token.rs

tla_syntax/
token.rs
