14template<
class Id, Id
id, nat_t w>
21 if constexpr (std::is_same_v<Id, wrap>) {
24 if (
nuw && res <
u)
return {};
32 if constexpr (std::is_same_v<UT, bool>)
37 if (b >= w)
return {};
39 if constexpr (std::is_same_v<UT, bool>)
43 if (
nuw && res <
u)
return {};
47 []<
bool flag =
false>() {
static_assert(flag,
"missing sub tag"); }();
49 }
else if constexpr (std::is_same_v<Id, shr>) {
50 if (b >= w)
return {};
51 if constexpr (
false) {}
52 else if constexpr (
id ==
shr::a)
return s >>
t;
53 else if constexpr (
id ==
shr::l)
return u >> v;
54 else []<
bool flag =
false>() {
static_assert(flag,
"missing sub tag"); }();
55 }
else if constexpr (std::is_same_v<Id, div>) {
56 if (b == 0)
return {};
57 if constexpr (
false) {}
59 else if constexpr (
id ==
div::udiv)
return u / v;
61 else if constexpr (
id ==
div::urem)
return u % v;
62 else []<
bool flag =
false>() {
static_assert(flag,
"missing sub tag"); }();
63 }
else if constexpr (std::is_same_v<Id, icmp>) {
65 auto pm = !(
u >> UT(w - 1)) && (v >> UT(w - 1));
66 auto mp = (
u >> UT(w - 1)) && !(v >> UT(w - 1));
73 }
else if constexpr (std::is_same_v<Id, extrema>) {
74 if constexpr (
false) {}
80 []<
bool flag =
false>() {
static_assert(flag,
"missing tag"); }();
86template<
class Id, Id
id>
87const Def*
fold(World& world,
const Def* type,
const Def*&
a,
const Def*& b,
const Def*
mode = {}) {
88 if (
a->isa<
Bot>() || b->isa<
Bot>())
return world.bot(type);
94 bool nsw =
false,
nuw =
false;
95 if constexpr (std::is_same_v<Id, wrap>) {
104 case i: res = fold<Id, id, i>(*la, *lb, nsw, nuw); break;
109 res = fold<Id, id, 64>(*la, *lb,
false,
false);
110 if (res && !std::is_same_v<Id, icmp>) *res %=
size;
113 return res ? world.lit(type, *res) : world.bot(type);
121template<
class Id, nat_t w> Res
fold(
u64 a, [[maybe_unused]]
bool nsw, [[maybe_unused]]
bool nuw) {
125 if constexpr (std::is_same_v<Id, abs>)
128 []<
bool flag =
false>() {
static_assert(flag,
"missing tag"); }
132template<
class Id>
const Def*
fold(World& world,
const Def* type,
const Def*&
a) {
133 if (
a->isa<
Bot>())
return world.bot(type);
138 bool nsw =
false,
nuw =
false;
142 case i: res = fold<Id, i>(*la, nsw, nuw); break;
146 res = fold<Id, 64>(*la,
false,
false);
147 if (res && !std::is_same_v<Id, icmp>) *res %=
size;
150 return res ? world.lit(type, *res) : world.bot(type);
167const Def* reassociate(Id
id, World& world, [[maybe_unused]]
const App* ab,
const Def*
a,
const Def* b) {
172 auto la =
a->isa<
Lit>();
173 auto [x, y] = xy ? xy->template args<2>() : std::array<const Def*, 2>{
nullptr,
nullptr};
174 auto [z,
w] = zw ? zw->template args<2>() : std::array<const Def*, 2>{
nullptr,
nullptr};
179 auto make_op = [&world,
id](
const Def*
a,
const Def* b) {
return world.call(
id,
Mode::none,
Defs{
a, b}); };
181 if (la && lz)
return make_op(make_op(
a, z), w);
182 if (lx && lz)
return make_op(make_op(x, z), make_op(y, w));
183 if (lz)
return make_op(z, make_op(
a, w));
184 if (lx)
return make_op(x, make_op(y, b));
188template<
class Id>
const Def* merge_cmps(std::array<std::array<u64, 2>, 2> tab,
const Def*
a,
const Def* b) {
189 static_assert(
sizeof(
sub_t) == 1,
"if this ever changes, please adjust the logic below");
190 static constexpr size_t num_bits = std::bit_width(
Annex::Num<Id> - 1_u64);
192 auto& world =
a->world();
196 if (a_cmp && b_cmp && a_cmp->arg() == b_cmp->arg()) {
199 sub_t a_sub = a_cmp.sub();
200 sub_t b_sub = b_cmp.sub();
201 for (
size_t i = 0; i != num_bits; ++i, res >>= 1, a_sub >>= 1, b_sub >>= 1)
202 res |= tab[a_sub & 1][b_sub & 1] << 7_u8;
203 res >>= (7_u8 -
u8(num_bits));
205 if constexpr (std::is_same_v<Id, math::cmp>)
206 return world.call(
math::cmp(res), a_cmp->decurry()->arg(), a_cmp->arg());
217 auto& world = type->world();
218 auto [
a, b] = arg->
projs<2>();
226 case nat::add:
return world.lit_nat(*la + *lb);
227 case nat::sub:
return *la < *lb ? world.lit_nat_0() : world.lit_nat(*la - *lb);
228 case nat::mul:
return world.lit_nat(*la * *lb);
240 if (*la == 1 &&
id ==
nat::mul)
return b;
243 if (lb && *lb == 0 &&
id ==
nat::sub)
return a;
248 case nat::sub:
return world.lit_nat(0);
253 return world.raw_app(type, callee, {
a, b});
257 auto& world = type->world();
259 if (
id ==
ncmp::t)
return world.lit_tt();
260 if (
id ==
ncmp::f)
return world.lit_ff();
262 auto [
a, b] = arg->
projs<2>();
269 case ncmp:: e:
return world.lit_bool(*la == *lb);
270 case ncmp::ne:
return world.lit_bool(*la != *lb);
271 case ncmp::l :
return world.lit_bool(*la < *lb);
272 case ncmp::le:
return world.lit_bool(*la <= *lb);
273 case ncmp::g :
return world.lit_bool(*la > *lb);
274 case ncmp::ge:
return world.lit_bool(*la >= *lb);
275 default: fe::unreachable();
281 return world.raw_app(type, callee, {
a, b});
285 auto& world = type->world();
286 auto callee = c->as<
App>();
287 auto [
a, b] = arg->
projs<2>();
289 if (
auto result = fold<icmp, id>(world, type,
a, b))
return result;
290 if (
id ==
icmp::f)
return world.lit_ff();
291 if (
id ==
icmp::t)
return world.lit_tt();
293 if (
id & (
icmp::e & 0xff))
return world.lit_tt();
294 if (
id ==
icmp::ne)
return world.lit_ff();
297 return world.raw_app(type, callee, {
a, b});
301 auto& world = type->world();
302 auto callee = c->as<
App>();
303 auto [
a, b] = arg->
projs<2>();
304 if (
auto result = fold<extrema, id>(world, type,
a, b))
return result;
305 return world.raw_app(type, callee, {
a, b});
309 auto& world = type->world();
311 auto [_, actual_type] = type->projs<2>();
312 auto make_res = [&,
mem =
mem](
const Def* res) {
return world.tuple({
mem, res}); };
314 if (
auto result = fold<abs>(world, actual_type,
a))
return make_res(result);
319 auto& world = type->world();
320 auto callee = c->as<
App>();
321 auto s = callee->decurry()->arg();
328 case bit1::f:
return world.lit_idx(*ls, 0);
329 case bit1::t:
return world.lit_idx(*ls, *ls - 1_u64);
335 if (
auto la =
Lit::isa(
a))
return world.lit_idx_mod(*ls, ~*la);
342 auto& world = type->world();
343 auto callee = c->as<
App>();
344 auto [
a, b] = arg->
projs<2>();
345 auto s = callee->decurry()->arg();
352 if (
auto res = merge_cmps<icmp>(tab,
a, b))
return res;
353 if (
auto res = merge_cmps<math::cmp>(tab,
a, b))
return res;
360 case bit2:: f:
return world.lit(type, 0);
361 case bit2:: t:
if (ls)
return world.lit(type, *ls-1_u64);
break;
362 case bit2:: fst:
return a;
363 case bit2:: snd:
return b;
371 if (la && lb && ls) {
373 case bit2::and_:
return world.lit_idx (*ls, *la & *lb);
374 case bit2:: or_:
return world.lit_idx (*ls, *la | *lb);
375 case bit2::xor_:
return world.lit_idx (*ls, *la ^ *lb);
376 case bit2::nand:
return world.lit_idx_mod(*ls, ~(*la & *lb));
377 case bit2:: nor:
return world.lit_idx_mod(*ls, ~(*la | *lb));
378 case bit2::nxor:
return world.lit_idx_mod(*ls, ~(*la ^ *lb));
379 case bit2:: iff:
return world.lit_idx_mod(*ls, ~ *la | *lb);
380 case bit2::niff:
return world.lit_idx (*ls, *la & ~*lb);
381 default: fe::unreachable();
386 auto unary = [&](
bool x,
bool y,
const Def*
a) ->
const Def* {
387 if (!x && !y)
return world.lit(type, 0);
388 if ( x && y)
return ls ? world.lit(type, *ls-1_u64) :
nullptr;
389 if (!x && y)
return a;
396 if (
auto res = unary(tab[0][0], tab[1][1],
a))
return res;
401 if (
auto res = unary(tab[0][0], tab[0][1], b))
return res;
402 }
else if (ls && *la == *ls - 1_u64) {
403 if (
auto res = unary(tab[1][0], tab[1][1], b))
return res;
409 if (
auto res = unary(tab[0][0], tab[1][0],
a))
return res;
410 }
else if (ls && *lb == *ls - 1_u64) {
411 if (
auto res = unary(tab[0][1], tab[1][1],
a))
return res;
415 if (
auto res = reassociate<bit2>(
id, world, callee,
a, b))
return res;
417 return world.raw_app(type, callee, {
a, b});
421 auto& world = type->world();
422 auto callee = c->as<
App>();
425 if (*i < *
s)
return world.lit_idx(*
s, *i);
426 if (
auto m =
Lit::isa(callee->arg()))
return *m ? world.bot(type) : world.lit_idx_mod(*
s, *i);
434 auto& world = arg->
world();
440 auto& world = type->world();
441 auto callee = c->as<
App>();
442 auto [
a, b] = arg->
projs<2>();
446 if (
auto result = fold<shr, id>(world, type,
a, b))
return result;
448 if (
auto la =
Lit::isa(
a); la && *la == 0) {
456 if (ls && *lb > *ls)
return world.bot(type);
466 return world.raw_app(type, callee, {
a, b});
470 auto& world = type->world();
471 auto callee = c->as<
App>();
472 auto [
a, b] = arg->
projs<2>();
473 auto mode = callee->arg();
477 if (
auto result = fold<wrap, id>(world, type,
a, b))
return result;
488 }
else if (*la == 1) {
503 default: fe::unreachable();
509 return world.call(
wrap::add,
mode,
Defs{a, world.lit_idx_mod(*ls, ~*lb + 1_u64)});
510 else if (
id ==
wrap::shl && ls && *lb > *ls)
511 return world.bot(type);
517 case wrap::sub:
return world.lit(type, 0);
524 if (
auto res = reassociate<wrap>(
id, world, callee,
a, b))
return res;
526 return world.raw_app(type, callee, {
a, b});
530 auto& world = full_type->
world();
532 auto [
a, b] = ab->projs<2>();
533 auto [_, type] = full_type->
projs<2>();
534 auto make_res = [&,
mem =
mem](
const Def* res) {
return world.tuple({
mem, res}); };
536 if (
auto result = fold<div, id>(world, type,
a, b))
return make_res(result);
539 if (*la == 0)
return make_res(
a);
543 if (*lb == 0)
return make_res(world.bot(type));
549 case div::srem:
return make_res(world.lit(type, 0));
550 case div::urem:
return make_res(world.lit(type, 0));
557 case div::sdiv:
return make_res(world.lit(type, 1));
558 case div::udiv:
return make_res(world.lit(type, 1));
559 case div::srem:
return make_res(world.lit(type, 0));
560 case div::urem:
return make_res(world.lit(type, 0));
568 auto& world = dst_t->
world();
569 auto s_t = x->
type()->as<
App>();
570 auto d_t = dst_t->as<
App>();
576 if (s_t == d_t)
return x;
577 if (x->isa<
Bot>())
return world.bot(d_t);
579 if (ls && ld && *ld < *ls)
return world.call(
conv::u, d, x);
584 if (*ld == 0)
return world.lit(d_t, *
l);
585 return world.lit(d_t, *
l % *ld);
594 else if (S == sw && D == dw) return world.lit(d_t, w2s<D>(mim::bitcast<w2s<S>>(*l)));
595 M( 1, 8)
M( 1, 16)
M( 1, 32)
M( 1, 64)
596 M( 8, 16)
M( 8, 32)
M( 8, 64)
599 else assert(
false &&
"TODO: conversion between different Idx sizes");
607 auto& world = dst_t->
world();
608 auto src_t = src->
type();
610 if (src->isa<
Bot>())
return world.bot(dst_t);
611 if (src_t == dst_t)
return src;
614 return other->arg()->
type() == dst_t ? other->arg() : world.call<
bitcast>(dst_t, other->arg());
617 if (dst_t->isa<
Nat>())
return world.lit(dst_t, *
l);
618 if (
Idx::isa(dst_t))
return world.lit(dst_t, *
l);
629 auto& world = type->world();
631 return world.lit_nat(8);
632 }
else if (type->isa<
Pi>()) {
633 return world.lit_nat(8);
638 case 16:
return world.lit_nat(2);
639 case 32:
return world.lit_nat(4);
640 case 64:
return world.lit_nat(8);
641 default: fe::unreachable();
643 }
else if (type->isa<
Sigma>() || type->isa<
Meet>()) {
646 for (
auto t : type->ops()) {
649 if (!
a || !
s)
return {};
652 offset =
pad(offset, *
a) + *
s;
656 u64 size = std::max(1_u64, offset);
662 }
else if (
auto arr = type->isa_imm<
Arr>()) {
667 }
else if (
auto join = type->isa<
Join>()) {
675 auto& world = type->world();
679 if (arg->
is_closed())
return world.lit_tt();
A (possibly paramterized) Array.
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...
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
bool is_closed() const
Has no free_vars()?
static constexpr nat_t size2bitwidth(nat_t n)
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
static std::optional< T > isa(const Def *def)
static T as(const Def *def)
A dependent function type.
const Lit * lit_idx_unsafe(u64 val)
#define MIM_core_NORMALIZER_IMPL
const Def * normalize_nat(const Def *type, const Def *callee, const Def *arg)
const Def * normalize_idx_unsafe(const Def *, const Def *, const Def *arg)
const Sigma * convert(const TBound< up > *b)
const Def * normalize_div(const Def *full_type, const Def *, const Def *arg)
const Def * normalize_pe(const Def *type, const Def *, const Def *arg)
const Def * normalize_extrema(const Def *type, const Def *c, const Def *arg)
const Def * normalize_icmp(const Def *type, const Def *c, const Def *arg)
const Def * normalize_bit1(const Def *type, const Def *c, const Def *a)
const Def * normalize_conv(const Def *dst_t, const Def *, const Def *x)
const Def * normalize_bit2(const Def *type, const Def *c, const Def *arg)
const Def * normalize_wrap(const Def *type, const Def *c, const Def *arg)
const Def * normalize_trait(const Def *, const Def *, const Def *type)
const Def * op(trait o, const Def *type)
const Def * normalize_abs(const Def *type, const Def *, const Def *arg)
const Def * normalize_idx(const Def *type, const Def *c, const Def *arg)
constexpr std::array< std::array< u64, 2 >, 2 > make_truth_table(bit2 id)
const Def * normalize_bitcast(const Def *dst_t, const Def *, const Def *src)
const Def * normalize_ncmp(const Def *type, const Def *callee, const Def *arg)
@ nuw
No Unsigned Wrap around.
@ nsw
No Signed Wrap around.
const Def * normalize_shr(const Def *type, const Def *c, const Def *arg)
std::optional< nat_t > isa_f(const Def *def)
D bitcast(const S &src)
A bitcast from src of type S to D.
bool commute(const Def *a, const Def *b)
Swap Lit to left - or smaller Def::gid, if no lit present.
TBound< true > Join
AKA union.
u64 pad(u64 offset, u64 align)
constexpr bool is_commutative(Id)
typename detail::w2s_< w >::type w2s
constexpr bool is_associative(Id id)
typename detail::w2u_< w >::type w2u
TBound< false > Meet
AKA intersection.
static constexpr size_t Num
static constexpr flags_t Base
#define MIM_1_8_16_32_64(m)