Safe Haskell	Safe-Inferred

DDC.Core.Transform.LiftX

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 nSource

Wrapper for liftAtDepthX that starts at depth 0.

liftAtDepthX Source

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 nSource

Wrapper for lowerAtDepthX that starts at depth 0.

lowerAtDepthX Source

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 whereSource

Methods

mapBoundAtDepthX Source

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

Instances

MapBoundX Bound n
MapBoundX (Witness a) n
MapBoundX (Cast a) n
MapBoundX (Alt a) n
MapBoundX (Exp a) n