20 : Def(
Node,
type, 2, implicit ? 1 : 0) {}
34 const Def*
dom()
const {
return op(0); }
35 const Def*
codom()
const {
return op(1); }
54 if (
auto pi = d->isa_mut<
Pi>(); pi && pi->is_implicit())
return pi;
58 static const Pi*
has_ret_pi(
const Def* d) {
return d->isa<
Pi>() ? d->as<
Pi>()->ret_pi() :
nullptr; }
114 : Def(
Node, pi, 2, 0) {}
117 using Filter = std::variant<bool, const Def*>;
122 const Def*
body()
const {
return op(1); }
140 static const Lam*
isa_cn(const Def* d) {
return Pi::isa_cn(d->type()) ? d->isa<Lam>() :
nullptr; }
230 template<
size_t N,
bool Callee,
bool Args>
231 static auto uncurry_(
const Def*
callee) {
232 if constexpr (N == std::dynamic_extent) {
234 while (
auto app =
callee->isa<App>()) {
235 if constexpr (Args) args.emplace_back(app->arg());
239 if constexpr (Callee && Args) {
240 std::ranges::reverse(args);
241 return std::pair{
callee, args};
242 }
else if constexpr (Args) {
243 std::ranges::reverse(args);
249 auto args = std::array<const Def*, N>();
250 for (
size_t i = N; i-- != 0;) {
251 if (
auto app =
callee->isa<App>()) {
252 if constexpr (Args) args[i] = app->arg();
255 if constexpr (Args) args[i] =
nullptr;
259 if constexpr (Callee && Args)
260 return std::pair{
callee, args};
261 else if constexpr (Args)
282 const Def*
arg()
const {
return op(1); }
320 template<
size_t N = std::dynamic_extent>
static auto uncurry(
const Def* def) {
return uncurry_<N, true, true >(def ); }
321 template<
size_t N = std::dynamic_extent>
auto uncurry()
const {
return uncurry_<N, true, true >(
this); }
323 static const Def*
uncurry_callee(
const Def* def) {
return uncurry_<std::dynamic_extent, true, false>(def ); }
324 const Def*
uncurry_callee()
const {
return uncurry_<std::dynamic_extent, true, false>(
this); }
326 template<
size_t N = std::dynamic_extent>
static auto uncurry_args(
const Def* def) {
return uncurry_<N, false, true>(def ); }
327 template<
size_t N = std::dynamic_extent>
auto uncurry_args()
const {
return uncurry_<N, false, true>(
this); }
351 if (
auto app = def->isa<
App>())
return {app, app->callee()->isa_mut<
Lam>()};
352 return {
nullptr,
nullptr};
371const Def*
compose_cn(
const Def* f,
const Def* g);
static constexpr size_t Num_Ops
static const Def * uncurry_callee(const Def *def)
const Pi * callee_type() const
const App * decurry() const
Returns App::callee again as App.
static constexpr auto Node
static auto uncurry(const Def *def)
const Def * callee() const
static auto uncurry_args(const Def *def)
const Def * uncurry_callee() const
auto uncurry_args() const
const Def * rebuild_(World &, const Def *, Defs) const final
bool is_set() const
Yields true if empty or the last op is set.
constexpr Node node() const noexcept
Def * set(size_t i, const Def *)
Successively set from left to right.
World & world() const noexcept
virtual const Def * check()
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
constexpr auto ops() const noexcept
constexpr flags_t flags() const noexcept
const Def * op(size_t i) const noexcept
nat_t num_vars() noexcept
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
bool is_external() const noexcept
const Def * var()
Not necessarily a Var: E.g., if the return type is [], this will yield ().
Def * unset()
Unsets all Def::ops; works even, if not set at all or only partially set.
constexpr auto reduce(const Def *arg) const
std::variant< bool, const Def * > Filter
const Def * filter() const
static const Lam * isa_cn(const Def *d)
static constexpr size_t Num_Ops
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.
static const Def * eta_expand(const Def *f)
Use true Filter.
Lam * set(Filter filter, const Def *body)
Lam * set_filter(Filter)
Set filter first.
static Lam * isa_mut_basicblock(const Def *d)
Only for mutables.
static const Lam * isa_returning(const Def *d)
constexpr size_t reduction_offset() const noexcept final
First Def::op that needs to be dealt with during reduction; e.g.
const Pi * ret_pi() const
static Lam * isa_mut_returning(const Def *d)
Only for mutables.
Lam * stub_(World &, const Def *) final
static constexpr auto Node
const Def * eta_reduce() const
Yields body(), if eta-convertible and nullptr otherwise.
static const Lam * isa_basicblock(const Def *d)
Lam * app(Filter filter, const Def *callee, const Def *arg)
Set body to an App of callee and arg.
const Def * rebuild_(World &, const Def *, Defs) const final
const Def * ret_dom() const
Lam * set_body(const Def *body)
Set body second.
Lam * stub(const Def *type)
static Lam * isa_mut_cn(const Def *d)
Only for mutables.
const Def * reduce_body(const Def *arg) const
const Def * ret_var()
Yields the Lam::var of the Lam::ret_pi.
const Def * codom() const
static const Def * eta_expand(Filter, const Def *f)
A dependent function type.
constexpr size_t reduction_offset() const noexcept final
First Def::op that needs to be dealt with during reduction; e.g.
const Def * ret_dom() const
Pi::domain of Pi::ret_pi.
const Def * check() final
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
Pi(const Def *type, bool implicit)
Constructor for a mutable Pi.
static const Pi * has_ret_pi(const Def *d)
Yields the Pi::ret_pi() of d, if it is in fact a Pi.
Pi * set_codom(const Def *codom)
static constexpr size_t Num_Ops
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
static const Pi * isa_cn(const Def *d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
static const Pi * isa_basicblock(const Def *d)
Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
static const Def * infer(const Def *dom, const Def *codom)
const Def * codom() const
static Pi * isa_implicit(const Def *d)
Is d an Pi::is_implicit (mutable) Pi?
Pi * set(const Def *dom, const Def *codom)
static constexpr auto Node
const Def * reduce(const Def *arg) const
const Pi * immutabilize() final
Tries to make an immutable from a mutable.
Pi * stub(const Def *type)
const Def * rebuild_(World &, const Def *, Defs) const final
const Pi * ret_pi() const
Yields the last Pi::dom, if Pi::isa_basicblock.
Pi * stub_(World &, const Def *) final
Pi * set_dom(const Def *dom)
static const Pi * isa_returning(const Def *d)
Is this a continuation (Pi::isa_cn) which has a Pi::ret_pi?
CRTP-based mixin to declare setters for Def::loc & Def::name using a covariant return type.
#define MIM_PROJ(NAME, CONST)
Use as mixin to wrap all kind of Def::proj and Def::projs variants.
Vector< const Def * > DefVec
std::pair< const App *, Lam * > isa_apped_mut_lam(const Def *def)
absl::flat_hash_map< K, V, GIDHash< K > > GIDMap
GIDMap< Lam *, To > LamMap
Lam * isa_workable(Lam *lam)
These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.
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:
absl::flat_hash_set< K, GIDHash< K > > GIDSet