Eliminates all types that have exactly one inhabitant, so that no Single/Wrap ever reaches a backend. More...

#include <mim/phase/single_erasure.h>

Inheritance diagram for mim::SingleErasure:

Public Member Functions
	SingleErasure (World &world, std::string name)
	SingleErasure (World &world, flags_t annex)
Public Member Functions inherited from mim::RWPhase
	RWPhase (World &world, std::string name, Analysis *analysis=nullptr)
	RWPhase (World &world, flags_t annex, Analysis *analysis=nullptr)
Analysis *	analysis ()
const Analysis *	analysis () const
const Def *	lattice (const Def *old_def) const
	Returns the abstract value computed by the associated Analysis for the given old-world Def, or nullptr if no value is available.
const Def *	abstracted (const Def *old_def) const
	Returns lattice(`old_def`) if it differs from `old_def` (i.e. we learned something), otherwise nullptr.
bool	is_top (const Def *old_def) const
virtual bool	analyze ()
	Runs the optional pre-analysis on old_world(), typically to a fixed point, before rewriting begins.
virtual void	rewrite_external (Def *)
const Def *	lookup (const Def *) override
	Lookup old_def by searching in reverse through the stack of maps.
World &	world ()=delete
	Hides both and forbids direct access.
World &	old_world ()
	Get old Defs from here.
World &	new_world ()
	Create new Defs into this.
Public Member Functions inherited from mim::Phase
	Phase (World &world, std::string name)
	Phase (World &world, flags_t annex)
virtual	~Phase ()=default
virtual std::unique_ptr< Phase >	recreate ()
	Creates a new instance; needed by a fixed-point PhaseMan.
virtual void	apply (const App *)
	Invoked if your Phase has additional args.
virtual void	apply (Phase &)
	Dito, but invoked by Phase::recreate.
virtual bool	redirects () const
	If true, Phase::create uses take_resolved().
virtual std::unique_ptr< Phase >	take_resolved ()
	The Phase to use instead; nullptr means elide.
World &	world ()
Driver &	driver ()
const fe::Log &	log () const
std::string_view	name () const
flags_t	annex () const
const fe::Vector< std::string > &	args ()
	Command-line arguments passed to this Phase's plugin via -X <plugin>:<arg>.
bool	todo () const
void	invalidate (bool todo=true)
	Signals that another round of fixed-point iteration is required, either as part of.
virtual void	run ()
	Entry point and generates some debug output; invokes Phase::start.
void	profile_count (std::string_view key, uint64_t n=1)
	Adds `n` to the custom fe::Profiler counter `key` of the current run; no-op unless profiling is enabled.
Public Member Functions inherited from mim::Rewriter
template<class D = Def>
D *	curr_mut () const
	Rewriter (World &world)
virtual	~Rewriter ()
void	reset ()
World &	world ()
void	push (Vars old_vars={}, Vars new_vars={})
void	pop ()
void	bind_old (const Var *var)
	Adds the old `var` - if any - to the innermost scope.
void	bind_new (const Var *var)
	Adds the new `var` - if any - to the innermost scope.
void	bind (const Var old_var, const Var new_var)
const Def *	map (const Def old_def, const Def new_def)
const Def *	map (const Def *old_def, Defs new_defs)
const Def *	map (Defs old_defs, const Def *new_def)
const Def *	map (Defs old_defs, Defs new_defs)
virtual const Def *	rewrite (const Def *)
virtual const Def *	rewrite_imm (const Def *)
virtual const Def *	rewrite_mut (Def *)
const Def *	rewrite_stub (Def old_mut, Def new_mut, fe::View< size_t > new2old)
	Like above, but `new_mut` may have a different number of ops than `old_mut:` new_mut->op(i) is rewritten from old_mut->op(new2old[i]).
virtual DefVec	rewrite (Defs)
virtual const Def *	rewrite_imm_Lit (const Lit *)
virtual const Def *	rewrite_imm_Axm (const Axm *)
virtual const Def *	rewrite_imm_Var (const Var *)
virtual const Def *	rewrite_imm_Proxy (const Proxy *)
virtual const Def *	rewrite_imm_Type (const Type *)
virtual const Def *	rewrite_imm_Level (const Level *)
virtual const Def *	rewrite_imm_LMax (const LMax *)
virtual const Def *	rewrite_imm_LSucc (const LSucc *)
virtual const Def *	rewrite_imm_Pi (const Pi *)
virtual const Def *	rewrite_imm_Lam (const Lam *)
virtual const Def *	rewrite_imm_Arr (const Arr *)
virtual const Def *	rewrite_imm_Pack (const Pack *)
virtual const Def *	rewrite_imm_Join (const Join *)
virtual const Def *	rewrite_imm_Top (const Top *)
virtual const Def *	rewrite_imm_Bot (const Bot *)
virtual const Def *	rewrite_imm_Reform (const Reform *)
virtual const Def *	rewrite_imm_Rule (const Rule *)
virtual const Def *	rewrite_imm_Nat (const Nat *)
virtual const Def *	rewrite_imm_Idx (const Idx *)
virtual const Def *	rewrite_imm_Nom (const Nom *)
virtual const Def *	rewrite_imm_Name (const Name *)
virtual const Def *	rewrite_imm_Struc (const Struc *)
virtual const Def *	rewrite_mut_Hole (Hole *)
virtual const Def *	rewrite_mut_Pi (Pi *)
virtual const Def *	rewrite_mut_Lam (Lam *)
virtual const Def *	rewrite_mut_Arr (Arr *)
virtual const Def *	rewrite_mut_Pack (Pack *)
virtual const Def *	rewrite_mut_Variant (Variant *)
virtual const Def *	rewrite_mut_Rule (Rule *)

