ddc-core-0.4.3.1: Disciplined Disciple Compiler core language and type checker.

Safe HaskellSafe
LanguageHaskell98

DDC.Core.Transform.SubstituteWX

Description

Capture avoiding substitution of witnesses in expressions.

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

Synopsis

Documentation

class SubstituteWX c where Source #

Minimal complete definition

substituteWithWX

Methods

substituteWithWX :: forall a n. Ord n => Witness a n -> Sub n -> c a n -> c a n Source #

Instances

SubstituteWX Witness Source # 

Methods

substituteWithWX :: Ord n => Witness a n -> Sub n -> Witness a n -> Witness a n Source #

SubstituteWX Cast Source # 

Methods

substituteWithWX :: Ord n => Witness a n -> Sub n -> Cast a n -> Cast a n Source #

SubstituteWX Alt Source # 

Methods

substituteWithWX :: Ord n => Witness a n -> Sub n -> Alt a n -> Alt a n Source #

SubstituteWX Exp Source # 

Methods

substituteWithWX :: Ord n => Witness a n -> Sub n -> Exp a n -> Exp a n Source #

substituteWX :: (Ord n, SubstituteWX c) => Bind n -> Witness a n -> c a n -> c a n Source #

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

substituteWXs :: (Ord n, SubstituteWX c) => [(Bind n, Witness a n)] -> c a n -> c a n Source #

Wrapper for substituteWithWX to substitute multiple things.