MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
normalizers.cpp
Go to the documentation of this file.
1#include <rang.hpp>
2
3#include <mim/tuple.h>
4#include <mim/world.h>
5
7
8using namespace std::string_literals;
9
10namespace mim::plug::refly {
11
12static_assert(sizeof(void*) <= sizeof(u64), "pointer doesn't fit into Lit");
13
14namespace {
15
16// The trick is that we simply "box" the pointer of @p def inside a Lit of type `%refly.Code`.
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));
20}
21
22// And here we are doing the reverse to retrieve the original pointer again.
23const Def* do_reflect(const Def* def) { return reinterpret_cast<const Def*>(def->as<Lit>()->get()); }
24
25void debug_print(const Def* lvl, const Def* def) {
26 auto& world = def->world();
27 auto level = Log::Level::Debug;
28 if (auto l = Lit::isa(lvl))
29 level = (nat_t)Log::Level::Error <= *l && *l <= (nat_t)Log::Level::Debug ? (Log::Level)*l : Log::Level::Debug;
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);
32 world.log().log(level, def->loc(), "id : {}", def->unique_name());
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());
38}
39
40} // namespace
41
42template<dbg id>
43const Def* normalize_dbg(const Def*, const Def*, const Def* arg) {
44 auto [lvl, x] = arg->projs<2>();
45 debug_print(lvl, x);
46 return id == dbg::perm ? nullptr : x;
47}
48
49const Def* normalize_reify(const Def*, const Def*, const Def* arg) { return do_reify(arg); }
50
51const Def* normalize_reflect(const Def*, const Def*, const Def* arg) { return do_reflect(arg); }
52
53const Def* normalize_refine(const Def*, const Def*, const Def* arg) {
54 auto [code, i, x] = arg->projs<3>();
55 if (auto l = Lit::isa(i)) {
56 auto def = do_reflect(code);
57 return do_reify(def->refine(*l, do_reflect(x)));
58 }
59
60 return {};
61}
62
63const Def* normalize_type(const Def*, const Def*, const Def* arg) { return arg->type(); }
64const Def* normalize_gid(const Def*, const Def*, const Def* arg) { return arg->world().lit_nat(arg->gid()); }
65
66template<equiv id>
67const Def* normalize_equiv(const Def*, const Def*, const Def* arg) {
68 auto [a, b] = arg->projs<2>();
69 bool eq = id & (equiv::aE & 0xff);
70
71 if (id & (equiv::Ae & 0xff)) {
72 auto res = Checker::alpha<Checker::Test>(a, b);
73 if (res ^ eq) mim::error(arg->loc(), "'{}' and '{}' {}alpha-equivalent", a, b, !res ? "not " : "");
74 } else {
75 auto res = a == b;
76 if (res ^ eq) mim::error(arg->loc(), "'{}' and '{}' {}structural-equivalent", a, b, !res ? "not " : "");
77 }
78 return a;
79}
80
81const Def* normalize_check(const Def* type, const Def*, const Def* arg) {
82 auto& w = type->world();
83 auto [cond, val, msg] = arg->projs<3>();
84
85 if (cond == w.lit_tt()) return val;
86 if (cond == w.lit_ff()) {
87 auto s = tuple2str(msg);
88 if (s.empty()) s = "unknown error"s;
89 w.ELOG(s.c_str());
90 }
91
92 return nullptr;
93}
94
96
97} // namespace mim::plug::refly
static bool alpha(const Def *d1, const Def *d2)
Definition check.h:96
Base class for all Defs.
Definition def.h:251
World & world() const noexcept
Definition def.cpp:436
auto projs(F f) const
Splits this Def via Def::projections into an Array (if A == std::dynamic_extent) or std::array (other...
Definition def.h:390
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:295
Loc loc() const
Definition def.h:503
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
Definition def.h:270
static std::optional< T > isa(const Def *def)
Definition def.h:810
Level
Definition log.h:22
const Lit * lit_nat(nat_t a)
Definition world.h:425
The refly Plugin
Definition remove_perm.h:7
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)
u64 nat_t
Definition types.h:43
std::string tuple2str(const Def *)
Definition tuple.cpp:54
void error(Loc loc, const char *f, Args &&... args)
Definition dbg.h:125
uint64_t u64
Definition types.h:34
@ Lit
Definition def.h:114
#define MIM_refly_NORMALIZER_IMPL
Definition autogen.h:141