MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches

This node is a hole in the IR that is inferred by its context later on. More...

#include <mim/check.h>

Inheritance diagram for mim::Hole:
[legend]

Public Member Functions

Hole * stub (const Def *type)
const Def * tuplefy (nat_t)
 If unset, explode to Tuple.
op
const Def * op () const
std::pair< Hole *, const Def * > find ()
 Transitively walks up Holes until the last one while path-compressing everything.
set/unset
Hole * set (const Def *op)
Hole * unset ()
Public Member Functions inherited from mim::Def
Worldworld () const noexcept
constexpr flags_t flags () const noexcept
constexpr u32 gid () const noexcept
 Global id - unique number for this Def.
constexpr u32 tid () const noexcept
 Trie id - only used in Trie.
constexpr u32 mark () const noexcept
 Used internally by free_vars().
constexpr size_t hash () const noexcept
constexpr Node node () const noexcept
std::string_view node_name () const
u32 judge () const noexcept
bool is_form () const noexcept
bool is_intro () const noexcept
bool is_elim () const noexcept
bool is_meta () const noexcept
const Def * type () const noexcept
 Yields the "raw" type of this Def (maybe nullptr).
const Def * unfold_type () const
 Yields the type of this Def and builds a new Type (UInc n) if necessary.
bool is_term () const
virtual const Def * arity () const
template<size_t N = std::dynamic_extent>
constexpr auto ops () const noexcept
const Def * op (size_t i) const noexcept
constexpr size_t num_ops () const noexcept
bool is_set () const
 Yields true if empty or the last op is set.
Def * set (size_t i, const Def *)
 Successively set from left to right.
Def * set (Defs ops)
 Set ops all at once (no Def::unset necessary beforehand).
Def * unset ()
 Unsets all Def::ops; works even, if not set at all or only partially set.
Def * set_type (const Def *)
 Update type.
Defs deps () const noexcept
const Def * dep (size_t i) const noexcept
size_t num_deps () const noexcept
bool has_dep () const
bool has_dep (Dep d) const
bool has_dep (unsigned u) const
nat_t num_projs () const
 Yields Def::arity(), if it is a Lit, or 1 otherwise.
nat_t num_tprojs () const
 As above but yields 1, if Flags::scalarize_threshold is exceeded.
