14const Def* merge_s(World& w, Ref elem, Ref sigma, Ref
mem) {
16 auto elems = sigma->projs();
19 return w.sigma({elem, sigma});
22const Def* merge_t(World& w, Ref elem, Ref tuple, Ref
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 *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)
Helper class to retrieve Infer::arg if present.
This is a thin wrapper for std::span<T, N> with the following additional features:
Ref var(Ref type, Def *mut)
Ref app(Ref callee, Ref arg)
const Def * call(Id id, Args &&... args)
const Type * type(Ref level)
Ref rewrite(Ref) override
Ref mem_def(Ref def)
Returns the (first) element of type mem::M from the given tuple.
Ref mem_var(Lam *lam)
Returns the memory argument of a function if it has one.
const Def * merge_sigma(const Def *def, Defs defs)
const Def * merge_tuple(const Def *def, Defs defs)