9 auto& world = type->world();
10 auto [a, b] = arg->
projs<2>();
11 auto [n, m] = callee->as<
App>()->
decurry()->args<2>([](
auto def) {
return Lit::isa(def); });
15 for (
size_t i = 0, e = *n; i != e; ++i) defs.emplace_back(a->proj(e, i));
16 for (
size_t i = 0, e = *m; i != e; ++i) defs.emplace_back(b->proj(e, i));
17 return world.tuple(defs);
24 auto& w = type->world();
25 auto [xs, x] = arg->
projs<2>();
27 if (
auto mut_pack = xs->isa_mut<
Pack>()) {
28 if (
auto imm = mut_pack->immutabilize())
35 for (
auto op :
tuple->ops())
36 if (op == x)
return w.lit_tt();
38 return tuple->is_closed() ? w.lit_ff() :
nullptr;
41 if (
auto pack = xs->isa<
Pack>()) {
42 if (pack->body() == x)
return w.lit_tt();
43 return pack->is_closed() ? w.lit_ff() :
nullptr;
50 auto& w = type->world();
51 auto callee = c->as<
App>();
52 auto is_os = callee->
arg();
53 auto [n_i, Is, n_o, Os, f] = is_os->
projs<5>();
54 auto [r, s] = callee->decurry()->args<2>();
63 if (lr && ls && *lr == 1 && *ls == 1)
return w.app(f, arg);
66 auto args = arg->
projs(*l_in);
68 if (lr && std::ranges::all_of(args, [](
const Def* arg) {
return arg->isa<
Tuple,
Pack>(); })) {
69 auto shapes = s->projs(*lr);
73 auto elems =
DefVec(*s_n, [&, f = f](
size_t s_i) {
74 auto inner_args =
DefVec(args.size(), [&](
size_t i) { return args[i]->proj(*s_n, s_i); });
76 return w.app(f, inner_args);
78 auto app_zip = w.app(w.annex<
zip>(), {w.lit_nat(*lr - 1), w.tuple(shapes.view().subspan(1))});
79 return w.app(w.app(app_zip, is_os), inner_args);
82 return w.tuple(elems);
auto projs(F f) const
Splits this Def via Def::projections into an Array (if A == std::dynamic_extent) or std::array (other...
static std::optional< T > isa(const Def *def)
A (possibly paramterized) Tuple.
Data constructor for a Sigma.
const Def * normalize_zip(const Def *type, const Def *c, const Def *arg)
const Def * normalize_concat(const Def *type, const Def *callee, const Def *arg)
const Def * normalize_contains(const Def *type, const Def *, const Def *arg)
Vector< const Def * > DefVec
std::deque< const App * > decurry(const Def *)
Yields curried Apps in a flat std::deque<const App*>.
#define MIM_tuple_NORMALIZER_IMPL