| 413 | let body2 = lift_no_intern(body, shift, cutoff + 1); |
| 414 | KExpr::let_(name.clone(), ty2, val2, body2, *nd) |
| 415 | }, |
| 416 | |
| 417 | ExprData::Prj(id, field, val, _) => { |
| 418 | let val2 = lift_no_intern(val, shift, cutoff); |
| 419 | KExpr::prj(id.clone(), *field, val2) |
| 420 | }, |
| 421 | |
| 422 | ExprData::FVar(..) |
| 423 | | ExprData::Sort(..) |
| 424 | | ExprData::Const(..) |
| 425 | | ExprData::Nat(..) |
| 426 | | ExprData::Str(..) => e.clone(), |
| 427 | } |
| 428 | } |
| 429 | |
| 430 | fn lift_cached<M: KernelMode>( |
| 431 | env: &mut InternTable<M>, |
| 432 | e: &KExpr<M>, |
| 433 | shift: u64, |
| 434 | cutoff: u64, |
| 435 | cache: &mut FxHashMap<(Addr, u64), KExpr<M>>, |
| 436 | ) -> KExpr<M> { |
| 437 | if shift == 0 || e.lbr() <= cutoff { |
| 438 | return e.clone(); |
| 439 | } |
| 440 | |
| 441 | // `shift` is fixed across a single call, so only `(addr, cutoff)` is |
| 442 | // needed to identify a unique traversal result. |
| 443 | let key = (e.hash_key(), cutoff); |
| 444 | if let Some(cached) = cache.get(&key) { |
| 445 | return cached.clone(); |
| 446 | } |
| 447 | |
| 448 | let result = match e.data() { |
| 449 | ExprData::Var(i, name, _) => { |
| 450 | let i = *i; |
| 451 | if i >= cutoff { |
| 452 | KExpr::var(i + shift, name.clone()) |
| 453 | } else { |
| 454 | let r = e.clone(); |
| 455 | cache.insert(key, r.clone()); |
| 456 | return r; |
| 457 | } |
| 458 | }, |
| 459 | |
| 460 | ExprData::App(f, x, _) => { |
| 461 | let f2 = lift_cached(env, f, shift, cutoff, cache); |
| 462 | let x2 = lift_cached(env, x, shift, cutoff, cache); |
| 463 | let r = env.intern_app(&f2, &x2); |
| 464 | cache.insert(key, r.clone()); |
| 465 | return r; |
| 466 | }, |
| 467 | |
| 468 | ExprData::Lam(name, bi, ty, body, _) => { |
| 469 | let ty2 = lift_cached(env, ty, shift, cutoff, cache); |
| 470 | let body2 = lift_cached(env, body, shift, cutoff + 1, cache); |
| 471 | KExpr::lam(name.clone(), bi.clone(), ty2, body2) |
| 472 | }, |