25 auto n = app->num_targs();
26 if (n == 0)
return app;
28 auto [it, _] = lam2info_.emplace(var_lam, std::tuple(Lattices(n), (
Lam*)
nullptr,
DefVec(n)));
29 auto& [lattice, prop_lam, old_args] = it->second;
32 if (std::ranges::all_of(lattice, [](
auto l) {
return l == Lattice::Keep; }))
return app;
34 DefVec new_args, new_doms, appxy_ops = {var_lam};
35 auto& args =
data(var_lam);
38 for (
size_t i = 0; i != n; ++i) {
40 case Lattice::Dead:
break;
43 DLOG(
"found proxy within app: {}@{} - wait till proxy is gone", var_lam, app);
45 }
else if (args[i] ==
nullptr) {
46 args[i] = app->arg(n, i);
47 }
else if (args[i] != app->arg(n, i)) {
48 appxy_ops.emplace_back(
world().lit_nat(i));
50 assert(args[i] == app->arg(n, i));
54 new_doms.emplace_back(var_lam->var(n, i)->type());
55 new_args.emplace_back(app->arg(n, i));
57 default: fe::unreachable();
61 DLOG(
"app->args(): {, }", app->args());
62 DLOG(
"args: {, }", args);
63 DLOG(
"new_args: {, }", new_args);
65 if (appxy_ops.size() > 1) {
66 auto appxy =
proxy(app->type(), appxy_ops, Appxy);
67 DLOG(
"appxy: '{}': {, }", appxy, appxy_ops);
71 assert(new_args.size() < n);
72 if (prop_lam ==
nullptr || !std::ranges::equal(old_args, args)) {
75 auto new_pi =
world().
pi(prop_dom, var_lam->codom());
76 prop_lam = var_lam->
stub(new_pi);
78 DLOG(
"new prop_lam: {}", prop_lam);
79 if (beta_red_) beta_red_->keep(prop_lam);
80 if (eta_exp_) eta_exp_->new2old(prop_lam, var_lam);
83 auto new_vars =
DefVec(n, [&, prop_lam = prop_lam](
size_t i) ->
const Def* {
85 case Lattice::Dead:
return proxy(var_lam->var(n, i)->type(), {var_lam, world().lit_nat(i)}, Varxy);
86 case Lattice::Prop:
return args[i];
87 case Lattice::Keep:
return prop_lam->var(j++);
88 default: fe::unreachable();
92 prop_lam->set(var_lam->reduce(
world().
tuple(new_vars)));
95 DLOG(
"var_lam => prop_lam: {}: {} => {}: {}", var_lam, var_lam->dom(), prop_lam, prop_lam->dom());
96 auto res = app->world().app(prop_lam, new_args);
100 lam2info_.insert_or_assign(key, std::tuple(Lattices(new_doms.size(), Lattice::Keep), (
Lam*)
nullptr,
DefVec()));