Thorin 1.9.0
The Higher ORder INtermediate representation
Loading...
Searching...
No Matches
thorin::Pi Class Reference

A dependent function type. More...

#include <thorin/lam.h>

Inheritance diagram for thorin::Pi:
[legend]

Public Member Functions

const Piimmutabilize () override
 Tries to make an immutable from a mutable.
 
Pistub (Ref type)
 
Get/Set implicit
bool is_implicit () const
 
Pimake_implicit ()
 
Pimake_explicit ()
 
dom

See also
proj
Ref dom () const
 
codom

See also
proj
Ref codom () const
 
Setters
See also
Setting Ops
Piset (Ref dom, Ref codom)
 
Piset_dom (Ref dom)
 
Piset_dom (Defs doms)
 
Piset_codom (Ref codom)
 
Piunset ()
 
- Public Member Functions inherited from thorin::Def
Worldworld () const
 
flags_t flags () const
 
u32 gid () const
 
hash_t hash () const
 
node_t node () const
 
std::string_view node_name () const
 
const Deftype () const
 Yields the raw type of this Def, i.e. maybe nullptr.
 
const Defunfold_type () const
 Yields the type of this Def and builds a new .Type (UInc n) if necessary.
 
bool is_term () const
 Yields true if this:T and T:(.Type 0).
 
Ref arity () const
 
std::optional< nat_tisa_lit_arity () const
 
nat_t as_lit_arity () const
 
template<size_t N = std::dynamic_extent>
auto ops () const
 
const Defop (size_t i) const
 
size_t num_ops () const
 
Defset (size_t i, const Def *def)
 Successively set from left to right.
 
Defreset (size_t i, const Def *def)
 Successively reset from left to right.
 
Defset (Defs ops)
 Def::set ops all at once.
 
Defreset (Defs ops)
 Def::reset ops all at once.
 
Defunset ()
 Unsets all Def::ops; works even, if not set at all or partially.
 
Defset_type (const Def *)
 
void unset_type ()
 
void update ()
 Resolves Infers of this Def's type.
 
bool is_set () const
 Yields true if empty or the last op is set.
 
Defs extended_ops () const
 
const Defextended_op (size_t i) const
 
size_t num_extended_ops () const
 
Defs partial_ops () const
 
const Defpartial_op (size_t i) const
 
size_t num_partial_ops () const
 
const Usesuses () const
 
size_t num_uses () const
 
unsigned dep () const
 
bool has_dep (Dep d) const
 
bool has_dep (unsigned u) const
 
bool dep_const () const
 
nat_t num_projs () const
 Yields Def::as_lit_arity(), if it is in fact a Lit, or 1 otherwise.
 
nat_t num_tprojs () const
 As above but yields 1, if Flags::scalerize_threshold is exceeded.
 
const Defproj (nat_t a, nat_t i) const
 Similar to World::extract while assuming an arity of a, but also works on Sigmas and Arrays.
 
const Defproj (nat_t i) const
 As above but takes Def::num_projs as arity.
 
const Deftproj (nat_t i) const
 As above but takes Def::num_tprojs.
 
template<nat_t A = -1_n, class F >
auto projs (F f) const
 Splits this Def via Def::projections into an Array (if A == -1_n) or std::array (otherwise).
 
template<class F >
auto tprojs (F f) const
 
template<class F >
auto projs (nat_t a, F f) const
 
template<nat_t A = -1_n>
auto projs () const
 
auto tprojs () const
 
auto projs (nat_t a) const
 
nat_t num_vars ()
 
nat_t num_tvars ()
 
Ref var (nat_t a, nat_t i)
 
Ref var (nat_t i)
 
Ref tvar (nat_t i)
 
template<nat_t A = std::dynamic_extent, class F >
auto vars (F f)
 
template<class F >
auto tvars (F f)
 
template<nat_t A = std::dynamic_extent>
auto vars ()
 
auto tvars ()
 
template<class F >
auto vars (nat_t a, F f)
 
auto vars (nat_t a)
 
Ref var ()
 Not necessarily a Var: E.g., if the return type is [], this will yield ().
 
const Varhas_var ()
 Only returns not nullptr, if Var of this mutable has ever been created.
 
const Varhas_var () const
 As above if this is a mutable.
 
Muts local_muts () const
 
Vars local_vars () const
 
Vars free_vars () const
 
Vars free_vars ()
 
bool is_open () const
 Has free_vars()?
 
bool is_closed () const
 Has no free_vars()?
 
Muts fv_consumers ()
 
bool is_external () const
 
void make_external ()
 
void make_internal ()
 
void transfer_external (Def *to)
 
template<class T = Def>
const T * isa_imm () const
 
