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    // Keywords
25    FofKw,
26    CnfKw,
27    TffKw,
28    ThfKw,
29    TpiKw,
30    IncludeKw,
31    AxiomKw,
32    HypothesisKw,
33    DefinitionKw,
34    AssumptionKw,
35    LemmaKw,
36    TheoremKw,
37    ConjectureKw,
38    NegatedConjectureKw,
39    PlainKw,
40    TypeKw,
41    FiDomainKw,
42    FiFunctorsKw,
43    FiPredicatesKw,
44    UnknownKw,
45    ForallKw,
46    ExistsKw,
47    AndKw,
48    OrKw,
49    NotKw,
50    ImpliesKw,
51    IffKw,
52    XorKw,
53    NorKw,
54    NandKw,
55    BoolKw,
56    IndividualKw,
57    IntKw,
58    RealKw,
59    RatKw,
60    TTypeKw,
61    OTypeKw,
62    ITypeKw,
63    BoolLiteral,
64
65    // Operators
66    DoubleEq,
67    NotEq,
68    LessEq,
69    GreaterEq,
70    AndAnd,
71    OrOr,
72    PlusPlus,
73    MinusMinus,
74    PlusEq,
75    MinusEq,
76    StarEq,
77    SlashEq,
78    PercentEq,
79    LeftShift,
80    RightShift,
81    Arrow,
82
83    // Single char tokens
84    LeftParen,
85    RightParen,
86    LeftBracket,
87    RightBracket,
88    LeftBrace,
89    RightBrace,
90    Colon,
91    Semicolon,
92    Dot,
93    Comma,
94    Question,
95    Bang,
96    At,
97    Hash,
98    Dollar,
99    Percent,
100    Caret,
101    Ampersand,
102    Star,
103    Plus,
104    Minus,
105    Eq,
106    LessThan,
107    GreaterThan,
108    Slash,
109    Backslash,
110    Pipe,
111    Tilde,
112}
113
114impl TokenType for VampireTokenType {
115    const END_OF_STREAM: Self = VampireTokenType::Eof;
116    type Role = oak_core::UniversalTokenRole;
117
118    fn role(&self) -> Self::Role {
119        match self {
120            VampireTokenType::Eof => oak_core::UniversalTokenRole::Eof,
121            VampireTokenType::Whitespace => oak_core::UniversalTokenRole::Whitespace,
122            VampireTokenType::LineComment | VampireTokenType::BlockComment => oak_core::UniversalTokenRole::Comment,
123            VampireTokenType::StringLiteral => oak_core::UniversalTokenRole::Literal,
124            VampireTokenType::IntegerLiteral | VampireTokenType::RealLiteral => oak_core::UniversalTokenRole::Literal,
125            VampireTokenType::Identifier => oak_core::UniversalTokenRole::Name,
126
127            VampireTokenType::FofKw
128            | VampireTokenType::CnfKw
129            | VampireTokenType::TffKw
130            | VampireTokenType::ThfKw
131            | VampireTokenType::TpiKw
132            | VampireTokenType::IncludeKw
133            | VampireTokenType::AxiomKw
134            | VampireTokenType::HypothesisKw
135            | VampireTokenType::DefinitionKw
136            | VampireTokenType::AssumptionKw
137            | VampireTokenType::LemmaKw
138            | VampireTokenType::TheoremKw
139            | VampireTokenType::ConjectureKw
140            | VampireTokenType::NegatedConjectureKw
141            | VampireTokenType::PlainKw
142            | VampireTokenType::TypeKw
143            | VampireTokenType::FiDomainKw
144            | VampireTokenType::FiFunctorsKw
145            | VampireTokenType::FiPredicatesKw
146            | VampireTokenType::UnknownKw
147            | VampireTokenType::ForallKw
148            | VampireTokenType::ExistsKw
149            | VampireTokenType::AndKw
150            | VampireTokenType::OrKw
151            | VampireTokenType::NotKw
152            | VampireTokenType::ImpliesKw
153            | VampireTokenType::IffKw
154            | VampireTokenType::XorKw
155            | VampireTokenType::NorKw
156            | VampireTokenType::NandKw
157            | VampireTokenType::BoolKw
158            | VampireTokenType::IndividualKw
159            | VampireTokenType::IntKw
160            | VampireTokenType::RealKw
161            | VampireTokenType::RatKw
162            | VampireTokenType::TTypeKw
163            | VampireTokenType::OTypeKw
164            | VampireTokenType::ITypeKw
165            | VampireTokenType::BoolLiteral => oak_core::UniversalTokenRole::Keyword,
166
167            _ => oak_core::UniversalTokenRole::Operator,
168        }
169    }
170}
171
172impl From<VampireTokenType> for u16 {
173    fn from(t: VampireTokenType) -> u16 {
174        t as u16
175    }
176}
177
178impl From<u16> for VampireTokenType {
179    fn from(i: u16) -> Self {
180        unsafe { std::mem::transmute(i as u8) }
181    }
182}
oak_vampire/lexer/token_type.rs

oak_vampire/lexer/
token_type.rs
