Thorin 1.9.0
The Higher ORder INtermediate representation
Loading...
Searching...
No Matches
ds2cps.cpp
Go to the documentation of this file.
2
3#include <iostream>
4
5#include <thorin/lam.h>
6
8
9namespace thorin::plug::direct {
10
12 auto& world = def->world();
13 if (auto app = def->isa<App>()) {
14 if (auto lam = app->callee()->isa_mut<Lam>()) {
15 world.DLOG("encountered lam app");
16 auto new_lam = rewrite_lam(lam);
17 world.DLOG("new lam: {} : {}", new_lam, new_lam->type());
18 world.DLOG("arg: {} : {}", app->arg(), app->arg()->type());
19 auto new_app = world.app(new_lam, app->arg());
20 world.DLOG("new app: {} : {}", new_app, new_app->type());
21 return new_app;
22 }
23 }
24 return def;
25}
26
27/// This function generates the cps function `f_cps : cn [a:A, cn B]` for a ds function `f: Π a : A -> B`.
28/// The translation is associated in the `rewritten_` map.
29Ref DS2CPS::rewrite_lam(Lam* lam) {
30 if (auto i = rewritten_.find(lam); i != rewritten_.end()) return i->second;
31
32 // only look at lambdas (ds not cps)
33 if (Lam::isa_cn(lam)) return lam;
34 // ignore ds on type level
35 if (lam->type()->codom()->isa<Type>()) return lam;
36 // ignore higher order function
37 if (lam->type()->codom()->isa<Pi>()) {
38 // We can not set the filter here as this causes segfaults.
39 return lam;
40 }
41
42 world().DLOG("rewrite DS function {} : {}", lam, lam->type());
43
44 auto ty = lam->type();
45 auto var = ty->has_var();
46 auto dom = ty->dom();
47 auto codom = ty->codom();
48 auto sigma = world().mut_sigma(2);
49 // replace ds dom var with cps sigma var (cps dom)
50 auto rw_codom = var ? VarRewriter(var, sigma->var(2, 0)).rewrite(codom) : codom;
51 sigma->set(0, dom);
52 sigma->set(1, world().cn(rw_codom));
53
54 world().DLOG("original codom: {}", codom);
55 world().DLOG("rewritten codom: {}", rw_codom);
56
57 auto cps_lam = world().mut_con(sigma)->set(lam->sym().str() + "_cps");
58
59 // rewrite vars of new function
60 // calls handled separately
61 world().DLOG("body: {} : {}", lam->body(), lam->body()->type());
62
63 auto new_ops = thorin::rewrite(lam, cps_lam->var(0_n));
64 auto filter = new_ops[0];
65 auto cps_body = new_ops[1];
66
67 world().DLOG("cps body: {} : {}", cps_body, cps_body->type());
68
69 cps_lam->app(filter, cps_lam->vars().back(), cps_body);
70
71 rewritten_[lam] = op_cps2ds_dep(cps_lam);
72 world().DLOG("replace {} : {}", lam, lam->type());
73 world().DLOG("with {} : {}", rewritten_[lam], rewritten_[lam]->type());
74
75 return rewritten_[lam];
76}
77
78} // namespace thorin::plug::direct
const Def * type() const
Yields the raw type of this Def, i.e. maybe nullptr.
Definition def.h:248
const Var * has_var()
Only returns not nullptr, if Var of this mutable has ever been created.
Definition def.h:407
Sym sym() const
Definition def.h:470
Def * set(size_t i, const Def *def)
Successively set from left to right.
Definition def.cpp:254
World & world() const
Definition def.cpp:421
A function.
Definition lam.h:97
Ref body() const
Definition lam.h:108
static const Lam * isa_cn(Ref d)
Definition lam.h:132
const Pi * type() const
Definition lam.h:109
Lam * set(Filter filter, const Def *body)
Definition lam.h:159
World & world()
Definition pass.h:296
A dependent function type.
Definition lam.h:11
Ref codom() const
Definition lam.h:40
Helper class to retrieve Infer::arg if present.
Definition def.h:87
virtual Ref rewrite(Ref)
Definition rewrite.cpp:9
Lam * mut_con(Ref dom)
Definition world.h:275
Sigma * mut_sigma(Ref type, size_t size)
Definition world.h:301
Ref app(Ref callee, Ref arg)
Definition world.cpp:183
Ref rewrite(Ref) override
Definition ds2cps.cpp:11
The direct style Plugin
Definition direct.h:7
const Def * op_cps2ds_dep(const Def *f)
Definition direct.h:11
DefVec rewrite(Def *mut, Ref arg)
Definition rewrite.cpp:45