MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
check.h
Go to the documentation of this file.
1#pragma once
2
3#include "mim/def.h"
4
5namespace mim {
6
7/// This node is a hole in the IR that is inferred by its context later on.
8/// It is modelled as a *mut*able Def.
9/// If inference was successful, it's Hole::op will be set to the inferred Def.
10class Hole : public Def, public Setters<Hole> {
11private:
12 Hole(const Def* type)
13 : Def(Node, type, 1, 0) {}
14
15public:
16 using Setters<Hole>::set;
17
18 /// @name op
19 ///@{
20 const Def* op() const { return Def::op(0); }
21 Hole* set(const Def* op) {
22 assert(op != this);
23 return Def::set(0, op)->as<Hole>();
24 }
25 Hole* reset(const Def* op) {
26 assert(op != this);
27 return Def::reset(0, op)->as<Hole>();
28 }
29 Hole* unset() { return Def::unset()->as<Hole>(); }
30 ///@}
31
32 /// [Union-Find](https://en.wikipedia.org/wiki/Disjoint-set_data_structure) to unify Hole%s.
33 /// Def::flags is used to keep track of rank for
34 /// [Union by rank](https://en.wikipedia.org/wiki/Disjoint-set_data_structure#Union_by_rank).
35 static const Def* find(const Def*);
36
37 Hole* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
38 /// If unset, explode to Tuple.
39 /// @returns the new Tuple, or `this` if unsuccessful.
40 const Def* tuplefy();
41
42 static constexpr auto Node = mim::Node::Hole;
43
44private:
45 flags_t rank() const { return flags(); }
46 flags_t& rank() { return flags_; }
47
48 const Def* rebuild_(World&, const Def*, Defs) const override;
49 Hole* stub_(World&, const Def*) override;
50
51 friend class World;
52 friend class Checker;
53};
54
55class Checker {
56public:
58 : world_(world) {}
59
60 World& world() { return world_; }
61
62 enum Mode {
63 /// In Mode::Check, type inference is happening and Hole%s will be resolved, if possible.
64 /// Also, two *free* but *different* Var%s **are** considered α-equivalent.
66 /// In Mode::Test, no type inference is happening and Hole%s will not be touched.
67 /// Also, Two *free* but *different* Var%s are **not** considered α-equivalent.
69 };
70
71 template<Mode mode> static bool alpha(const Def* d1, const Def* d2) {
72 return Checker(d1->world()).alpha_<mode>(d1, d2);
73 }
74
75 /// Can @p value be assigned to sth of @p type?
76 /// @note This is different from `equiv(type, value->type())` since @p type may be dependent.
77 [[nodiscard]] static const Def* assignable(const Def* type, const Def* value) {
78 return Checker(type->world()).assignable_(type, value);
79 }
80
81 /// Yields `defs.front()`, if all @p defs are Check::alpha-equivalent (`Mode::Test`) and `nullptr` otherwise.
82 static const Def* is_uniform(Defs defs);
83
84private:
85#ifdef MIM_ENABLE_CHECKS
86 template<Mode> bool fail();
87 const Def* fail();
88#else
89 template<Mode> bool fail() { return false; }
90 const Def* fail() { return {}; }
91#endif
92
93 template<Mode> bool alpha_(const Def* d1, const Def* d2);
94 template<Mode> bool alpha_internal(const Def*, const Def*);
95 [[nodiscard]] const Def* assignable_(const Def* type, const Def* value);
96
97 World& world_;
98 MutMap<const Def*> binders_;
99 fe::Arena arena_;
100};
101
102} // namespace mim
static const Def * is_uniform(Defs defs)
Yields defs.front(), if all defs are Check::alpha-equivalent (Mode::Test) and nullptr otherwise.
Definition check.cpp:240
static bool alpha(const Def *d1, const Def *d2)
Definition check.h:71
Checker(World &world)
Definition check.h:57
World & world()
Definition check.h:60
@ Test
In Mode::Test, no type inference is happening and Holes will not be touched.
Definition check.h:68
@ Check
In Mode::Check, type inference is happening and Holes will be resolved, if possible.
Definition check.h:65
static const Def * assignable(const Def *type, const Def *value)
Can value be assigned to sth of type?
Definition check.h:77
Base class for all Defs.
Definition def.h:198
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:266
World & world() const noexcept
Definition def.cpp:413
constexpr flags_t flags() const noexcept
Definition def.h:216
const Def * op(size_t i) const noexcept
Definition def.h:264
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:242
flags_t flags_
Definition def.h:569
Def * unset()
Unsets all Def::ops; works even, if not set at all or partially.
Definition def.cpp:282
Def * reset(size_t i, const Def *def)
Successively reset from left to right.
Definition def.h:286
Dbg dbg() const
Definition def.h:449
Hole * reset(const Def *op)
Definition check.h:25
const Def * op() const
Definition check.h:20
Hole * set(const Def *op)
Definition check.h:21
friend class Checker
Definition check.h:52
const Def * tuplefy()
If unset, explode to Tuple.
Definition check.cpp:59
static constexpr auto Node
Definition check.h:42
friend class World
Definition check.h:51
Hole * stub(const Def *type)
Definition check.h:37
static const Def * find(const Def *)
Union-Find to unify Holes.
Definition check.cpp:44
Hole * unset()
Definition check.h:29
Hole * stub_(World &, const Def *) override
Definition def.cpp:151
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:110
CRTP-based Mixin to declare setters for Def::loc & Def::name using a covariant return type.
Definition def.h:143
The World represents the whole program and manages creation of MimIR nodes (Defs).
Definition world.h:33
Definition ast.h:14
View< const Def * > Defs
Definition def.h:49
u64 flags_t
Definition types.h:45
@ Hole
Definition def.h:85
GIDMap< Def *, To > MutMap
Definition def.h:56