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

DDC.Type.Transform.BoundT

Description

Lifting and lowering of deBruijn indices in types.

Synopsis

# Documentation

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

Wrapper for liftAtDepthX that starts at depth 0.

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

Wrapper for lowerAtDepthX that starts at depth 0.

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

Minimal complete definition

mapBoundAtDepthT

Methods

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

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 Source # MethodsmapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> TypeSum n -> TypeSum n Source # Ord n => MapBoundT Type n Source # MethodsmapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Type n -> Type n Source # Source # MethodsmapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Bound n -> Bound n Source # Ord n => MapBoundT Bind n Source # MethodsmapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Bind n -> Bind n Source #