16 for (
auto mut :
old_world().externals().muts())
19 while (!queue.empty()) {
20 auto def = queue.pop();
22 if (
auto app = def->isa<
App>(); app && app->
axm())
23 for (
auto arg : app->arg()->projs())
24 if (
auto lam = arg->isa_mut<
Lam>()) pinned.push(lam);
26 for (
auto d : def->deps())
30 while (!pinned.empty()) {
31 auto def = pinned.pop();
32 if (
auto lam = def->isa_mut<
Lam>()) preserved_.emplace(lam);
33 for (
auto d : def->deps())
49 auto new_pi = Rewriter::rewrite_imm_Pi(pi)->as<
Pi>();
56 auto dom = new_pi->dom();
62 if (
auto [sigma, old_var] = dom->isa_binder<
Sigma>(); sigma) {
63 auto n = sigma->num_ops();
64 auto new_sigma = w.mut_sigma(sigma->type(), n + 1);
65 new_sigma->set(0,
mem);
68 for (
size_t i = 0; i != n; ++i) {
69 auto shift = w.tuple(
DefVec(n, [&](
size_t j) {
return j < i ? new_sigma->var(n + 1, j + 1) :
mem; }));
71 new_sigma->set(i + 1, rw.rewrite(sigma->op(i)));
73 return w.cn(new_sigma);
77 new_dom.emplace_back(
mem);
78 for (
size_t i = 0, e = new_pi->num_doms(); i != e; ++i)
79 new_dom.emplace_back(new_pi->dom(i));
86 if (
is_bootstrapping() || preserving_)
return Rewriter::rewrite_mut_Lam(old_lam);
89 if (preserved_.contains(old_lam)) {
90 auto _ =
Restore(preserving_,
true);
91 return Rewriter::rewrite_mut_Lam(old_lam);
95 map(old_lam, new_lam);
98 if (
auto n = old_lam->
num_vars(); n != 0) {
99 auto offset = new_lam->num_doms() - old_lam->num_doms();
100 for (
size_t i = 0; i != n; ++i)
107 if (!old_lam->
is_set())
return new_lam;
116 if (
is_bootstrapping() || preserving_ || !curr_mem_)
return Rewriter::rewrite_imm_App(app);
124 auto mem = curr_mem_;
128 auto new_pi = new_callee->
type()->isa<
Pi>();
129 if (old_pi && new_pi && new_pi->num_doms() == old_pi->num_doms() + 1) {
131 auto n = old_pi->num_doms();
134 for (
size_t i = 0; i != n; ++i)
135 args[i + 1] = new_arg->proj(n, i);
136 new_arg = w.tuple(
args);
139 auto new_app = w.app(new_callee, new_arg);
140 advance_mem(new_app);
155 auto rank = [](
const Def* op) {
return isa_mem(op) ? 1 : (op->type() &&
Pi::isa_cn(op->type()) ? 2 : 0); };
158 auto n =
tuple->num_ops();
160 for (
int r = 0; r != 3; ++r)
161 for (
size_t i = 0; i != n; ++i)
166void AddMem::advance_mem(
const Def* def) {
167 if (
auto m =
mem_def(def)) curr_mem_ = m;
const Def * callee() const
bool is_set() const
Yields true if empty or the last op is set.
Def * set(size_t i, const Def *)
Successively set from left to right.
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
const Def * var(nat_t a, nat_t i) noexcept
nat_t num_vars() noexcept
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
const Def * filter() const
Lam * set(Filter filter, const Def *body)
const Vector< std::string > & args()
Command-line arguments passed to this Phase's plugin via -X <plugin>:<arg>.
A dependent function type.
static const Pi * isa_cn(const Def *d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
World & new_world()
Create new Defs into this.
bool is_bootstrapping() const
Returns whether we are currently bootstrapping (rewriting annexes).
void start() override
Actual entry.
World & old_world()
Get old Defs from here.
RAII guard that restores ref to its current value at the end of the scope.
virtual const Def * map(const Def *old_def, const Def *new_def)
virtual const Def * rewrite(const Def *)
Data constructor for a Sigma.
Extends Rewriter for variable substitution.
Lam * mut_lam(const Pi *pi)
const Def * rewrite_imm_Tuple(const Tuple *) override
const Def * rewrite_imm_Pi(const Pi *) override
const Def * rewrite(const Def *) override
const Def * rewrite_mut_Lam(Lam *) override
const Def * rewrite_imm_App(const App *) override
void start() override
Actual entry.
bool has_leading_mem(const Pi *pi)
Does pi already thread memory - a leading mem.M, either directly or grouped as the first component of...
const Def * mem_var(Lam *lam)
Returns the memory argument of a function if it has one.
const Def * mem_def(const Def *def)
Returns the (first) element of type mem.M a from the given tuple.
const App * isa_mem(const Def *def)
If def is a mem.M-typed value, yields its memory type mem.M a; otherwise nullptr.
Vector< const Def * > DefVec