mim::Check Class Reference

#include <mim/check.h>

Public Types
enum	Mode {   C ,   T }

Public Member Functions
	Check (World &world)
World &	world ()

Static Public Member Functions
template<Mode mode = C>
static bool	alpha (const Def *d1, const Def *d2)
static bool	test_alpha (const Def *d1, const Def *d2)
static const Def *	coerce (const Def *type, const Def *value)
	Can value be assigned to sth of type?
static const Def *	is_uniform (Defs defs)
	Yields defs.front(), if all defs are Check::alpha-equivalent (Mode::Test) and nullptr otherwise.

Detailed Description

Definition at line 76 of file check.h.

Member Enumeration Documentation

Mode

enum mim::Check::Mode

Enumerator
C	In Mode::Check, type inference is happening and Holes will be resolved, if possible. Also, two free but different Vars are considered α-equivalent.
T	In Mode::Test, no type inference is happening and Holes will not be touched. Also, Two free but different Vars are not considered α-equivalent.

Definition at line 83 of file check.h.

Constructor & Destructor Documentation

Check()

mim::Check::Check ( World & world )

inlineexplicit

Definition at line 78 of file check.h.

References world().

Referenced by alpha(), and coerce().

Member Function Documentation

alpha()

template<Mode mode = C>

bool mim::Check::alpha ( const Def * d1, const Def * d2 )

inlinestatic

Definition at line 93 of file check.h.

References Check(), and mim::Def::world().

Referenced by mim::Match::accepts(), mim::Def::check(), mim::ast::MatchExpr::Arm::emit(), mim::World::inj(), is_uniform(), mim::level_of(), mim::World::match(), mim::World::solve_levels(), and test_alpha().

coerce()

const Def * mim::Check::coerce ( const Def * type, const Def * value )

inlinestaticnodiscard

Can value be assigned to sth of type?

Note

This is different from equiv(type, value->type()) since type may be dependent.

Definition at line 105 of file check.h.

References Check(), and mim::Def::type().

Referenced by mim::World::app(), mim::ast::assign(), mim::Def::check(), mim::Def::check(), mim::World::inj(), mim::World::inj(), mim::World::name(), and mim::World::tuple().

is_uniform()

const Def * mim::Check::is_uniform ( Defs defs )

static

Yields defs.front(), if all defs are Check::alpha-equivalent (Mode::Test) and nullptr otherwise.

Definition at line 120 of file check.cpp.

References alpha().

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

test_alpha()

bool mim::Check::test_alpha ( const Def * d1, const Def * d2 )

inlinestatic

Definition at line 101 of file check.h.

References alpha().

Referenced by mim::Match::accepts(), mim::World::inj(), and mim::plug::refly::normalize_alpha().

world()

World & mim::Check::world ( )

inline

Definition at line 81 of file check.h.

Referenced by Check().

---

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

• include/mim/check.h
• src/mim/check.cpp