| 360 | let result = lift_cached(env, e, shift, cutoff, &mut cache); |
| 361 | env.lift_scratch = cache; |
| 362 | result |
| 363 | } |
| 364 | |
| 365 | fn lift_no_intern<M: KernelMode>( |
| 366 | e: &KExpr<M>, |
| 367 | shift: u64, |
| 368 | cutoff: u64, |
| 369 | ) -> KExpr<M> { |
| 370 | if shift == 0 || e.lbr() <= cutoff { |
| 371 | return e.clone(); |
| 372 | } |
| 373 | |
| 374 | match e.data() { |
| 375 | ExprData::Var(i, name, _) => { |
| 376 | let i = *i; |
| 377 | if i >= cutoff { KExpr::var(i + shift, name.clone()) } else { e.clone() } |
| 378 | }, |
| 379 | |
| 380 | ExprData::App(f, x, _) => { |
| 381 | let f2 = lift_no_intern(f, shift, cutoff); |
| 382 | let x2 = lift_no_intern(x, shift, cutoff); |
| 383 | KExpr::app(f2, x2) |
| 384 | }, |
| 385 | |
| 386 | ExprData::Lam(name, bi, ty, body, _) => { |
| 387 | let ty2 = lift_no_intern(ty, shift, cutoff); |
| 388 | let body2 = lift_no_intern(body, shift, cutoff + 1); |
| 389 | KExpr::lam(name.clone(), bi.clone(), ty2, body2) |
| 390 | }, |
| 391 | |
| 392 | ExprData::All(name, bi, ty, body, _) => { |
| 393 | let ty2 = lift_no_intern(ty, shift, cutoff); |
| 394 | let body2 = lift_no_intern(body, shift, cutoff + 1); |
| 395 | KExpr::all(name.clone(), bi.clone(), ty2, body2) |
| 396 | }, |
| 397 | |
| 398 | ExprData::Let(name, ty, val, body, nd, _) => { |
| 399 | let ty2 = lift_no_intern(ty, shift, cutoff); |
| 400 | let val2 = lift_no_intern(val, shift, cutoff); |
| 401 | let body2 = lift_no_intern(body, shift, cutoff + 1); |
| 402 | KExpr::let_(name.clone(), ty2, val2, body2, *nd) |
| 403 | }, |
| 404 | |
| 405 | ExprData::Prj(id, field, val, _) => { |
| 406 | let val2 = lift_no_intern(val, shift, cutoff); |
| 407 | KExpr::prj(id.clone(), *field, val2) |
| 408 | }, |
| 409 | |
| 410 | ExprData::FVar(..) |
| 411 | | ExprData::Sort(..) |
| 412 | | ExprData::Const(..) |
| 413 | | ExprData::Nat(..) |
| 414 | | ExprData::Str(..) => e.clone(), |
| 415 | } |
| 416 | } |