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 a 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

Minimal complete definition

substituteWithT

Methods

substituteWithT :: forall n. Ord n => Bound n -> Type n -> Set n -> BindStack n -> 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

Methods

substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> TypeSum n -> TypeSum n

SubstituteT Type

Methods

substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> Type n -> Type n

SubstituteT Bind

Methods

substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> Bind n -> Bind n

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.