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