MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
lam.cpp
Go to the documentation of this file.
1#include "mim/lam.h"
2
3#include "mim/world.h"
4
5using namespace std::string_literals;
6
7namespace mim {
8
9/*
10 * Pi
11 */
12
13const Pi* Pi::ret_pi() const {
14 if (num_doms() > 0) {
15 auto ret = dom(num_doms() - 1);
16 if (auto pi = Pi::isa_basicblock(ret)) return pi;
17 }
18
19 return nullptr;
20}
21
22Pi* Pi::set_dom(Defs doms) { return Def::set(0, world().sigma(doms))->as<Pi>(); }
23
24/*
25 * Lam
26 */
27
28Lam* Lam::set_filter(Filter filter) { return Def::set(0, world().filter(filter))->as<Lam>(); }
29Lam* Lam::set(Filter filter, const Def* body) { return Def::set({world().filter(filter), body})->as<Lam>(); }
30Lam* Lam::app(Filter f, const Def* callee, const Def* arg) {
31 return Def::set({world().filter(f), world().app(callee, arg)})->as<Lam>();
32}
33Lam* Lam::app(Filter filter, const Def* callee, Defs args) { return app(filter, callee, world().tuple(args)); }
34
35Lam* Lam::branch(Filter filter, const Def* cond, const Def* t, const Def* f, const Def* arg) {
36 return app(filter, world().select(cond, t, f), arg ? arg : world().tuple());
37}
38
39Defs Lam::reduce(Defs args) const { return Def::reduce(world().tuple(args)); }
40
41// TODO maybe we can eta-reduce immutable Lams in some edge casess like: lm _: [] = f ();
42
43const Def* Lam::eta_reduce() const {
44 if (auto var = has_var()) {
45 if (auto app = body()->isa<App>())
46 if (app->arg() == var && !app->callee()->free_vars().contains(var)) return app->callee();
47 }
48 return nullptr;
49}
50
51Lam* Lam::eta_expand(Filter filter, const Def* f) {
52 auto& w = f->world();
53 auto eta = w.mut_lam(f->type()->as<Pi>());
54 eta->set(f->dbg())->debug_prefix("eta_"s);
55 return eta->app(filter, f, eta->var());
56}
57
58/*
59 * Helpers
60 */
61
62const Def* compose_cn(const Def* f, const Def* g) {
63 auto& world = f->world();
64 world.DLOG("compose f (B->C): {} : {}", f, f->type());
65 world.DLOG("compose g (A->B): {} : {}", g, g->type());
66
67 auto F = f->type()->as<Pi>();
68 auto G = g->type()->as<Pi>();
69
70 assert(Pi::isa_returning(F));
71 assert(Pi::isa_returning(G));
72
73 auto A = G->dom(2, 0);
74 auto B = G->ret_dom();
75 auto C = F->ret_dom();
76 // The type check of codom G = dom F is better handled by the application type checking
77
78 world.DLOG("compose f (B->C): {} : {}", f, F);
79 world.DLOG("compose g (A->B): {} : {}", g, G);
80 world.DLOG(" A: {}", A);
81 world.DLOG(" B: {}", B);
82 world.DLOG(" C: {}", C);
83
84 auto h = world.mut_fun(A, C)->set("comp_"s + f->sym().str() + "_"s + g->sym().str());
85 auto hcont = world.mut_con(B)->set("comp_"s + f->sym().str() + "_"s + g->sym().str() + "_cont"s);
86
87 h->app(true, g, {h->var((nat_t)0), hcont});
88
89 auto hcont_var = hcont->var(); // Warning: not var(0) => only one var => normalization flattens tuples down here.
90 hcont->app(true, f, {hcont_var, h->var(1) /* ret_var */});
91
92 return h;
93}
94
95} // namespace mim
Base class for all Defs.
Definition def.h:251
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:263
World & world() const noexcept
Definition def.cpp:439
const Def * var(nat_t a, nat_t i) noexcept
Definition def.h:429
constexpr auto reduce(const Def *arg) const
Definition def.h:563
const Var * has_var()
Only returns not nullptr, if Var of this mutable has ever been created.
Definition def.h:433
std::variant< bool, const Def * > Filter
Definition lam.h:119
const Def * filter() const
Definition lam.h:123
Lam * set(Filter filter, const Def *body)
Definition lam.cpp:29
static Lam * eta_expand(Filter, const Def *f)
Definition lam.cpp:51
Lam * set_filter(Filter)
Set filter first.
Definition lam.cpp:28
Defs reduce(Defs) const
Definition lam.cpp:39
const Def * eta_reduce() const
Yields body(), if eta-convertible and nullptr otherwise.
Definition lam.cpp:43
Lam * branch(Filter filter, const Def *cond, const Def *t, const Def *f, const Def *arg=nullptr)
Set body to an App of (f, t)#cond mem or (f, t)#cond () if mem is nullptr.
Definition lam.cpp:35
Lam * app(Filter filter, const Def *callee, const Def *arg)
Set body to an App of callee and arg.
Definition lam.cpp:30
const Def * body() const
Definition lam.h:124
A dependent function type.
Definition lam.h:15
const Def * ret_dom() const
Pi::domain of Pi::ret_pi.
Definition lam.h:70
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
Definition lam.h:18
static const Pi * isa_basicblock(const Def *d)
Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
Definition lam.h:52
const Def * dom() const
Definition lam.h:36
const Pi * ret_pi() const
Yields the last Pi::dom, if Pi::isa_basicblock.
Definition lam.cpp:13
Pi * set_dom(const Def *dom)
Definition lam.h:78
static const Pi * isa_returning(const Def *d)
Is this a continuation (Pi::isa_cn) which has a Pi::ret_pi?
Definition lam.h:50
const Def * filter(Lam::Filter filter)
Definition world.h:293
const Def * app(const Def *callee, const Def *arg)
Definition world.cpp:194
Definition ast.h:14
View< const Def * > Defs
Definition def.h:76
u64 nat_t
Definition types.h:43
const Def * compose_cn(const Def *f, const Def *g)
The high level view is:
Definition lam.cpp:62