11 auto& world = type->world();
12 return world.raw_app(type, callee, arg);
26 for (
auto kv :
tuple->ops())
27 if (kv->proj(2, 0) == k)
return kv->proj(2, 1);
36 auto& w = arg->
world();
37 auto [c, k] = arg->
projs<2>();
41 for (
auto kv :
tuple->ops()) {
43 if (key == k)
return w.lit_tt();
45 return tuple->is_closed() ? w.lit_ff() :
nullptr;
48 if (
auto pack =
init->arg()->isa_imm<
Pack>()) w.WLOG(
"packs not yet implemented: {}", pack);
56 auto& w = type->world();
57 auto [ms, kv] = arg->
projs<2>();
60 auto [K, V, n, arg] =
init->uncurry_args<4>();
66 for (
size_t i = 0, e = *l; i != e; ++i) {
68 auto cur =
tuple->proj(e, i);
72 new_ops.emplace_back(kv);
74 new_ops.emplace_back(
tuple->proj(e, i));
78 if (!updated) new_ops.emplace_back(kv);
82 auto new_n = w.lit_nat(new_ops.size());
83 auto app = w.app(w.annex(
insert), K);
86 return w.app(w.app(app, new_n), new_ops);
90 if (
auto pack =
init->arg()->isa_imm<
Pack>()) w.WLOG(
"packs not yet implemented: {}", pack);
static auto isa(const Def *def)
World & world() const noexcept
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_insert(const Def *type, const Def *, const Def *arg)
const Def * normalize_size(const Def *, const Def *, const Def *arg)
const Def * normalize_contains(const Def *, const Def *, const Def *arg)
const Def * normalize_get(const Def *, const Def *, const Def *arg)
const Def * normalize_init(const Def *type, const Def *callee, const Def *arg)
Vector< const Def * > DefVec
#define MIM_ord_NORMALIZER_IMPL