Combined η-normalization: folds η-reduction and η-expansion into a single, idempotent phase. More...
#include <mim/phase/eta_conv.h>
Public Member Functions | |
| EtaConv (World &world) | |
| EtaConv (World &world, flags_t annex) | |
| Public Member Functions inherited from mim::InplaceRWPhase | |
| InplaceRWPhase (World &world, std::string name, Analysis *analysis=nullptr) | |
| InplaceRWPhase (World &world, flags_t annex, Analysis *analysis=nullptr) | |
| World & | world () |
| bool | rewrite_annexes () const override |
| void | rewrite_annex (flags_t, Sym, const Def *) override |
| void | rewrite_external (Def *) override |
| Public Member Functions inherited from mim::RWBase | |
| Analysis * | analysis () |
| const Analysis * | analysis () const |
| const Def * | lattice (const Def *def) const |
Returns the abstract value computed by the associated Analysis for def, or nullptr if no value is available. | |
| const Def * | abstracted (const Def *def) const |
Returns lattice(def) if it differs from def (i.e. we learned something), otherwise nullptr. | |
| bool | is_bootstrapping () const |
| Returns whether we are currently bootstrapping (rewriting annexes). | |
| 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 (std::unique_ptr< World > &&ptr) | |
| Rewriter (World &world) | |
| virtual | ~Rewriter () |
| void | reset (std::unique_ptr< World > &&ptr) |
| void | reset () |
| World & | world () |
| virtual void | push () |
| virtual void | pop () |
| virtual const Def * | map (const Def *old_def, const Def *new_def) |
| const Def * | map_root (const Def *old_def, const Def *new_def) |
| Like map() but records into the root map, so the entry outlives the current push()/pop() scope. | |
| 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 * | lookup (const Def *old_def) |
| Lookup old_def by searching in reverse through the stack of maps. | |
| virtual const Def * | rewrite_imm (const Def *) |
| virtual const Def * | rewrite_stub (Def *, Def *) |
| virtual DefVec | rewrite (Defs) |
| virtual const Def * | rewrite_imm_Seq (const Seq *seq) |
| virtual const Def * | rewrite_mut_Seq (Seq *seq) |
Private Member Functions | |
| bool | analyze () final |
| Runs the optional pre-analysis on Phase::world, typically to a fixed point, before rewriting begins. | |
| const Def * | rewrite_root (const Def *def) final |
| An annex or external must keep its shape: neither η-reduce nor η-expand a root. | |
| const Def * | rewrite (const Def *) final |
| const Def * | rewrite_imm_App (const App *) final |
| const Def * | rewrite_imm_Var (const Var *) final |
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. | |
| const Def * | rewrite_mut (Def *mut) override |
| Protected Member Functions inherited from mim::RWBase | |
| void | start () override |
| Actual entry. | |
| virtual void | finalize () |
| Run after all roots have been walked - but for an RWPhase still before the two worlds are swapped. | |
| RWBase (World &world, std::string name, Analysis *analysis) | |
| RWBase (World &world, flags_t annex, Analysis *analysis) | |
| RWBase (World &world, std::string name, Analysis *analysis, std::unique_ptr< World > &&new_world) | |
Rewrite the World of Phase::world into new_world. | |
| RWBase (World &world, flags_t annex, Analysis *analysis, std::unique_ptr< World > &&new_world) | |
| Protected Member Functions inherited from mim::Rewriter | |
| auto | enter (Def *new_mut) |
Updates curr_mut() to new_mut and restores it at the end of the scope. | |
| Protected Attributes inherited from mim::Phase | |
| std::string | name_ |
| Protected Attributes inherited from mim::Rewriter | |
| std::deque< Def2Def > | old2news_ |
Combined η-normalization: folds η-reduction and η-expansion into a single, idempotent phase.
A Lam should appear either only in callee position (Known) or not (Unknown). A Lam that occurs in an unknown position more than once (Unknown_N) or in both positions (Both) is η-expanded (g f -> g (λx.f x)); a genuine η-redex λx.f x whose f does not want to be expanded is η-reduced.
The analysis is wrapper-transparent: a use of a wrapper λx.f x is counted as a use of f at the same position/multiplicity instead of counting f as Known (the wrapper's callee). This makes f's classification identical whether f is bare or wrapped, so the canonical η-form is a genuine fixed point - the phase does not fight itself and can share one big compile.phases tt fixed-point loop with BetaRed and mem.seo without oscillating.
Definition at line 21 of file eta_conv.h.
|
inline |
Definition at line 23 of file eta_conv.h.
References mim::InplaceRWPhase::InplaceRWPhase(), and mim::InplaceRWPhase::world().
Definition at line 25 of file eta_conv.h.
References mim::Phase::annex(), mim::InplaceRWPhase::InplaceRWPhase(), and mim::InplaceRWPhase::world().
|
finalprivatevirtual |
Runs the optional pre-analysis on Phase::world, typically to a fixed point, before rewriting begins.
If analysis() is set, this is the natural place to iterate until Phase::todo() becomes false. If no Analysis is needed, simply return false.
Reimplemented from mim::RWBase.
Definition at line 5 of file eta_conv.cpp.
References mim::InplaceRWPhase::world().
Reimplemented from mim::Rewriter.
Definition at line 37 of file eta_conv.cpp.
References mim::Lam::eta_expand(), mim::Phase::invalidate(), mim::Def::is_ground(), mim::Phase::log(), mim::Phase::profile_count(), rewrite(), and mim::Rewriter::rewrite().
Referenced by rewrite(), and rewrite_imm_App().
Definition at line 78 of file eta_conv.cpp.
References mim::World::app(), mim::App::arg(), mim::App::callee(), rewrite(), and mim::InplaceRWPhase::world().
Definition at line 83 of file eta_conv.cpp.
References mim::Var::binder(), mim::World::var(), and mim::InplaceRWPhase::world().
An annex or external must keep its shape: neither η-reduce nor η-expand a root.
Reimplemented from mim::RWBase.
Definition at line 82 of file eta_conv.h.
References rewrite_root().
Referenced by rewrite_root().