oxilean_parse/parser_impl/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::ast_impl::*;
6use crate::error_impl::ParseError;
7use crate::tokens::{StringPart, Token, TokenKind};
8
9/// Parser state.
10pub struct Parser {
11    /// Token stream
12    tokens: Vec<Token>,
13    /// Current position
14    pos: usize,
15}
16impl Parser {
17    /// Create a new parser from tokens.
18    pub fn new(tokens: Vec<Token>) -> Self {
19        Self { tokens, pos: 0 }
20    }
21    /// Get the current token.
22    fn current(&self) -> &Token {
23        self.tokens
24            .get(self.pos)
25            .unwrap_or(&self.tokens[self.tokens.len() - 1])
26    }
27    /// Peek at the next token (one ahead of current).
28    fn peek(&self) -> &Token {
29        self.tokens
30            .get(self.pos + 1)
31            .unwrap_or(&self.tokens[self.tokens.len() - 1])
32    }
33    /// Peek at the token two ahead of current.
34    #[allow(dead_code)]
35    fn peek2(&self) -> &Token {
36        self.tokens
37            .get(self.pos + 2)
38            .unwrap_or(&self.tokens[self.tokens.len() - 1])
39    }
40    /// Check if we're at the end of input.
41    /// Return `true` when the token stream is exhausted.
42    pub fn is_eof(&self) -> bool {
43        matches!(self.current().kind, TokenKind::Eof)
44    }
45    /// Advance past the current token and return it.
46    ///
47    /// Public so that callers that drive the parser declaration-by-declaration
48    /// (e.g. the build executor) can skip past error positions.
49    pub fn advance(&mut self) -> Token {
50        let tok = self.current().clone();
51        if !self.is_eof() {
52            self.pos += 1;
53        }
54        tok
55    }
56    /// Expect a specific token kind; error if not found.
57    fn expect(&mut self, kind: TokenKind) -> Result<Token, ParseError> {
58        if self.current().kind == kind {
59            Ok(self.advance())
60        } else {
61            Err(ParseError::unexpected(
62                vec![format!("{}", kind)],
63                self.current().kind.clone(),
64                self.current().span.clone(),
65            ))
66        }
67    }
68    /// Check if current token matches a kind (no consume).
69    fn check(&self, kind: &TokenKind) -> bool {
70        &self.current().kind == kind
71    }
72    /// Consume a token if it matches, returning true on success.
73    fn consume(&mut self, kind: TokenKind) -> bool {
74        if self.check(&kind) {
75            self.advance();
76            true
77        } else {
78            false
79        }
80    }
81    /// Check if the current token is an identifier matching the given string.
82    fn check_ident(&self, name: &str) -> bool {
83        matches!(& self.current().kind, TokenKind::Ident(s) if s == name)
84    }
85    /// Consume an identifier matching the given string.
86    #[allow(dead_code)]
87    fn consume_ident(&mut self, name: &str) -> bool {
88        if self.check_ident(name) {
89            self.advance();
90            true
91        } else {
92            false
93        }
94    }
95}
96impl Parser {
97    /// Parse a top-level declaration.
98    pub fn parse_decl(&mut self) -> Result<Located<Decl>, ParseError> {
99        let start = self.current().span.clone();
100        if self.check(&TokenKind::At) && self.peek().kind == TokenKind::LBracket {
101            return self.parse_attribute_decl();
102        }
103        if self.check(&TokenKind::Attribute) {
104            return self.parse_attribute_keyword();
105        }
106        match &self.current().kind {
107            TokenKind::Axiom => self.parse_axiom(),
108            TokenKind::Definition => self.parse_definition(),
109            TokenKind::Theorem | TokenKind::Lemma => self.parse_theorem(),
110            TokenKind::Inductive => self.parse_inductive(),
111            TokenKind::Import => self.parse_import(),
112            TokenKind::Namespace => self.parse_namespace(),
113            TokenKind::Structure => self.parse_structure(),
114            TokenKind::Class => self.parse_class(),
115            TokenKind::Instance => self.parse_instance(),
116            TokenKind::Section => self.parse_section(),
117            TokenKind::Variable
118            | TokenKind::Variables
119            | TokenKind::Parameter
120            | TokenKind::Parameters => self.parse_variable(),
121            TokenKind::Open => self.parse_open(),
122            TokenKind::Hash => self.parse_hash_cmd(),
123            _ => Err(ParseError::unexpected(
124                vec!["declaration".to_string()],
125                self.current().kind.clone(),
126                start,
127            )),
128        }
129    }
130    /// Parse an axiom declaration: `axiom name {u, v} : type`
131    fn parse_axiom(&mut self) -> Result<Located<Decl>, ParseError> {
132        let start = self.current().span.clone();
133        self.expect(TokenKind::Axiom)?;
134        let name = self.parse_ident()?;
135        let univ_params = self.parse_univ_params()?;
136        self.expect(TokenKind::Colon)?;
137        let ty = self.parse_expr()?;
138        let end = ty.span.clone();
139        Ok(Located::new(
140            Decl::Axiom {
141                name,
142                univ_params,
143                ty,
144                attrs: vec![],
145            },
146            start.merge(&end),
147        ))
148    }
149    /// Parse a definition: `def name {u} : type := value`
150    fn parse_definition(&mut self) -> Result<Located<Decl>, ParseError> {
151        let start = self.current().span.clone();
152        self.expect(TokenKind::Definition)?;
153        let name = self.parse_ident()?;
154        let univ_params = self.parse_univ_params()?;
155        let ty = if self.consume(TokenKind::Colon) {
156            Some(self.parse_expr()?)
157        } else {
158            None
159        };
160        self.expect(TokenKind::Assign)?;
161        let val = self.parse_expr()?;
162        let end = val.span.clone();
163        Ok(Located::new(
164            Decl::Definition {
165                name,
166                univ_params,
167                ty,
168                val,
169                where_clauses: vec![],
170                attrs: vec![],
171            },
172            start.merge(&end),
173        ))
174    }
175    /// Parse a theorem or lemma: `theorem name : type := proof`
176    fn parse_theorem(&mut self) -> Result<Located<Decl>, ParseError> {
177        let start = self.current().span.clone();
178        if self.check(&TokenKind::Theorem) {
179            self.expect(TokenKind::Theorem)?;
180        } else {
181            self.expect(TokenKind::Lemma)?;
182        }
183        let name = self.parse_ident()?;
184        let univ_params = self.parse_univ_params()?;
185        self.expect(TokenKind::Colon)?;
186        let ty = self.parse_expr()?;
187        self.expect(TokenKind::Assign)?;
188        let proof = self.parse_expr()?;
189        let end = proof.span.clone();
190        Ok(Located::new(
191            Decl::Theorem {
192                name,
193                univ_params,
194                ty,
195                proof,
196                where_clauses: vec![],
197                attrs: vec![],
198            },
199            start.merge(&end),
200        ))
201    }
202    /// Parse an inductive type: `inductive Name : Type | ctor : ...`
203    fn parse_inductive(&mut self) -> Result<Located<Decl>, ParseError> {
204        let start = self.current().span.clone();
205        self.expect(TokenKind::Inductive)?;
206        let name = self.parse_ident()?;
207        let univ_params = self.parse_univ_params()?;
208        let params = self.parse_binders()?;
209        let indices = Vec::new();
210        self.expect(TokenKind::Colon)?;
211        let ty = self.parse_expr()?;
212        let mut ctors = Vec::new();
213        if self.consume(TokenKind::Bar) {
214            loop {
215                let ctor_name = self.parse_ident()?;
216                self.expect(TokenKind::Colon)?;
217                let ctor_ty = self.parse_expr()?;
218                ctors.push(Constructor {
219                    name: ctor_name,
220                    ty: ctor_ty,
221                });
222                if !self.consume(TokenKind::Bar) {
223                    break;
224                }
225            }
226        }
227        let end = self.current().span.clone();
228        Ok(Located::new(
229            Decl::Inductive {
230                name,
231                univ_params,
232                params,
233                indices,
234                ty,
235                ctors,
236            },
237            start.merge(&end),
238        ))
239    }
240    /// Parse an import: `import Foo.Bar`
241    fn parse_import(&mut self) -> Result<Located<Decl>, ParseError> {
242        let start = self.current().span.clone();
243        self.expect(TokenKind::Import)?;
244        let mut path = vec![self.parse_ident()?];
245        while self.consume(TokenKind::Dot) {
246            path.push(self.parse_ident()?);
247        }
248        let end = self.current().span.clone();
249        Ok(Located::new(Decl::Import { path }, start.merge(&end)))
250    }
251    /// Parse a namespace: `namespace Name ... end Name`
252    fn parse_namespace(&mut self) -> Result<Located<Decl>, ParseError> {
253        let start = self.current().span.clone();
254        self.expect(TokenKind::Namespace)?;
255        let name = self.parse_ident()?;
256        let mut decls = Vec::new();
257        while !self.check(&TokenKind::End) && !self.is_eof() {
258            decls.push(self.parse_decl()?);
259        }
260        self.expect(TokenKind::End)?;
261        if !self.is_eof() && self.check_ident(&name) {
262            self.advance();
263        }
264        let end = self.current().span.clone();
265        Ok(Located::new(
266            Decl::Namespace { name, decls },
267            start.merge(&end),
268        ))
269    }
270    /// Parse a structure: `structure Name where field : Type ...`
271    fn parse_structure(&mut self) -> Result<Located<Decl>, ParseError> {
272        let start = self.current().span.clone();
273        self.expect(TokenKind::Structure)?;
274        let name = self.parse_ident()?;
275        let univ_params = self.parse_univ_params()?;
276        let mut extends = Vec::new();
277        if self.check_ident("extends") {
278            self.advance();
279            extends.push(self.parse_ident()?);
280            while self.consume(TokenKind::Comma) {
281                extends.push(self.parse_ident()?);
282            }
283        }
284        self.expect(TokenKind::Where)?;
285        let fields = self.parse_field_decls()?;
286        let end = self.current().span.clone();
287        Ok(Located::new(
288            Decl::Structure {
289                name,
290                univ_params,
291                extends,
292                fields,
293            },
294            start.merge(&end),
295        ))
296    }
297    /// Parse a class: `class Name where method : Type ...`
298    fn parse_class(&mut self) -> Result<Located<Decl>, ParseError> {
299        let start = self.current().span.clone();
300        self.expect(TokenKind::Class)?;
301        let name = self.parse_ident()?;
302        let univ_params = self.parse_univ_params()?;
303        let mut extends = Vec::new();
304        if self.check_ident("extends") {
305            self.advance();
306            extends.push(self.parse_ident()?);
307            while self.consume(TokenKind::Comma) {
308                extends.push(self.parse_ident()?);
309            }
310        }
311        self.expect(TokenKind::Where)?;
312        let fields = self.parse_field_decls()?;
313        let end = self.current().span.clone();
314        Ok(Located::new(
315            Decl::ClassDecl {
316                name,
317                univ_params,
318                extends,
319                fields,
320            },
321            start.merge(&end),
322        ))
323    }
324    /// Parse field declarations for structures/classes.
325    fn parse_field_decls(&mut self) -> Result<Vec<FieldDecl>, ParseError> {
326        let mut fields = Vec::new();
327        while !self.is_eof() && !self.check(&TokenKind::End) && !self.is_decl_start() {
328            if let TokenKind::Ident(_) = &self.current().kind {
329                if self.peek().kind == TokenKind::Colon {
330                    let field_name = self.parse_ident()?;
331                    self.expect(TokenKind::Colon)?;
332                    let ty = self.parse_field_type()?;
333                    let default = if self.consume(TokenKind::Assign) {
334                        Some(self.parse_field_type()?)
335                    } else {
336                        None
337                    };
338                    fields.push(FieldDecl {
339                        name: field_name,
340                        ty,
341                        default,
342                    });
343                } else {
344                    break;
345                }
346            } else {
347                break;
348            }
349        }
350        Ok(fields)
351    }
352    /// Parse an expression for a field type, stopping before `ident :` patterns
353    /// that would indicate the start of the next field.
354    fn parse_field_type(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
355        let start = self.current().span.clone();
356        let mut expr = self.parse_primary()?;
357        while !self.is_eof() && !self.is_stop_token() {
358            if let TokenKind::Ident(_) = &self.current().kind {
359                if self.peek().kind == TokenKind::Colon {
360                    break;
361                }
362            }
363            if self.check(&TokenKind::Arrow) {
364                self.advance();
365                let rhs = self.parse_field_type()?;
366                let span = start.merge(&rhs.span);
367                let binder = Binder {
368                    name: "_".to_string(),
369                    ty: Some(Box::new(expr)),
370                    info: BinderKind::Default,
371                };
372                expr = Located::new(SurfaceExpr::Pi(vec![binder], Box::new(rhs)), span);
373            } else if self.can_start_expr() {
374                let arg = self.parse_primary()?;
375                let span = start.merge(&arg.span);
376                expr = Located::new(SurfaceExpr::App(Box::new(expr), Box::new(arg)), span);
377            } else {
378                break;
379            }
380        }
381        Ok(expr)
382    }
383    /// Parse an instance: `instance [name] : ClassName Type where method := ...`
384    fn parse_instance(&mut self) -> Result<Located<Decl>, ParseError> {
385        let start = self.current().span.clone();
386        self.expect(TokenKind::Instance)?;
387        let name = if let TokenKind::Ident(_) = &self.current().kind {
388            if self.peek().kind == TokenKind::Colon {
389                let n = self.parse_ident()?;
390                Some(n)
391            } else {
392                None
393            }
394        } else {
395            None
396        };
397        self.expect(TokenKind::Colon)?;
398        let class_name = self.parse_ident()?;
399        let ty = self.parse_expr()?;
400        let mut defs = Vec::new();
401        if self.consume(TokenKind::Where) {
402            while !self.is_eof() && !self.check(&TokenKind::End) && !self.is_decl_start() {
403                if let TokenKind::Ident(_) = &self.current().kind {
404                    if self.peek().kind == TokenKind::Assign {
405                        let method_name = self.parse_ident()?;
406                        self.expect(TokenKind::Assign)?;
407                        let method_body = self.parse_expr()?;
408                        defs.push((method_name, method_body));
409                    } else {
410                        break;
411                    }
412                } else {
413                    break;
414                }
415            }
416        }
417        let end = self.current().span.clone();
418        Ok(Located::new(
419            Decl::InstanceDecl {
420                name,
421                class_name,
422                ty,
423                defs,
424            },
425            start.merge(&end),
426        ))
427    }
428    /// Parse a section: `section Name ... end Name`
429    fn parse_section(&mut self) -> Result<Located<Decl>, ParseError> {
430        let start = self.current().span.clone();
431        self.expect(TokenKind::Section)?;
432        let name = self.parse_ident()?;
433        let mut decls = Vec::new();
434        while !self.check(&TokenKind::End) && !self.is_eof() {
435            decls.push(self.parse_decl()?);
436        }
437        self.expect(TokenKind::End)?;
438        if !self.is_eof() && self.check_ident(&name) {
439            self.advance();
440        }
441        let end = self.current().span.clone();
442        Ok(Located::new(
443            Decl::SectionDecl { name, decls },
444            start.merge(&end),
445        ))
446    }
447    /// Parse variable/parameter declarations: `variable (x : T)`
448    fn parse_variable(&mut self) -> Result<Located<Decl>, ParseError> {
449        let start = self.current().span.clone();
450        self.advance();
451        let binders = self.parse_binders()?;
452        let end = self.current().span.clone();
453        Ok(Located::new(Decl::Variable { binders }, start.merge(&end)))
454    }
455    /// Parse open: `open Name [in expr]` or `open Name (name1 name2)`
456    fn parse_open(&mut self) -> Result<Located<Decl>, ParseError> {
457        let start = self.current().span.clone();
458        self.expect(TokenKind::Open)?;
459        let mut path = vec![self.parse_ident()?];
460        while self.consume(TokenKind::Dot) {
461            path.push(self.parse_ident()?);
462        }
463        let mut names = Vec::new();
464        if self.consume(TokenKind::LParen) {
465            while !self.check(&TokenKind::RParen) && !self.is_eof() {
466                names.push(self.parse_ident()?);
467            }
468            self.expect(TokenKind::RParen)?;
469        }
470        let end = self.current().span.clone();
471        Ok(Located::new(Decl::Open { path, names }, start.merge(&end)))
472    }
473    /// Parse attribute prefix: `@[simp, ext] theorem ...`
474    fn parse_attribute_decl(&mut self) -> Result<Located<Decl>, ParseError> {
475        let start = self.current().span.clone();
476        self.expect(TokenKind::At)?;
477        self.expect(TokenKind::LBracket)?;
478        let mut attrs = Vec::new();
479        attrs.push(self.parse_ident()?);
480        while self.consume(TokenKind::Comma) {
481            attrs.push(self.parse_ident()?);
482        }
483        self.expect(TokenKind::RBracket)?;
484        let decl = self.parse_decl()?;
485        let end = decl.span.clone();
486        Ok(Located::new(
487            Decl::Attribute {
488                attrs,
489                decl: Box::new(decl),
490            },
491            start.merge(&end),
492        ))
493    }
494    /// Parse attribute keyword form: `attribute [simp] name`
495    fn parse_attribute_keyword(&mut self) -> Result<Located<Decl>, ParseError> {
496        let start = self.current().span.clone();
497        self.expect(TokenKind::Attribute)?;
498        self.expect(TokenKind::LBracket)?;
499        let mut attrs = Vec::new();
500        attrs.push(self.parse_ident()?);
501        while self.consume(TokenKind::Comma) {
502            attrs.push(self.parse_ident()?);
503        }
504        self.expect(TokenKind::RBracket)?;
505        let name = self.parse_ident()?;
506        let end_span = self.current().span.clone();
507        let inner = Located::new(
508            Decl::Axiom {
509                name,
510                univ_params: vec![],
511                ty: Located::new(SurfaceExpr::Hole, end_span.clone()),
512                attrs: vec![],
513            },
514            end_span.clone(),
515        );
516        Ok(Located::new(
517            Decl::Attribute {
518                attrs,
519                decl: Box::new(inner),
520            },
521            start.merge(&end_span),
522        ))
523    }
524    /// Parse hash commands: `#check expr`, `#eval expr`, `#print name`
525    fn parse_hash_cmd(&mut self) -> Result<Located<Decl>, ParseError> {
526        let start = self.current().span.clone();
527        self.expect(TokenKind::Hash)?;
528        let cmd = self.parse_ident()?;
529        let arg = self.parse_expr()?;
530        let end = arg.span.clone();
531        Ok(Located::new(Decl::HashCmd { cmd, arg }, start.merge(&end)))
532    }
533    /// Check if current token starts a declaration.
534    fn is_decl_start(&self) -> bool {
535        matches!(
536            self.current().kind,
537            TokenKind::Axiom
538                | TokenKind::Definition
539                | TokenKind::Theorem
540                | TokenKind::Lemma
541                | TokenKind::Opaque
542                | TokenKind::Inductive
543                | TokenKind::Structure
544                | TokenKind::Class
545                | TokenKind::Instance
546                | TokenKind::Namespace
547                | TokenKind::Section
548                | TokenKind::Variable
549                | TokenKind::Variables
550                | TokenKind::Parameter
551                | TokenKind::Parameters
552                | TokenKind::Open
553                | TokenKind::Attribute
554                | TokenKind::Import
555                | TokenKind::Export
556                | TokenKind::Hash
557        ) || (self.check(&TokenKind::At) && self.peek().kind == TokenKind::LBracket)
558    }
559    /// Parse universe parameters: `{u, v}` - only when LBrace follows
560    fn parse_univ_params(&mut self) -> Result<Vec<String>, ParseError> {
561        if self.consume(TokenKind::LBrace) {
562            let mut params = Vec::new();
563            if let TokenKind::Ident(name) = &self.current().kind {
564                params.push(name.clone());
565                self.advance();
566            }
567            while self.consume(TokenKind::Comma) {
568                if let TokenKind::Ident(name) = &self.current().kind {
569                    params.push(name.clone());
570                    self.advance();
571                }
572            }
573            self.expect(TokenKind::RBrace)?;
574            Ok(params)
575        } else {
576            Ok(Vec::new())
577        }
578    }
579}
580impl Parser {
581    /// Parse an expression (entry point, lowest precedence).
582    pub fn parse_expr(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
583        self.parse_expr_prec(0)
584    }
585    /// Parse expression with precedence climbing.
586    ///
587    /// Precedence table (low to high):
588    ///   1  : Arrow (right-assoc)
589    ///   5  : Iff
590    ///   8  : OrOr / Or
591    ///  12  : AndAnd / And
592    ///  20  : Eq Ne Lt Le Gt Ge (comparison, non-assoc)
593    ///  30  : Plus Minus (left-assoc)
594    ///  40  : Star Slash Percent (left-assoc)
595    ///  50  : Caret (right-assoc, exponentiation)
596    /// 100  : Application (juxtaposition)
597    fn parse_expr_prec(&mut self, min_prec: u32) -> Result<Located<SurfaceExpr>, ParseError> {
598        let start = self.current().span.clone();
599        let mut expr = self.parse_prefix()?;
600        loop {
601            if self.check(&TokenKind::Dot) {
602                if let TokenKind::Ident(_) = &self.peek().kind {
603                    self.advance();
604                    let field = self.parse_ident()?;
605                    let span = start.merge(&self.current().span);
606                    expr = Located::new(SurfaceExpr::Proj(Box::new(expr), field), span);
607                    continue;
608                }
609            }
610            break;
611        }
612        while !self.is_eof() && !self.is_stop_token() {
613            let (prec, assoc) = self.get_infix_prec_assoc();
614            if prec < min_prec {
615                break;
616            }
617            if self.check(&TokenKind::Arrow) {
618                self.advance();
619                let next_prec = if assoc == Assoc::Right {
620                    prec
621                } else {
622                    prec + 1
623                };
624                let rhs = self.parse_expr_prec(next_prec)?;
625                let span = start.merge(&rhs.span);
626                let binder = Binder {
627                    name: "_".to_string(),
628                    ty: Some(Box::new(expr)),
629                    info: BinderKind::Default,
630                };
631                expr = Located::new(SurfaceExpr::Pi(vec![binder], Box::new(rhs)), span);
632            } else if let Some(op_name) = self.get_binop_name() {
633                let op_tok = self.advance();
634                let op_span = op_tok.span.clone();
635                let next_prec = if assoc == Assoc::Right {
636                    prec
637                } else {
638                    prec + 1
639                };
640                let rhs = self.parse_expr_prec(next_prec)?;
641                let span = start.merge(&rhs.span);
642                let op_var = Located::new(SurfaceExpr::Var(op_name), op_span);
643                let app1 = Located::new(
644                    SurfaceExpr::App(Box::new(op_var), Box::new(expr)),
645                    span.clone(),
646                );
647                expr = Located::new(SurfaceExpr::App(Box::new(app1), Box::new(rhs)), span);
648            } else if prec == 100 {
649                if self.can_start_expr() {
650                    let arg = self.parse_app_arg()?;
651                    let span = start.merge(&arg.span);
652                    expr = Located::new(SurfaceExpr::App(Box::new(expr), Box::new(arg)), span);
653                } else {
654                    break;
655                }
656            } else {
657                break;
658            }
659        }
660        Ok(expr)
661    }
662    /// Parse an application argument.
663    /// Handles named arguments: `(x := e)` as well as normal primaries.
664    fn parse_app_arg(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
665        if self.check(&TokenKind::LParen) {
666            if let TokenKind::Ident(_) = &self.peek().kind {
667                if self.peek2().kind == TokenKind::Assign {
668                    return self.parse_named_arg();
669                }
670            }
671        }
672        self.parse_primary()
673    }
674    /// Parse a named argument: `(x := expr)`
675    fn parse_named_arg(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
676        let start = self.current().span.clone();
677        self.expect(TokenKind::LParen)?;
678        let name = self.parse_ident()?;
679        self.expect(TokenKind::Assign)?;
680        let val = self.parse_expr()?;
681        self.expect(TokenKind::RParen)?;
682        let end = self.current().span.clone();
683        Ok(Located::new(
684            SurfaceExpr::NamedArg(
685                Box::new(Located::new(SurfaceExpr::Hole, start.clone())),
686                name,
687                Box::new(val),
688            ),
689            start.merge(&end),
690        ))
691    }
692    /// Return the binary operator name for the current token, if it is a binop.
693    fn get_binop_name(&self) -> Option<String> {
694        match &self.current().kind {
695            TokenKind::Plus => Some("+".to_string()),
696            TokenKind::Minus => Some("-".to_string()),
697            TokenKind::Star => Some("*".to_string()),
698            TokenKind::Slash => Some("/".to_string()),
699            TokenKind::Percent => Some("%".to_string()),
700            TokenKind::Caret => Some("^".to_string()),
701            TokenKind::AndAnd => Some("&&".to_string()),
702            TokenKind::OrOr => Some("||".to_string()),
703            TokenKind::And => Some("And".to_string()),
704            TokenKind::Or => Some("Or".to_string()),
705            TokenKind::Iff => Some("Iff".to_string()),
706            TokenKind::Eq => Some("Eq".to_string()),
707            TokenKind::Ne => Some("Ne".to_string()),
708            TokenKind::BangEq => Some("Ne".to_string()),
709            TokenKind::Lt => Some("Lt".to_string()),
710            TokenKind::Le => Some("Le".to_string()),
711            TokenKind::Gt => Some("Gt".to_string()),
712            TokenKind::Ge => Some("Ge".to_string()),
713            _ => None,
714        }
715    }
716    /// Check if current token is a stop token (ends expression parsing).
717    fn is_stop_token(&self) -> bool {
718        matches!(
719            self.current().kind,
720            TokenKind::RParen
721                | TokenKind::RBrace
722                | TokenKind::RBracket
723                | TokenKind::RAngle
724                | TokenKind::Comma
725                | TokenKind::In
726                | TokenKind::Bar
727                | TokenKind::Semicolon
728                | TokenKind::Then
729                | TokenKind::Else
730                | TokenKind::With
731                | TokenKind::Where
732                | TokenKind::End
733                | TokenKind::From
734                | TokenKind::By
735                | TokenKind::Assign
736        )
737    }
738    /// Check if current token can start an expression.
739    fn can_start_expr(&self) -> bool {
740        matches!(
741            self.current().kind,
742            TokenKind::Ident(_)
743                | TokenKind::Nat(_)
744                | TokenKind::String(_)
745                | TokenKind::Type
746                | TokenKind::Prop
747                | TokenKind::Sort
748                | TokenKind::Fun
749                | TokenKind::Forall
750                | TokenKind::Exists
751                | TokenKind::Let
752                | TokenKind::If
753                | TokenKind::Match
754                | TokenKind::Do
755                | TokenKind::Have
756                | TokenKind::Suffices
757                | TokenKind::Show
758                | TokenKind::Underscore
759                | TokenKind::LParen
760                | TokenKind::LBracket
761                | TokenKind::LAngle
762                | TokenKind::Not
763                | TokenKind::Bang
764                | TokenKind::Question
765        )
766    }
767    /// Get infix operator precedence and associativity.
768    fn get_infix_prec_assoc(&self) -> (u32, Assoc) {
769        match &self.current().kind {
770            TokenKind::Arrow => (1, Assoc::Right),
771            TokenKind::Iff => (5, Assoc::Left),
772            TokenKind::OrOr | TokenKind::Or => (8, Assoc::Left),
773            TokenKind::AndAnd | TokenKind::And => (12, Assoc::Left),
774            TokenKind::Eq
775            | TokenKind::Ne
776            | TokenKind::BangEq
777            | TokenKind::Lt
778            | TokenKind::Le
779            | TokenKind::Gt
780            | TokenKind::Ge => (20, Assoc::Left),
781            TokenKind::Plus | TokenKind::Minus => (30, Assoc::Left),
782            TokenKind::Star | TokenKind::Slash | TokenKind::Percent => (40, Assoc::Left),
783            TokenKind::Caret => (50, Assoc::Right),
784            _ => (100, Assoc::Left),
785        }
786    }
787}
788impl Parser {
789    /// Parse a prefix expression (unary operators or primary).
790    fn parse_prefix(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
791        let start = self.current().span.clone();
792        match &self.current().kind {
793            TokenKind::Not | TokenKind::Bang => {
794                self.advance();
795                let operand = self.parse_prefix()?;
796                let span = start.merge(&operand.span);
797                let not_var = Located::new(SurfaceExpr::Var("Not".to_string()), start);
798                Ok(Located::new(
799                    SurfaceExpr::App(Box::new(not_var), Box::new(operand)),
800                    span,
801                ))
802            }
803            TokenKind::Minus => {
804                self.advance();
805                let operand = self.parse_prefix()?;
806                let span = start.merge(&operand.span);
807                let neg_var = Located::new(SurfaceExpr::Var("Neg".to_string()), start);
808                Ok(Located::new(
809                    SurfaceExpr::App(Box::new(neg_var), Box::new(operand)),
810                    span,
811                ))
812            }
813            _ => self.parse_primary(),
814        }
815    }
816    /// Parse primary expression (atoms and compound forms).
817    fn parse_primary(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
818        let start = self.current().span.clone();
819        match &self.current().kind.clone() {
820            TokenKind::Ident(name) => {
821                let name = name.clone();
822                self.advance();
823                Ok(Located::new(SurfaceExpr::Var(name), start))
824            }
825            TokenKind::Nat(n) => {
826                let n = *n;
827                self.advance();
828                Ok(Located::new(SurfaceExpr::Lit(Literal::Nat(n)), start))
829            }
830            TokenKind::String(s) => {
831                let s = s.clone();
832                self.advance();
833                Ok(Located::new(SurfaceExpr::Lit(Literal::String(s)), start))
834            }
835            TokenKind::Type => {
836                self.advance();
837                if let TokenKind::Ident(u) = &self.current().kind {
838                    let u = u.clone();
839                    let end = self.current().span.clone();
840                    self.advance();
841                    Ok(Located::new(
842                        SurfaceExpr::Sort(SortKind::TypeU(u)),
843                        start.merge(&end),
844                    ))
845                } else if let TokenKind::Nat(n) = &self.current().kind {
846                    if *n > 0 {
847                        let u = format!("{}", n);
848                        let end = self.current().span.clone();
849                        self.advance();
850                        Ok(Located::new(
851                            SurfaceExpr::Sort(SortKind::TypeU(u)),
852                            start.merge(&end),
853                        ))
854                    } else {
855                        Ok(Located::new(SurfaceExpr::Sort(SortKind::Type), start))
856                    }
857                } else {
858                    Ok(Located::new(SurfaceExpr::Sort(SortKind::Type), start))
859                }
860            }
861            TokenKind::Prop => {
862                self.advance();
863                Ok(Located::new(SurfaceExpr::Sort(SortKind::Prop), start))
864            }
865            TokenKind::Sort => {
866                self.advance();
867                if let TokenKind::Ident(u) = &self.current().kind {
868                    let u = u.clone();
869                    let end = self.current().span.clone();
870                    self.advance();
871                    Ok(Located::new(
872                        SurfaceExpr::Sort(SortKind::SortU(u)),
873                        start.merge(&end),
874                    ))
875                } else {
876                    Ok(Located::new(SurfaceExpr::Sort(SortKind::Prop), start))
877                }
878            }
879            TokenKind::Fun => self.parse_lambda(),
880            TokenKind::Forall => self.parse_pi(),
881            TokenKind::Exists => self.parse_exists(),
882            TokenKind::Let => self.parse_let(),
883            TokenKind::If => self.parse_if(),
884            TokenKind::Match => self.parse_match(),
885            TokenKind::Do => self.parse_do(),
886            TokenKind::Have => self.parse_have(),
887            TokenKind::Suffices => self.parse_suffices(),
888            TokenKind::Show => self.parse_show(),
889            TokenKind::Underscore => {
890                self.advance();
891                Ok(Located::new(SurfaceExpr::Hole, start))
892            }
893            TokenKind::Question => {
894                self.advance();
895                Ok(Located::new(SurfaceExpr::Hole, start))
896            }
897            TokenKind::LParen => self.parse_paren_or_tuple(),
898            TokenKind::LBracket => self.parse_list_literal(),
899            TokenKind::LAngle => self.parse_anonymous_ctor(),
900            _ => Err(ParseError::unexpected(
901                vec!["expression".to_string()],
902                self.current().kind.clone(),
903                start,
904            )),
905        }
906    }
907    /// Parse lambda expression: `fun (x : T) => body`
908    fn parse_lambda(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
909        let start = self.current().span.clone();
910        self.expect(TokenKind::Fun)?;
911        let binders = self.parse_binders()?;
912        self.expect(TokenKind::Arrow)?;
913        let body = self.parse_expr()?;
914        let end = body.span.clone();
915        Ok(Located::new(
916            SurfaceExpr::Lam(binders, Box::new(body)),
917            start.merge(&end),
918        ))
919    }
920    /// Parse Pi type: `forall (x : T), body`
921    fn parse_pi(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
922        let start = self.current().span.clone();
923        self.expect(TokenKind::Forall)?;
924        let binders = self.parse_binders()?;
925        self.expect(TokenKind::Comma)?;
926        let body = self.parse_expr()?;
927        let end = body.span.clone();
928        Ok(Located::new(
929            SurfaceExpr::Pi(binders, Box::new(body)),
930            start.merge(&end),
931        ))
932    }
933    /// Parse existential quantifier: `∃ binders, body` → `Exists (fun binders => body)`
934    fn parse_exists(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
935        let start = self.current().span.clone();
936        self.expect(TokenKind::Exists)?;
937        let binders = self.parse_binders()?;
938        self.expect(TokenKind::Comma)?;
939        let body = self.parse_expr()?;
940        let end = body.span.clone();
941        let span = start.merge(&end);
942        let exists_var = Located::new(SurfaceExpr::Var("Exists".to_string()), span.clone());
943        let lam = Located::new(SurfaceExpr::Lam(binders, Box::new(body)), span.clone());
944        Ok(Located::new(
945            SurfaceExpr::App(Box::new(exists_var), Box::new(lam)),
946            span,
947        ))
948    }
949    /// Parse let expression: `let x : T := val in body`
950    fn parse_let(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
951        let start = self.current().span.clone();
952        self.expect(TokenKind::Let)?;
953        let name = self.parse_ident()?;
954        let ty = if self.consume(TokenKind::Colon) {
955            Some(Box::new(self.parse_expr()?))
956        } else {
957            None
958        };
959        self.expect(TokenKind::Assign)?;
960        let val = self.parse_expr()?;
961        self.expect(TokenKind::In)?;
962        let body = self.parse_expr()?;
963        let end = body.span.clone();
964        Ok(Located::new(
965            SurfaceExpr::Let(name, ty, Box::new(val), Box::new(body)),
966            start.merge(&end),
967        ))
968    }
969    /// Parse if-then-else: `if cond then t else e`
970    fn parse_if(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
971        let start = self.current().span.clone();
972        self.expect(TokenKind::If)?;
973        let cond = self.parse_expr()?;
974        self.expect(TokenKind::Then)?;
975        let then_branch = self.parse_expr()?;
976        self.expect(TokenKind::Else)?;
977        let else_branch = self.parse_expr()?;
978        let end = else_branch.span.clone();
979        Ok(Located::new(
980            SurfaceExpr::If(Box::new(cond), Box::new(then_branch), Box::new(else_branch)),
981            start.merge(&end),
982        ))
983    }
984    /// Parse match expression: `match e with | pat => rhs | ...`
985    fn parse_match(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
986        let start = self.current().span.clone();
987        self.expect(TokenKind::Match)?;
988        let scrutinee = self.parse_expr()?;
989        self.expect(TokenKind::With)?;
990        let mut arms = Vec::new();
991        self.consume(TokenKind::Bar);
992        loop {
993            let pat = self.parse_pattern()?;
994            let guard = if self.check(&TokenKind::If) {
995                self.advance();
996                Some(self.parse_expr_prec(2)?)
997            } else {
998                None
999            };
1000            self.expect(TokenKind::Arrow)?;
1001            let rhs = self.parse_expr()?;
1002            arms.push(MatchArm {
1003                pattern: pat,
1004                guard,
1005                rhs,
1006            });
1007            if !self.consume(TokenKind::Bar) {
1008                break;
1009            }
1010        }
1011        let end = self.current().span.clone();
1012        Ok(Located::new(
1013            SurfaceExpr::Match(Box::new(scrutinee), arms),
1014            start.merge(&end),
1015        ))
1016    }
1017    /// Parse a pattern for match arms.
1018    fn parse_pattern(&mut self) -> Result<Located<Pattern>, ParseError> {
1019        let start = self.current().span.clone();
1020        match &self.current().kind.clone() {
1021            TokenKind::Underscore => {
1022                self.advance();
1023                Ok(Located::new(Pattern::Wild, start))
1024            }
1025            TokenKind::Nat(n) => {
1026                let n = *n;
1027                self.advance();
1028                Ok(Located::new(Pattern::Lit(Literal::Nat(n)), start))
1029            }
1030            TokenKind::String(s) => {
1031                let s = s.clone();
1032                self.advance();
1033                Ok(Located::new(Pattern::Lit(Literal::String(s)), start))
1034            }
1035            TokenKind::Ident(name) => {
1036                let name = name.clone();
1037                self.advance();
1038                let mut sub_pats = Vec::new();
1039                while self.can_start_pattern() {
1040                    sub_pats.push(self.parse_atomic_pattern()?);
1041                }
1042                if sub_pats.is_empty() {
1043                    Ok(Located::new(Pattern::Var(name), start))
1044                } else {
1045                    let end = sub_pats
1046                        .last()
1047                        .expect("sub_pats non-empty per else branch")
1048                        .span
1049                        .clone();
1050                    Ok(Located::new(
1051                        Pattern::Ctor(name, sub_pats),
1052                        start.merge(&end),
1053                    ))
1054                }
1055            }
1056            TokenKind::LParen => {
1057                self.advance();
1058                let inner = self.parse_pattern()?;
1059                self.expect(TokenKind::RParen)?;
1060                Ok(inner)
1061            }
1062            _ => Err(ParseError::unexpected(
1063                vec!["pattern".to_string()],
1064                self.current().kind.clone(),
1065                start,
1066            )),
1067        }
1068    }
1069    /// Parse an atomic pattern (used as sub-patterns for constructors).
1070    fn parse_atomic_pattern(&mut self) -> Result<Located<Pattern>, ParseError> {
1071        let start = self.current().span.clone();
1072        match &self.current().kind.clone() {
1073            TokenKind::Underscore => {
1074                self.advance();
1075                Ok(Located::new(Pattern::Wild, start))
1076            }
1077            TokenKind::Nat(n) => {
1078                let n = *n;
1079                self.advance();
1080                Ok(Located::new(Pattern::Lit(Literal::Nat(n)), start))
1081            }
1082            TokenKind::String(s) => {
1083                let s = s.clone();
1084                self.advance();
1085                Ok(Located::new(Pattern::Lit(Literal::String(s)), start))
1086            }
1087            TokenKind::Ident(name) => {
1088                let name = name.clone();
1089                self.advance();
1090                Ok(Located::new(Pattern::Var(name), start))
1091            }
1092            TokenKind::LParen => {
1093                self.advance();
1094                let inner = self.parse_pattern()?;
1095                self.expect(TokenKind::RParen)?;
1096                Ok(inner)
1097            }
1098            _ => Err(ParseError::unexpected(
1099                vec!["pattern".to_string()],
1100                self.current().kind.clone(),
1101                start,
1102            )),
1103        }
1104    }
1105    /// Check if current token can start a pattern.
1106    fn can_start_pattern(&self) -> bool {
1107        matches!(
1108            self.current().kind,
1109            TokenKind::Ident(_)
1110                | TokenKind::Nat(_)
1111                | TokenKind::String(_)
1112                | TokenKind::Underscore
1113                | TokenKind::LParen
1114        )
1115    }
1116    /// Parse do notation: `do { action1; action2; ... }` or `do action1; action2`
1117    fn parse_do(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1118        let start = self.current().span.clone();
1119        self.expect(TokenKind::Do)?;
1120        let has_brace = self.consume(TokenKind::LBrace);
1121        let mut actions = Vec::new();
1122        loop {
1123            if has_brace && self.check(&TokenKind::RBrace) {
1124                break;
1125            }
1126            if self.is_eof() {
1127                break;
1128            }
1129            let action = self.parse_do_action()?;
1130            actions.push(action);
1131            if !self.consume(TokenKind::Semicolon) {
1132                break;
1133            }
1134        }
1135        if has_brace {
1136            self.expect(TokenKind::RBrace)?;
1137        }
1138        let end = self.current().span.clone();
1139        Ok(Located::new(SurfaceExpr::Do(actions), start.merge(&end)))
1140    }
1141    /// Parse a single do-notation action.
1142    fn parse_do_action(&mut self) -> Result<DoAction, ParseError> {
1143        if self.check(&TokenKind::Let) {
1144            self.advance();
1145            let name = self.parse_ident()?;
1146            if self.consume(TokenKind::Colon) {
1147                let ty = self.parse_expr()?;
1148                self.expect(TokenKind::Assign)?;
1149                let val = self.parse_expr()?;
1150                return Ok(DoAction::LetTyped(name, ty, val));
1151            }
1152            self.expect(TokenKind::Assign)?;
1153            let val = self.parse_expr()?;
1154            return Ok(DoAction::Let(name, val));
1155        }
1156        if let TokenKind::Ident(_) = &self.current().kind {
1157            if self.peek().kind == TokenKind::LeftArrow {
1158                let name = self.parse_ident()?;
1159                self.expect(TokenKind::LeftArrow)?;
1160                let val = self.parse_expr()?;
1161                return Ok(DoAction::Bind(name, val));
1162            }
1163        }
1164        let expr = self.parse_expr()?;
1165        Ok(DoAction::Expr(expr))
1166    }
1167    /// Parse have expression: `have h : T := proof; body`
1168    fn parse_have(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1169        let start = self.current().span.clone();
1170        self.expect(TokenKind::Have)?;
1171        let name = self.parse_ident()?;
1172        self.expect(TokenKind::Colon)?;
1173        let ty = self.parse_expr()?;
1174        self.expect(TokenKind::Assign)?;
1175        let proof = self.parse_expr()?;
1176        self.expect(TokenKind::Semicolon)?;
1177        let body = self.parse_expr()?;
1178        let end = body.span.clone();
1179        Ok(Located::new(
1180            SurfaceExpr::Have(name, Box::new(ty), Box::new(proof), Box::new(body)),
1181            start.merge(&end),
1182        ))
1183    }
1184    /// Parse suffices expression: `suffices h : T by tactic; body`
1185    fn parse_suffices(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1186        let start = self.current().span.clone();
1187        self.expect(TokenKind::Suffices)?;
1188        let name = self.parse_ident()?;
1189        self.expect(TokenKind::Colon)?;
1190        let ty = self.parse_expr()?;
1191        self.expect(TokenKind::By)?;
1192        let tactic = self.parse_expr()?;
1193        let end = tactic.span.clone();
1194        Ok(Located::new(
1195            SurfaceExpr::Suffices(name, Box::new(ty), Box::new(tactic)),
1196            start.merge(&end),
1197        ))
1198    }
1199    /// Parse show expression: `show T from expr`
1200    fn parse_show(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1201        let start = self.current().span.clone();
1202        self.expect(TokenKind::Show)?;
1203        let ty = self.parse_expr()?;
1204        self.expect(TokenKind::From)?;
1205        let proof = self.parse_expr()?;
1206        let end = proof.span.clone();
1207        Ok(Located::new(
1208            SurfaceExpr::Show(Box::new(ty), Box::new(proof)),
1209            start.merge(&end),
1210        ))
1211    }
1212    /// Parse parenthesized expression, tuple, or type annotation.
1213    ///
1214    /// `(e)` -- grouping
1215    /// `(e : T)` -- type annotation
1216    /// `(e, f, ...)` -- tuple
1217    fn parse_paren_or_tuple(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1218        let start = self.current().span.clone();
1219        self.expect(TokenKind::LParen)?;
1220        if self.consume(TokenKind::RParen) {
1221            return Ok(Located::new(SurfaceExpr::Tuple(vec![]), start));
1222        }
1223        let first = self.parse_expr()?;
1224        if self.consume(TokenKind::Colon) {
1225            let ty = self.parse_expr()?;
1226            let span = start.merge(&ty.span);
1227            self.expect(TokenKind::RParen)?;
1228            return Ok(Located::new(
1229                SurfaceExpr::Ann(Box::new(first), Box::new(ty)),
1230                span,
1231            ));
1232        }
1233        if self.consume(TokenKind::Comma) {
1234            let mut elems = vec![first];
1235            elems.push(self.parse_expr()?);
1236            while self.consume(TokenKind::Comma) {
1237                elems.push(self.parse_expr()?);
1238            }
1239            self.expect(TokenKind::RParen)?;
1240            let end = self.current().span.clone();
1241            return Ok(Located::new(SurfaceExpr::Tuple(elems), start.merge(&end)));
1242        }
1243        self.expect(TokenKind::RParen)?;
1244        Ok(first)
1245    }
1246    /// Parse list literal: `[e1, e2, ...]` or `[]`
1247    fn parse_list_literal(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1248        let start = self.current().span.clone();
1249        self.expect(TokenKind::LBracket)?;
1250        let mut elems = Vec::new();
1251        if !self.check(&TokenKind::RBracket) {
1252            elems.push(self.parse_expr()?);
1253            while self.consume(TokenKind::Comma) {
1254                elems.push(self.parse_expr()?);
1255            }
1256        }
1257        self.expect(TokenKind::RBracket)?;
1258        let end = self.current().span.clone();
1259        Ok(Located::new(SurfaceExpr::ListLit(elems), start.merge(&end)))
1260    }
1261    /// Parse anonymous constructor: `(langle) a, b, c (rangle)`
1262    fn parse_anonymous_ctor(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1263        let start = self.current().span.clone();
1264        self.expect(TokenKind::LAngle)?;
1265        let mut elems = Vec::new();
1266        if !self.check(&TokenKind::RAngle) {
1267            elems.push(self.parse_expr()?);
1268            while self.consume(TokenKind::Comma) {
1269                elems.push(self.parse_expr()?);
1270            }
1271        }
1272        self.expect(TokenKind::RAngle)?;
1273        let end = self.current().span.clone();
1274        Ok(Located::new(
1275            SurfaceExpr::AnonymousCtor(elems),
1276            start.merge(&end),
1277        ))
1278    }
1279}
1280impl Parser {
1281    /// Parse binders for lambda, forall, variable declarations.
1282    ///
1283    /// Supports:
1284    /// - `(x : T)` -- explicit
1285    /// - `{x : T}` -- implicit
1286    /// - `[x : T]` -- instance
1287    /// - `{{x : T}}` -- strict implicit
1288    /// - `x` -- simple binder without type
1289    /// - Multiple binder groups
1290    pub fn parse_binders(&mut self) -> Result<Vec<Binder>, ParseError> {
1291        let mut binders = Vec::new();
1292        loop {
1293            match &self.current().kind {
1294                TokenKind::LParen => {
1295                    self.advance();
1296                    self.parse_binder_group(&mut binders, BinderKind::Default)?;
1297                    self.expect(TokenKind::RParen)?;
1298                }
1299                TokenKind::LBrace => {
1300                    if self.peek().kind == TokenKind::LBrace {
1301                        self.advance();
1302                        self.advance();
1303                        self.parse_binder_group(&mut binders, BinderKind::StrictImplicit)?;
1304                        self.expect(TokenKind::RBrace)?;
1305                        self.expect(TokenKind::RBrace)?;
1306                    } else {
1307                        self.advance();
1308                        self.parse_binder_group(&mut binders, BinderKind::Implicit)?;
1309                        self.expect(TokenKind::RBrace)?;
1310                    }
1311                }
1312                TokenKind::LBracket => {
1313                    self.advance();
1314                    self.parse_binder_group(&mut binders, BinderKind::Instance)?;
1315                    self.expect(TokenKind::RBracket)?;
1316                }
1317                TokenKind::Ident(_) | TokenKind::Underscore => {
1318                    let name = if self.check(&TokenKind::Underscore) {
1319                        self.advance();
1320                        "_".to_string()
1321                    } else {
1322                        self.parse_ident()?
1323                    };
1324                    binders.push(Binder {
1325                        name,
1326                        ty: None,
1327                        info: BinderKind::Default,
1328                    });
1329                }
1330                _ => break,
1331            }
1332            if !matches!(
1333                self.current().kind,
1334                TokenKind::LParen
1335                    | TokenKind::LBrace
1336                    | TokenKind::LBracket
1337                    | TokenKind::Ident(_)
1338                    | TokenKind::Underscore
1339            ) {
1340                break;
1341            }
1342        }
1343        Ok(binders)
1344    }
1345    /// Parse a binder group inside delimiters: `x y : T` or `x : T, y : T`
1346    fn parse_binder_group(
1347        &mut self,
1348        binders: &mut Vec<Binder>,
1349        kind: BinderKind,
1350    ) -> Result<(), ParseError> {
1351        let mut names = Vec::new();
1352        loop {
1353            let name = if self.check(&TokenKind::Underscore) {
1354                self.advance();
1355                "_".to_string()
1356            } else if let TokenKind::Ident(_) = &self.current().kind {
1357                self.parse_ident()?
1358            } else {
1359                break;
1360            };
1361            names.push(name);
1362            if self.check(&TokenKind::Colon) {
1363                break;
1364            }
1365            if self.check(&TokenKind::Comma) {
1366                break;
1367            }
1368        }
1369        if names.is_empty() {
1370            return Err(ParseError::unexpected(
1371                vec!["identifier".to_string()],
1372                self.current().kind.clone(),
1373                self.current().span.clone(),
1374            ));
1375        }
1376        let ty = if self.consume(TokenKind::Colon) {
1377            Some(self.parse_expr()?)
1378        } else {
1379            None
1380        };
1381        for name in names {
1382            binders.push(Binder {
1383                name,
1384                ty: ty.as_ref().map(|t| Box::new(t.clone())),
1385                info: kind.clone(),
1386            });
1387        }
1388        while self.consume(TokenKind::Comma) {
1389            let name = if self.check(&TokenKind::Underscore) {
1390                self.advance();
1391                "_".to_string()
1392            } else {
1393                self.parse_ident()?
1394            };
1395            let more_ty = if self.consume(TokenKind::Colon) {
1396                Some(Box::new(self.parse_expr()?))
1397            } else {
1398                None
1399            };
1400            binders.push(Binder {
1401                name,
1402                ty: more_ty,
1403                info: kind.clone(),
1404            });
1405        }
1406        Ok(())
1407    }
1408}
1409impl Parser {
1410    /// Parse where clauses for definitions and theorems.
1411    #[allow(dead_code)]
1412    fn parse_where_clauses(&mut self) -> Result<Vec<WhereClause>, ParseError> {
1413        let mut clauses = Vec::new();
1414        if !self.check_ident("where") {
1415            return Ok(clauses);
1416        }
1417        self.advance();
1418        loop {
1419            if self.is_eof() || self.is_decl_start() {
1420                break;
1421            }
1422            let name = self.parse_ident()?;
1423            let params = self.parse_binders()?;
1424            let ty = if self.consume(TokenKind::Colon) {
1425                Some(self.parse_expr()?)
1426            } else {
1427                None
1428            };
1429            self.expect(TokenKind::Assign)?;
1430            let val = self.parse_expr()?;
1431            clauses.push(WhereClause {
1432                name,
1433                params,
1434                ty,
1435                val,
1436            });
1437            if !self.consume(TokenKind::Comma) {
1438                break;
1439            }
1440        }
1441        Ok(clauses)
1442    }
1443    /// Parse calc expression: `calc x = y := proof1 _ = z := proof2`
1444    #[allow(dead_code)]
1445    fn parse_calc(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1446        let start = self.current().span.clone();
1447        if !self.check_ident("calc") {
1448            return Err(ParseError::unexpected(
1449                vec!["calc".to_string()],
1450                self.current().kind.clone(),
1451                start,
1452            ));
1453        }
1454        self.advance();
1455        let mut steps = Vec::new();
1456        let lhs = self.parse_expr()?;
1457        let rel = self.parse_ident()?;
1458        let rhs = self.parse_expr()?;
1459        self.expect(TokenKind::Assign)?;
1460        let proof = self.parse_expr()?;
1461        steps.push(CalcStep {
1462            lhs,
1463            rel,
1464            rhs,
1465            proof,
1466        });
1467        while self.consume(TokenKind::Underscore) {
1468            let rel = self.parse_ident()?;
1469            let rhs = self.parse_expr()?;
1470            self.expect(TokenKind::Assign)?;
1471            let proof = self.parse_expr()?;
1472            let prev_rhs = steps
1473                .last()
1474                .expect("steps non-empty: first step pushed before loop")
1475                .rhs
1476                .clone();
1477            steps.push(CalcStep {
1478                lhs: prev_rhs,
1479                rel,
1480                rhs,
1481                proof,
1482            });
1483        }
1484        let end = self.current().span.clone();
1485        Ok(Located::new(SurfaceExpr::Calc(steps), start.merge(&end)))
1486    }
1487    /// Parse by-tactic expression: `by simp; ring`
1488    #[allow(dead_code)]
1489    fn parse_by_tactic(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1490        let start = self.current().span.clone();
1491        self.expect(TokenKind::By)?;
1492        let mut tactics = Vec::new();
1493        loop {
1494            if self.is_eof() || self.is_stop_token() {
1495                break;
1496            }
1497            let tactic_name = self.parse_ident()?;
1498            let span = self.current().span.clone();
1499            tactics.push(Located::new(tactic_name, span));
1500            if !self.consume(TokenKind::Semicolon) {
1501                break;
1502            }
1503        }
1504        let end = self.current().span.clone();
1505        Ok(Located::new(
1506            SurfaceExpr::ByTactic(tactics),
1507            start.merge(&end),
1508        ))
1509    }
1510    /// Parse return expression (for do notation): `return e`
1511    #[allow(dead_code)]
1512    fn parse_return(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1513        let start = self.current().span.clone();
1514        if !self.check_ident("return") {
1515            return Err(ParseError::unexpected(
1516                vec!["return".to_string()],
1517                self.current().kind.clone(),
1518                start,
1519            ));
1520        }
1521        self.advance();
1522        let val = self.parse_expr()?;
1523        let end = val.span.clone();
1524        Ok(Located::new(
1525            SurfaceExpr::Return(Box::new(val)),
1526            start.merge(&end),
1527        ))
1528    }
1529    /// Parse range expression: `a..b`, `..b`, `a..`
1530    #[allow(dead_code)]
1531    fn parse_range(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1532        let start = self.current().span.clone();
1533        let start_expr = if self.check(&TokenKind::Dot) && self.peek().kind == TokenKind::Dot {
1534            None
1535        } else {
1536            Some(Box::new(self.parse_expr()?))
1537        };
1538        if !self.check(&TokenKind::Dot) || self.peek().kind != TokenKind::Dot {
1539            return Err(ParseError::unexpected(
1540                vec!["..".to_string()],
1541                self.current().kind.clone(),
1542                self.current().span.clone(),
1543            ));
1544        }
1545        self.advance();
1546        self.advance();
1547        let end_expr = if self.is_stop_token() {
1548            None
1549        } else {
1550            Some(Box::new(self.parse_expr()?))
1551        };
1552        let end = self.current().span.clone();
1553        Ok(Located::new(
1554            SurfaceExpr::Range(start_expr, end_expr),
1555            start.merge(&end),
1556        ))
1557    }
1558    /// Parse string interpolation: `s!"hello {name}"`
1559    #[allow(dead_code)]
1560    fn parse_string_interp(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1561        let start = self.current().span.clone();
1562        if let TokenKind::String(s) = &self.current().kind {
1563            let s = s.clone();
1564            self.advance();
1565            let part = StringPart::Literal(s);
1566            let end = self.current().span.clone();
1567            Ok(Located::new(
1568                SurfaceExpr::StringInterp(vec![part]),
1569                start.merge(&end),
1570            ))
1571        } else {
1572            Err(ParseError::unexpected(
1573                vec!["string".to_string()],
1574                self.current().kind.clone(),
1575                start,
1576            ))
1577        }
1578    }
1579    /// Parse implicit argument application
1580    #[allow(dead_code)]
1581    fn parse_implicit_app(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1582        let start = self.current().span.clone();
1583        let mut expr = self.parse_primary()?;
1584        loop {
1585            if self.check(&TokenKind::LBrace) {
1586                self.advance();
1587                let arg = self.parse_expr()?;
1588                self.expect(TokenKind::RBrace)?;
1589                let span = start.merge(&arg.span);
1590                expr = Located::new(SurfaceExpr::App(Box::new(expr), Box::new(arg)), span);
1591            } else {
1592                break;
1593            }
1594        }
1595        Ok(expr)
1596    }
1597    /// Parse constructor with named fields: `{ field := value, ... }`
1598    #[allow(dead_code)]
1599    fn parse_named_ctor(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1600        let start = self.current().span.clone();
1601        self.expect(TokenKind::LBrace)?;
1602        let mut fields = Vec::new();
1603        if !self.check(&TokenKind::RBrace) {
1604            loop {
1605                let field_name = self.parse_ident()?;
1606                self.expect(TokenKind::Assign)?;
1607                let field_val = self.parse_expr()?;
1608                fields.push((field_name, field_val));
1609                if !self.consume(TokenKind::Comma) {
1610                    break;
1611                }
1612            }
1613        }
1614        self.expect(TokenKind::RBrace)?;
1615        let end = self.current().span.clone();
1616        let mut result = Located::new(SurfaceExpr::Hole, start.clone());
1617        for (field_name, field_val) in fields {
1618            result = Located::new(
1619                SurfaceExpr::NamedArg(Box::new(result), field_name, Box::new(field_val)),
1620                start.merge(&end),
1621            );
1622        }
1623        Ok(result)
1624    }
1625    /// Attempt error recovery by synchronizing to the next safe token
1626    #[allow(dead_code)]
1627    fn synchronize(&mut self) {
1628        while !self.is_eof() {
1629            match &self.current().kind {
1630                TokenKind::Semicolon | TokenKind::Comma | TokenKind::End => {
1631                    self.advance();
1632                    break;
1633                }
1634                TokenKind::Axiom
1635                | TokenKind::Definition
1636                | TokenKind::Theorem
1637                | TokenKind::Lemma => break,
1638                _ => {
1639                    self.advance();
1640                }
1641            }
1642        }
1643    }
1644    /// Parse optional type annotation after an expression
1645    #[allow(dead_code)]
1646    fn parse_optional_type_ann(&mut self) -> Result<Option<Located<SurfaceExpr>>, ParseError> {
1647        if self.consume(TokenKind::Colon) {
1648            Ok(Some(self.parse_expr()?))
1649        } else {
1650            Ok(None)
1651        }
1652    }
1653    /// Parse an identifier.
1654    fn parse_ident(&mut self) -> Result<String, ParseError> {
1655        if let TokenKind::Ident(name) = &self.current().kind {
1656            let name = name.clone();
1657            self.advance();
1658            Ok(name)
1659        } else {
1660            Err(ParseError::unexpected(
1661                vec!["identifier".to_string()],
1662                self.current().kind.clone(),
1663                self.current().span.clone(),
1664            ))
1665        }
1666    }
1667}
1668/// Associativity of an operator.
1669#[derive(Clone, Copy, Debug, PartialEq, Eq)]
1670enum Assoc {
1671    /// Left-associative
1672    Left,
1673    /// Right-associative
1674    Right,
1675}
oxilean_parse/parser_impl/types.rs

oxilean_parse/parser_impl/
types.rs
