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            TokenKind::By => self.parse_by_tactic(),
901            _ => Err(ParseError::unexpected(
902                vec!["expression".to_string()],
903                self.current().kind.clone(),
904                start,
905            )),
906        }
907    }
908    /// Parse lambda expression: `fun (x : T) => body`
909    fn parse_lambda(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
910        let start = self.current().span.clone();
911        self.expect(TokenKind::Fun)?;
912        let binders = self.parse_binders()?;
913        self.expect(TokenKind::Arrow)?;
914        let body = self.parse_expr()?;
915        let end = body.span.clone();
916        Ok(Located::new(
917            SurfaceExpr::Lam(binders, Box::new(body)),
918            start.merge(&end),
919        ))
920    }
921    /// Parse Pi type: `forall (x : T), body`
922    fn parse_pi(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
923        let start = self.current().span.clone();
924        self.expect(TokenKind::Forall)?;
925        let binders = self.parse_binders()?;
926        self.expect(TokenKind::Comma)?;
927        let body = self.parse_expr()?;
928        let end = body.span.clone();
929        Ok(Located::new(
930            SurfaceExpr::Pi(binders, Box::new(body)),
931            start.merge(&end),
932        ))
933    }
934    /// Parse existential quantifier: `∃ binders, body` → `Exists (fun binders => body)`
935    fn parse_exists(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
936        let start = self.current().span.clone();
937        self.expect(TokenKind::Exists)?;
938        let binders = self.parse_binders()?;
939        self.expect(TokenKind::Comma)?;
940        let body = self.parse_expr()?;
941        let end = body.span.clone();
942        let span = start.merge(&end);
943        let exists_var = Located::new(SurfaceExpr::Var("Exists".to_string()), span.clone());
944        let lam = Located::new(SurfaceExpr::Lam(binders, Box::new(body)), span.clone());
945        Ok(Located::new(
946            SurfaceExpr::App(Box::new(exists_var), Box::new(lam)),
947            span,
948        ))
949    }
950    /// Parse let expression: `let x : T := val in body`
951    fn parse_let(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
952        let start = self.current().span.clone();
953        self.expect(TokenKind::Let)?;
954        let name = self.parse_ident()?;
955        let ty = if self.consume(TokenKind::Colon) {
956            Some(Box::new(self.parse_expr()?))
957        } else {
958            None
959        };
960        self.expect(TokenKind::Assign)?;
961        let val = self.parse_expr()?;
962        self.expect(TokenKind::In)?;
963        let body = self.parse_expr()?;
964        let end = body.span.clone();
965        Ok(Located::new(
966            SurfaceExpr::Let(name, ty, Box::new(val), Box::new(body)),
967            start.merge(&end),
968        ))
969    }
970    /// Parse if-then-else: `if cond then t else e`
971    fn parse_if(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
972        let start = self.current().span.clone();
973        self.expect(TokenKind::If)?;
974        let cond = self.parse_expr()?;
975        self.expect(TokenKind::Then)?;
976        let then_branch = self.parse_expr()?;
977        self.expect(TokenKind::Else)?;
978        let else_branch = self.parse_expr()?;
979        let end = else_branch.span.clone();
980        Ok(Located::new(
981            SurfaceExpr::If(Box::new(cond), Box::new(then_branch), Box::new(else_branch)),
982            start.merge(&end),
983        ))
984    }
985    /// Parse match expression: `match e with | pat => rhs | ...`
986    fn parse_match(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
987        let start = self.current().span.clone();
988        self.expect(TokenKind::Match)?;
989        let scrutinee = self.parse_expr()?;
990        self.expect(TokenKind::With)?;
991        let mut arms = Vec::new();
992        self.consume(TokenKind::Bar);
993        loop {
994            let pat = self.parse_pattern()?;
995            let guard = if self.check(&TokenKind::If) {
996                self.advance();
997                Some(self.parse_expr_prec(2)?)
998            } else {
999                None
1000            };
1001            self.expect(TokenKind::Arrow)?;
1002            let rhs = self.parse_expr()?;
1003            arms.push(MatchArm {
1004                pattern: pat,
1005                guard,
1006                rhs,
1007            });
1008            if !self.consume(TokenKind::Bar) {
1009                break;
1010            }
1011        }
1012        let end = self.current().span.clone();
1013        Ok(Located::new(
1014            SurfaceExpr::Match(Box::new(scrutinee), arms),
1015            start.merge(&end),
1016        ))
1017    }
1018    /// Parse a pattern for match arms.
1019    fn parse_pattern(&mut self) -> Result<Located<Pattern>, ParseError> {
1020        let start = self.current().span.clone();
1021        match &self.current().kind.clone() {
1022            TokenKind::Underscore => {
1023                self.advance();
1024                Ok(Located::new(Pattern::Wild, start))
1025            }
1026            TokenKind::Nat(n) => {
1027                let n = *n;
1028                self.advance();
1029                Ok(Located::new(Pattern::Lit(Literal::Nat(n)), start))
1030            }
1031            TokenKind::String(s) => {
1032                let s = s.clone();
1033                self.advance();
1034                Ok(Located::new(Pattern::Lit(Literal::String(s)), start))
1035            }
1036            TokenKind::Ident(name) => {
1037                let name = name.clone();
1038                self.advance();
1039                let mut sub_pats = Vec::new();
1040                while self.can_start_pattern() {
1041                    sub_pats.push(self.parse_atomic_pattern()?);
1042                }
1043                if sub_pats.is_empty() {
1044                    Ok(Located::new(Pattern::Var(name), start))
1045                } else {
1046                    let end = sub_pats
1047                        .last()
1048                        .expect("sub_pats non-empty per else branch")
1049                        .span
1050                        .clone();
1051                    Ok(Located::new(
1052                        Pattern::Ctor(name, sub_pats),
1053                        start.merge(&end),
1054                    ))
1055                }
1056            }
1057            TokenKind::LParen => {
1058                self.advance();
1059                let inner = self.parse_pattern()?;
1060                self.expect(TokenKind::RParen)?;
1061                Ok(inner)
1062            }
1063            _ => Err(ParseError::unexpected(
1064                vec!["pattern".to_string()],
1065                self.current().kind.clone(),
1066                start,
1067            )),
1068        }
1069    }
1070    /// Parse an atomic pattern (used as sub-patterns for constructors).
1071    fn parse_atomic_pattern(&mut self) -> Result<Located<Pattern>, ParseError> {
1072        let start = self.current().span.clone();
1073        match &self.current().kind.clone() {
1074            TokenKind::Underscore => {
1075                self.advance();
1076                Ok(Located::new(Pattern::Wild, start))
1077            }
1078            TokenKind::Nat(n) => {
1079                let n = *n;
1080                self.advance();
1081                Ok(Located::new(Pattern::Lit(Literal::Nat(n)), start))
1082            }
1083            TokenKind::String(s) => {
1084                let s = s.clone();
1085                self.advance();
1086                Ok(Located::new(Pattern::Lit(Literal::String(s)), start))
1087            }
1088            TokenKind::Ident(name) => {
1089                let name = name.clone();
1090                self.advance();
1091                Ok(Located::new(Pattern::Var(name), start))
1092            }
1093            TokenKind::LParen => {
1094                self.advance();
1095                let inner = self.parse_pattern()?;
1096                self.expect(TokenKind::RParen)?;
1097                Ok(inner)
1098            }
1099            _ => Err(ParseError::unexpected(
1100                vec!["pattern".to_string()],
1101                self.current().kind.clone(),
1102                start,
1103            )),
1104        }
1105    }
1106    /// Check if current token can start a pattern.
1107    fn can_start_pattern(&self) -> bool {
1108        matches!(
1109            self.current().kind,
1110            TokenKind::Ident(_)
1111                | TokenKind::Nat(_)
1112                | TokenKind::String(_)
1113                | TokenKind::Underscore
1114                | TokenKind::LParen
1115        )
1116    }
1117    /// Parse do notation: `do { action1; action2; ... }` or `do action1; action2`
1118    fn parse_do(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1119        let start = self.current().span.clone();
1120        self.expect(TokenKind::Do)?;
1121        let has_brace = self.consume(TokenKind::LBrace);
1122        let mut actions = Vec::new();
1123        loop {
1124            if has_brace && self.check(&TokenKind::RBrace) {
1125                break;
1126            }
1127            if self.is_eof() {
1128                break;
1129            }
1130            let action = self.parse_do_action()?;
1131            actions.push(action);
1132            if !self.consume(TokenKind::Semicolon) {
1133                break;
1134            }
1135        }
1136        if has_brace {
1137            self.expect(TokenKind::RBrace)?;
1138        }
1139        let end = self.current().span.clone();
1140        Ok(Located::new(SurfaceExpr::Do(actions), start.merge(&end)))
1141    }
1142    /// Parse a single do-notation action.
1143    fn parse_do_action(&mut self) -> Result<DoAction, ParseError> {
1144        if self.check(&TokenKind::Let) {
1145            self.advance();
1146            let name = self.parse_ident()?;
1147            if self.consume(TokenKind::Colon) {
1148                let ty = self.parse_expr()?;
1149                self.expect(TokenKind::Assign)?;
1150                let val = self.parse_expr()?;
1151                return Ok(DoAction::LetTyped(name, ty, val));
1152            }
1153            self.expect(TokenKind::Assign)?;
1154            let val = self.parse_expr()?;
1155            return Ok(DoAction::Let(name, val));
1156        }
1157        if let TokenKind::Ident(_) = &self.current().kind {
1158            if self.peek().kind == TokenKind::LeftArrow {
1159                let name = self.parse_ident()?;
1160                self.expect(TokenKind::LeftArrow)?;
1161                let val = self.parse_expr()?;
1162                return Ok(DoAction::Bind(name, val));
1163            }
1164        }
1165        let expr = self.parse_expr()?;
1166        Ok(DoAction::Expr(expr))
1167    }
1168    /// Parse have expression: `have h : T := proof; body`
1169    fn parse_have(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1170        let start = self.current().span.clone();
1171        self.expect(TokenKind::Have)?;
1172        let name = self.parse_ident()?;
1173        self.expect(TokenKind::Colon)?;
1174        let ty = self.parse_expr()?;
1175        self.expect(TokenKind::Assign)?;
1176        let proof = self.parse_expr()?;
1177        self.expect(TokenKind::Semicolon)?;
1178        let body = self.parse_expr()?;
1179        let end = body.span.clone();
1180        Ok(Located::new(
1181            SurfaceExpr::Have(name, Box::new(ty), Box::new(proof), Box::new(body)),
1182            start.merge(&end),
1183        ))
1184    }
1185    /// Parse suffices expression: `suffices h : T by tactic; body`
1186    fn parse_suffices(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1187        let start = self.current().span.clone();
1188        self.expect(TokenKind::Suffices)?;
1189        let name = self.parse_ident()?;
1190        self.expect(TokenKind::Colon)?;
1191        let ty = self.parse_expr()?;
1192        self.expect(TokenKind::By)?;
1193        let tactic = self.parse_expr()?;
1194        let end = tactic.span.clone();
1195        Ok(Located::new(
1196            SurfaceExpr::Suffices(name, Box::new(ty), Box::new(tactic)),
1197            start.merge(&end),
1198        ))
1199    }
1200    /// Parse show expression: `show T from expr`
1201    fn parse_show(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1202        let start = self.current().span.clone();
1203        self.expect(TokenKind::Show)?;
1204        let ty = self.parse_expr()?;
1205        self.expect(TokenKind::From)?;
1206        let proof = self.parse_expr()?;
1207        let end = proof.span.clone();
1208        Ok(Located::new(
1209            SurfaceExpr::Show(Box::new(ty), Box::new(proof)),
1210            start.merge(&end),
1211        ))
1212    }
1213    /// Parse parenthesized expression, tuple, or type annotation.
1214    ///
1215    /// `(e)` -- grouping
1216    /// `(e : T)` -- type annotation
1217    /// `(e, f, ...)` -- tuple
1218    fn parse_paren_or_tuple(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1219        let start = self.current().span.clone();
1220        self.expect(TokenKind::LParen)?;
1221        if self.consume(TokenKind::RParen) {
1222            return Ok(Located::new(SurfaceExpr::Tuple(vec![]), start));
1223        }
1224        let first = self.parse_expr()?;
1225        if self.consume(TokenKind::Colon) {
1226            let ty = self.parse_expr()?;
1227            let span = start.merge(&ty.span);
1228            self.expect(TokenKind::RParen)?;
1229            return Ok(Located::new(
1230                SurfaceExpr::Ann(Box::new(first), Box::new(ty)),
1231                span,
1232            ));
1233        }
1234        if self.consume(TokenKind::Comma) {
1235            let mut elems = vec![first];
1236            elems.push(self.parse_expr()?);
1237            while self.consume(TokenKind::Comma) {
1238                elems.push(self.parse_expr()?);
1239            }
1240            self.expect(TokenKind::RParen)?;
1241            let end = self.current().span.clone();
1242            return Ok(Located::new(SurfaceExpr::Tuple(elems), start.merge(&end)));
1243        }
1244        self.expect(TokenKind::RParen)?;
1245        Ok(first)
1246    }
1247    /// Parse list literal: `[e1, e2, ...]` or `[]`
1248    fn parse_list_literal(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1249        let start = self.current().span.clone();
1250        self.expect(TokenKind::LBracket)?;
1251        let mut elems = Vec::new();
1252        if !self.check(&TokenKind::RBracket) {
1253            elems.push(self.parse_expr()?);
1254            while self.consume(TokenKind::Comma) {
1255                elems.push(self.parse_expr()?);
1256            }
1257        }
1258        self.expect(TokenKind::RBracket)?;
1259        let end = self.current().span.clone();
1260        Ok(Located::new(SurfaceExpr::ListLit(elems), start.merge(&end)))
1261    }
1262    /// Parse anonymous constructor: `(langle) a, b, c (rangle)`
1263    fn parse_anonymous_ctor(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1264        let start = self.current().span.clone();
1265        self.expect(TokenKind::LAngle)?;
1266        let mut elems = Vec::new();
1267        if !self.check(&TokenKind::RAngle) {
1268            elems.push(self.parse_expr()?);
1269            while self.consume(TokenKind::Comma) {
1270                elems.push(self.parse_expr()?);
1271            }
1272        }
1273        self.expect(TokenKind::RAngle)?;
1274        let end = self.current().span.clone();
1275        Ok(Located::new(
1276            SurfaceExpr::AnonymousCtor(elems),
1277            start.merge(&end),
1278        ))
1279    }
1280}
1281impl Parser {
1282    /// Parse binders for lambda, forall, variable declarations.
1283    ///
1284    /// Supports:
1285    /// - `(x : T)` -- explicit
1286    /// - `{x : T}` -- implicit
1287    /// - `[x : T]` -- instance
1288    /// - `{{x : T}}` -- strict implicit
1289    /// - `x` -- simple binder without type
1290    /// - Multiple binder groups
1291    pub fn parse_binders(&mut self) -> Result<Vec<Binder>, ParseError> {
1292        let mut binders = Vec::new();
1293        loop {
1294            match &self.current().kind {
1295                TokenKind::LParen => {
1296                    self.advance();
1297                    self.parse_binder_group(&mut binders, BinderKind::Default)?;
1298                    self.expect(TokenKind::RParen)?;
1299                }
1300                TokenKind::LBrace => {
1301                    if self.peek().kind == TokenKind::LBrace {
1302                        self.advance();
1303                        self.advance();
1304                        self.parse_binder_group(&mut binders, BinderKind::StrictImplicit)?;
1305                        self.expect(TokenKind::RBrace)?;
1306                        self.expect(TokenKind::RBrace)?;
1307                    } else {
1308                        self.advance();
1309                        self.parse_binder_group(&mut binders, BinderKind::Implicit)?;
1310                        self.expect(TokenKind::RBrace)?;
1311                    }
1312                }
1313                TokenKind::LBracket => {
1314                    self.advance();
1315                    self.parse_binder_group(&mut binders, BinderKind::Instance)?;
1316                    self.expect(TokenKind::RBracket)?;
1317                }
1318                TokenKind::Ident(_) | TokenKind::Underscore => {
1319                    let name = if self.check(&TokenKind::Underscore) {
1320                        self.advance();
1321                        "_".to_string()
1322                    } else {
1323                        self.parse_ident()?
1324                    };
1325                    binders.push(Binder {
1326                        name,
1327                        ty: None,
1328                        info: BinderKind::Default,
1329                    });
1330                }
1331                _ => break,
1332            }
1333            if !matches!(
1334                self.current().kind,
1335                TokenKind::LParen
1336                    | TokenKind::LBrace
1337                    | TokenKind::LBracket
1338                    | TokenKind::Ident(_)
1339                    | TokenKind::Underscore
1340            ) {
1341                break;
1342            }
1343        }
1344        Ok(binders)
1345    }
1346    /// Parse a binder group inside delimiters: `x y : T` or `x : T, y : T`
1347    fn parse_binder_group(
1348        &mut self,
1349        binders: &mut Vec<Binder>,
1350        kind: BinderKind,
1351    ) -> Result<(), ParseError> {
1352        let mut names = Vec::new();
1353        loop {
1354            let name = if self.check(&TokenKind::Underscore) {
1355                self.advance();
1356                "_".to_string()
1357            } else if let TokenKind::Ident(_) = &self.current().kind {
1358                self.parse_ident()?
1359            } else {
1360                break;
1361            };
1362            names.push(name);
1363            if self.check(&TokenKind::Colon) {
1364                break;
1365            }
1366            if self.check(&TokenKind::Comma) {
1367                break;
1368            }
1369        }
1370        if names.is_empty() {
1371            return Err(ParseError::unexpected(
1372                vec!["identifier".to_string()],
1373                self.current().kind.clone(),
1374                self.current().span.clone(),
1375            ));
1376        }
1377        let ty = if self.consume(TokenKind::Colon) {
1378            Some(self.parse_expr()?)
1379        } else {
1380            None
1381        };
1382        for name in names {
1383            binders.push(Binder {
1384                name,
1385                ty: ty.as_ref().map(|t| Box::new(t.clone())),
1386                info: kind.clone(),
1387            });
1388        }
1389        while self.consume(TokenKind::Comma) {
1390            let name = if self.check(&TokenKind::Underscore) {
1391                self.advance();
1392                "_".to_string()
1393            } else {
1394                self.parse_ident()?
1395            };
1396            let more_ty = if self.consume(TokenKind::Colon) {
1397                Some(Box::new(self.parse_expr()?))
1398            } else {
1399                None
1400            };
1401            binders.push(Binder {
1402                name,
1403                ty: more_ty,
1404                info: kind.clone(),
1405            });
1406        }
1407        Ok(())
1408    }
1409}
1410impl Parser {
1411    /// Parse where clauses for definitions and theorems.
1412    #[allow(dead_code)]
1413    fn parse_where_clauses(&mut self) -> Result<Vec<WhereClause>, ParseError> {
1414        let mut clauses = Vec::new();
1415        if !self.check_ident("where") {
1416            return Ok(clauses);
1417        }
1418        self.advance();
1419        loop {
1420            if self.is_eof() || self.is_decl_start() {
1421                break;
1422            }
1423            let name = self.parse_ident()?;
1424            let params = self.parse_binders()?;
1425            let ty = if self.consume(TokenKind::Colon) {
1426                Some(self.parse_expr()?)
1427            } else {
1428                None
1429            };
1430            self.expect(TokenKind::Assign)?;
1431            let val = self.parse_expr()?;
1432            clauses.push(WhereClause {
1433                name,
1434                params,
1435                ty,
1436                val,
1437            });
1438            if !self.consume(TokenKind::Comma) {
1439                break;
1440            }
1441        }
1442        Ok(clauses)
1443    }
1444    /// Parse calc expression: `calc x = y := proof1 _ = z := proof2`
1445    #[allow(dead_code)]
1446    fn parse_calc(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1447        let start = self.current().span.clone();
1448        if !self.check_ident("calc") {
1449            return Err(ParseError::unexpected(
1450                vec!["calc".to_string()],
1451                self.current().kind.clone(),
1452                start,
1453            ));
1454        }
1455        self.advance();
1456        let mut steps = Vec::new();
1457        let lhs = self.parse_expr()?;
1458        let rel = self.parse_ident()?;
1459        let rhs = self.parse_expr()?;
1460        self.expect(TokenKind::Assign)?;
1461        let proof = self.parse_expr()?;
1462        steps.push(CalcStep {
1463            lhs,
1464            rel,
1465            rhs,
1466            proof,
1467        });
1468        while self.consume(TokenKind::Underscore) {
1469            let rel = self.parse_ident()?;
1470            let rhs = self.parse_expr()?;
1471            self.expect(TokenKind::Assign)?;
1472            let proof = self.parse_expr()?;
1473            let prev_rhs = steps
1474                .last()
1475                .expect("steps non-empty: first step pushed before loop")
1476                .rhs
1477                .clone();
1478            steps.push(CalcStep {
1479                lhs: prev_rhs,
1480                rel,
1481                rhs,
1482                proof,
1483            });
1484        }
1485        let end = self.current().span.clone();
1486        Ok(Located::new(SurfaceExpr::Calc(steps), start.merge(&end)))
1487    }
1488    /// Parse by-tactic expression: `by simp; ring`
1489    #[allow(dead_code)]
1490    fn parse_by_tactic(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1491        let start = self.current().span.clone();
1492        self.expect(TokenKind::By)?;
1493        let mut tactics = Vec::new();
1494        loop {
1495            if self.is_eof() || self.is_stop_token() {
1496                break;
1497            }
1498            let tactic_name = self.parse_ident()?;
1499            let span = self.current().span.clone();
1500            tactics.push(Located::new(tactic_name, span));
1501            if !self.consume(TokenKind::Semicolon) {
1502                break;
1503            }
1504        }
1505        let end = self.current().span.clone();
1506        Ok(Located::new(
1507            SurfaceExpr::ByTactic(tactics),
1508            start.merge(&end),
1509        ))
1510    }
1511    /// Parse return expression (for do notation): `return e`
1512    #[allow(dead_code)]
1513    fn parse_return(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1514        let start = self.current().span.clone();
1515        if !self.check_ident("return") {
1516            return Err(ParseError::unexpected(
1517                vec!["return".to_string()],
1518                self.current().kind.clone(),
1519                start,
1520            ));
1521        }
1522        self.advance();
1523        let val = self.parse_expr()?;
1524        let end = val.span.clone();
1525        Ok(Located::new(
1526            SurfaceExpr::Return(Box::new(val)),
1527            start.merge(&end),
1528        ))
1529    }
1530    /// Parse range expression: `a..b`, `..b`, `a..`
1531    #[allow(dead_code)]
1532    fn parse_range(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1533        let start = self.current().span.clone();
1534        let start_expr = if self.check(&TokenKind::Dot) && self.peek().kind == TokenKind::Dot {
1535            None
1536        } else {
1537            Some(Box::new(self.parse_expr()?))
1538        };
1539        if !self.check(&TokenKind::Dot) || self.peek().kind != TokenKind::Dot {
1540            return Err(ParseError::unexpected(
1541                vec!["..".to_string()],
1542                self.current().kind.clone(),
1543                self.current().span.clone(),
1544            ));
1545        }
1546        self.advance();
1547        self.advance();
1548        let end_expr = if self.is_stop_token() {
1549            None
1550        } else {
1551            Some(Box::new(self.parse_expr()?))
1552        };
1553        let end = self.current().span.clone();
1554        Ok(Located::new(
1555            SurfaceExpr::Range(start_expr, end_expr),
1556            start.merge(&end),
1557        ))
1558    }
1559    /// Parse string interpolation: `s!"hello {name}"`
1560    #[allow(dead_code)]
1561    fn parse_string_interp(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1562        let start = self.current().span.clone();
1563        if let TokenKind::String(s) = &self.current().kind {
1564            let s = s.clone();
1565            self.advance();
1566            let part = StringPart::Literal(s);
1567            let end = self.current().span.clone();
1568            Ok(Located::new(
1569                SurfaceExpr::StringInterp(vec![part]),
1570                start.merge(&end),
1571            ))
1572        } else {
1573            Err(ParseError::unexpected(
1574                vec!["string".to_string()],
1575                self.current().kind.clone(),
1576                start,
1577            ))
1578        }
1579    }
1580    /// Parse implicit argument application
1581    #[allow(dead_code)]
1582    fn parse_implicit_app(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1583        let start = self.current().span.clone();
1584        let mut expr = self.parse_primary()?;
1585        loop {
1586            if self.check(&TokenKind::LBrace) {
1587                self.advance();
1588                let arg = self.parse_expr()?;
1589                self.expect(TokenKind::RBrace)?;
1590                let span = start.merge(&arg.span);
1591                expr = Located::new(SurfaceExpr::App(Box::new(expr), Box::new(arg)), span);
1592            } else {
1593                break;
1594            }
1595        }
1596        Ok(expr)
1597    }
1598    /// Parse constructor with named fields: `{ field := value, ... }`
1599    #[allow(dead_code)]
1600    fn parse_named_ctor(&mut self) -> Result<Located<SurfaceExpr>, ParseError> {
1601        let start = self.current().span.clone();
1602        self.expect(TokenKind::LBrace)?;
1603        let mut fields = Vec::new();
1604        if !self.check(&TokenKind::RBrace) {
1605            loop {
1606                let field_name = self.parse_ident()?;
1607                self.expect(TokenKind::Assign)?;
1608                let field_val = self.parse_expr()?;
1609                fields.push((field_name, field_val));
1610                if !self.consume(TokenKind::Comma) {
1611                    break;
1612                }
1613            }
1614        }
1615        self.expect(TokenKind::RBrace)?;
1616        let end = self.current().span.clone();
1617        let mut result = Located::new(SurfaceExpr::Hole, start.clone());
1618        for (field_name, field_val) in fields {
1619            result = Located::new(
1620                SurfaceExpr::NamedArg(Box::new(result), field_name, Box::new(field_val)),
1621                start.merge(&end),
1622            );
1623        }
1624        Ok(result)
1625    }
1626    /// Attempt error recovery by synchronizing to the next safe token
1627    #[allow(dead_code)]
1628    fn synchronize(&mut self) {
1629        while !self.is_eof() {
1630            match &self.current().kind {
1631                TokenKind::Semicolon | TokenKind::Comma | TokenKind::End => {
1632                    self.advance();
1633                    break;
1634                }
1635                TokenKind::Axiom
1636                | TokenKind::Definition
1637                | TokenKind::Theorem
1638                | TokenKind::Lemma => break,
1639                _ => {
1640                    self.advance();
1641                }
1642            }
1643        }
1644    }
1645    /// Parse optional type annotation after an expression
1646    #[allow(dead_code)]
1647    fn parse_optional_type_ann(&mut self) -> Result<Option<Located<SurfaceExpr>>, ParseError> {
1648        if self.consume(TokenKind::Colon) {
1649            Ok(Some(self.parse_expr()?))
1650        } else {
1651            Ok(None)
1652        }
1653    }
1654    /// Parse an identifier.
1655    fn parse_ident(&mut self) -> Result<String, ParseError> {
1656        if let TokenKind::Ident(name) = &self.current().kind {
1657            let name = name.clone();
1658            self.advance();
1659            Ok(name)
1660        } else {
1661            Err(ParseError::unexpected(
1662                vec!["identifier".to_string()],
1663                self.current().kind.clone(),
1664                self.current().span.clone(),
1665            ))
1666        }
1667    }
1668}
1669/// Associativity of an operator.
1670#[derive(Clone, Copy, Debug, PartialEq, Eq)]
1671enum Assoc {
1672    /// Left-associative
1673    Left,
1674    /// Right-associative
1675    Right,
1676}
oxilean_parse/parser_impl/types.rs

oxilean_parse/parser_impl/
types.rs
