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::app(Filter f, const Def* callee, const Def* arg) { return set_filter(f)->set_body(world().app(callee, arg)); }
30Lam* Lam::app(Filter filter, const Def* callee, Defs args) { return app(filter, callee, world().tuple(args)); }
31
32Lam* Lam::branch(Filter filter, const Def* cond, const Def* t, const Def* f, const Def* mem) {
33 return app(filter, world().select(cond, t, f), mem ? mem : world().tuple());
34}
35
36/*
37 * Helpers
38 */
39
40std::deque<const App*> decurry(const Def* def) {
41 std::deque<const App*> apps;
42 while (auto app = def->isa<App>()) {
43 apps.emplace_front(app);
44 def = app->callee();
45 }
46 return apps;
47}
48
49const Def* compose_cn(const Def* f, const Def* g) {
50 auto& world = f->world();
51 world.DLOG("compose f (B->C): {} : {}", f, f->type());
52 world.DLOG("compose g (A->B): {} : {}", g, g->type());
53
54 auto F = f->type()->as<Pi>();
55 auto G = g->type()->as<Pi>();
56
57 assert(Pi::isa_returning(F));
58 assert(Pi::isa_returning(G));
59
60 auto A = G->dom(2, 0);
61 auto B = G->ret_dom();
62 auto C = F->ret_dom();
63 // The type check of codom G = dom F is better handled by the application type checking
64
65 world.DLOG("compose f (B->C): {} : {}", f, F);
66 world.DLOG("compose g (A->B): {} : {}", g, G);
67 world.DLOG(" A: {}", A);
68 world.DLOG(" B: {}", B);
69 world.DLOG(" C: {}", C);
70
71 auto h = world.mut_fun(A, C)->set("comp_"s + f->sym().str() + "_"s + g->sym().str());
72 auto hcont = world.mut_con(B)->set("comp_"s + f->sym().str() + "_"s + g->sym().str() + "_cont"s);
73
74 h->app(true, g, {h->var((nat_t)0), hcont});
75
76 auto hcont_var = hcont->var(); // Warning: not var(0) => only one var => normalization flattens tuples down here.
77 hcont->app(true, f, {hcont_var, h->var(1) /* ret_var */});
78
79 return h;
80}
81
82std::pair<const Def*, DefVec> collect_args(const Def* def) {
83 DefVec args;
84 if (auto app = def->isa<App>()) {
85 auto callee = app->callee();
86 auto arg = app->arg();
87 auto [inner_callee, args] = collect_args(callee);
88 args.push_back(arg);
89 return {inner_callee, args};
90 } else {
91 return {def, args};
92 }
93}
94
95} // namespace mim
Base class for all Defs.
Definition def.h:197
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:240
World & world() const noexcept
Definition def.cpp:387
std::variant< bool, const Def * > Filter
Definition lam.h:114
const Def * filter() const
Definition lam.h:118
Lam * branch(Filter filter, const Def *cond, const Def *t, const Def *f, const Def *mem=nullptr)
Set body to an App of (f, t)#cond mem or (f, t)#cond () if mem is nullptr.
Definition lam.cpp:32
Lam * set_filter(Filter)
Set filter first.
Definition lam.cpp:28
Lam * app(Filter filter, const Def *callee, const Def *arg)
Set body to an App of callee and arg.
Definition lam.cpp:29
Lam * set_body(const Def *body)
Set body second.
Definition lam.h:167
A dependent function type.
Definition lam.h:11
const Def * ret_dom() const
Pi::domain of Pi::ret_pi.
Definition lam.h:66
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
Definition lam.h:14
static const Pi * isa_basicblock(const Def *d)
Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
Definition lam.h:48
const Def * dom() const
Definition lam.h:32
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:74
static const Pi * isa_returning(const Def *d)
Is this a continuation (Pi::isa_cn) which has a Pi::ret_pi?
Definition lam.h:46
Definition ast.h:14
View< const Def * > Defs
Definition def.h:48
u64 nat_t
Definition types.h:43
Vector< const Def * > DefVec
Definition def.h:49
std::pair< const Def *, DefVec > collect_args(const Def *def)
Helper function to cope with the fact that normalizers take all arguments and not only its axm argume...
Definition lam.cpp:82
std::deque< const App * > decurry(const Def *)
Yields curried Apps in a flat std::deque<const App*>.
Definition lam.cpp:40
const Def * compose_cn(const Def *f, const Def *g)
The high level view is:
Definition lam.cpp:49