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

Safe HaskellSafe-Inferred

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 nSource

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

substituteTs :: (SubstituteT c, Ord n) => [(Bind n, Type n)] -> c n -> c nSource

Wrapper for substituteT to substitute multiple things.

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

Substitute a Type for Bound in some thing.

class SubstituteT c whereSource

Methods

substituteWithTSource

Arguments

:: forall n . Ord n 
=> Bound n

Bound variable that we're subsituting into.

-> Type n

Type to substitute.

-> Set n

Names of free varaibles in the type to substitute.

-> BindStack n

Bind stack.

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

data BindStack n Source

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.

pushBindSource

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.

substBoundSource

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.