DDC.Core.Transform.BoundX

Lifting and lowering level-0 deBruijn indices in core things.

Level-0 indices are used for both value and witness variables.

Documentation

liftX :: MapBoundX c n => Int -> c n -> c n

Wrapper for liftAtDepthX that starts at depth 0.

liftAtDepthX

Arguments

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

lowerX :: MapBoundX c n => Int -> c n -> c n

Wrapper for lowerAtDepthX that starts at depth 0.

lowerAtDepthX

Arguments

:: MapBoundX 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 MapBoundX c n where

Minimal complete definition

mapBoundAtDepthX

Methods

mapBoundAtDepthX :: (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 liftX and lowerX.

Instances

MapBoundX Bound n

Methods

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

MapBoundX (Witness a) n

Methods

mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Witness a n -> Witness a n

MapBoundX (Cast a) n

Methods

mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Cast a n -> Cast a n

MapBoundX (Alt a) n

Methods

mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Alt a n -> Alt a n

MapBoundX (Exp a) n

Methods

mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Exp a n -> Exp a n