DDC.Type.Transform.SubstituteT

Capture avoiding substitution of types in types.

Documentation

substituteT :: (SubstituteT c, Ord n) => Bind n -> Type n -> c n -> c n

Substitute a Type for the Bound corresponding to some Bind in a thing.

substituteTs :: (SubstituteT c, Ord n) => [(Bind n, Type n)] -> c n -> c n

Wrapper for substituteT to substitute multiple things.

substituteBoundT :: (SubstituteT c, Ord n) => Bound n -> Type n -> c n -> c n

Substitute a Type for Bound in some thing.

class SubstituteT c where

Methods

substituteWithT

Arguments

:: forall n . Ord n

=> Bound n

Bound variable that we're subsituting into.

-> Type n

Type to substitute.

-> Set n

Names of free varaibles in the type to substitute.

-> BindStack n

Bind stack.

-> c n

-> c n

Substitute a type into some thing. In the target, if we find a named binder that would capture a free variable in the type to substitute, then we rewrite that binder to anonymous form, avoiding the capture.

Instances

SubstituteT TypeSum

SubstituteT Type

SubstituteT Bind

data BindStack n

Stack of anonymous binders that we've entered under during substitution.

Constructors

BindStack

Fields

stackBinds :: ![Bind n]

Holds anonymous binders that were already in the program, as well as named binders that are being rewritten to anonymous ones. In the resulting expression all these binders will be anonymous.

stackAll :: ![Bind n]

Holds all binders, independent of whether they are being rewritten or not.

stackAnons :: !Int

Number of BAnon in stackBinds.

stackNamed :: !Int

Number of BName in stackBinds.

pushBind

Arguments

:: Ord n

=> Set n

Names that need to be rewritten.

-> BindStack n

Current bind stack.

-> Bind n

Bind to push.

-> (BindStack n, Bind n)

New stack and possibly anonymised bind.

Push a bind onto a bind stack, anonymizing it if need be to avoid variable capture.

pushBinds :: Ord n => Set n -> BindStack n -> [Bind n] -> (BindStack n, [Bind n])

Push several binds onto the bind stack, anonymyzing them if need be to avoid variable capture.

substBound

Arguments

:: Ord n

=> BindStack n

Current Bind stack during substitution.

-> Bound n

Bound we're substituting for.

-> Bound n

Bound we're looking at now.

-> Either (Bound n) Int

Compare a Bound against the one we're substituting for.