oxilean_parse/lexer/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::tokens::{Span, StringPart, Token, TokenKind};
6
7/// A lexer mode stack.
8#[allow(dead_code)]
9#[allow(missing_docs)]
10pub struct LexerModeStack {
11    /// The stack of modes
12    pub stack: Vec<LexerMode>,
13}
14impl LexerModeStack {
15    /// Create a new mode stack starting in Normal mode.
16    #[allow(dead_code)]
17    pub fn new() -> Self {
18        LexerModeStack {
19            stack: vec![LexerMode::Normal],
20        }
21    }
22    /// Push a new mode.
23    #[allow(dead_code)]
24    pub fn push(&mut self, mode: LexerMode) {
25        self.stack.push(mode);
26    }
27    /// Pop the current mode, returning to the previous.
28    #[allow(dead_code)]
29    pub fn pop(&mut self) -> Option<LexerMode> {
30        if self.stack.len() > 1 {
31            self.stack.pop()
32        } else {
33            None
34        }
35    }
36    /// Returns the current mode.
37    #[allow(dead_code)]
38    pub fn current(&self) -> &LexerMode {
39        self.stack.last().unwrap_or(&LexerMode::Normal)
40    }
41    /// Returns the depth of the stack.
42    #[allow(dead_code)]
43    pub fn depth(&self) -> usize {
44        self.stack.len()
45    }
46}
47/// Lexer for tokenizing OxiLean source code.
48///
49/// Supports:
50/// - Keywords and identifiers (including Unicode letters: Greek, math symbols)
51/// - Number literals: decimal, hex (`0x`), binary (`0b`), octal (`0o`)
52/// - Float literals: `3.14`, `1.0e10`, `1.5e-3`
53/// - String literals with enhanced escape sequences (`\u{1234}`, `\x41`, `\0`)
54/// - Char literals: `'a'`, `'\n'`, `'\x41'`
55/// - Interpolated strings: `s!"hello {name}"`
56/// - Doc comments: `/-- ... -/` (block) and `--- ...` (line)
57/// - Operators: `>=`, `..`, `=>`, `<-`, `->`, etc.
58pub struct Lexer {
59    /// Input source code
60    input: Vec<char>,
61    /// Current position
62    pos: usize,
63    /// Current line (1-indexed)
64    line: usize,
65    /// Current column (1-indexed)
66    column: usize,
67}
68impl Lexer {
69    /// Create a new lexer from source code.
70    pub fn new(input: &str) -> Self {
71        Self {
72            input: input.chars().collect(),
73            pos: 0,
74            line: 1,
75            column: 1,
76        }
77    }
78    /// Get the current character without consuming it.
79    fn peek(&self) -> Option<char> {
80        self.input.get(self.pos).copied()
81    }
82    /// Get the character at offset from current position.
83    fn peek_ahead(&self, offset: usize) -> Option<char> {
84        self.input.get(self.pos + offset).copied()
85    }
86    /// Consume and return the current character.
87    fn advance(&mut self) -> Option<char> {
88        let ch = self.peek()?;
89        self.pos += 1;
90        if ch == '\n' {
91            self.line += 1;
92            self.column = 1;
93        } else {
94            self.column += 1;
95        }
96        Some(ch)
97    }
98    /// Skip whitespace and comments (but not doc comments).
99    fn skip_whitespace(&mut self) {
100        while let Some(ch) = self.peek() {
101            if ch.is_whitespace() {
102                self.advance();
103            } else if ch == '-' && self.peek_ahead(1) == Some('-') {
104                if self.peek_ahead(2) == Some('-') {
105                    break;
106                }
107                self.advance();
108                self.advance();
109                while let Some(ch) = self.peek() {
110                    if ch == '\n' {
111                        break;
112                    }
113                    self.advance();
114                }
115            } else if ch == '/' && self.peek_ahead(1) == Some('-') {
116                if self.peek_ahead(2) == Some('-') {
117                    break;
118                }
119                self.advance();
120                self.advance();
121                let mut depth = 1;
122                while depth > 0 {
123                    match self.peek() {
124                        Some('/') if self.peek_ahead(1) == Some('-') => {
125                            self.advance();
126                            self.advance();
127                            depth += 1;
128                        }
129                        Some('-') if self.peek_ahead(1) == Some('/') => {
130                            self.advance();
131                            self.advance();
132                            depth -= 1;
133                        }
134                        Some(_) => {
135                            self.advance();
136                        }
137                        None => break,
138                    }
139                }
140            } else {
141                break;
142            }
143        }
144    }
145    /// Lex a line doc comment: `--- ...` (everything until newline).
146    fn lex_line_doc_comment(&mut self, start: usize, start_line: usize, start_col: usize) -> Token {
147        self.advance();
148        self.advance();
149        self.advance();
150        if self.peek() == Some(' ') {
151            self.advance();
152        }
153        let mut s = String::new();
154        while let Some(ch) = self.peek() {
155            if ch == '\n' {
156                break;
157            }
158            s.push(ch);
159            self.advance();
160        }
161        Token::new(
162            TokenKind::DocComment(s),
163            Span::new(start, self.pos, start_line, start_col),
164        )
165    }
166    /// Lex a block doc comment: `/-- ... -/`.
167    fn lex_block_doc_comment(
168        &mut self,
169        start: usize,
170        start_line: usize,
171        start_col: usize,
172    ) -> Token {
173        self.advance();
174        self.advance();
175        self.advance();
176        if self.peek() == Some(' ') {
177            self.advance();
178        }
179        let mut s = String::new();
180        let mut depth = 1;
181        while depth > 0 {
182            match self.peek() {
183                Some('/') if self.peek_ahead(1) == Some('-') => {
184                    self.advance();
185                    self.advance();
186                    depth += 1;
187                    if depth > 1 {
188                        s.push_str("/-");
189                    }
190                }
191                Some('-') if self.peek_ahead(1) == Some('/') => {
192                    depth -= 1;
193                    if depth > 0 {
194                        s.push_str("-/");
195                    }
196                    self.advance();
197                    self.advance();
198                }
199                Some(ch) => {
200                    s.push(ch);
201                    self.advance();
202                }
203                None => break,
204            }
205        }
206        let s = s.trim_end().to_string();
207        Token::new(
208            TokenKind::DocComment(s),
209            Span::new(start, self.pos, start_line, start_col),
210        )
211    }
212    /// Lex an identifier or keyword.
213    /// Identifiers can contain Unicode letters (Greek, mathematical symbols, etc.),
214    /// digits, underscores, and primes.
215    fn lex_ident(&mut self, start: usize, start_line: usize, start_col: usize) -> Token {
216        let mut s = String::new();
217        if self.peek() == Some('_')
218            && !self
219                .peek_ahead(1)
220                .is_some_and(|c| c.is_alphanumeric() || c == '_')
221        {
222            self.advance();
223            return Token::new(
224                TokenKind::Underscore,
225                Span::new(start, self.pos, start_line, start_col),
226            );
227        }
228        while let Some(ch) = self.peek() {
229            if ch.is_alphanumeric() || ch == '_' || ch == '\'' {
230                s.push(ch);
231                self.advance();
232            } else {
233                break;
234            }
235        }
236        let kind = match s.as_str() {
237            "axiom" => TokenKind::Axiom,
238            "definition" | "def" => TokenKind::Definition,
239            "theorem" => TokenKind::Theorem,
240            "lemma" => TokenKind::Lemma,
241            "opaque" => TokenKind::Opaque,
242            "inductive" => TokenKind::Inductive,
243            "structure" => TokenKind::Structure,
244            "class" => TokenKind::Class,
245            "instance" => TokenKind::Instance,
246            "namespace" => TokenKind::Namespace,
247            "section" => TokenKind::Section,
248            "variable" => TokenKind::Variable,
249            "variables" => TokenKind::Variables,
250            "parameter" => TokenKind::Parameter,
251            "parameters" => TokenKind::Parameters,
252            "constant" => TokenKind::Constant,
253            "constants" => TokenKind::Constants,
254            "end" => TokenKind::End,
255            "import" => TokenKind::Import,
256            "export" => TokenKind::Export,
257            "open" => TokenKind::Open,
258            "attribute" => TokenKind::Attribute,
259            "return" => TokenKind::Return,
260            "Type" => TokenKind::Type,
261            "Prop" => TokenKind::Prop,
262            "Sort" => TokenKind::Sort,
263            "fun" => TokenKind::Fun,
264            "forall" => TokenKind::Forall,
265            "let" => TokenKind::Let,
266            "in" => TokenKind::In,
267            "if" => TokenKind::If,
268            "then" => TokenKind::Then,
269            "else" => TokenKind::Else,
270            "match" => TokenKind::Match,
271            "with" => TokenKind::With,
272            "do" => TokenKind::Do,
273            "have" => TokenKind::Have,
274            "suffices" => TokenKind::Suffices,
275            "show" => TokenKind::Show,
276            "where" => TokenKind::Where,
277            "from" => TokenKind::From,
278            "by" => TokenKind::By,
279            "exists" => TokenKind::Exists,
280            _ => TokenKind::Ident(s),
281        };
282        Token::new(kind, Span::new(start, self.pos, start_line, start_col))
283    }
284    /// Lex a hex number literal: `0x1A3F`.
285    fn lex_hex_number(&mut self, start: usize, start_line: usize, start_col: usize) -> Token {
286        let mut num = 0u64;
287        let mut has_digits = false;
288        while let Some(ch) = self.peek() {
289            if let Some(d) = ch.to_digit(16) {
290                num = num.wrapping_mul(16).wrapping_add(d as u64);
291                has_digits = true;
292                self.advance();
293            } else if ch == '_' {
294                self.advance();
295            } else {
296                break;
297            }
298        }
299        if !has_digits {
300            return Token::new(
301                TokenKind::Error("expected hex digits after 0x".to_string()),
302                Span::new(start, self.pos, start_line, start_col),
303            );
304        }
305        Token::new(
306            TokenKind::Nat(num),
307            Span::new(start, self.pos, start_line, start_col),
308        )
309    }
310    /// Lex a binary number literal: `0b1010`.
311    fn lex_bin_number(&mut self, start: usize, start_line: usize, start_col: usize) -> Token {
312        let mut num = 0u64;
313        let mut has_digits = false;
314        while let Some(ch) = self.peek() {
315            match ch {
316                '0' => {
317                    num = num.wrapping_mul(2);
318                    has_digits = true;
319                    self.advance();
320                }
321                '1' => {
322                    num = num.wrapping_mul(2).wrapping_add(1);
323                    has_digits = true;
324                    self.advance();
325                }
326                '_' => {
327                    self.advance();
328                }
329                _ => break,
330            }
331        }
332        if !has_digits {
333            return Token::new(
334                TokenKind::Error("expected binary digits after 0b".to_string()),
335                Span::new(start, self.pos, start_line, start_col),
336            );
337        }
338        Token::new(
339            TokenKind::Nat(num),
340            Span::new(start, self.pos, start_line, start_col),
341        )
342    }
343    /// Lex an octal number literal: `0o17`.
344    fn lex_oct_number(&mut self, start: usize, start_line: usize, start_col: usize) -> Token {
345        let mut num = 0u64;
346        let mut has_digits = false;
347        while let Some(ch) = self.peek() {
348            if let Some(d) = ch.to_digit(8) {
349                num = num.wrapping_mul(8).wrapping_add(d as u64);
350                has_digits = true;
351                self.advance();
352            } else if ch == '_' {
353                self.advance();
354            } else {
355                break;
356            }
357        }
358        if !has_digits {
359            return Token::new(
360                TokenKind::Error("expected octal digits after 0o".to_string()),
361                Span::new(start, self.pos, start_line, start_col),
362            );
363        }
364        Token::new(
365            TokenKind::Nat(num),
366            Span::new(start, self.pos, start_line, start_col),
367        )
368    }
369    /// Lex a number (decimal integer or float, or hex/bin/oct).
370    fn lex_number(&mut self, start: usize, start_line: usize, start_col: usize) -> Token {
371        if self.peek() == Some('0') {
372            match self.peek_ahead(1) {
373                Some('x') | Some('X') => {
374                    self.advance();
375                    self.advance();
376                    return self.lex_hex_number(start, start_line, start_col);
377                }
378                Some('b') | Some('B') => {
379                    self.advance();
380                    self.advance();
381                    return self.lex_bin_number(start, start_line, start_col);
382                }
383                Some('o') | Some('O') => {
384                    self.advance();
385                    self.advance();
386                    return self.lex_oct_number(start, start_line, start_col);
387                }
388                _ => {}
389            }
390        }
391        let mut int_str = String::new();
392        while let Some(ch) = self.peek() {
393            if ch.is_ascii_digit() {
394                int_str.push(ch);
395                self.advance();
396            } else if ch == '_' && self.peek_ahead(1).is_some_and(|c| c.is_ascii_digit()) {
397                self.advance();
398            } else {
399                break;
400            }
401        }
402        let is_float =
403            self.peek() == Some('.') && self.peek_ahead(1).is_some_and(|c| c.is_ascii_digit());
404        if is_float {
405            self.advance();
406            let mut frac_str = String::new();
407            frac_str.push_str(&int_str);
408            frac_str.push('.');
409            while let Some(ch) = self.peek() {
410                if ch.is_ascii_digit() {
411                    frac_str.push(ch);
412                    self.advance();
413                } else {
414                    break;
415                }
416            }
417            if self.peek() == Some('e') || self.peek() == Some('E') {
418                frac_str.push('e');
419                self.advance();
420                if self.peek() == Some('+') || self.peek() == Some('-') {
421                    frac_str.push(self.advance().expect("peek confirmed '+' or '-' exists"));
422                }
423                while let Some(ch) = self.peek() {
424                    if ch.is_ascii_digit() {
425                        frac_str.push(ch);
426                        self.advance();
427                    } else {
428                        break;
429                    }
430                }
431            }
432            let val: f64 = frac_str.parse().unwrap_or(0.0);
433            return Token::new(
434                TokenKind::Float(val),
435                Span::new(start, self.pos, start_line, start_col),
436            );
437        }
438        if self.peek() == Some('e') || self.peek() == Some('E') {
439            let mut exp_str = String::new();
440            exp_str.push_str(&int_str);
441            exp_str.push('e');
442            self.advance();
443            if self.peek() == Some('+') || self.peek() == Some('-') {
444                exp_str.push(self.advance().expect("peek confirmed '+' or '-' exists"));
445            }
446            while let Some(ch) = self.peek() {
447                if ch.is_ascii_digit() {
448                    exp_str.push(ch);
449                    self.advance();
450                } else {
451                    break;
452                }
453            }
454            let val: f64 = exp_str.parse().unwrap_or(0.0);
455            return Token::new(
456                TokenKind::Float(val),
457                Span::new(start, self.pos, start_line, start_col),
458            );
459        }
460        let num: u64 = int_str.parse().unwrap_or(0);
461        Token::new(
462            TokenKind::Nat(num),
463            Span::new(start, self.pos, start_line, start_col),
464        )
465    }
466    /// Parse an escape sequence inside a string or char literal.
467    /// Returns the resolved character or None on error.
468    fn parse_escape_char(&mut self) -> Option<char> {
469        match self.peek() {
470            Some('n') => {
471                self.advance();
472                Some('\n')
473            }
474            Some('t') => {
475                self.advance();
476                Some('\t')
477            }
478            Some('r') => {
479                self.advance();
480                Some('\r')
481            }
482            Some('\\') => {
483                self.advance();
484                Some('\\')
485            }
486            Some('"') => {
487                self.advance();
488                Some('"')
489            }
490            Some('\'') => {
491                self.advance();
492                Some('\'')
493            }
494            Some('0') => {
495                self.advance();
496                Some('\0')
497            }
498            Some('x') => {
499                self.advance();
500                let hi = self.advance().and_then(|c| c.to_digit(16))?;
501                let lo = self.advance().and_then(|c| c.to_digit(16))?;
502                let val = (hi * 16 + lo) as u8;
503                Some(val as char)
504            }
505            Some('u') => {
506                self.advance();
507                if self.peek() != Some('{') {
508                    return None;
509                }
510                self.advance();
511                let mut code = 0u32;
512                let mut has_digit = false;
513                while let Some(ch) = self.peek() {
514                    if ch == '}' {
515                        self.advance();
516                        break;
517                    }
518                    let d = ch.to_digit(16)?;
519                    code = code * 16 + d;
520                    has_digit = true;
521                    self.advance();
522                }
523                if !has_digit {
524                    return None;
525                }
526                char::from_u32(code)
527            }
528            Some(ch) => {
529                self.advance();
530                Some(ch)
531            }
532            None => None,
533        }
534    }
535    /// Lex a string literal (with enhanced escape sequences).
536    fn lex_string(&mut self, start: usize, start_line: usize, start_col: usize) -> Token {
537        self.advance();
538        let mut s = String::new();
539        while let Some(ch) = self.peek() {
540            if ch == '"' {
541                self.advance();
542                return Token::new(
543                    TokenKind::String(s),
544                    Span::new(start, self.pos, start_line, start_col),
545                );
546            } else if ch == '\\' {
547                self.advance();
548                if let Some(escaped) = self.parse_escape_char() {
549                    s.push(escaped);
550                } else {
551                    s.push('?');
552                }
553            } else {
554                s.push(ch);
555                self.advance();
556            }
557        }
558        Token::new(
559            TokenKind::Error("unterminated string".to_string()),
560            Span::new(start, self.pos, start_line, start_col),
561        )
562    }
563    /// Lex a char literal: `'a'`, `'\n'`, `'\x41'`, `'\u{03B1}'`.
564    fn lex_char(&mut self, start: usize, start_line: usize, start_col: usize) -> Token {
565        self.advance();
566        let ch = if self.peek() == Some('\\') {
567            self.advance();
568            match self.parse_escape_char() {
569                Some(c) => c,
570                None => {
571                    return Token::new(
572                        TokenKind::Error("invalid escape in char literal".to_string()),
573                        Span::new(start, self.pos, start_line, start_col),
574                    );
575                }
576            }
577        } else {
578            match self.advance() {
579                Some(c) => c,
580                None => {
581                    return Token::new(
582                        TokenKind::Error("unterminated char literal".to_string()),
583                        Span::new(start, self.pos, start_line, start_col),
584                    );
585                }
586            }
587        };
588        if self.peek() == Some('\'') {
589            self.advance();
590            Token::new(
591                TokenKind::Char(ch),
592                Span::new(start, self.pos, start_line, start_col),
593            )
594        } else {
595            Token::new(
596                TokenKind::Error("unterminated char literal".to_string()),
597                Span::new(start, self.pos, start_line, start_col),
598            )
599        }
600    }
601    /// Lex an interpolated string: `s!"hello {name}"`.
602    /// Assumes `s` and `!` have NOT been consumed yet; we are at 's'.
603    fn lex_interpolated_string(
604        &mut self,
605        start: usize,
606        start_line: usize,
607        start_col: usize,
608    ) -> Token {
609        self.advance();
610        self.advance();
611        self.advance();
612        let mut parts: Vec<StringPart> = Vec::new();
613        let mut current_lit = String::new();
614        while let Some(ch) = self.peek() {
615            if ch == '"' {
616                self.advance();
617                if !current_lit.is_empty() {
618                    parts.push(StringPart::Literal(current_lit));
619                }
620                return Token::new(
621                    TokenKind::InterpolatedString(parts),
622                    Span::new(start, self.pos, start_line, start_col),
623                );
624            } else if ch == '{' {
625                self.advance();
626                if !current_lit.is_empty() {
627                    parts.push(StringPart::Literal(current_lit.clone()));
628                    current_lit.clear();
629                }
630                let mut interp_tokens = Vec::new();
631                let mut depth = 1;
632                loop {
633                    let tok = self.next_token_raw();
634                    match &tok.kind {
635                        TokenKind::LBrace => depth += 1,
636                        TokenKind::RBrace => {
637                            depth -= 1;
638                            if depth == 0 {
639                                break;
640                            }
641                        }
642                        TokenKind::Eof => break,
643                        _ => {}
644                    }
645                    interp_tokens.push(tok);
646                }
647                parts.push(StringPart::Interpolation(interp_tokens));
648            } else if ch == '\\' {
649                self.advance();
650                if let Some(escaped) = self.parse_escape_char() {
651                    current_lit.push(escaped);
652                } else {
653                    current_lit.push('?');
654                }
655            } else {
656                current_lit.push(ch);
657                self.advance();
658            }
659        }
660        Token::new(
661            TokenKind::Error("unterminated interpolated string".to_string()),
662            Span::new(start, self.pos, start_line, start_col),
663        )
664    }
665    /// Lex a single token without skipping whitespace first.
666    /// Used internally for interpolated string sub-lexing.
667    fn next_token_raw(&mut self) -> Token {
668        self.skip_whitespace();
669        let start = self.pos;
670        let start_line = self.line;
671        let start_col = self.column;
672        let Some(ch) = self.peek() else {
673            return Token::new(
674                TokenKind::Eof,
675                Span::new(start, start, start_line, start_col),
676            );
677        };
678        if ch.is_alphabetic() || ch == '_' {
679            return self.lex_ident(start, start_line, start_col);
680        }
681        if ch.is_ascii_digit() {
682            return self.lex_number(start, start_line, start_col);
683        }
684        if ch == '"' {
685            return self.lex_string(start, start_line, start_col);
686        }
687        self.advance();
688        let kind = match ch {
689            '(' => TokenKind::LParen,
690            ')' => TokenKind::RParen,
691            '{' => TokenKind::LBrace,
692            '}' => TokenKind::RBrace,
693            '[' => TokenKind::LBracket,
694            ']' => TokenKind::RBracket,
695            ',' => TokenKind::Comma,
696            ';' => TokenKind::Semicolon,
697            '.' if self.peek() == Some('.') => {
698                self.advance();
699                TokenKind::DotDot
700            }
701            '.' => TokenKind::Dot,
702            '|' if self.peek() == Some('|') => {
703                self.advance();
704                TokenKind::OrOr
705            }
706            '|' => TokenKind::Bar,
707            '@' => TokenKind::At,
708            '#' => TokenKind::Hash,
709            '+' => TokenKind::Plus,
710            '-' if self.peek() == Some('>') => {
711                self.advance();
712                TokenKind::Arrow
713            }
714            '-' => TokenKind::Minus,
715            '>' if self.peek() == Some('=') => {
716                self.advance();
717                TokenKind::Ge
718            }
719            '>' => TokenKind::Gt,
720            '*' => TokenKind::Star,
721            '/' => TokenKind::Slash,
722            '%' => TokenKind::Percent,
723            '^' => TokenKind::Caret,
724            '_' => TokenKind::Underscore,
725            '?' => TokenKind::Question,
726            '!' if self.peek() == Some('=') => {
727                self.advance();
728                TokenKind::BangEq
729            }
730            '!' => TokenKind::Bang,
731            '&' if self.peek() == Some('&') => {
732                self.advance();
733                TokenKind::AndAnd
734            }
735            ':' if self.peek() == Some('=') => {
736                self.advance();
737                TokenKind::Assign
738            }
739            ':' => TokenKind::Colon,
740            '=' if self.peek() == Some('>') => {
741                self.advance();
742                TokenKind::FatArrow
743            }
744            '=' => TokenKind::Eq,
745            '<' if self.peek() == Some('-') => {
746                self.advance();
747                TokenKind::LeftArrow
748            }
749            '<' if self.peek() == Some('=') => {
750                self.advance();
751                TokenKind::Le
752            }
753            '<' => TokenKind::Lt,
754            '\u{2190}' => TokenKind::LeftArrow,
755            '\u{2264}' | '\u{2A7D}' => TokenKind::Le,
756            '\u{2265}' | '\u{2A7E}' => TokenKind::Ge,
757            '\u{2260}' => TokenKind::Ne,
758            '\u{2192}' => TokenKind::Arrow,
759            '\u{21D2}' => TokenKind::FatArrow,
760            '\u{2227}' => TokenKind::And,
761            '\u{2228}' => TokenKind::Or,
762            '\u{00AC}' => TokenKind::Not,
763            '\u{2194}' => TokenKind::Iff,
764            '\u{2200}' => TokenKind::Forall,
765            '\u{2203}' => TokenKind::Exists,
766            '\u{03BB}' => TokenKind::Fun,
767            '\u{27E8}' => TokenKind::LAngle,
768            '\u{27E9}' => TokenKind::RAngle,
769            _ => TokenKind::Error(format!("unexpected character: {}", ch)),
770        };
771        Token::new(kind, Span::new(start, self.pos, start_line, start_col))
772    }
773    /// Get the next token.
774    pub fn next_token(&mut self) -> Token {
775        self.skip_whitespace();
776        let start = self.pos;
777        let start_line = self.line;
778        let start_col = self.column;
779        let Some(ch) = self.peek() else {
780            return Token::new(
781                TokenKind::Eof,
782                Span::new(start, start, start_line, start_col),
783            );
784        };
785        if ch == '/' && self.peek_ahead(1) == Some('-') && self.peek_ahead(2) == Some('-') {
786            return self.lex_block_doc_comment(start, start_line, start_col);
787        }
788        if ch == '-' && self.peek_ahead(1) == Some('-') && self.peek_ahead(2) == Some('-') {
789            return self.lex_line_doc_comment(start, start_line, start_col);
790        }
791        if ch == 's' && self.peek_ahead(1) == Some('!') && self.peek_ahead(2) == Some('"') {
792            return self.lex_interpolated_string(start, start_line, start_col);
793        }
794        if ch.is_alphabetic() || ch == '_' {
795            return self.lex_ident(start, start_line, start_col);
796        }
797        if ch.is_ascii_digit() {
798            return self.lex_number(start, start_line, start_col);
799        }
800        if ch == '"' {
801            return self.lex_string(start, start_line, start_col);
802        }
803        if ch == '\'' {
804            let is_char_lit = if self.peek_ahead(1) == Some('\\') {
805                true
806            } else {
807                self.peek_ahead(2) == Some('\'')
808            };
809            if is_char_lit {
810                return self.lex_char(start, start_line, start_col);
811            }
812        }
813        self.advance();
814        let kind = match ch {
815            '(' => TokenKind::LParen,
816            ')' => TokenKind::RParen,
817            '{' => TokenKind::LBrace,
818            '}' => TokenKind::RBrace,
819            '[' => TokenKind::LBracket,
820            ']' => TokenKind::RBracket,
821            ',' => TokenKind::Comma,
822            ';' => TokenKind::Semicolon,
823            '.' if self.peek() == Some('.') => {
824                self.advance();
825                TokenKind::DotDot
826            }
827            '.' => TokenKind::Dot,
828            '|' if self.peek() == Some('|') => {
829                self.advance();
830                TokenKind::OrOr
831            }
832            '|' => TokenKind::Bar,
833            '@' => TokenKind::At,
834            '#' => TokenKind::Hash,
835            '+' => TokenKind::Plus,
836            '-' if self.peek() == Some('>') => {
837                self.advance();
838                TokenKind::Arrow
839            }
840            '-' => TokenKind::Minus,
841            '>' if self.peek() == Some('=') => {
842                self.advance();
843                TokenKind::Ge
844            }
845            '>' => TokenKind::Gt,
846            '*' => TokenKind::Star,
847            '/' => TokenKind::Slash,
848            '%' => TokenKind::Percent,
849            '^' => TokenKind::Caret,
850            '_' => TokenKind::Underscore,
851            '?' => TokenKind::Question,
852            '\'' => TokenKind::Error("unexpected tick '".to_string()),
853            '!' if self.peek() == Some('=') => {
854                self.advance();
855                TokenKind::BangEq
856            }
857            '!' => TokenKind::Bang,
858            '&' if self.peek() == Some('&') => {
859                self.advance();
860                TokenKind::AndAnd
861            }
862            ':' if self.peek() == Some('=') => {
863                self.advance();
864                TokenKind::Assign
865            }
866            ':' => TokenKind::Colon,
867            '=' if self.peek() == Some('>') => {
868                self.advance();
869                TokenKind::FatArrow
870            }
871            '=' => TokenKind::Eq,
872            '<' if self.peek() == Some('-') => {
873                self.advance();
874                TokenKind::LeftArrow
875            }
876            '<' if self.peek() == Some('=') => {
877                self.advance();
878                TokenKind::Le
879            }
880            '<' => TokenKind::Lt,
881            '\u{2190}' => TokenKind::LeftArrow,
882            '\u{2264}' | '\u{2A7D}' => TokenKind::Le,
883            '\u{2265}' | '\u{2A7E}' => TokenKind::Ge,
884            '\u{2260}' => TokenKind::Ne,
885            '\u{2192}' => TokenKind::Arrow,
886            '\u{21D2}' => TokenKind::FatArrow,
887            '\u{2227}' => TokenKind::And,
888            '\u{2228}' => TokenKind::Or,
889            '\u{00AC}' => TokenKind::Not,
890            '\u{2194}' => TokenKind::Iff,
891            '\u{2200}' => TokenKind::Forall,
892            '\u{2203}' => TokenKind::Exists,
893            '\u{03BB}' => TokenKind::Fun,
894            '\u{27E8}' => TokenKind::LAngle,
895            '\u{27E9}' => TokenKind::RAngle,
896            _ => TokenKind::Error(format!("unexpected character: {}", ch)),
897        };
898        Token::new(kind, Span::new(start, self.pos, start_line, start_col))
899    }
900    /// Tokenize the entire input.
901    pub fn tokenize(&mut self) -> Vec<Token> {
902        let mut tokens = Vec::new();
903        loop {
904            let tok = self.next_token();
905            let is_eof = matches!(tok.kind, TokenKind::Eof);
906            tokens.push(tok);
907            if is_eof {
908                break;
909            }
910        }
911        tokens
912    }
913}
914/// A simple string scanner with position tracking.
915#[allow(dead_code)]
916#[allow(missing_docs)]
917pub struct Scanner<'a> {
918    /// The source text
919    src: &'a str,
920    /// Current byte position
921    pos: usize,
922    /// Current line number (1-based)
923    line: usize,
924    /// Current column number (1-based)
925    col: usize,
926}
927impl<'a> Scanner<'a> {
928    /// Create a new scanner at the start of the source.
929    #[allow(dead_code)]
930    pub fn new(src: &'a str) -> Self {
931        Scanner {
932            src,
933            pos: 0,
934            line: 1,
935            col: 1,
936        }
937    }
938    /// Peek at the current character without consuming it.
939    #[allow(dead_code)]
940    pub fn peek(&self) -> Option<char> {
941        self.src[self.pos..].chars().next()
942    }
943    /// Consume the next character.
944    #[allow(dead_code)]
945    #[allow(clippy::should_implement_trait)]
946    pub fn next(&mut self) -> Option<char> {
947        let c = self.src[self.pos..].chars().next()?;
948        self.pos += c.len_utf8();
949        if c == '\n' {
950            self.line += 1;
951            self.col = 1;
952        } else {
953            self.col += 1;
954        }
955        Some(c)
956    }
957    /// Returns true if the scanner is at the end.
958    #[allow(dead_code)]
959    pub fn is_eof(&self) -> bool {
960        self.pos >= self.src.len()
961    }
962    /// Returns the current position.
963    #[allow(dead_code)]
964    pub fn position(&self) -> usize {
965        self.pos
966    }
967    /// Returns the current line.
968    #[allow(dead_code)]
969    pub fn line(&self) -> usize {
970        self.line
971    }
972    /// Returns the current column.
973    #[allow(dead_code)]
974    pub fn col(&self) -> usize {
975        self.col
976    }
977    /// Skip whitespace.
978    #[allow(dead_code)]
979    pub fn skip_whitespace(&mut self) {
980        while self.peek().map(|c| c.is_whitespace()).unwrap_or(false) {
981            self.next();
982        }
983    }
984    /// Consume characters while the predicate holds, returning the matched slice.
985    #[allow(dead_code)]
986    pub fn consume_while<F: Fn(char) -> bool>(&mut self, pred: F) -> &'a str {
987        let start = self.pos;
988        while self.peek().is_some_and(&pred) {
989            self.next();
990        }
991        &self.src[start..self.pos]
992    }
993    /// Returns the remaining source.
994    #[allow(dead_code)]
995    pub fn remaining(&self) -> &'a str {
996        &self.src[self.pos..]
997    }
998}
999/// A lexer position record for backtracking.
1000#[allow(dead_code)]
1001#[allow(missing_docs)]
1002#[derive(Debug, Clone, Copy)]
1003pub struct LexerPos {
1004    /// Byte offset
1005    pub offset: usize,
1006    /// Line number
1007    pub line: usize,
1008    /// Column number
1009    pub col: usize,
1010}
1011/// A lexer rule table.
1012#[allow(dead_code)]
1013#[allow(missing_docs)]
1014pub struct LexerRuleTable {
1015    /// All rules in this table
1016    pub rules: Vec<LexerRule>,
1017}
1018impl LexerRuleTable {
1019    /// Create a new empty table.
1020    #[allow(dead_code)]
1021    pub fn new() -> Self {
1022        LexerRuleTable { rules: Vec::new() }
1023    }
1024    /// Add a rule.
1025    #[allow(dead_code)]
1026    pub fn add(&mut self, rule: LexerRule) {
1027        self.rules.push(rule);
1028    }
1029    /// Find the first rule whose start class matches a character.
1030    #[allow(dead_code)]
1031    pub fn find_rule(&self, c: char) -> Option<&LexerRule> {
1032        self.rules.iter().find(|r| r.start.matches(c))
1033    }
1034    /// Returns the number of rules.
1035    #[allow(dead_code)]
1036    pub fn len(&self) -> usize {
1037        self.rules.len()
1038    }
1039    /// Returns true if the table is empty.
1040    #[allow(dead_code)]
1041    pub fn is_empty(&self) -> bool {
1042        self.rules.is_empty()
1043    }
1044}
1045/// A token category for grouping.
1046#[allow(dead_code)]
1047#[allow(missing_docs)]
1048#[derive(Debug, Clone, PartialEq, Eq)]
1049pub enum TokenCategory {
1050    /// Identifier tokens
1051    Ident,
1052    /// Keyword tokens
1053    Keyword,
1054    /// Literal tokens
1055    Literal,
1056    /// Operator tokens
1057    Operator,
1058    /// Delimiter tokens (parens, brackets, etc.)
1059    Delimiter,
1060    /// Whitespace/trivia tokens
1061    Trivia,
1062    /// EOF token
1063    Eof,
1064}
1065/// A token diff record showing insertions/deletions between two token sequences.
1066#[allow(dead_code)]
1067#[allow(missing_docs)]
1068#[derive(Debug, Clone)]
1069pub struct TokenDiff {
1070    /// Number of tokens only in left
1071    pub only_left: usize,
1072    /// Number of tokens only in right
1073    pub only_right: usize,
1074    /// Number of matching tokens
1075    pub matching: usize,
1076}
1077/// A summary of a lexed file.
1078#[allow(dead_code)]
1079#[allow(missing_docs)]
1080#[derive(Debug, Default)]
1081pub struct LexSummary {
1082    /// Total token count
1083    pub token_count: usize,
1084    /// Number of identifier tokens
1085    pub ident_count: usize,
1086    /// Number of keyword tokens
1087    pub keyword_count: usize,
1088    /// Number of operator tokens
1089    pub operator_count: usize,
1090    /// Number of literal tokens
1091    pub literal_count: usize,
1092    /// Number of comment tokens
1093    pub comment_count: usize,
1094    /// Number of whitespace tokens
1095    pub whitespace_count: usize,
1096}
1097impl LexSummary {
1098    /// Create a new empty summary.
1099    #[allow(dead_code)]
1100    pub fn new() -> Self {
1101        LexSummary::default()
1102    }
1103    /// Format the summary as a string.
1104    #[allow(dead_code)]
1105    pub fn format(&self) -> String {
1106        format!(
1107            "tokens={} idents={} keywords={} ops={} literals={} comments={} ws={}",
1108            self.token_count,
1109            self.ident_count,
1110            self.keyword_count,
1111            self.operator_count,
1112            self.literal_count,
1113            self.comment_count,
1114            self.whitespace_count
1115        )
1116    }
1117}
1118/// A keyword trie node for fast keyword detection.
1119#[allow(dead_code)]
1120#[allow(missing_docs)]
1121pub struct KeywordTrie {
1122    /// Children by character
1123    children: std::collections::HashMap<char, KeywordTrie>,
1124    /// Whether this node is a terminal keyword
1125    pub is_keyword: bool,
1126}
1127impl KeywordTrie {
1128    /// Create an empty trie.
1129    #[allow(dead_code)]
1130    pub fn new() -> Self {
1131        KeywordTrie {
1132            children: std::collections::HashMap::new(),
1133            is_keyword: false,
1134        }
1135    }
1136    /// Insert a keyword into the trie.
1137    #[allow(dead_code)]
1138    pub fn insert(&mut self, keyword: &str) {
1139        let mut node = self;
1140        for c in keyword.chars() {
1141            node = node.children.entry(c).or_default();
1142        }
1143        node.is_keyword = true;
1144    }
1145    /// Check if a string is in the trie.
1146    #[allow(dead_code)]
1147    pub fn contains(&self, s: &str) -> bool {
1148        let mut node = self;
1149        for c in s.chars() {
1150            match node.children.get(&c) {
1151                Some(child) => node = child,
1152                None => return false,
1153            }
1154        }
1155        node.is_keyword
1156    }
1157}
1158/// A lexer rule: a name, a start class, and a continuation class.
1159#[allow(dead_code)]
1160#[allow(missing_docs)]
1161#[derive(Debug, Clone)]
1162pub struct LexerRule {
1163    /// Name of the token kind produced
1164    pub kind: String,
1165    /// Character class for the first character
1166    pub start: CharClass,
1167    /// Character class for continuation characters
1168    pub cont: CharClass,
1169}
1170impl LexerRule {
1171    /// Create a new lexer rule.
1172    #[allow(dead_code)]
1173    pub fn new(kind: &str, start: CharClass, cont: CharClass) -> Self {
1174        LexerRule {
1175            kind: kind.to_string(),
1176            start,
1177            cont,
1178        }
1179    }
1180}
1181/// A trivia (whitespace/comment) accumulator.
1182#[allow(dead_code)]
1183#[allow(missing_docs)]
1184#[derive(Debug, Default)]
1185pub struct TriviaAccumulator {
1186    /// Accumulated trivia text
1187    pub text: String,
1188    /// Whether any newlines were found
1189    pub has_newlines: bool,
1190}
1191impl TriviaAccumulator {
1192    /// Create a new accumulator.
1193    #[allow(dead_code)]
1194    pub fn new() -> Self {
1195        TriviaAccumulator {
1196            text: String::new(),
1197            has_newlines: false,
1198        }
1199    }
1200    /// Add trivia text.
1201    #[allow(dead_code)]
1202    pub fn push(&mut self, s: &str) {
1203        if s.contains('\n') {
1204            self.has_newlines = true;
1205        }
1206        self.text.push_str(s);
1207    }
1208    /// Clear the accumulator.
1209    #[allow(dead_code)]
1210    pub fn clear(&mut self) {
1211        self.text.clear();
1212        self.has_newlines = false;
1213    }
1214}
1215/// A simple character frequency table over a source string.
1216#[allow(dead_code)]
1217#[allow(missing_docs)]
1218pub struct CharFreqTable {
1219    /// Frequency counts indexed by char code (0..128)
1220    pub counts: [u32; 128],
1221}
1222impl CharFreqTable {
1223    /// Build a frequency table from source.
1224    #[allow(dead_code)]
1225    #[allow(clippy::should_implement_trait)]
1226    pub fn from_str(src: &str) -> Self {
1227        let mut counts = [0u32; 128];
1228        for c in src.chars() {
1229            if (c as usize) < 128 {
1230                counts[c as usize] += 1;
1231            }
1232        }
1233        CharFreqTable { counts }
1234    }
1235    /// Get the count for a character.
1236    #[allow(dead_code)]
1237    pub fn count(&self, c: char) -> u32 {
1238        if (c as usize) < 128 {
1239            self.counts[c as usize]
1240        } else {
1241            0
1242        }
1243    }
1244}
1245/// A simple tokenisation result with raw text.
1246#[allow(dead_code)]
1247#[allow(missing_docs)]
1248#[derive(Debug, Clone)]
1249pub struct RawToken {
1250    /// Kind string
1251    pub kind: String,
1252    /// Raw text of the token
1253    pub text: String,
1254    /// Start byte offset
1255    pub start: usize,
1256    /// End byte offset
1257    pub end: usize,
1258    /// Line number
1259    pub line: usize,
1260    /// Column number
1261    pub col: usize,
1262}
1263/// A filtered view of a token sequence.
1264#[allow(dead_code)]
1265#[allow(missing_docs)]
1266pub struct FilteredTokenStream {
1267    /// The underlying tokens
1268    pub tokens: Vec<RawToken>,
1269    /// Current index
1270    pos: usize,
1271}
1272impl FilteredTokenStream {
1273    /// Create from a token list, filtering out whitespace.
1274    #[allow(dead_code)]
1275    pub fn new(tokens: Vec<RawToken>) -> Self {
1276        let tokens = tokens.into_iter().filter(|t| t.kind != "WS").collect();
1277        FilteredTokenStream { tokens, pos: 0 }
1278    }
1279    /// Peek at the current token.
1280    #[allow(dead_code)]
1281    pub fn peek(&self) -> Option<&RawToken> {
1282        self.tokens.get(self.pos)
1283    }
1284    /// Consume the current token.
1285    #[allow(dead_code)]
1286    #[allow(clippy::should_implement_trait)]
1287    pub fn next(&mut self) -> Option<&RawToken> {
1288        let tok = self.tokens.get(self.pos)?;
1289        self.pos += 1;
1290        Some(tok)
1291    }
1292    /// Returns true if at end.
1293    #[allow(dead_code)]
1294    pub fn is_eof(&self) -> bool {
1295        self.pos >= self.tokens.len()
1296    }
1297    /// Returns remaining token count.
1298    #[allow(dead_code)]
1299    pub fn remaining(&self) -> usize {
1300        self.tokens.len().saturating_sub(self.pos)
1301    }
1302    /// Returns position.
1303    #[allow(dead_code)]
1304    pub fn position(&self) -> usize {
1305        self.pos
1306    }
1307}
1308/// A simple character class for lexer rules.
1309#[allow(dead_code)]
1310#[allow(missing_docs)]
1311#[derive(Debug, Clone)]
1312pub enum CharClass {
1313    /// Matches any ASCII letter
1314    Alpha,
1315    /// Matches any ASCII digit
1316    Digit,
1317    /// Matches any ASCII alphanumeric
1318    AlphaNum,
1319    /// Matches whitespace
1320    Whitespace,
1321    /// Matches a specific character
1322    Exact(char),
1323    /// Matches any character in a set
1324    OneOf(Vec<char>),
1325    /// Matches any character not in a set
1326    NoneOf(Vec<char>),
1327}
1328impl CharClass {
1329    /// Returns true if the character matches this class.
1330    #[allow(dead_code)]
1331    pub fn matches(&self, c: char) -> bool {
1332        match self {
1333            CharClass::Alpha => c.is_ascii_alphabetic(),
1334            CharClass::Digit => c.is_ascii_digit(),
1335            CharClass::AlphaNum => c.is_ascii_alphanumeric(),
1336            CharClass::Whitespace => c.is_whitespace(),
1337            CharClass::Exact(x) => c == *x,
1338            CharClass::OneOf(set) => set.contains(&c),
1339            CharClass::NoneOf(set) => !set.contains(&c),
1340        }
1341    }
1342}
1343/// A lexer mode for context-sensitive lexing.
1344#[allow(dead_code)]
1345#[allow(missing_docs)]
1346#[derive(Debug, Clone, PartialEq, Eq)]
1347pub enum LexerMode {
1348    /// Normal mode
1349    Normal,
1350    /// Inside a string literal
1351    StringLit,
1352    /// Inside a comment
1353    Comment,
1354    /// Inside a tactic block
1355    Tactic,
1356}
1357/// A lexer state machine with explicit transitions.
1358#[allow(dead_code)]
1359#[allow(missing_docs)]
1360#[derive(Debug, Clone, PartialEq, Eq)]
1361pub enum LexerState {
1362    /// Initial state
1363    Start,
1364    /// Scanning identifier
1365    Ident,
1366    /// Scanning number
1367    Number,
1368    /// Scanning operator
1369    Operator,
1370    /// Scanning string
1371    StringStart,
1372    /// Scanning line comment
1373    LineComment,
1374    /// Done
1375    Done,
1376}
1377/// A utility to find the line boundaries in a source string.
1378#[allow(dead_code)]
1379#[allow(missing_docs)]
1380pub struct LineMap {
1381    /// Byte offsets of each line start
1382    pub line_starts: Vec<usize>,
1383}
1384impl LineMap {
1385    /// Build a LineMap from source text.
1386    #[allow(dead_code)]
1387    #[allow(clippy::should_implement_trait)]
1388    pub fn from_str(src: &str) -> Self {
1389        let mut line_starts = vec![0];
1390        for (i, c) in src.char_indices() {
1391            if c == '\n' {
1392                line_starts.push(i + 1);
1393            }
1394        }
1395        LineMap { line_starts }
1396    }
1397    /// Returns the line number (1-based) for a byte offset.
1398    #[allow(dead_code)]
1399    pub fn line_for_offset(&self, offset: usize) -> usize {
1400        match self.line_starts.binary_search(&offset) {
1401            Ok(idx) => idx + 1,
1402            Err(idx) => idx,
1403        }
1404    }
1405    /// Returns the column (1-based) for a byte offset.
1406    #[allow(dead_code)]
1407    pub fn col_for_offset(&self, offset: usize) -> usize {
1408        let line = self.line_for_offset(offset);
1409        let line_start = self.line_starts.get(line - 1).copied().unwrap_or(0);
1410        offset - line_start + 1
1411    }
1412    /// Returns the total number of lines.
1413    #[allow(dead_code)]
1414    pub fn line_count(&self) -> usize {
1415        self.line_starts.len()
1416    }
1417}
oxilean_parse/lexer/types.rs

oxilean_parse/lexer/
types.rs
