Safe Haskell	Safe
Language	Haskell2010

ReWire.Eidos.Subst

Description

Substitution and binder-refreshing for Eidos (doc/eidos.md §2, G2).

The uniqueness discipline makes substitution an environment map — no capture is possible while the invariant holds — and concentrates the invariant's maintenance in ONE primitive: refreshExp/refreshDefn, the audited clone. Every pass that duplicates a term (inlining, specialization, beta reduction, case-of-known-constructor) must route the duplicated copy through a refresh; the linter's uniqueness rule re-checks the invariant globally under --debug-lint.

Contracts:

substVars inserts each payload AS IS: sound only when each payload lands at most once (or is binder-free). For the general case use substVarsRefreshing, which refreshes every inserted copy.
refreshExp freshens every binder in the term (term binders, join labels, and — via refreshDefn — signature type variables, propagating the renaming through every type in the body) and leaves free names untouched.
Supplies: passes obtain fresh uniques from a state seeded above the program's maximum (nextUniq).

Synopsis

maxUniq :: Data a => a -> Uniq
nextUniq :: Data a => a -> Uniq
refreshExp :: MonadState Uniq m => Exp -> m Exp
refreshDefn :: MonadState Uniq m => Defn -> m Defn
instantiateDefn :: MonadState Uniq m => Text -> [Ty] -> Defn -> m Defn
substVars :: IntMap Exp -> Exp -> Exp
substVarsRefreshing :: MonadState Uniq m => IntMap Exp -> Exp -> m Exp
occCounts :: Exp -> IntMap Int
freeUniqs :: Exp -> IntSet
occIds :: Exp -> IntMap Id

Documentation

maxUniq :: Data a => a -> Uniq Source #

The largest unique occurring anywhere in a program — or any other Data value holding Ids and TyVars — (binders and occurrences; the primitive basis' negative uniques never win).

nextUniq :: Data a => a -> Uniq Source #

A safe starting value for a pass's unique supply.

refreshExp :: MonadState Uniq m => Exp -> m Exp Source #

Freshen every binder in an expression; free names (and all types, when no signature variables are being renamed) are untouched.

refreshDefn :: MonadState Uniq m => Defn -> m Defn Source #

Clone a definition with fresh binders throughout: a fresh definition name (self-references in the body follow it), fresh signature type variables (the renaming propagates through every type in the parameters and body), and fresh parameter and local binders.

instantiateDefn :: MonadState Uniq m => Text -> [Ty] -> Defn -> m Defn Source #

Clone a definition at a type instantiation (the specializer's flavor of the audited clone): the signature's variables are substituted away by the given type arguments (the clone is monomorphic when they are closed), every type in the parameters and body follows, and every binder is refreshed. The clone is named by the given occurrence text with a fresh unique; self-references in the body are NOT remapped — they still name the origin at its instantiated type arguments, for the caller's spine rewrite to resolve.

substVars :: IntMap Exp -> Exp -> Exp Source #

Substitute expressions for variable occurrences (by unique). Each payload is inserted as is: use only when each payload can land at most once, or is binder-free; otherwise use substVarsRefreshing.

substVarsRefreshing :: MonadState Uniq m => IntMap Exp -> Exp -> m Exp Source #

Substitute expressions for variable occurrences, refreshing every inserted copy (the uniqueness-preserving form).

occCounts :: Exp -> IntMap Int Source #

Variable- and jump-occurrence counts by unique (an occurrence of a join label at a jump counts for the label's Id). Dead binders are absent from the map.

freeUniqs :: Exp -> IntSet Source #

The free variables of an expression, by unique: occurrences whose binding site is not within the expression. (Global binder uniqueness makes this a plain set difference — no shadowing is possible.)

occIds :: Exp -> IntMap Id Source #

One representative occurrence Id per occurring unique. An occurrence carries its binder's signature, so this recovers binder Ids (e.g. for captured locals) without an enclosing environment.