template<class T = Def>
const T * as_imm () const
 
template<class T = Def, class R >
const T * isa_imm (R(T::*f)() const) const
 
template<class T = Def, bool invert = false>
T * isa_mut () const
 If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.
 
template<class T = Def, bool invert = false>
T * as_mut () const
 Asserts that this is a mutable, casts constness away and performs a static_cast to T.
 
Dbg dbg () const
 
Loc loc () const
 
Sym sym () const
 
std::string unique_name () const
 name + "_" + Def::gid
 
template<bool Ow = false>
const Defset (Loc l) const
 
template<bool Ow = false>
Defset (Loc l)
 
template<bool Ow = false>
const Defset (Sym s) const
 
template<bool Ow = false>
Defset (Sym s)
 
template<bool Ow = false>
const Defset (std::string s) const
 
template<bool Ow = false>
Defset (std::string s)
 
template<bool Ow = false>
const Defset (Loc l, Sym s) const
 
template<bool Ow = false>
Defset (Loc l, Sym s)
 
template<bool Ow = false>
const Defset (Loc l, std::string s) const
 
template<bool Ow = false>
Defset (Loc l, std::string s)
 
template<bool Ow = false>
const Defset (Dbg d) const
 
template<bool Ow = false>
Defset (Dbg d)
 
const Defdebug_prefix (std::string) const
 
const Defdebug_suffix (std::string) const
 
Defstub (World &w, Ref type)
 
Defstub (Ref type)
 
Ref rebuild (World &w, Ref type, Defs ops) const
 Def::rebuilds this Def while using new_op as substitute for its i'th Def::op.
 
Ref rebuild (Ref type, Defs ops) const
 
const Defrefine (size_t i, const Def *new_op) const
 
DefVec reduce (const Def *arg) const
 Rewrites Def::ops by substituting this mutable's Var with arg.
 
DefVec reduce (const Def *arg)
 
void dump () const
 
void dump (int max) const
 
void write (int max) const
 
void write (int max, const char *file) const
 
std::ostream & stream (std::ostream &, int max) const
 
void dot (std::ostream &os, uint32_t max=0xFFFFFF, bool types=false) const
 
void dot (const char *file=nullptr, uint32_t max=0xFFFFFF, bool types=false) const
 Same as above but write to file or std::cout if file is nullptr.
 
void dot (const std::string &file, uint32_t max=0xFFFFFF, bool types=false) const
 

Static Public Member Functions

Continuations

Checks certain properties of this Pi regarding continuations.

static const Piisa_cn (Ref d)
 Is this a continuation - i.e. is the Pi::codom thorin::Bottom?
 
static const Piisa_returning (Ref d)
 Is this a continuation (Pi::isa_cn) which has a Pi::ret_pi?
 
static const Piisa_basicblock (Ref d)
 Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
 

Protected Member Functions

 Pi (const Def *type, const Def *dom, const Def *codom, bool implicit)
 Constructor for an immutable Pi.
 
 Pi (const Def *type, bool implicit)
 Constructor for a *mut*able Pi.
 
- Protected Member Functions inherited from thorin::Def
 Def (World *, node_t, const Def *type, Defs ops, flags_t flags)
 Constructor for an immutable Def.
 
 Def (node_t n, const Def *type, Defs ops, flags_t flags)
 As above but World retrieved from type.
 
 Def (node_t, const Def *type, size_t num_ops, flags_t flags)
 Constructor for a mutable Def.
 
virtual ~Def ()=default
 
Sym sym (const char *) const
 
Sym sym (std::string_view) const
 
Sym sym (std::string) const
 

Private Member Functions

Pistub_ (World &, Ref) override
 

Return Continuation

const Piret_pi () const
 Yields the last Pi::dom, if it Pi::isa_basicblock.
 
Ref ret_dom () const
 Pi::domain of Pi::ret_pi.
 
static const Piret_pi (Ref d)
 Yields the Pi::ret_pi() of d, if it is in fact a Pi.
 

Type Checking

void check () override
 
static Ref infer (Ref dom, Ref codom)
 

Additional Inherited Members

- Protected Attributes inherited from thorin::Def
Dbg dbg_
 
union { 
 
NormalizeFn normalizer_
 Axiom only: Axioms use this member to store their normalizer.
 
const Axiomaxiom_
 App only: Curried Apps of Axioms use this member to propagate the Axiom.
 
const Varvar_
 Mutable only: Var of a mutable.
 
Worldworld_
 
};  
 
flags_t flags_
 
u8 curry_
 
u8 trip_
 

Detailed Description

A dependent function type.

See also
Lam

Definition at line 11 of file lam.h.

Constructor & Destructor Documentation

