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

Safe HaskellSafe-Inferred

DDC.Type.Transform.LiftT

Description

Lifting of deBruijn indices in a type.

Synopsis

Documentation

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

Wrapper for liftAtDepthX that starts at depth 0.

liftAtDepthTSource

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 nSource

Wrapper for lowerAtDepthX that starts at depth 0.

lowerAtDepthTSource

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 whereSource

Methods

mapBoundAtDepthTSource

Arguments

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

Function to apply to the bound occ. It is passed the current binding depth.

-> Int

Current binding depth.

-> c n

Lift expression indices in this thing.

-> 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 
Ord n => MapBoundT Type n 
MapBoundT Bound n 
Ord n => MapBoundT Bind n 
Ord n => MapBoundT (Witness a) n 
Ord n => MapBoundT (Cast a) n 
Ord n => MapBoundT (Alt a) n 
Ord n => MapBoundT (Exp a) n