8using namespace std::string_literals;
12static_assert(
sizeof(
void*) <=
sizeof(
u64),
"pointer doesn't fit into Lit");
17const Def* do_reify(
const Def* def) {
18 auto& world = def->
world();
19 return world.
lit(world.call<
Code>(def->
type()),
reinterpret_cast<u64>(def));
23const Def* do_reflect(
const Def* def) {
return reinterpret_cast<const Def*
>(def->as<
Lit>()->
get()); }
25void debug_print(
const Def* lvl,
const Def* def) {
26 auto& world = def->
world();
30 world.log().log(level, __FILE__, __LINE__,
"{}debug_print: {}{}", rang::fg::yellow, def, rang::fg::reset);
31 world.log().log(level, def->
loc(),
"def : {}", def);
33 world.log().log(level, def->
type()->
loc(),
"type: {}", def->
type());
34 world.log().log(level, def->
loc(),
"node: {}", def->
node_name());
35 world.log().log(level, def->
loc(),
"ops : {}", def->
num_ops());
36 world.log().log(level, def->
loc(),
"proj: {}", def->
num_projs());
37 world.log().log(level, def->
loc(),
"eops: {}", def->
num_deps());
44 auto [lvl, x] = arg->
projs<2>();
54 auto [code, i, x] = arg->
projs<3>();
56 auto def = do_reflect(code);
57 return do_reify(def->refine(*l, do_reflect(x)));
68 auto [a, b] = arg->
projs<2>();
73 if (res ^ eq)
mim::error(arg->
loc(),
"'{}' and '{}' {}alpha-equivalent", a, b, !res ?
"not " :
"");
76 if (res ^ eq)
mim::error(arg->
loc(),
"'{}' and '{}' {}structural-equivalent", a, b, !res ?
"not " :
"");
82 auto& w =
type->world();
83 auto [cond, val, msg] = arg->
projs<3>();
85 if (cond == w.lit_tt())
return val;
86 if (cond == w.lit_ff()) {
88 if (s.empty()) s =
"unknown error"s;
static bool alpha(const Def *d1, const Def *d2)
size_t num_deps() const noexcept
World & world() const noexcept
std::string_view node_name() const
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).
nat_t num_projs() const
Yields Def::arity(), if it is a Lit, or 1 otherwise.
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
std::string unique_name() const
name + "_" + Def::gid
constexpr size_t num_ops() const noexcept
static std::optional< T > isa(const Def *def)
const Lit * lit(const Def *type, u64 val)
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