◆ Pi() [1/2]

thorin::Pi::Pi ( const Def type,
const Def dom,
const Def codom,
bool  implicit 
)
inlineprotected

Constructor for an immutable Pi.

Definition at line 14 of file lam.h.

References codom(), and dom().

◆ Pi() [2/2]

thorin::Pi::Pi ( const Def type,
bool  implicit 
)
inlineprotected

Constructor for a *mut*able Pi.

Definition at line 17 of file lam.h.

Member Function Documentation

◆ check()

void thorin::Pi::check ( )
overridevirtual

Reimplemented from thorin::Def.

Definition at line 249 of file check.cpp.

References thorin::Check::alpha(), codom(), dom(), thorin::error(), infer(), and thorin::Def::type().

◆ codom()

Ref thorin::Pi::codom ( ) const
inline

◆ dom()

◆ immutabilize()

const Pi * thorin::Pi::immutabilize ( )
overridevirtual

Tries to make an immutable from a mutable.

This usually works if the mutable isn't recursive and its var isn't used.

Reimplemented from thorin::Def.

Definition at line 169 of file def.cpp.

References codom(), thorin::PooledSet< T >::contains(), dom(), thorin::Def::free_vars(), thorin::Def::has_var(), thorin::World::pi(), thorin::Def::var(), and thorin::Def::world().

◆ infer()

Ref thorin::Pi::infer ( Ref  dom,
Ref  codom 
)
static

Definition at line 244 of file check.cpp.

References codom(), dom(), thorin::Kind, thorin::Def::unfold_type(), and thorin::Def::world().

Referenced by check(), and thorin::World::pi().

◆ is_implicit()

bool thorin::Pi::is_implicit ( ) const
inline

Definition at line 23 of file lam.h.

References thorin::Def::flags().

Referenced by thorin::World::iapp().

◆ isa_basicblock()

static const Pi * thorin::Pi::isa_basicblock ( Ref  d)
inlinestatic

◆ isa_cn()

◆ isa_returning()

static const Pi * thorin::Pi::isa_returning ( Ref  d)
inlinestatic

◆ make_explicit()

Pi * thorin::Pi::make_explicit ( )
inline

Definition at line 25 of file lam.h.

References thorin::Def::flags_.

◆ make_implicit()

Pi * thorin::Pi::make_implicit ( )
inline

Definition at line 24 of file lam.h.

References thorin::Def::flags_.

◆ ret_dom()

Ref thorin::Pi::ret_dom ( ) const
inline

Pi::domain of Pi::ret_pi.

Definition at line 67 of file lam.h.

References dom(), and ret_pi().

Referenced by thorin::compose_cn().

◆ ret_pi() [1/2]

const Pi * thorin::Pi::ret_pi ( ) const

Yields the last Pi::dom, if it Pi::isa_basicblock.

Definition at line 13 of file lam.cpp.

References dom(), and isa_basicblock().

Referenced by isa_basicblock(), isa_returning(), and ret_dom().

◆ ret_pi() [2/2]

static const Pi * thorin::Pi::ret_pi ( Ref  d)
inlinestatic

Yields the Pi::ret_pi() of d, if it is in fact a Pi.

Definition at line 63 of file lam.h.

References ret_pi().

Referenced by thorin::ll::Emitter::emit_imported(), thorin::Lam::ret_pi(), ret_pi(), and thorin::Lam::ret_var().

◆ set()

Pi * thorin::Pi::set ( Ref  dom,
Ref  codom 
)
inline

Definition at line 73 of file lam.h.

References codom(), dom(), set_codom(), and set_dom().

Referenced by stub().

◆ set_codom()

Pi * thorin::Pi::set_codom ( Ref  codom)
inline

Definition at line 76 of file lam.h.

References codom(), and thorin::Def::set().

Referenced by set().

◆ set_dom() [1/2]

Pi * thorin::Pi::set_dom ( Defs  doms)

Definition at line 22 of file lam.cpp.

References thorin::Def::set(), and thorin::Def::world().

◆ set_dom() [2/2]

Pi * thorin::Pi::set_dom ( Ref  dom)
inline

Definition at line 74 of file lam.h.

References dom(), and thorin::Def::set().

Referenced by set().

◆ stub()

Pi * thorin::Pi::stub ( Ref  type)
inline

◆ stub_()

Pi * thorin::Pi::stub_ ( World w,
Ref  t 
)
overrideprivatevirtual

Reimplemented from thorin::Def.

Definition at line 141 of file def.cpp.

Referenced by stub().

◆ unset()

Pi * thorin::Pi::unset ( )
inline

Definition at line 77 of file lam.h.

References thorin::Def::unset().


The documentation for this class was generated from the following files: