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

DDC.Type.Transform.SubstituteT

Description

Capture avoiding substitution of types in types.

Synopsis

# Documentation

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

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 Source #

Wrapper for substituteT to substitute multiple things.

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

Substitute a Type for Bound in some thing.

class SubstituteT c where Source #

Minimal complete definition

substituteWithT

Methods

substituteWithT :: forall n. Ord n => Bound n -> Type n -> Set n -> BindStack n -> c n -> c n Source #

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

 Source # MethodssubstituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> TypeSum n -> TypeSum n Source # Source # MethodssubstituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> Type n -> Type n Source # Source # MethodssubstituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> Bind n -> Bind n Source #

data BindStack n Source #

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

Constructors

 BindStack FieldsstackBinds :: ![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 :: !IntNumber of BAnon in stackBinds.stackNamed :: !IntNumber of BName in stackBinds.

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]) Source #

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

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.