oak_coq/parser/
element_type.rs

1use oak_core::{ElementType, UniversalElementRole};
2
3/// Element types for the Coq AST.
4#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
5#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
6pub enum CoqElementType {
7    /// Whitespace.
8    Whitespace,
9    /// Newline.
10    Newline,
11    /// Comment.
12    Comment,
13    // Literals
14    /// String literal.
15    StringLiteral,
16    /// Number literal.
17    NumberLiteral,
18    /// Identifier.
19    Identifier,
20
21    // Keywords
22    /// `Theorem` keyword.
23    Theorem,
24    /// `Lemma` keyword.
25    Lemma,
26    /// `Remark` keyword.
27    Remark,
28    /// `Fact` keyword.
29    Fact,
30    /// `Corollary` keyword.
31    Corollary,
32    /// `Proposition` keyword.
33    Proposition,
34    /// `Definition` keyword.
35    Definition,
36    /// `Example` keyword.
37    Example,
38    /// `Fixpoint` keyword.
39    Fixpoint,
40    /// `CoFixpoint` keyword.
41    CoFixpoint,
42    /// `Inductive` keyword.
43    Inductive,
44    /// `CoInductive` keyword.
45    CoInductive,
46    /// `Record` keyword.
47    Record,
48    /// `Structure` keyword.
49    Structure,
50    /// `Variant` keyword.
51    Variant,
52    /// `Module` keyword.
53    Module,
54    /// `Section` keyword.
55    Section,
56    /// `End` keyword.
57    End,
58    /// `Require` keyword.
59    Require,
60    /// `Import` keyword.
61    Import,
62    /// `Export` keyword.
63    Export,
64    /// `Proof` keyword.
65    Proof,
66    /// `Qed` keyword.
67    Qed,
68    /// `Defined` keyword.
69    Defined,
70    /// `Admitted` keyword.
71    Admitted,
72    /// `If` keyword.
73    If,
74    /// `Then` keyword.
75    Then,
76    /// `Else` keyword.
77    Else,
78    /// `Type` keyword.
79    Type,
80    /// `Prop` keyword.
81    Prop,
82    /// `Set` keyword.
83    Set,
84    /// `Check` keyword.
85    Check,
86    /// `Print` keyword.
87    Print,
88    /// `Search` keyword.
89    Search,
90    /// `Locate` keyword.
91    Locate,
92    /// `About` keyword.
93    About,
94    /// `Match` keyword.
95    Match,
96    /// `With` keyword.
97    With,
98    /// `Forall` symbol or keyword.
99    Forall,
100    /// `Exists` symbol or keyword.
101    Exists,
102    /// `Fun` keyword.
103    Fun,
104    /// `Let` keyword.
105    Let,
106    /// `In` keyword.
107    In,
108    /// `Class` keyword.
109    Class,
110    /// `Instance` keyword.
111    Instance,
112    /// `Intros` tactic keyword.
113    Intros,
114    /// `Simpl` tactic keyword.
115    Simpl,
116    /// `Reflexivity` tactic keyword.
117    Reflexivity,
118    /// `Rewrite` tactic keyword.
119    Rewrite,
120    /// `Apply` tactic keyword.
121    Apply,
122    /// `Exact` tactic keyword.
123    Exact,
124    /// `Assumption` tactic keyword.
125    Assumption,
126    /// `Auto` tactic keyword.
127    Auto,
128    /// `Trivial` tactic keyword.
129    Trivial,
130    /// `Discriminate` tactic keyword.
131    Discriminate,
132    /// `Injection` tactic keyword.
133    Injection,
134    /// `Inversion` tactic keyword.
135    Inversion,
136    /// `Destruct` tactic keyword.
137    Destruct,
138    /// `Induction` tactic keyword.
139    Induction,
140    /// `Generalize` tactic keyword.
141    Generalize,
142    /// `Clear` tactic keyword.
143    Clear,
144    /// `Unfold` tactic keyword.
145    Unfold,
146    /// `Fold` tactic keyword.
147    Fold,
148    /// `Compute` tactic keyword.
149    Compute,
150    /// `Eval` tactic keyword.
151    Eval,
152    /// `Show` tactic keyword.
153    Show,
154    /// `Goal` keyword.
155    Goal,
156    /// `Goals` keyword.
157    Goals,
158    /// `Undo` command keyword.
159    Undo,
160    /// `Restart` command keyword.
161    Restart,
162    /// `Admit` tactic keyword.
163    Admit,
164    /// `Abort` command keyword.
165    Abort,
166    /// `Parameter` keyword.
167    Parameter,
168    /// `Axiom` keyword.
169    Axiom,
170    /// `Variable` keyword.
171    Variable,
172    /// `Hypothesis` keyword.
173    Hypothesis,
174    /// `Chapter` keyword.
175    Chapter,
176    /// `Open` keyword.
177    Open,
178    /// `Close` keyword.
179    Close,
180    /// `Scope` keyword.
181    Scope,
182    /// `Notation` keyword.
183    Notation,
184    /// `Infix` keyword.
185    Infix,
186    /// `Reserved` keyword.
187    Reserved,
188    /// `Bind` keyword.
189    Bind,
190    /// `Delimit` keyword.
191    Delimit,
192    /// `Arguments` keyword.
193    Arguments,
194    /// `Implicit` keyword.
195    Implicit,
196    /// `Coercion` keyword.
197    Coercion,
198    /// `Identity` keyword.
199    Identity,
200    /// `Canonical` keyword.
201    Canonical,
202
203    // Operators and delimiters
204    /// Arrow `->`.
205    Arrow,
206    /// Double arrow `=>`.
207    DoubleArrow,
208    /// Colon `:`.
209    Colon,
210    /// Semicolon `;`.
211    Semicolon,
212    /// Comma `,`.
213    Comma,
214    /// Dot `.`.
215    Dot,
216    /// Pipe `|`.
217    Pipe,
218    /// Underscore `_`.
219    Underscore,
220    /// Equal `=`.
221    Equal,
222    /// Plus `+`.
223    Plus,
224    /// Minus `-`.
225    Minus,
226    /// Star `*`.
227    Star,
228    /// Slash `/`.
229    Slash,
230    /// Percent `%`.
231    Percent,
232    /// Less than `<`.
233    Less,
234    /// Greater than `>`.
235    Greater,
236    /// Less than or equal to `<=`.
237    LessEqual,
238    /// Greater than or equal to `>=`.
239    GreaterEqual,
240    /// Not equal `<>`.
241    NotEqual,
242    /// Tilde `~`.
243    Tilde,
244    /// At `@`.
245    At,
246    /// Question mark `?`.
247    Question,
248    /// Exclamation mark `!`.
249    Exclamation,
250    /// Ampersand `&`.
251    Ampersand,
252    /// Hash `#`.
253    Hash,
254    /// Dollar `$`.
255    Dollar,
256    /// Backslash `\`.
257    Backslash,
258    /// Caret `^`.
259    Caret,
260    /// Left parenthesis `(`.
261    LeftParen,
262    /// Right parenthesis `)`.
263    RightParen,
264    /// Left bracket `[`.
265    LeftBracket,
266    /// Right bracket `]`.
267    RightBracket,
268    /// Left brace `{`.
269    LeftBrace,
270    /// Right brace `}`.
271    RightBrace,
272    /// Double colon `::`.
273    DoubleColon,
274    /// Double colon equal `::=`.
275    DoubleColonEqual,
276    /// Colon equal `:=`.
277    ColonEqual,
278    /// Turnstile `|-`.
279    Turnstile,
280    /// Logical AND `/\`.
281    And,
282    /// Logical OR `\/`.
283    Or,
284    /// Left arrow `<-`.
285    LeftArrow,
286
287    // Elements
288    /// Root node.
289    Root,
290    /// Declaration node.
291    Declaration,
292    /// Statement node.
293    Statement,
294    /// Expression node.
295    Expression,
296    /// Parsing error.
297    Error,
298    /// End of stream.
299    Eof,
300}
301
302impl ElementType for CoqElementType {
303    type Role = UniversalElementRole;
304
305    fn role(&self) -> Self::Role {
306        match self {
307            _ => UniversalElementRole::None,
308        }
309    }
310}
311
312impl From<crate::lexer::token_type::CoqTokenType> for CoqElementType {
313    fn from(token: crate::lexer::token_type::CoqTokenType) -> Self {
314        match token {
315            crate::lexer::token_type::CoqTokenType::Whitespace => CoqElementType::Whitespace,
316            crate::lexer::token_type::CoqTokenType::Newline => CoqElementType::Newline,
317            crate::lexer::token_type::CoqTokenType::Comment => CoqElementType::Comment,
318            crate::lexer::token_type::CoqTokenType::StringLiteral => CoqElementType::StringLiteral,
319            crate::lexer::token_type::CoqTokenType::NumberLiteral => CoqElementType::NumberLiteral,
320            crate::lexer::token_type::CoqTokenType::Identifier => CoqElementType::Identifier,
321            crate::lexer::token_type::CoqTokenType::Theorem => CoqElementType::Theorem,
322            crate::lexer::token_type::CoqTokenType::Lemma => CoqElementType::Lemma,
323            crate::lexer::token_type::CoqTokenType::Remark => CoqElementType::Remark,
324            crate::lexer::token_type::CoqTokenType::Fact => CoqElementType::Fact,
325            crate::lexer::token_type::CoqTokenType::Corollary => CoqElementType::Corollary,
326            crate::lexer::token_type::CoqTokenType::Proposition => CoqElementType::Proposition,
327            crate::lexer::token_type::CoqTokenType::Definition => CoqElementType::Definition,
328            crate::lexer::token_type::CoqTokenType::Example => CoqElementType::Example,
329            crate::lexer::token_type::CoqTokenType::Fixpoint => CoqElementType::Fixpoint,
330            crate::lexer::token_type::CoqTokenType::CoFixpoint => CoqElementType::CoFixpoint,
331            crate::lexer::token_type::CoqTokenType::Inductive => CoqElementType::Inductive,
332            crate::lexer::token_type::CoqTokenType::CoInductive => CoqElementType::CoInductive,
333            crate::lexer::token_type::CoqTokenType::Record => CoqElementType::Record,
334            crate::lexer::token_type::CoqTokenType::Structure => CoqElementType::Structure,
335            crate::lexer::token_type::CoqTokenType::Variant => CoqElementType::Variant,
336            crate::lexer::token_type::CoqTokenType::Module => CoqElementType::Module,
337            crate::lexer::token_type::CoqTokenType::Section => CoqElementType::Section,
338            crate::lexer::token_type::CoqTokenType::End => CoqElementType::End,
339            crate::lexer::token_type::CoqTokenType::Require => CoqElementType::Require,
340            crate::lexer::token_type::CoqTokenType::Import => CoqElementType::Import,
341            crate::lexer::token_type::CoqTokenType::Export => CoqElementType::Export,
342            crate::lexer::token_type::CoqTokenType::Proof => CoqElementType::Proof,
343            crate::lexer::token_type::CoqTokenType::Qed => CoqElementType::Qed,
344            crate::lexer::token_type::CoqTokenType::Defined => CoqElementType::Defined,
345            crate::lexer::token_type::CoqTokenType::Admitted => CoqElementType::Admitted,
346            crate::lexer::token_type::CoqTokenType::If => CoqElementType::If,
347            crate::lexer::token_type::CoqTokenType::Then => CoqElementType::Then,
348            crate::lexer::token_type::CoqTokenType::Else => CoqElementType::Else,
349            crate::lexer::token_type::CoqTokenType::Type => CoqElementType::Type,
350            crate::lexer::token_type::CoqTokenType::Prop => CoqElementType::Prop,
351            crate::lexer::token_type::CoqTokenType::Set => CoqElementType::Set,
352            crate::lexer::token_type::CoqTokenType::Check => CoqElementType::Check,
353            crate::lexer::token_type::CoqTokenType::Print => CoqElementType::Print,
354            crate::lexer::token_type::CoqTokenType::Search => CoqElementType::Search,
355            crate::lexer::token_type::CoqTokenType::Locate => CoqElementType::Locate,
356            crate::lexer::token_type::CoqTokenType::About => CoqElementType::About,
357            crate::lexer::token_type::CoqTokenType::Match => CoqElementType::Match,
358            crate::lexer::token_type::CoqTokenType::With => CoqElementType::With,
359            crate::lexer::token_type::CoqTokenType::Forall => CoqElementType::Forall,
360            crate::lexer::token_type::CoqTokenType::Exists => CoqElementType::Exists,
361            crate::lexer::token_type::CoqTokenType::Fun => CoqElementType::Fun,
362            crate::lexer::token_type::CoqTokenType::Let => CoqElementType::Let,
363            crate::lexer::token_type::CoqTokenType::In => CoqElementType::In,
364            crate::lexer::token_type::CoqTokenType::Class => CoqElementType::Class,
365            crate::lexer::token_type::CoqTokenType::Instance => CoqElementType::Instance,
366            crate::lexer::token_type::CoqTokenType::Intros => CoqElementType::Intros,
367            crate::lexer::token_type::CoqTokenType::Simpl => CoqElementType::Simpl,
368            crate::lexer::token_type::CoqTokenType::Reflexivity => CoqElementType::Reflexivity,
369            crate::lexer::token_type::CoqTokenType::Rewrite => CoqElementType::Rewrite,
370            crate::lexer::token_type::CoqTokenType::Apply => CoqElementType::Apply,
371            crate::lexer::token_type::CoqTokenType::Exact => CoqElementType::Exact,
372            crate::lexer::token_type::CoqTokenType::Assumption => CoqElementType::Assumption,
373            crate::lexer::token_type::CoqTokenType::Auto => CoqElementType::Auto,
374            crate::lexer::token_type::CoqTokenType::Trivial => CoqElementType::Trivial,
375            crate::lexer::token_type::CoqTokenType::Discriminate => CoqElementType::Discriminate,
376            crate::lexer::token_type::CoqTokenType::Injection => CoqElementType::Injection,
377            crate::lexer::token_type::CoqTokenType::Inversion => CoqElementType::Inversion,
378            crate::lexer::token_type::CoqTokenType::Destruct => CoqElementType::Destruct,
379            crate::lexer::token_type::CoqTokenType::Induction => CoqElementType::Induction,
380            crate::lexer::token_type::CoqTokenType::Generalize => CoqElementType::Generalize,
381            crate::lexer::token_type::CoqTokenType::Clear => CoqElementType::Clear,
382            crate::lexer::token_type::CoqTokenType::Unfold => CoqElementType::Unfold,
383            crate::lexer::token_type::CoqTokenType::Fold => CoqElementType::Fold,
384            crate::lexer::token_type::CoqTokenType::Compute => CoqElementType::Compute,
385            crate::lexer::token_type::CoqTokenType::Eval => CoqElementType::Eval,
386            crate::lexer::token_type::CoqTokenType::Show => CoqElementType::Show,
387            crate::lexer::token_type::CoqTokenType::Goal => CoqElementType::Goal,
388            crate::lexer::token_type::CoqTokenType::Goals => CoqElementType::Goals,
389            crate::lexer::token_type::CoqTokenType::Undo => CoqElementType::Undo,
390            crate::lexer::token_type::CoqTokenType::Restart => CoqElementType::Restart,
391            crate::lexer::token_type::CoqTokenType::Admit => CoqElementType::Admit,
392            crate::lexer::token_type::CoqTokenType::Abort => CoqElementType::Abort,
393            crate::lexer::token_type::CoqTokenType::Parameter => CoqElementType::Parameter,
394            crate::lexer::token_type::CoqTokenType::Axiom => CoqElementType::Axiom,
395            crate::lexer::token_type::CoqTokenType::Variable => CoqElementType::Variable,
396            crate::lexer::token_type::CoqTokenType::Hypothesis => CoqElementType::Hypothesis,
397            crate::lexer::token_type::CoqTokenType::Chapter => CoqElementType::Chapter,
398            crate::lexer::token_type::CoqTokenType::Open => CoqElementType::Open,
399            crate::lexer::token_type::CoqTokenType::Close => CoqElementType::Close,
400            crate::lexer::token_type::CoqTokenType::Scope => CoqElementType::Scope,
401            crate::lexer::token_type::CoqTokenType::Notation => CoqElementType::Notation,
402            crate::lexer::token_type::CoqTokenType::Infix => CoqElementType::Infix,
403            crate::lexer::token_type::CoqTokenType::Reserved => CoqElementType::Reserved,
404            crate::lexer::token_type::CoqTokenType::Bind => CoqElementType::Bind,
405            crate::lexer::token_type::CoqTokenType::Delimit => CoqElementType::Delimit,
406            crate::lexer::token_type::CoqTokenType::Arguments => CoqElementType::Arguments,
407            crate::lexer::token_type::CoqTokenType::Implicit => CoqElementType::Implicit,
408            crate::lexer::token_type::CoqTokenType::Coercion => CoqElementType::Coercion,
409            crate::lexer::token_type::CoqTokenType::Identity => CoqElementType::Identity,
410            crate::lexer::token_type::CoqTokenType::Canonical => CoqElementType::Canonical,
411            crate::lexer::token_type::CoqTokenType::Arrow => CoqElementType::Arrow,
412            crate::lexer::token_type::CoqTokenType::DoubleArrow => CoqElementType::DoubleArrow,
413            crate::lexer::token_type::CoqTokenType::Colon => CoqElementType::Colon,
414            crate::lexer::token_type::CoqTokenType::Semicolon => CoqElementType::Semicolon,
415            crate::lexer::token_type::CoqTokenType::Comma => CoqElementType::Comma,
416            crate::lexer::token_type::CoqTokenType::Dot => CoqElementType::Dot,
417            crate::lexer::token_type::CoqTokenType::Pipe => CoqElementType::Pipe,
418            crate::lexer::token_type::CoqTokenType::Underscore => CoqElementType::Underscore,
419            crate::lexer::token_type::CoqTokenType::Equal => CoqElementType::Equal,
420            crate::lexer::token_type::CoqTokenType::Plus => CoqElementType::Plus,
421            crate::lexer::token_type::CoqTokenType::Minus => CoqElementType::Minus,
422            crate::lexer::token_type::CoqTokenType::Star => CoqElementType::Star,
423            crate::lexer::token_type::CoqTokenType::Slash => CoqElementType::Slash,
424            crate::lexer::token_type::CoqTokenType::Percent => CoqElementType::Percent,
425            crate::lexer::token_type::CoqTokenType::Less => CoqElementType::Less,
426            crate::lexer::token_type::CoqTokenType::Greater => CoqElementType::Greater,
427            crate::lexer::token_type::CoqTokenType::LessEqual => CoqElementType::LessEqual,
428            crate::lexer::token_type::CoqTokenType::GreaterEqual => CoqElementType::GreaterEqual,
429            crate::lexer::token_type::CoqTokenType::NotEqual => CoqElementType::NotEqual,
430            crate::lexer::token_type::CoqTokenType::Tilde => CoqElementType::Tilde,
431            crate::lexer::token_type::CoqTokenType::At => CoqElementType::At,
432            crate::lexer::token_type::CoqTokenType::Question => CoqElementType::Question,
433            crate::lexer::token_type::CoqTokenType::Exclamation => CoqElementType::Exclamation,
434            crate::lexer::token_type::CoqTokenType::Ampersand => CoqElementType::Ampersand,
435            crate::lexer::token_type::CoqTokenType::Hash => CoqElementType::Hash,
436            crate::lexer::token_type::CoqTokenType::Dollar => CoqElementType::Dollar,
437            crate::lexer::token_type::CoqTokenType::Backslash => CoqElementType::Backslash,
438            crate::lexer::token_type::CoqTokenType::Caret => CoqElementType::Caret,
439            crate::lexer::token_type::CoqTokenType::LeftParen => CoqElementType::LeftParen,
440            crate::lexer::token_type::CoqTokenType::RightParen => CoqElementType::RightParen,
441            crate::lexer::token_type::CoqTokenType::LeftBracket => CoqElementType::LeftBracket,
442            crate::lexer::token_type::CoqTokenType::RightBracket => CoqElementType::RightBracket,
443            crate::lexer::token_type::CoqTokenType::LeftBrace => CoqElementType::LeftBrace,
444            crate::lexer::token_type::CoqTokenType::RightBrace => CoqElementType::RightBrace,
445            crate::lexer::token_type::CoqTokenType::DoubleColon => CoqElementType::DoubleColon,
446            crate::lexer::token_type::CoqTokenType::DoubleColonEqual => CoqElementType::DoubleColonEqual,
447            crate::lexer::token_type::CoqTokenType::ColonEqual => CoqElementType::ColonEqual,
448            crate::lexer::token_type::CoqTokenType::Turnstile => CoqElementType::Turnstile,
449            crate::lexer::token_type::CoqTokenType::And => CoqElementType::And,
450            crate::lexer::token_type::CoqTokenType::Or => CoqElementType::Or,
451            crate::lexer::token_type::CoqTokenType::LeftArrow => CoqElementType::LeftArrow,
452            crate::lexer::token_type::CoqTokenType::Root => CoqElementType::Root,
453            crate::lexer::token_type::CoqTokenType::Declaration => CoqElementType::Declaration,
454            crate::lexer::token_type::CoqTokenType::Statement => CoqElementType::Statement,
455            crate::lexer::token_type::CoqTokenType::Expression => CoqElementType::Expression,
456            crate::lexer::token_type::CoqTokenType::Error => CoqElementType::Error,
457            crate::lexer::token_type::CoqTokenType::Eof => CoqElementType::Eof,
458        }
459    }
460}
oak_coq/parser/element_type.rs

oak_coq/parser/
element_type.rs
