DDC.Core.Transform.SubstituteTX

Capture avoiding substitution of types in expressions.

If a binder would capture a variable then it is anonymized to deBruijn form.

Documentation

class SubstituteTX c where

Minimal complete definition

substituteWithTX

Methods

substituteWithTX :: forall n. Ord n => Type n -> Sub n -> c n -> c n

Instances

SubstituteTX Type

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Type n -> Type n

SubstituteTX Bind

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Bind n -> Bind n

SubstituteTX (Witness a)

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Witness a n -> Witness a n

SubstituteTX (Cast a)

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Cast a n -> Cast a n

SubstituteTX (Alt a)

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Alt a n -> Alt a n

SubstituteTX (Exp a)

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Exp a n -> Exp a n

substituteTX :: (SubstituteTX c, Ord n) => Bind n -> Type n -> c n -> c n

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

substituteTXs :: (SubstituteTX c, Ord n) => [(Bind n, Type n)] -> c n -> c n

Wrapper for substituteT to substitute multiple types.

substituteBoundTX :: (SubstituteTX c, Ord n) => Bound n -> Type n -> c n -> c n

Substitute a Type for a Bound in some thing.