28 auto [m, v] = w.call(
op,
Defs{mem_, w.tuple({x, c})})->projs<2>();
55 fe::throwf(
"affine.op.mul should have been rewritten to affine.semiop.mul and then to core.mul");
85 auto strides = [&](
const Def* s,
size_t n) {
87 if (n) str[n - 1] = w.lit_nat(1);
88 for (
size_t k = n - 1; k-- != 0;)
90 for (
size_t k = 0; k != n; ++k)
98 auto xs = idxs->projs();
99 auto str = strides(s, xs.size());
100 const Def* lin = w.lit(w.type_i64(), 0);
101 for (
size_t k = 0; k != xs.size(); ++k) {
111 auto m = s->num_projs();
112 auto str = strides(s, m);
113 return w.tuple(
DefVec(m, [&](
size_t d) {
124 auto [mn, sinout, f, idxs] = app->
callee()->as<
App>()->uncurry_args<4>();
125 auto [sin, sout] = sinout->projs<2>();
131 auto lifted = w.tuple(
DefVec(ins.size(), [&](
size_t i) { return w.call(core::conv::u, w.lit_i64(), ins[i]); }));
133 auto f_lam = f->isa_mut<
Lam>();
135 Lam* idx_map_lam =
nullptr;
136 Lam* rw_idx_lam =
nullptr;
137 if (
auto idx_lam =
lookup(f_lam)) {
138 if (
auto idx_lam_mut = idx_lam->isa_mut<
Lam>();
139 idx_lam_mut && idx_lam_mut->
num_vars() == 2 && idx_lam_mut->var(0)->type() ==
mem->type())
141 idx_map_lam = idx_lam->as_mut<
Lam>();
147 auto lam_pi =
rewrite(f_lam->type())->as<
Pi>();
149 idx_map_lam = w.mut_lam(w.pi({mem->type(), lam_pi->dom()}, {mem->type(), lam_pi->codom()}));
150 map(f_lam, idx_map_lam);
153 map(f_lam->var(), idx_map_lam->
var(1));
154 for (
size_t i = 0; i != f_lam->num_vars(); ++i)
155 map(f_lam->var(i), idx_map_lam->
var(1)->
proj(f_lam->num_vars(), i));
156 mem_ = idx_map_lam->
var(0);
158 auto get_body = [&]() ->
const Def* {
159 if (rw_idx_lam)
return rw_idx_lam->
reduce_body(idx_map_lam->
var(1));
162 idx_map_lam->
set(
true, w.tuple({mem_, get_body()}))->
set(f_lam->dbg());
166 auto outs = w.app(idx_map_lam, {
mem, lifted});
169 auto narrowed = w.tuple(
DefVec(sout_n->num_projs(), [&](
size_t j) {
170 return w.call(core::conv::u, sout_n->proj(j), outs->proj(2, 1)->proj(j));
173 return w.tuple({outs->proj(0), narrowed});
176 return RWPhase::rewrite_imm_App(app);
const Def * proj(nat_t a, nat_t i) const
Similar to World::extract while assuming an arity of a, but also works on Sigmas and Arrays.