Private Member Functions
const Def *	rewrite_imm_Single (const Single *) final
const Def *	rewrite_imm_Wrap (const Wrap *) final
const Def *	rewrite_imm_Variant (const Variant *) final
const Def *	rewrite_imm_Inj (const Inj *) final
const Def *	rewrite_imm_Match (const Match *) final
const Def *	rewrite_imm_Sigma (const Sigma *) final
const Def *	rewrite_mut_Sigma (Sigma *) final
const Def *	rewrite_imm_Tuple (const Tuple *) final
const Def *	rewrite_imm_Extract (const Extract *) final
const Def *	rewrite_imm_Insert (const Insert *) final
const Def *	rewrite_imm_Seq (const Seq *) final
const Def *	rewrite_mut_Seq (Seq *) final
Erasure
All arguments live in old_world(), all results in new_world().

Additional Inherited Members
Static Public Member Functions inherited from mim::Phase
static std::unique_ptr< Phase >	create (const Flags2Phases &phases, const Def *def)
template<class A, class P>
static void	hook (Flags2Phases &phases)
template<class P, class... Args>
static void	run (Args &&... args)
	Runs a single Phase.
Protected Member Functions inherited from mim::RWPhase
void	start () override
	Actual entry.
virtual void	finalize ()
	Run after all roots have been walked but still before the two worlds are swapped.
const Def *	rewrite_imm_App (const App *) override
const Def *	rewrite_stub (Def , Def ) override
const Def *	coerce (const Def new_type, const Def new_val)
	Converts the new `new_val` into a value of the new `new_type`, where a checking position demands it.
const Def *	rewrite_stub (Def old_mut, Def new_mut, fe::View< size_t > new2old)
	Like above, but `new_mut` may have a different number of ops than `old_mut:` new_mut->op(i) is rewritten from old_mut->op(new2old[i]).
Protected Member Functions inherited from mim::Rewriter
Def2Def &	old2new ()
	The map of the innermost push() scope.
bool	has_intersection (const Def *old_def)
	Does `old_def` depend on the old Vars of any scope?
auto	enter (Def *new_mut)
	Updates curr_mut() to `new_mut` and restores it at the end of the scope.
const Def *	seal (Def old_mut, Def new_mut)
	The tail of rewrite_stub: immutabilizes `new_mut` in hindsight, as rewriting may have made it vacuous.
static bool	splittable (const Def *type)
	Does coerce() explode and reassemble values of `type`?
Protected Attributes inherited from mim::Phase
std::string	name_
Protected Attributes inherited from mim::Rewriter
fe::Vector< Scope >	scopes_

Detailed Description

Eliminates all types that have exactly one inhabitant, so that no Single/Wrap ever reaches a backend.

