#include <mim/check.h>

Public Types
enum	Mode { Check , Test }

Public Member Functions
	Checker (World &world)

World &	world ()

Static Public Member Functions
template<Mode mode>
static bool	alpha (const Def d1, const Def d2)

static const Def *	assignable (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 55 of file check.h.

Member Enumeration Documentation

◆ Mode

enum mim::Checker::Mode

Enumerator

Check

In Mode::Check, type inference is happening and Holes will be resolved, if possible.

Also, two free but different Vars are considered α-equivalent.

Test

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 62 of file check.h.

Constructor & Destructor Documentation

◆ Checker()

mim::Checker::Checker ( World & world )

inline

Definition at line 57 of file check.h.

References world().

Referenced by alpha(), and assignable().

Member Function Documentation

◆ alpha()

template<Mode mode>

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

inlinestatic

Definition at line 71 of file check.h.

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

Referenced by mim::Arr::check(), mim::Pi::check(), mim::Sigma::check(), mim::World::extract(), mim::World::insert(), is_uniform(), mim::Axiom::rebuild_(), and mim::World::test().

◆ assignable()

static const Def * mim::Checker::assignable	(	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 77 of file check.h.

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

Referenced by mim::World::app(), mim::Lam::check(), mim::World::insert(), and mim::World::tuple().

◆ is_uniform()

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

static

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

Definition at line 240 of file check.cpp.

References alpha().

Referenced by mim::World::sigma(), and mim::World::tuple().

◆ world()

World & mim::Checker::world ( )

inline

Definition at line 60 of file check.h.

Referenced by Checker().

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

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

Public Types

Public Member Functions

Static Public Member Functions