18 :
Def(Node,
type, 2, implicit ? 1 : 0) {}
82 void check()
override;
102 :
Def(Node, pi, 2, 0) {}
158 using Filter = std::variant<bool, const Def*>;
177 void check()
override;
240 if (
auto app = def->isa<
App>())
return {app, app->callee()->
isa_mut<
Lam>()};
241 return {
nullptr,
nullptr};
245std::deque<const App*>
decurry(
const Def*);
263const Def*
compose_cn(
const Def* f,
const Def* g);
266std::pair<const Def*, std::vector<const Def*>>
collect_args(
const Def* def);
const Def * callee() const
const App * decurry() const
Returns App::callee again as App.
const Pi * callee_type() const
const Axiom * axiom() const
Ref var()
Not necessarily a Var: E.g., if the return type is [], this will yield ().
bool is_set() const
Yields true if empty or the last op is set.
const Def * op(size_t i) const
Def * unset()
Unsets all Def::ops; works even, if not set at all or partially.
const Def * type() const
Yields the raw type of this Def, i.e. maybe nullptr.
T * isa_mut() const
If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.
Def * set(size_t i, const Def *def)
Successively set from left to right.
std::variant< bool, const Def * > Filter
static Lam * isa_mut_returning(Ref d)
Only for mutables.
Ref ret_var()
Yields the Lam::var of the Lam::ret_pi.
Lam * app(Filter filter, const Def *callee, const Def *arg)
Set body to an App of callee and arg.
Lam * test(Filter filter, const Def *val, const Def *idx, const Def *match, const Def *clash, const Def *mem)
static const Lam * isa_basicblock(Ref d)
static const Lam * isa_cn(Ref d)
static const Lam * isa_returning(Ref d)
Lam * stub_(World &, Ref) override
const Pi * ret_pi() const
static Lam * isa_mut_cn(Ref d)
Only for mutables.
Lam * set_filter(Filter)
Set filter first.
Lam * set_body(const Def *body)
Set body second.
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.
Lam * set(Filter filter, const Def *body)
static Lam * isa_mut_basicblock(Ref d)
Only for mutables.
A dependent function type.
static const Pi * isa_returning(Ref d)
Is this a continuation (Pi::isa_cn) which has a Pi::ret_pi?
static const Pi * isa_basicblock(Ref d)
Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
static const Pi * ret_pi(Ref d)
Yields the Pi::ret_pi() of d, if it is in fact a Pi.
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
Pi * stub_(World &, Ref) override
Ref ret_dom() const
Pi::domain of Pi::ret_pi.
Pi * set(Ref dom, Ref codom)
static const Pi * isa_cn(Ref d)
Is this a continuation - i.e. is the Pi::codom thorin::Bottom?
const Pi * immutabilize() override
Tries to make an immutable from a mutable.
static Ref infer(Ref dom, Ref codom)
Pi * set_codom(Ref codom)
Pi(const Def *type, bool implicit)
Constructor for a *mut*able Pi.
const Pi * ret_pi() const
Yields the last Pi::dom, if it Pi::isa_basicblock.
Helper class to retrieve Infer::arg if present.
This is a thin wrapper for std::span<T, N> with the following additional features:
The World represents the whole program and manages creation of Thorin nodes (Defs).
#define THORIN_PROJ(NAME, CONST)
Use as mixin to wrap all kind of Def::proj and Def::projs variants.
#define THORIN_DEF_MIXIN(T)
const Def * compose_cn(const Def *f, const Def *g)
The high level view is:
absl::flat_hash_map< K, V, GIDHash< K >, GIDEq< K > > GIDMap
std::pair< const Def *, std::vector< const Def * > > collect_args(const Def *def)
Helper function to cope with the fact that normalizers take all arguments and not only its axiom argu...
GIDMap< Lam *, To > LamMap
absl::flat_hash_set< K, GIDHash< K >, GIDEq< K > > GIDSet
const App * isa_callee(const Def *def, size_t i)
std::deque< const App * > decurry(const Def *)
Yields curried Apps in a flat std::deque<const App*>.
std::pair< const App *, Lam * > isa_apped_mut_lam(const Def *def)
Lam * isa_workable(Lam *lam)
These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.