ddc-core- Disciple Core language and type checker.

Safe HaskellSafe-Infered



Capture avoiding substitution of types in types.



class SubstituteT c whereSource




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

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.

data BindStack n Source

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




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.



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



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