Such a type carries no information, so its erasure is the unit: «e» becomes [] and ‹e› becomes (). Within an aggregate the component is dropped altogether, which shifts the indices of its successors. Besides Single this also catches the unit [] and Idx 1 - and any aggregate built from those. A Variant with a single case | A is isomorphic to A and erased to it. A singleton above * has no unit to erase to and degrades to the type of its inhabitant instead. Where an erased value meets a shape that still demands its components (e.g. an Axm's signature), it is coerce()d: dropped components are re-inserted as their sole inhabitants, and Cns are η-wrapped.

Definition at line 15 of file single_erasure.h.

Constructor & Destructor Documentation

◆ SingleErasure() [1/2]

mim::SingleErasure::SingleErasure	(	World &	world,
		std::string	name )

inline

Definition at line 17 of file single_erasure.h.

References mim::Phase::name(), mim::RWPhase::RWPhase(), and mim::RWPhase::world().

◆ SingleErasure() [2/2]

mim::SingleErasure::SingleErasure	(	World &	world,
		flags_t	annex )

inline

Definition at line 19 of file single_erasure.h.

References mim::Phase::annex(), mim::RWPhase::RWPhase(), and mim::RWPhase::world().

Member Function Documentation

◆ rewrite_imm_Extract()

const Def * mim::SingleErasure::rewrite_imm_Extract ( const Extract * extract )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 84 of file single_erasure.cpp.

References mim::World::extract(), mim::Extract::index(), mim::RWPhase::new_world(), mim::RWPhase::old_world(), mim::Rewriter::rewrite(), mim::Rewriter::rewrite_imm_Extract(), mim::Extract::tuple(), and mim::Def::type().

◆ rewrite_imm_Inj()

const Def * mim::SingleErasure::rewrite_imm_Inj ( const Inj * inj )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 54 of file single_erasure.cpp.

References mim::Variant::isa_lone(), mim::Rewriter::rewrite(), mim::Rewriter::rewrite_imm_Inj(), mim::Def::type(), and mim::Inj::value().

◆ rewrite_imm_Insert()

const Def * mim::SingleErasure::rewrite_imm_Insert ( const Insert * insert )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 96 of file single_erasure.cpp.

References mim::World::insert(), mim::RWPhase::new_world(), mim::RWPhase::old_world(), mim::Rewriter::rewrite(), and mim::Rewriter::rewrite_imm_Insert().

◆ rewrite_imm_Match()

const Def * mim::SingleErasure::rewrite_imm_Match ( const Match * match )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 59 of file single_erasure.cpp.

References mim::World::app(), mim::Match::arm(), mim::Variant::isa_lone(), mim::RWPhase::new_world(), mim::Rewriter::rewrite(), mim::Rewriter::rewrite_imm_Match(), mim::Match::scrutinee(), and mim::Def::unfold_type().

◆ rewrite_imm_Seq()

const Def * mim::SingleErasure::rewrite_imm_Seq ( const Seq * seq )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 109 of file single_erasure.cpp.

References mim::Def::is_intro(), mim::RWPhase::new_world(), mim::RWPhase::old_world(), mim::World::prod(), mim::Rewriter::rewrite_imm_Seq(), and mim::Def::type().

◆ rewrite_imm_Sigma()

const Def * mim::SingleErasure::rewrite_imm_Sigma ( const Sigma * sigma )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 65 of file single_erasure.cpp.

References mim::RWPhase::new_world(), mim::Def::ops(), mim::Rewriter::rewrite(), mim::Rewriter::rewrite_imm_Sigma(), and mim::World::sigma().

◆ rewrite_imm_Single()

const Def * mim::SingleErasure::rewrite_imm_Single ( const Single * single )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 37 of file single_erasure.cpp.

References mim::Phase::log(), and mim::Phase::profile_count().

◆ rewrite_imm_Tuple()

const Def * mim::SingleErasure::rewrite_imm_Tuple ( const Tuple * tuple )

finalprivatevirtual

Reimplemented from mim::RWPhase.

Definition at line 79 of file single_erasure.cpp.

References mim::RWPhase::old_world(), mim::RWPhase::rewrite_imm_Tuple(), and mim::Def::type().

◆ rewrite_imm_Variant()

const Def * mim::SingleErasure::rewrite_imm_Variant ( const Variant * variant )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 49 of file single_erasure.cpp.

References mim::Variant::isa_lone(), mim::Rewriter::rewrite(), and mim::Rewriter::rewrite_imm_Variant().

◆ rewrite_imm_Wrap()

const Def * mim::SingleErasure::rewrite_imm_Wrap ( const Wrap * wrap )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 44 of file single_erasure.cpp.

References mim::Phase::profile_count().

◆ rewrite_mut_Seq()

const Def * mim::SingleErasure::rewrite_mut_Seq ( Seq * seq )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 114 of file single_erasure.cpp.

References mim::Seq::body(), mim::Def::is_intro(), mim::Def::is_set(), mim::RWPhase::new_world(), mim::RWPhase::old_world(), mim::World::prod(), mim::Rewriter::rewrite_mut_Seq(), and mim::Def::type().

◆ rewrite_mut_Sigma()

const Def * mim::SingleErasure::rewrite_mut_Sigma ( Sigma * old_sigma )

finalprivatevirtual

Reimplemented from mim::Rewriter.

Definition at line 71 of file single_erasure.cpp.

References mim::World::mut_sigma(), mim::RWPhase::new_world(), mim::Rewriter::rewrite(), mim::Rewriter::rewrite_mut_Sigma(), mim::RWPhase::rewrite_stub(), and mim::Def::type().

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

include/mim/phase/single_erasure.h
src/mim/phase/single_erasure.cpp

Public Member Functions

Private Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ SingleErasure() [1/2]

◆ SingleErasure() [2/2]

Member Function Documentation

◆ rewrite_imm_Extract()

◆ rewrite_imm_Inj()

◆ rewrite_imm_Insert()

◆ rewrite_imm_Match()

◆ rewrite_imm_Seq()

◆ rewrite_imm_Sigma()

◆ rewrite_imm_Single()

◆ rewrite_imm_Tuple()

◆ rewrite_imm_Variant()

◆ rewrite_imm_Wrap()

◆ rewrite_mut_Seq()

◆ rewrite_mut_Sigma()