7using namespace std::string_literals;
11static_assert(
sizeof(
void*) <=
sizeof(
u64),
"pointer doesn't fit into Lit");
16const Def* do_reify(
const Def* def) {
17 auto& world = def->world();
18 return world.lit(world.call<
Code>(def->type()),
reinterpret_cast<u64>(def));
22const Def* do_reflect(
const Def* def) {
return reinterpret_cast<const Def*
>(def->as<
Lit>()->get()); }
24void debug_print(
const Def* lvl,
const Def* def) {
25 auto& world = def->world();
29 world.log().log(level, __FILE__, __LINE__,
"{}debug_print: {}{}", rang::fg::yellow, def, rang::fg::reset);
30 world.log().log(level, def->loc(),
"def : {}", def);
31 world.log().log(level, def->loc(),
"id : {}", def->unique_name());
32 world.log().log(level, def->type()->loc(),
"type: {}", def->type());
33 world.log().log(level, def->loc(),
"node: {}", def->node_name());
34 world.log().log(level, def->loc(),
"ops : {}", def->num_ops());
35 world.log().log(level, def->loc(),
"proj: {}", def->num_projs());
36 world.log().log(level, def->loc(),
"eops: {}", def->num_deps());
42 auto [lvl, x] = arg->
projs<2>();
52 auto [code, i, x] = arg->
projs<3>();
54 auto def = do_reflect(code);
55 return do_reify(def->refine(*l, do_reflect(x)));
65 auto [a, b] = arg->
projs<2>();
70 if (res ^ eq)
mim::error(arg->
loc(),
"'{}' and '{}' {}alpha-equivalent", a, b, !res ?
"not " :
"");
73 if (res ^ eq)
mim::error(arg->
loc(),
"'{}' and '{}' {}structural-equivalent", a, b, !res ?
"not " :
"");
79 auto& w =
type->world();
80 auto [cond, val, msg] = arg->
projs<3>();
82 if (cond == w.lit_tt())
return val;
83 if (cond == w.lit_ff()) {
85 if (s.empty()) s =
"unknown error"s;
static bool alpha(const Def *d1, const Def *d2)
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).
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
static std::optional< T > isa(const Def *def)
const Lit * lit_nat(nat_t a)
const Def * normalize_reify(const Def *, const Def *, const Def *arg)
const Def * normalize_dbg(const Def *, const Def *, const Def *arg)
const Def * normalize_check(const Def *type, const Def *, const Def *arg)
const Def * normalize_refine(const Def *, const Def *, const Def *arg)
const Def * normalize_equiv(const Def *, const Def *, const Def *arg)
const Def * normalize_gid(const Def *, const Def *, const Def *arg)
const Def * normalize_type(const Def *, const Def *, const Def *arg)
const Def * normalize_reflect(const Def *, const Def *, const Def *arg)
std::string tuple2str(const Def *)
void error(Loc loc, const char *f, Args &&... args)
#define MIM_refly_NORMALIZER_IMPL