Parse atomic (primary) expression
(&mut self)
| 517 | |
| 518 | /// Parse atomic (primary) expression |
| 519 | fn parse_atomic_expr(&mut self) -> crate::Result<Expr> { |
| 520 | let token = self.current(); |
| 521 | |
| 522 | match &token.kind { |
| 523 | TokenKind::Ident(name) => { |
| 524 | let name = name.clone(); |
| 525 | let span = token.span; |
| 526 | self.advance(); |
| 527 | Ok(Expr::Ident(Ident::new(name, span))) |
| 528 | } |
| 529 | |
| 530 | TokenKind::Number(n) => { |
| 531 | let n = n.clone(); |
| 532 | let span = token.span; |
| 533 | self.advance(); |
| 534 | let num = n.parse::<u64>().map_err(|_| { |
| 535 | ParseError::new(span, "Invalid number".to_string()) |
| 536 | })?; |
| 537 | Ok(Expr::Lit(LitExpr { |
| 538 | span, |
| 539 | kind: LitKind::Nat(num), |
| 540 | })) |
| 541 | } |
| 542 | |
| 543 | TokenKind::String(s) => { |
| 544 | let s = s.clone(); |
| 545 | let span = token.span; |
| 546 | self.advance(); |
| 547 | Ok(Expr::Lit(LitExpr { |
| 548 | span, |
| 549 | kind: LitKind::String(s), |
| 550 | })) |
| 551 | } |
| 552 | |
| 553 | TokenKind::Underscore => { |
| 554 | let span = token.span; |
| 555 | self.advance(); |
| 556 | Ok(Expr::Hole { span }) |
| 557 | } |
| 558 | |
| 559 | TokenKind::Type => { |
| 560 | let span = token.span; |
| 561 | self.advance(); |
| 562 | Ok(Expr::Universe { |
| 563 | span, |
| 564 | kind: UniverseKind::Type, |
| 565 | }) |
| 566 | } |
| 567 | |
| 568 | TokenKind::Prop => { |
| 569 | let span = token.span; |
| 570 | self.advance(); |
| 571 | Ok(Expr::Universe { |
| 572 | span, |
| 573 | kind: UniverseKind::Prop, |
| 574 | }) |
| 575 | } |
| 576 |
no test coverage detected