14const Def* merge_s(World& w,
const Def* elem,
const Def* sigma,
const Def* mem) {
16 auto elems = sigma->projs();
19 return w.sigma({elem, sigma});
22const Def* merge_t(World& w,
const Def* elem,
const Def* tuple,
const Def* mem) {
24 auto elems = tuple->projs();
27 return w.tuple({elem, tuple});
30const Def* eta_expand(World& w,
const Def* f) {
32 eta->app(
false, f, eta->var());
39 if (
auto i = rewritten_.find(def); i != rewritten_.end())
return i->second;
42 world().DLOG(
"rewriting for axm: {} within {}", for_ax,
curr_mut());
43 auto [begin, end, step, init, body, exit] = for_ax->args<6>();
45 auto body_lam = body->isa_mut<
Lam>();
47 if (!body_lam) body = eta_expand(
world(), body);
48 if (!exit_lam) exit = eta_expand(
world(), exit);
52 auto phis = head_lam->
vars();
53 auto iter = phis.front();
54 auto acc =
world().
tuple(phis.view().subspan(1));
63 head_lam->branch(
false, cmp, new_body, new_exit,
mem);
64 new_yield->app(
false, head_lam, merge_t(
world(), new_iter, new_yield->
var(),
mem));
65 new_body->
set(body->reduce(
world().
tuple({iter, acc, new_yield})));
66 new_exit->
set(exit->reduce(acc));
68 return rewritten_[def] =
world().
app(head_lam, merge_t(
world(), begin, init,
mem));
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.
Lam * set(Filter filter, const Def *body)
static const Pi * isa_cn(const Def *d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
const Type * type(const Def *level)
const Def * sigma(Defs ops)
const Def * app(const Def *callee, const Def *arg)
const Def * tuple(Defs ops)
const Def * var(const Def *type, Def *mut)
const Def * call(Id id, Args &&... args)
Complete curried call of annexes obeying implicits.
Lam * mut_con(const Def *dom)
const Def * rewrite(const Def *) override
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 from the given tuple.
const Def * merge_sigma(const Def *def, Defs defs)
const Def * merge_tuple(const Def *def, Defs defs)