82 void check()
override;
165 using Filter = std::variant<bool, const Def*>;
184 void check()
override;
257 if (
auto app = def->isa<
App>())
return {app, app->callee()->isa_mut<
Lam>()};
258 return {
nullptr,
nullptr};
262std::deque<const App*>
decurry(
const Def*);
280const Def*
compose_cn(
const Def* f,
const Def* g);
283std::pair<const Def*, std::vector<const Def*>>
collect_args(
const Def* def);
const Pi * callee_type() const
const Axiom * axiom() const
Ref rebuild_(World &, Ref, Defs) const override
const App * decurry() const
Returns App::callee again as App.
static constexpr auto Node
const Def * callee() const
bool is_set() const
Yields true if empty or the last op is set.
Def * set(size_t i, const Def *def)
Successively set from left to right.
Ref var()
Not necessarily a Var: E.g., if the return type is [], this will yield ().
const Def * op(size_t i) const
Def * unset()
Unsets all Def::ops; works even, if not set at all or partially.
std::variant< bool, const Def * > Filter
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)
Lam * set_filter(Filter)
Set filter first.
static Lam * isa_mut_basicblock(Ref d)
Only for mutables.
Lam * stub_(World &, Ref) override
const Pi * ret_pi() const
static Lam * isa_mut_returning(Ref d)
Only for mutables.
static constexpr auto Node
Lam * test(Filter filter, const Def *val, const Def *idx, const Def *match, const Def *clash, const Def *mem)
static Lam * isa_mut_cn(Ref d)
Only for mutables.
Lam * app(Filter filter, const Def *callee, const Def *arg)
Set body to an App of callee and arg.
Lam * set_body(const Def *body)
Set body second.
static const Lam * isa_cn(Ref d)
static const Lam * isa_basicblock(Ref d)
Ref rebuild_(World &, Ref, Defs) const override
Ref ret_var()
Yields the Lam::var of the Lam::ret_pi.
static const Lam * isa_returning(Ref d)
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 Ref infer(Ref dom, Ref codom)
Pi(const Def *type, bool implicit)
Constructor for a *mut*able Pi.
Pi * set_codom(Ref codom)
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
Pi * set(Ref dom, Ref codom)
Ref rebuild_(World &, Ref, Defs) const override
Pi * stub_(World &, Ref) override
static constexpr auto Node
const Pi * immutabilize() override
Tries to make an immutable from a mutable.
static const Pi * isa_cn(Ref d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
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)
const Pi * ret_pi() const
Yields the last Pi::dom, if it Pi::isa_basicblock.
Ref ret_dom() const
Pi::domain of Pi::ret_pi.
Helper class to retrieve Infer::arg if present.
CRTP-based Mixin to declare setters for Def::loc & Def::name using a covariant return type.
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 MimIR nodes (Defs).
#define MIM_PROJ(NAME, CONST)
Use as mixin to wrap all kind of Def::proj and Def::projs variants.
std::pair< const App *, Lam * > isa_apped_mut_lam(const Def *def)
absl::flat_hash_set< K, GIDHash< K >, GIDEq< K > > GIDSet
GIDMap< Lam *, To > LamMap
Lam * isa_workable(Lam *lam)
These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.
std::deque< const App * > decurry(const Def *)
Yields curried Apps in a flat std::deque<const App*>.
absl::flat_hash_map< K, V, GIDHash< K >, GIDEq< K > > GIDMap
const App * isa_callee(const Def *def, size_t i)
const Def * compose_cn(const Def *f, const Def *g)
The high level view is:
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...