MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
direct.h
Go to the documentation of this file.
1#pragma once
2
3#include <mim/rewrite.h>
4#include <mim/world.h>
5
7
9
10/// @name %%direct.cps2ds_dep
11/// ```
12/// let k: Cn [t: T, Cn U t] = ...;
13/// let f: [t: T] → U = %direct.cps2ds_dep (T, lm (t': T): * = [t → t']U) k;
14/// ```
15///@{
16inline const Def* op_cps2ds_dep(const Def* k) {
17 auto& w = k->world();
18 auto K = Pi::isa_cn(k->type());
19 auto T = K->dom(2, 0);
20 auto U = Pi::isa_cn(K->dom(2, 1))->dom();
21 auto l = w.mut_lam(T, w.type())->set("Uf");
22 auto body = U;
23
24 if (auto dom = K->dom()->isa_mut<Sigma>())
25 if (auto var = dom->has_var())
26 body = VarRewriter(var, l->var()).rewrite(U); // TODO typeof(dom->var()) != typeof(l->var())
27 l->set(true, body);
28
29 return w.app(w.app(w.annex<direct::cps2ds_dep>(), {T, l}), k);
30}
31///@}
32
33} // namespace mim::plug::direct
Base class for all Defs.
Definition def.h:251
World & world() const noexcept
Definition def.cpp:439
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.cpp:447
static const Pi * isa_cn(const Def *d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
Definition lam.h:48
const Def * dom() const
Definition lam.h:36
A dependent tuple type.
Definition tuple.h:20
const Def * rewrite(const Def *) final
Definition rewrite.cpp:181
The direct style Plugin
Definition direct.h:8
const Def * op_cps2ds_dep(const Def *k)
Definition direct.h:16