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

DDC.Core.Transform.BoundX

Description

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

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

Synopsis

# Documentation

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

Wrapper for liftAtDepthX that starts at depth 0.

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

Wrapper for lowerAtDepthX that starts at depth 0.

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

Minimal complete definition

mapBoundAtDepthX

Methods

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

Instances

 Source # MethodsmapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Bound n -> Bound n Source # MapBoundX (Witness a) n Source # MethodsmapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Witness a n -> Witness a n Source # MapBoundX (Cast a) n Source # MethodsmapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Cast a n -> Cast a n Source # MapBoundX (Alt a) n Source # MethodsmapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Alt a n -> Alt a n Source # MapBoundX (Exp a) n Source # MethodsmapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Exp a n -> Exp a n Source #