oak_vampire/lexer/
token_type.rs

1use oak_core::TokenType;
2
3/// Vampire token types.
4#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
5#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
6pub enum VampireTokenType {
7    /// End of file.
8    Eof,
9    /// Whitespace.
10    Whitespace,
11    /// Line comment.
12    LineComment,
13    /// Block comment.
14    BlockComment,
15    /// String literal.
16    StringLiteral,
17    /// Integer literal.
18    IntegerLiteral,
19    /// Real literal.
20    RealLiteral,
21    /// Identifier.
22    Identifier,
23
24    /// The `fof` keyword (first-order formula).
25    FofKw,
26    /// The `cnf` keyword (conjunctive normal form).
27    CnfKw,
28    /// The `tff` keyword (typed first-order formula).
29    TffKw,
30    /// The `thf` keyword (typed higher-order formula).
31    ThfKw,
32    /// The `tpi` keyword (typed predicate inference).
33    TpiKw,
34    /// The `include` keyword.
35    IncludeKw,
36    /// The `axiom` keyword.
37    AxiomKw,
38    /// The `hypothesis` keyword.
39    HypothesisKw,
40    /// The `definition` keyword.
41    DefinitionKw,
42    /// The `assumption` keyword.
43    AssumptionKw,
44    /// The `lemma` keyword.
45    LemmaKw,
46    /// The `theorem` keyword.
47    TheoremKw,
48    /// The `conjecture` keyword.
49    ConjectureKw,
50    /// The `negated_conjecture` keyword.
51    NegatedConjectureKw,
52    /// The `plain` keyword.
53    PlainKw,
54    /// The `type` keyword.
55    TypeKw,
56    /// The `fi_domain` keyword.
57    FiDomainKw,
58    /// The `fi_functors` keyword.
59    FiFunctorsKw,
60    /// The `fi_predicates` keyword.
61    FiPredicatesKw,
62    /// The `unknown` keyword.
63    UnknownKw,
64    /// The `!` (forall) quantifier keyword.
65    ForallKw,
66    /// The `?` (exists) quantifier keyword.
67    ExistsKw,
68    /// The `&` (and) logical operator keyword.
69    AndKw,
70    /// The `|` (or) logical operator keyword.
71    OrKw,
72    /// The `~` (not) logical operator keyword.
73    NotKw,
74    /// The `=>` (implies) logical operator keyword.
75    ImpliesKw,
76    /// The `<=>` (if and only if) logical operator keyword.
77    IffKw,
78    /// The `<~>` (xor) logical operator keyword.
79    XorKw,
80    /// The `~|` (nor) logical operator keyword.
81    NorKw,
82    /// The `~&` (nand) logical operator keyword.
83    NandKw,
84    /// The `$bool` type keyword.
85    BoolKw,
86    /// The `$i` (individual) type keyword.
87    IndividualKw,
88    /// The `$int` type keyword.
89    IntKw,
90    /// The `$real` type keyword.
91    RealKw,
92    /// The `$rat` type keyword.
93    RatKw,
94    /// The `$tType` type keyword.
95    TTypeKw,
96    /// The `$o` type keyword.
97    OTypeKw,
98    /// The `$iType` type keyword.
99    ITypeKw,
100    /// Boolean literal (`$true` or `$false`).
101    BoolLiteral,
102
103    /// The `==` equality operator.
104    DoubleEq,
105    /// The `!=` inequality operator.
106    NotEq,
107    /// The `<=` less-than-or-equal operator.
108    LessEq,
109    /// The `>=` greater-than-or-equal operator.
110    GreaterEq,
111    /// The `&&` logical and operator.
112    AndAnd,
113    /// The `||` logical or operator.
114    OrOr,
115    /// The `++` increment operator.
116    PlusPlus,
117    /// The `--` decrement operator.
118    MinusMinus,
119    /// The `+=` addition assignment operator.
120    PlusEq,
121    /// The `-=` subtraction assignment operator.
122    MinusEq,
123    /// The `*=` multiplication assignment operator.
124    StarEq,
125    /// The `/=` division assignment operator.
126    SlashEq,
127    /// The `%=` modulo assignment operator.
128    PercentEq,
129    /// The `<<` left shift operator.
130    LeftShift,
131    /// The `>>` right shift operator.
132    RightShift,
133    /// The `->` arrow operator.
134    Arrow,
135
136    /// Left parenthesis `(`.
137    LeftParen,
138    /// Right parenthesis `)`.
139    RightParen,
140    /// Left bracket `[`.
141    LeftBracket,
142    /// Right bracket `]`.
143    RightBracket,
144    /// Left brace `{`.
145    LeftBrace,
146    /// Right brace `}`.
147    RightBrace,
148    /// Colon `:`.
149    Colon,
150    /// Semicolon `;`.
151    Semicolon,
152    /// Dot `.`.
153    Dot,
154    /// Comma `,`.
155    Comma,
156    /// Question mark `?`.
157    Question,
158    /// Exclamation mark `!`.
159    Bang,
160    /// At sign `@`.
161    At,
162    /// Hash `#`.
163    Hash,
164    /// Dollar sign `$`.
165    Dollar,
166    /// Percent `%`.
167    Percent,
168    /// Caret `^`.
169    Caret,
170    /// Ampersand `&`.
171    Ampersand,
172    /// Asterisk `*`.
173    Star,
174    /// Plus `+`.
175    Plus,
176    /// Minus `-`.
177    Minus,
178    /// Equals `=`.
179    Eq,
180    /// Less-than `<`.
181    LessThan,
182    /// Greater-than `>`.
183    GreaterThan,
184    /// Slash `/`.
185    Slash,
186    /// Backslash `\`.
187    Backslash,
188    /// Pipe `|`.
189    Pipe,
190    /// Tilde `~`.
191    Tilde,
192}
193
194impl TokenType for VampireTokenType {
195    const END_OF_STREAM: Self = VampireTokenType::Eof;
196    type Role = oak_core::UniversalTokenRole;
197
198    fn role(&self) -> Self::Role {
199        match self {
200            VampireTokenType::Eof => oak_core::UniversalTokenRole::Eof,
201            VampireTokenType::Whitespace => oak_core::UniversalTokenRole::Whitespace,
202            VampireTokenType::LineComment | VampireTokenType::BlockComment => oak_core::UniversalTokenRole::Comment,
203            VampireTokenType::StringLiteral => oak_core::UniversalTokenRole::Literal,
204            VampireTokenType::IntegerLiteral | VampireTokenType::RealLiteral => oak_core::UniversalTokenRole::Literal,
205            VampireTokenType::Identifier => oak_core::UniversalTokenRole::Name,
206
207            VampireTokenType::FofKw
208            | VampireTokenType::CnfKw
209            | VampireTokenType::TffKw
210            | VampireTokenType::ThfKw
211            | VampireTokenType::TpiKw
212            | VampireTokenType::IncludeKw
213            | VampireTokenType::AxiomKw
214            | VampireTokenType::HypothesisKw
215            | VampireTokenType::DefinitionKw
216            | VampireTokenType::AssumptionKw
217            | VampireTokenType::LemmaKw
218            | VampireTokenType::TheoremKw
219            | VampireTokenType::ConjectureKw
220            | VampireTokenType::NegatedConjectureKw
221            | VampireTokenType::PlainKw
222            | VampireTokenType::TypeKw
223            | VampireTokenType::FiDomainKw
224            | VampireTokenType::FiFunctorsKw
225            | VampireTokenType::FiPredicatesKw
226            | VampireTokenType::UnknownKw
227            | VampireTokenType::ForallKw
228            | VampireTokenType::ExistsKw
229            | VampireTokenType::AndKw
230            | VampireTokenType::OrKw
231            | VampireTokenType::NotKw
232            | VampireTokenType::ImpliesKw
233            | VampireTokenType::IffKw
234            | VampireTokenType::XorKw
235            | VampireTokenType::NorKw
236            | VampireTokenType::NandKw
237            | VampireTokenType::BoolKw
238            | VampireTokenType::IndividualKw
239            | VampireTokenType::IntKw
240            | VampireTokenType::RealKw
241            | VampireTokenType::RatKw
242            | VampireTokenType::TTypeKw
243            | VampireTokenType::OTypeKw
244            | VampireTokenType::ITypeKw
245            | VampireTokenType::BoolLiteral => oak_core::UniversalTokenRole::Keyword,
246
247            _ => oak_core::UniversalTokenRole::Operator,
248        }
249    }
250}
251
252impl From<VampireTokenType> for u16 {
253    fn from(t: VampireTokenType) -> u16 {
254        t as u16
255    }
256}
257
258impl From<u16> for VampireTokenType {
259    fn from(i: u16) -> Self {
260        unsafe { std::mem::transmute(i as u8) }
261    }
262}
oak_vampire/lexer/token_type.rs

oak_vampire/lexer/
token_type.rs