const Def * proj (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 Def * proj (nat_t i) const
 As above but takes Def::num_projs as arity.
const Def * tproj (nat_t i) const
 As above but takes Def::num_tprojs.
template<nat_t A = std::dynamic_extent, class F>
auto projs (F f) const
 Splits this Def via Def::projections into an Array (if A == std::dynamic_extent) 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 = std::dynamic_extent>
auto projs () const
auto tprojs () const
auto projs (nat_t a) const
nat_t num_vars () noexcept
nat_t num_tvars () noexcept
const Def * var (nat_t a, nat_t i) noexcept
const Def * var (nat_t i) noexcept
const Def * tvar (nat_t i) noexcept
template<nat_t A = std::dynamic_extent, class F>
auto vars (F f) noexcept
template<class F>
auto tvars (F f) noexcept
template<nat_t A = std::dynamic_extent>
auto vars () noexcept
auto tvars () noexcept
template<class F>
auto vars (nat_t a, F f) noexcept
auto vars (nat_t a) noexcept
const Def * 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.
const Def * var_type ()
 If this is a binder, compute the type of its Variable.
Muts local_muts () const
 Mutables reachable by following immutable deps(); mut->local_muts() is by definition the set { mut }.
Vars local_vars () const
 Vars reachable by following immutable deps().
Vars free_vars () const
 Compute a global solution by transitively following mutables as well.
Vars free_vars ()
Muts users ()
 Set of mutables where this mutable is locally referenced.
bool is_open () const
 Has free_vars()?
bool is_closed () const
 Has no free_vars()?
bool is_external () const noexcept
void externalize ()
void internalize ()
void transfer_external (Def *to)
bool is_annex () const noexcept
bool is_mutable () const noexcept
template<class T = Def>
const T * isa_imm () const
template<class T = Def>
const T * as_imm () const
template<class T = Def, bool invert = false>
T * isa_mut () const
 If this is mutable, 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 Def * set (Loc l) const
template<bool Ow = false>
Def * set (Loc l)
template<bool Ow = false>
const Def * set (Sym s) const
template<bool Ow = false>
Def * set (Sym s)
template<bool Ow = false>
const Def * set (std::string s) const
template<bool Ow = false>
Def * set (std::string s)
template<bool Ow = false>
const Def * set (Loc l, Sym s) const
template<bool Ow = false>
Def * set (Loc l, Sym s)
template<bool Ow = false>
const Def * set (Loc l, std::string s) const
template<bool Ow = false>
Def * set (Loc l, std::string s)
template<bool Ow = false>
const Def * set (Dbg d) const
template<bool Ow = false>
Def * set (Dbg d)
const Def * debug_prefix (std::string) const
const Def * debug_suffix (std::string) const
Def * stub (World &w, const Def *type)
Def * stub (const Def *type)
const Def * rebuild (World &w, const Def *type, Defs ops) const
 Def::rebuilds this Def while using new_op as substitute for its i'th Def::op.
const Def * rebuild (const Def *type, Defs ops) const
virtual const Def * immutabilize ()
 Tries to make an immutable from a mutable.
bool is_immutabilizable ()
const Def * refine (size_t i, const Def *new_op) const
template<size_t N = std::dynamic_extent>
constexpr auto reduce (const Def *arg) const
virtual constexpr size_t reduction_offset () const noexcept
 First Def::op that needs to be dealt with during reduction; e.g.
virtual const Def * check (size_t i, const Def *def)
 Checks whether the ith operand can be set to def.
virtual const Def * check ()
 After all Def::ops have been Def::set, this method will be invoked to check the type of this mutable.
bool needs_zonk () const
 Yields true, if Def::local_muts() contain a Hole that is set.
const Def * zonk () const
 If Holes have been filled, reconstruct the program without them.
const Def * zonk_mut () const
 If *mutable, zonks all ops and tries to immutabilize it; otherwise just zonk.
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
Public Member Functions inherited from mim::Setters< Hole >
const Holeset (Loc l) const

Static Public Member Functions

isa
static const Def * isa_set (const Def *def)
static Hole * isa_unset (const Def *def)
static const Def * find (const Def *def)
 If def is a Hole, find last in chain, otherwise yields def again.
Static Public Member Functions inherited from mim::Def
static DefVec zonk (Defs defs)
 zonks all defs and returns a new DefVec.
static Cmp cmp (const Def *a, const Def *b)
static bool less (const Def *a, const Def *b)
static bool greater (const Def *a, const Def *b)

Static Public Attributes

static constexpr auto Node = mim::Node::Hole
static constexpr size_t Num_Ops = 1

Private Member Functions

const Def * rebuild_ (World &, const Def *, Defs) const final
Hole * stub_ (World &, const Def *) final

Friends

class World
class Checker

Additional Inherited Members

enum class  Cmp {
  L ,
  G ,
  E ,
  U
}
Protected Member Functions inherited from mim::Def
 Def (World *, Node, const Def *type, Defs ops, flags_t flags)
 Constructor for an immutable Def.
 Def (Node, const Def *type, Defs ops, flags_t flags)
 As above but World retrieved from type.
 Def (Node, 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
Protected Attributes inherited from mim::Def
Dbg dbg_
union { 
NormalizeFn normalizer_
 Axm only: Axms use this member to store their normalizer.
const Axmaxm_
 App only: Curried Apps of Axms use this member to propagate the Axm.
const Varvar_
 Mutable only: Var of a mutable.
Worldworld_
}; 
flags_t flags_
u8 curry_ = 0
u8 trip_ = 0

Detailed Description

This node is a hole in the IR that is inferred by its context later on.

It is modelled as a mutable Def. If inference was successful, it's Hole::op will be set to the inferred Def.

Note
Holes are not type-checked as they are used during type-checking - causing a chicken-and-egg problem.

Definition at line 14 of file check.h.

Member Function Documentation

◆ find() [1/2]

std::pair< Hole *, const Def * > mim::Hole::find ( )

Transitively walks up Holes until the last one while path-compressing everything.

Returns
the final Hole in the chain and final op() (if any).

Definition at line 50 of file check.cpp.

References mim::Def::op().

◆ find() [2/2]

const Def * mim::Hole::find ( const Def * def)
inlinestatic

If def is a Hole, find last in chain, otherwise yields def again.

Definition at line 59 of file check.h.

References mim::Def::isa_mut(), and op().

◆ isa_set()

const Def * mim::Hole::isa_set ( const Def * def)
inlinestatic

Definition at line 48 of file check.h.

References mim::Def::is_set(), and mim::Def::op().

Referenced by mim::Def::needs_zonk().

◆ isa_unset()

Hole * mim::Hole::isa_unset ( const Def * def)
inlinestatic

Definition at line 53 of file check.h.

References mim::Def::isa_mut().

Referenced by mim::World::extract().

◆ op()

const Def * mim::Hole::op ( ) const
inline

Definition at line 24 of file check.h.

References mim::Def::op().

Referenced by find(), and set().

◆ rebuild_()

const Def * mim::Hole::rebuild_ ( World & ,
const Def * ,
Defs  ) const
finalprivatevirtual

Implements mim::Def.

Definition at line 109 of file def.cpp.

References World.

◆ set()

Hole * mim::Hole::set ( const Def * op)
inline

Definition at line 33 of file check.h.

References op(), and mim::Def::set().

Referenced by stub(), and tuplefy().

◆ stub()

Hole * mim::Hole::stub ( const Def * type)
inline

Definition at line 40 of file check.h.

References mim::Def::dbg(), set(), stub_(), mim::Def::type(), and mim::Def::world().

◆ stub_()

Hole * mim::Hole::stub_ ( World & w,
const Def * t )
finalprivatevirtual

Reimplemented from mim::Def.

Definition at line 152 of file def.cpp.

References World.

Referenced by stub().

◆ tuplefy()

const Def * mim::Hole::tuplefy ( nat_t n)

If unset, explode to Tuple.

Returns
the new Tuple, or this if unsuccessful.

Definition at line 75 of file check.cpp.

References mim::Def::is_set(), mim::Def::isa_mut(), mim::Def::proj(), set(), mim::Def::type(), mim::Def::var(), and mim::Def::world().

◆ unset()

Hole * mim::Hole::unset ( )
inline

Definition at line 37 of file check.h.

References mim::Def::unset().

◆ Checker

friend class Checker
friend

Definition at line 76 of file check.h.

References Checker.

Referenced by Checker.

◆ World

friend class World
friend

Definition at line 75 of file check.h.

References World.

Referenced by rebuild_(), stub_(), and World.

Member Data Documentation

◆ Node

auto mim::Hole::Node = mim::Node::Hole
staticconstexpr

Definition at line 68 of file check.h.

◆ Num_Ops

size_t mim::Hole::Num_Ops = 1
staticconstexpr

Definition at line 69 of file check.h.


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