DDC.Type.Transform.BoundT

Lifting and lowering of deBruijn indices in types.

Documentation

liftT :: MapBoundT c n => Int -> c n -> c n

Wrapper for liftAtDepthX that starts at depth 0.

liftAtDepthT

Arguments

:: MapBoundT c n

=> Int

Number of levels to lift.

-> Int

Current binding depth.

-> c n

Lift expression indices in this thing.

-> c n

Lift debruijn indices less than or equal to the given depth.

lowerT :: MapBoundT c n => Int -> c n -> c n

Wrapper for lowerAtDepthX that starts at depth 0.

lowerAtDepthT

Arguments

:: MapBoundT c n

=> Int

Number of levels to lower.

-> Int

Current binding depth.

-> c n

Lower expression indices in this thing.

-> c n

Lower debruijn indices less than or equal to the given depth.

class MapBoundT c n where

Minimal complete definition

mapBoundAtDepthT

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> c n -> c n

Apply a function to all bound variables in the program. The function is passed the current binding depth. This is used to defined both liftT and lowerT.

Instances

Ord n => MapBoundT TypeSum n

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> TypeSum n -> TypeSum n

Ord n => MapBoundT Type n

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Type n -> Type n

MapBoundT Bound n

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Bound n -> Bound n

Ord n => MapBoundT Bind n

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Bind n -> Bind n