Validate quotient constant structure. Checks: - Correct address matches the expected QuotKind - Correct universe parameter count per variant - Eq type exists with correct shape (1 universe param, 1 ctor Eq.refl)
(
&mut self,
id: &KId<M>,
kind: QuotKind,
lvls: u64,
ty: &KExpr<M>,
)
| 610 | classify_elapsed.unwrap_or_default(), |
| 611 | body_elapsed.unwrap_or_default(), |
| 612 | ); |
| 613 | } |
| 614 | |
| 615 | result |
| 616 | } |
| 617 | |
| 618 | // ----------------------------------------------------------------------- |
| 619 | // #5: Quotient type validation |
| 620 | // ----------------------------------------------------------------------- |
| 621 | |
| 622 | /// Validate declaration expressions before inference. |
| 623 | /// |
| 624 | /// This is the Ix equivalent of Lean's declaration-admission closure and |
| 625 | /// universe-param checks: declarations must be closed at the top level, and |
| 626 | /// every `Param(idx)` in their type/value/rules must refer to one of the |
| 627 | /// declaration's own universe parameters. |
| 628 | pub(crate) fn validate_const_well_scoped( |
| 629 | &mut self, |
| 630 | c: &KConst<M>, |
| 631 | ) -> Result<(), TcError<M>> { |
| 632 | self.validate_const_well_scoped_timed(c, None) |
| 633 | } |
| 634 | |
| 635 | fn validate_const_well_scoped_timed( |
| 636 | &mut self, |
| 637 | c: &KConst<M>, |
| 638 | mut timing: Option<&mut ValidationTiming>, |
| 639 | ) -> Result<(), TcError<M>> { |
| 640 | let lvl_bound = u64_to_usize::<M>(c.lvls())?; |
| 641 | let ty_start = timing.as_ref().map(|_| Instant::now()); |
| 642 | self.validate_expr_well_scoped( |
| 643 | c.ty(), |
| 644 | 0, |
| 645 | lvl_bound, |
| 646 | timing.as_deref_mut(), |
| 647 | )?; |
| 648 | if let (Some(t), Some(start)) = (timing.as_deref_mut(), ty_start) { |
| 649 | t.ty += start.elapsed(); |
| 650 | } |
| 651 | match c { |
| 652 | KConst::Defn { val, .. } => { |
| 653 | let val_start = timing.as_ref().map(|_| Instant::now()); |
| 654 | self.validate_expr_well_scoped( |
| 655 | val, |
| 656 | 0, |
| 657 | lvl_bound, |
| 658 | timing.as_deref_mut(), |
| 659 | )?; |
| 660 | if let (Some(t), Some(start)) = (timing.as_deref_mut(), val_start) { |
| 661 | t.val += start.elapsed(); |
| 662 | } |
| 663 | }, |
| 664 | KConst::Recr { rules, .. } => { |
| 665 | let rules_start = timing.as_ref().map(|_| Instant::now()); |
| 666 | for rule in rules { |
| 667 | self.validate_expr_well_scoped( |
| 668 | &rule.rhs, |
| 669 | 0, |
no test coverage detected