3#include <fe/worklist.h>
14 auto queue = fe::BFSWorklist<DefSet>();
15 auto pinned = fe::BFSWorklist<DefSet>();
16 for (
auto mut :
old_world().externals().muts())
19 while (!queue.empty()) {
20 auto def = queue.pop();
25 for (
auto arg : app->arg()->projs())
26 if (
auto lam = arg->isa_mut<
Lam>()) pinned.push(lam);
28 for (
auto d : def->deps())
32 while (!pinned.empty()) {
33 auto def = pinned.pop();
34 if (
auto lam = def->isa_mut<
Lam>()) preserved_.emplace(lam);
35 for (
auto d : def->deps())
49 if (
auto sigma = old_def->
isa_imm<
Sigma>())
return rewrite_imm_Sigma(sigma);
58 tuple && std::ranges::any_of(
tuple->ops(), [](
const Def* op) { return isa_mem(op); }))
69 auto new_pi = Rewriter::rewrite_imm_Pi(pi)->as<
Pi>();
76 auto dom = new_pi->dom();
82 if (
auto [sigma, old_var] = dom->isa_binder<
Sigma>(); sigma) {
83 auto n = sigma->num_ops();
84 auto new_sigma = w.mut_sigma(sigma->type(), n + 1);
85 new_sigma->set(0,
mem);
88 for (
size_t i = 0; i != n; ++i) {
89 auto shift = w.tuple(
DefVec(n, [&](
size_t j) {
return j < i ? new_sigma->var(n + 1, j + 1) :
mem; }));
91 new_sigma->set(i + 1, rw.rewrite(sigma->op(i)));
93 return w.cn(new_sigma);
97 new_dom.emplace_back(
mem);
98 for (
size_t i = 0, e = new_pi->num_doms(); i != e; ++i)
99 new_dom.emplace_back(new_pi->dom(i));
100 return w.cn(new_dom);
106 if (
is_bootstrapping() || preserving_)
return Rewriter::rewrite_mut_Lam(old_lam);
109 if (preserved_.contains(old_lam)) {
110 auto _ = fe::Restore(preserving_,
true);
111 return Rewriter::rewrite_mut_Lam(old_lam);
115 map(old_lam, new_lam);
118 if (
auto n = old_lam->
num_vars(); n != 0) {
119 auto offset = new_lam->num_doms() - old_lam->num_doms();
120 for (
size_t i = 0; i != n; ++i)
127 if (!old_lam->
is_set())
return new_lam;
136 if (
is_bootstrapping() || preserving_ || !curr_mem_)
return Rewriter::rewrite_imm_App(app);
143 auto [_, k] = app->args<2>();
144 return w.app(
rewrite(k), curr_mem_);
151 auto mem = curr_mem_;
155 auto new_pi = new_callee->
type()->isa<
Pi>();
156 if (old_pi && new_pi && new_pi->num_doms() == old_pi->num_doms() + 1) {
158 auto n = old_pi->num_doms();
161 for (
size_t i = 0; i != n; ++i)
162 args[i + 1] = new_arg->proj(n, i);
163 new_arg = w.tuple(
args);
166 auto new_app = w.app(new_callee, new_arg);
167 advance_mem(new_app);
182 auto rank = [](
const Def* op) {
return isa_mem(op) ? 1 : (op->type() &&
Pi::isa_cn(op->type()) ? 2 : 0); };
185 auto n =
tuple->num_ops();
187 for (
int r = 0; r != 3; ++r)
188 for (
size_t i = 0; i != n; ++i)
193void AddMem::advance_mem(
const Def* def) {
194 if (
auto m =
mem_def(def)) curr_mem_ = m;
const Def * callee() const
A (possibly paramterized) Array.
static auto isa(const Def *def)
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.
DbgKey dbg_key() const
Cheap handle for other->set(this->dbg_key()).
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 T * isa_imm() const
const Def * filter() const
Lam * set(Filter filter, const Def *body)
const fe::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)
bool is_bootstrapping() const
Returns whether we are currently bootstrapping (rewriting annexes).
World & new_world()
Create new Defs into this.
World & old_world()
Get old Defs from here.
virtual const Def * rewrite_imm_Seq(const Seq *seq)
virtual const Def * map(const Def *old_def, const Def *new_def)
virtual const Def * rewrite(const Def *)
Data constructor for a Sigma.
VarRewriter(World &world)
Lam * mut_lam(const Pi *pi)
bool analyze() final
Runs the optional pre-analysis on Phase::world, typically to a fixed point, before rewriting begins.
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
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.
fe::Vector< const Def * > DefVec