(
&mut self,
root: &KExpr<M>,
root_depth: u64,
lvl_bound: usize,
mut timing: Option<&mut ValidationTiming>,
)
| 498 | } |
| 499 | |
| 500 | fn validate_expr_well_scoped( |
| 501 | &mut self, |
| 502 | root: &KExpr<M>, |
| 503 | root_depth: u64, |
| 504 | lvl_bound: usize, |
| 505 | mut timing: Option<&mut ValidationTiming>, |
| 506 | ) -> Result<(), TcError<M>> { |
| 507 | let mut stack: Vec<(&KExpr<M>, u64)> = vec![(root, root_depth)]; |
| 508 | let mut seen_exprs: FxHashSet<(Addr, u64)> = FxHashSet::default(); |
| 509 | let mut seen_univs: FxHashSet<Addr> = FxHashSet::default(); |
| 510 | while let Some((e, depth)) = stack.pop() { |
| 511 | if !seen_exprs.insert((e.hash_key(), depth)) { |
| 512 | continue; |
| 513 | } |
| 514 | match e.data() { |
| 515 | ExprData::Var(idx, _, _) => { |
| 516 | if *idx >= depth { |
| 517 | let ctx_len = usize::try_from(depth).unwrap_or(usize::MAX); |
| 518 | return Err(TcError::VarOutOfRange { idx: *idx, ctx_len }); |
| 519 | } |
| 520 | }, |
| 521 | ExprData::Sort(u, _) => { |
| 522 | let univ_start = timing.as_ref().map(|_| Instant::now()); |
| 523 | self.validate_univ_params_seen(u, lvl_bound, &mut seen_univs)?; |
| 524 | if let (Some(t), Some(start)) = (timing.as_deref_mut(), univ_start) { |
| 525 | t.univ += start.elapsed(); |
| 526 | } |
| 527 | }, |
| 528 | ExprData::Const(id, us, _) => { |
| 529 | let c = self.get_const(id)?; |
| 530 | if u64_to_usize::<M>(c.lvls())? != us.len() { |
| 531 | return Err(TcError::UnivParamMismatch { |
| 532 | expected: c.lvls(), |
| 533 | got: us.len(), |
| 534 | }); |
| 535 | } |
| 536 | for u in us { |
| 537 | let univ_start = timing.as_ref().map(|_| Instant::now()); |
| 538 | self.validate_univ_params_seen(u, lvl_bound, &mut seen_univs)?; |
| 539 | if let (Some(t), Some(start)) = (timing.as_deref_mut(), univ_start) |
| 540 | { |
| 541 | t.univ += start.elapsed(); |
| 542 | } |
| 543 | } |
| 544 | }, |
| 545 | ExprData::App(f, a, _) => { |
| 546 | stack.push((f, depth)); |
| 547 | stack.push((a, depth)); |
| 548 | }, |
| 549 | ExprData::Lam(_, _, ty, body, _) | ExprData::All(_, _, ty, body, _) => { |
| 550 | stack.push((ty, depth)); |
| 551 | let body_depth = depth.checked_add(1).ok_or_else(|| { |
| 552 | TcError::Other("binder depth overflow during validation".into()) |
| 553 | })?; |
| 554 | stack.push((body, body_depth)); |
| 555 | }, |
| 556 | ExprData::Let(_, ty, val, body, _, _) => { |
| 557 | stack.push((ty, depth)); |
no test coverage detected