DDC.Core.Transform.SubstituteXX

Capture avoiding substitution of expressions in expressions.

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

Documentation

class SubstituteXX c where

Minimal complete definition

substituteWithXX

Methods

substituteWithXX :: forall a n. Ord n => Exp a n -> Sub n -> c a n -> c a n

Instances

SubstituteXX Cast

Methods

substituteWithXX :: Ord n => Exp a n -> Sub n -> Cast a n -> Cast a n

SubstituteXX Alt

Methods

substituteWithXX :: Ord n => Exp a n -> Sub n -> Alt a n -> Alt a n

SubstituteXX Exp

Methods

substituteWithXX :: Ord n => Exp a n -> Sub n -> Exp a n -> Exp a n

substituteXX :: (Ord n, SubstituteXX c) => Bind n -> Exp a n -> c a n -> c a n

Wrapper for substituteWithX that determines the set of free names in the expression being substituted, and starts with an empty binder stack.

substituteXXs :: (Ord n, SubstituteXX c) => [(Bind n, Exp a n)] -> c a n -> c a n

Wrapper for substituteX to substitute multiple expressions.

substituteXArg :: (Ord n, SubstituteXX c, SubstituteWX c, SubstituteTX (c a)) => Bind n -> Exp a n -> c a n -> c a n

Substitute the argument of an application into an expression. Perform type substitution for an XType and witness substitution for an XWitness

substituteXArgs :: (Ord n, SubstituteXX c, SubstituteWX c, SubstituteTX (c a)) => [(Bind n, Exp a n)] -> c a n -> c a n

Wrapper for substituteXArgs to substitute multiple arguments.