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 *mutable* 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 ///@}
26
27 Hole* unset() { return Def::unset()->as<Hole>(); }
28 Hole* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
29
30 /// If unset, explode to Tuple.
31 /// @returns the new Tuple, or `this` if unsuccessful.
32 const Def* tuplefy(nat_t);
33
34 /// [Union-Find](https://en.wikipedia.org/wiki/Disjoint-set_data_structure) to unify Hole%s.
35 static const Def* find(const Def*);
36
37 static constexpr auto Node = mim::Node::Hole;
38
39private:
40 const Def* rebuild_(World&, const Def*, Defs) const override;
41 Hole* stub_(World&, const Def*) override;
42
43 friend class World;
44 friend class Checker;
45};
46
47class Checker {
48public:
50 : world_(world) {}
51
52 World& world() { return world_; }
53
54 enum Mode {
55 /// In Mode::Check, type inference is happening and Hole%s will be resolved, if possible.
56 /// Also, two *free* but *different* Var%s **are** considered α-equivalent.
58 /// In Mode::Test, no type inference is happening and Hole%s will not be touched.
59 /// Also, Two *free* but *different* Var%s are **not** considered α-equivalent.
61 };
62
63 template<Mode mode> static bool alpha(const Def* d1, const Def* d2) {
64 return Checker(d1->world()).alpha_<mode>(d1, d2);
65 }
66
67 /// Can @p value be assigned to sth of @p type?
68 /// @note This is different from `equiv(type, value->type())` since @p type may be dependent.
69 [[nodiscard]] static const Def* assignable(const Def* type, const Def* value) {
70 return Checker(type->world()).assignable_(type, value);
71 }
72
73 /// Yields `defs.front()`, if all @p defs are Check::alpha-equivalent (`Mode::Test`) and `nullptr` otherwise.
74 static const Def* is_uniform(Defs defs);
75
76private:
77#ifdef MIM_ENABLE_CHECKS
78 template<Mode> bool fail();
79 const Def* fail();
80#else
81 template<Mode> bool fail() { return false; }
82 const Def* fail() { return {}; }
83#endif
84
85 template<Mode> bool alpha_(const Def* d1, const Def* d2);
86 template<Mode> bool alpha_internal(const Def*, const Def*);
87 [[nodiscard]] const Def* assignable_(const Def* type, const Def* value);
88
89 World& world_;
90 MutMap<const Def*> binders_;
91 fe::Arena arena_;
92};
93
94} // 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:248
static bool alpha(const Def *d1, const Def *d2)
Definition check.h:63
Checker(World &world)
Definition check.h:49
World & world()
Definition check.h:52
@ Test
In Mode::Test, no type inference is happening and Holes will not be touched.
Definition check.h:60
@ Check
In Mode::Check, type inference is happening and Holes will be resolved, if possible.
Definition check.h:57
static const Def * assignable(const Def *type, const Def *value)
Can value be assigned to sth of type?
Definition check.h:69
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:241
World & world() const noexcept
Definition def.cpp:371
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
Def * unset()
Unsets all Def::ops; works even, if not set at all or partially.
Definition def.cpp:253
Dbg dbg() const
Definition def.h:444
const Def * op() const
Definition check.h:20
Hole * set(const Def *op)
Definition check.h:21
friend class Checker
Definition check.h:44
const Def * tuplefy(nat_t)
If unset, explode to Tuple.
Definition check.cpp:64
static constexpr auto Node
Definition check.h:37
friend class World
Definition check.h:43
Hole * stub(const Def *type)
Definition check.h:28
static const Def * find(const Def *)
Union-Find to unify Holes.
Definition check.cpp:44
Hole * unset()
Definition check.h:27
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 nat_t
Definition types.h:43
@ Hole
Definition def.h:85
GIDMap< Def *, To > MutMap
Definition def.h:56