11 auto callee = c->as<
App>();
12 auto f = callee->arg();
15 if constexpr (
id ==
fold::r) std::swap(acc,
vec);
19 for (
auto op :
tuple->ops()) acc = w.app(f, {acc, op});
21 for (
auto op :
tuple->ops() | std::ranges::views::reverse) acc = w.app(f, {op, acc});
25 if (
auto pack =
vec->isa_imm<
Pack>()) w.WLOG(
"packs not yet implemented: {}", pack);
32 auto callee = c->as<
App>();
33 auto p = callee->
arg();
37 for (
auto op :
tuple->ops())
42 if (
auto pack =
vec->isa_imm<
Pack>()) w.WLOG(
"packs not yet implemented: {}", pack);
48 auto& w =
vec->world();
52 for (
auto op :
tuple->ops()) {
53 auto [_, ins] = seen.emplace(op);
54 if (!ins)
return w.lit_ff();
56 return tuple->is_closed() ? w.lit_tt() :
nullptr;
59 if (
auto pack =
vec->isa_imm<
Pack>()) {
60 if (
auto l =
Lit::isa(pack->shape()))
return w.lit_ff();
67 if (type->as<
Arr>()->
shape()->isa<
Bot>())
return nullptr;
69 auto& w = type->world();
70 auto callee = c->as<
App>();
71 auto [n, m] = callee->args<2>([](
auto def) {
return Lit::isa(def); });
74 if (!n || !m)
return nullptr;
75 if (n == 1 && m == 1)
return w.tuple();
77 if (
auto tup_vec =
vec->isa<
Tuple>()) {
78 if (
auto tup_is = is->isa<
Tuple>(); tup_is && tup_is->
is_closed()) {
80 auto set = absl::btree_set<nat_t>();
81 for (
auto opi : tup_is->ops()) set.emplace(
Lit::as(opi));
83 for (
size_t i = 0, e = tup_vec->num_ops(); i != e; ++i)
84 if (!set.contains(i)) defs.emplace_back(tup_vec->op(i));
89 if (
auto tup_pack =
vec->isa_imm<
Pack>())
return w.pack(*n - *m, tup_pack->body());
A (possibly paramterized) Array.
const Def * shape() const
auto projs(F f) const
Splits this Def via Def::projections into an Array (if A == std::dynamic_extent) or std::array (other...
bool is_closed() const
Has no free_vars()?
static std::optional< T > isa(const Def *def)
static T as(const Def *def)
A (possibly paramterized) Tuple.
Data constructor for a Sigma.
const Def * normalize_scan(const Def *, const Def *c, const Def *vec)
const Def * normalize_is_unique(const Def *, const Def *, const Def *vec)
const Def * normalize_diff(const Def *type, const Def *c, const Def *arg)
const Def * normalize_fold(const Def *, const Def *c, const Def *arg)
Vector< const Def * > DefVec
GIDSet< const Def * > DefSet
#define MIM_vec_NORMALIZER_IMPL