10 if (
auto i = old2new_.find(def); i != old2new_.end())
return i->second;
20 DefVec new_doms, new_vars, new_args;
21 auto skip = old_lam->ret_var() && old_lam->is_closed();
22 auto old_doms = old_lam->doms();
24 for (
auto dom : old_doms.view().rsubspan(skip))
25 if (!dom->isa<
Pi>()) new_doms.emplace_back(dom);
27 if (skip) new_doms.emplace_back(old_lam->doms().back());
28 if (new_doms.size() == old_lam->num_doms())
return def;
30 auto new_lam = old_lam->
stub(
world().cn(new_doms));
32 for (
size_t arg_i = 0, var_i = 0, n = app->num_args() - skip; arg_i != n; ++arg_i) {
33 auto arg = app->arg(arg_i);
34 if (old_lam->dom(arg_i)->isa<
Pi>()) {
35 new_vars.emplace_back(arg);
37 new_vars.emplace_back(new_lam->var(var_i++));
38 new_args.emplace_back(arg);
43 new_vars.emplace_back(new_lam->vars().back());
44 new_args.emplace_back(app->args().back());
47 new_lam->
set(old_lam->reduce(
world().tuple(new_vars)));
48 world().DLOG(
"{} -> {}: {} -> {})", old_lam, new_lam, old_lam->dom(), new_lam->dom());
50 return old2new_[def] =
world().
app(new_lam, new_args);