1#include <absl/container/btree_set.h>
10#include "absl/container/fixed_array.h"
17 auto callee = c->as<
App>();
18 auto f = callee->arg();
21 if constexpr (
id ==
fold::r) std::swap(acc,
vec);
25 for (
auto op :
tuple->ops())
26 acc = w.app(f, {acc, op});
28 for (
auto op :
tuple->ops() | std::ranges::views::reverse)
29 acc = w.app(f, {op, acc});
33 if (
auto pack =
vec->isa_imm<
Pack>()) w.WLOG(
"packs not yet implemented: {}", pack);
37 return w.app(f, {acc, l});
39 return w.app(f, {
l, acc});
47 auto& w = type->world();
49 auto [ni, n] = ni_n->projs<2>([](
const Def* def) {
return Lit::isa(def); });
51 if (!ni || !n)
return {};
52 if (ni >= w.flags().scalarize_threshold || n >= w.flags().scalarize_threshold)
return {};
54 auto res = absl::FixedArray<const Def*>(*n);
55 auto tup = absl::FixedArray<const Def*>(*ni);
57 for (
size_t j = 0; j != n; ++j) {
58 for (
size_t i = 0; i != ni; ++i)
59 tup[i] = arg->
proj(*ni, i)->
proj(*n, j);
61 res[j] = w.app(f, tup);
70 auto callee = c->as<
App>();
71 auto p = callee->
arg();
75 for (
auto op :
tuple->ops())
80 if (
auto pack =
vec->isa_imm<
Pack>()) w.WLOG(
"packs not yet implemented: {}", pack);
86 auto& w =
vec->world();
90 for (
auto op :
tuple->ops()) {
91 auto [_, ins] = seen.emplace(op);
92 if (!ins)
return w.lit_ff();
94 return tuple->is_closed() ? w.lit_tt() :
nullptr;
97 if (
auto pack =
vec->isa_imm<
Pack>()) {
98 if (
auto l =
Lit::isa(pack->arity()))
return w.lit_ff();
101 if (
vec->isa<
Lit>())
return w.lit_tt();
107 auto [a, b] = arg->
projs<2>();
108 auto [n, m] = callee->as<
App>()->decurry()->args<2>([](
auto def) {
return Lit::isa(def); });
109 if (n && *n == 0)
return b;
110 if (m && *m == 0)
return a;
116 if (
auto arr = type->isa<
Arr>()) {
117 if (arr->arity()->isa<
Bot>())
return nullptr;
120 auto& w = type->world();
121 auto callee = c->as<
App>();
122 auto [n, m] = callee->args<2>([](
auto def) {
return Lit::isa(def); });
125 if (!n || !m)
return nullptr;
126 if (n == 1 && m == 1)
return w.tuple();
128 if (
auto tup_vec =
vec->isa<
Tuple>()) {
129 if (
auto tup_is = is->isa<
Tuple>(); tup_is && tup_is->
is_closed()) {
131 auto set = absl::btree_set<nat_t>();
132 for (
auto opi : tup_is->ops())
135 for (
size_t i = 0, e = tup_vec->num_ops(); i != e; ++i)
136 if (!set.contains(i)) defs.emplace_back(tup_vec->op(i));
137 return w.tuple(defs);
142 for (
size_t i = 0, e = tup_vec->num_ops(); i != e; ++i)
143 if (i != lit_is) defs.emplace_back(tup_vec->op(i));
144 return w.tuple(defs);
148 if (
auto tup_pack =
vec->isa_imm<
Pack>())
return w.pack(*n - *m, tup_pack->body());
auto uncurry_args() const
A (possibly paramterized) Array.
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.
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_open() const
Has free_vars()?
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_cat(const Def *, const Def *callee, const Def *arg)
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)
const Def * normalize_zip(const Def *type, const Def *c, const Def *arg)
Vector< const Def * > DefVec
const Def * cat_tuple(nat_t n, nat_t m, const Def *a, const Def *b)
GIDSet< const Def * > DefSet
#define MIM_vec_NORMALIZER_IMPL