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});
33 if (
auto i = rewritten_.find(def); i != rewritten_.end())
return i->second;
36 world().DLOG(
"rewriting for axiom: {} within {}", for_ax,
curr_mut());
37 auto [begin, end, step, init, body, exit] = for_ax->args<6>();
39 auto body_lam = body->isa_mut<
Lam>();
41 if (!body_lam || !exit_lam)
return def;
45 auto phis = head_lam->
vars();
46 auto iter = phis.front();
47 auto acc =
world().
tuple(phis.view().subspan(1));
56 head_lam->branch(
false, cmp, new_body, new_exit,
mem);
57 new_yield->app(
false, head_lam, merge_t(
world(), new_iter, new_yield->
var(),
mem));
58 new_body->
set(
false, body->reduce(
world().tuple({iter, acc, new_yield})).back());
59 new_exit->
set(
false, exit->reduce(acc).back());
61 return rewritten_[def] =
world().
app(head_lam, merge_t(
world(), begin, init,
mem));
Def * set(size_t i, const Def *)
Successively set from left to right.
T * isa_mut() const
If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.
Lam * set(Filter filter, const Def *body)
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)
auto match(const Def *def)
const Def * merge_tuple(const Def *def, Defs defs)