14const Def* merge_s(
const Def* elem,
const Def* sigma,
const Def* mem) {
15 auto&
w = elem->world();
17 auto elems = sigma->projs();
20 return w.sigma({elem, sigma});
23const Def* merge_t(
const Def* elem,
const Def* tuple,
const Def* mem) {
24 auto&
w = elem->world();
26 auto elems = tuple->projs();
29 return w.tuple({elem, tuple});
38 DLOG(
"rewriting for axm: `{}`", for_ax);
39 auto [old_body, old_exit, args] = for_ax->uncurry_args<3>();
40 auto [new_begin, new_end, new_step, new_init] = args->projs<4>([
this](
const Def* def) {
return rewrite(def); });
42 auto old_body_lam = old_body->isa_mut<
Lam>();
48 auto new_head_lam =
new_world().
mut_con(merge_s(new_begin->type(), new_init->type(), new_mem))->
set(
"head");
49 auto new_phis = new_head_lam->
vars();
50 auto new_iter = new_phis.front();
61 new_head_lam->branch(
false, new_cmp, new_body, new_exit, new_mem);
62 new_yield->app(
false, new_head_lam, merge_t(new_inc, new_yield->var(), new_mem));
65 map(old_body_lam->var(), {new_iter, new_acc, new_yield});
66 new_body->set({
rewrite(old_body_lam->filter()),
rewrite(old_body_lam->body())});
70 map(old_exit_lam->
var(), new_acc);
74 return new_world().
app(new_head_lam, merge_t(new_begin, new_init, new_mem));
77 return Rewriter::rewrite_imm_App(app);
static auto isa(const Def *def)
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
const Def * filter() const
Lam * set(Filter filter, const Def *body)
static Lam * eta_expand(Filter, const Def *f)
World & new_world()
Create new Defs into this.
bool is_bootstrapping() const
Returns whether we are currently bootstrapping (rewriting annexes).
virtual const Def * map(const Def *old_def, const Def *new_def)
virtual const Def * rewrite(const Def *)
const Def * sigma(Defs ops)
const Def * app(const Def *callee, const Def *arg)
const Def * tuple(Defs ops)
const Def * call(const Def *callee, T &&arg, Args &&... args)
Lam * mut_con(const Def *dom)
const Def * rewrite_imm_App(const App *) final
#define DLOG(...)
Vaporizes to nothingness in Debug build.
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 Def * cat_tuple(nat_t n, nat_t m, const Def *a, const Def *b)
const Def * cat_sigma(nat_t n, nat_t m, const Def *a, const Def *b)
auto elems(std::ostream &os, const auto &range)
Wrap all elements in range through os << T(elem).