Safe Haskell | None |
---|

The functions in this module can be used to help size inference (which, in turn, helps deriving upper bounds of array sizes and helps optimization).

- type SizeCap a = Data a -> Data a
- sizeProp :: (Syntax a, Type b) => (Size (Internal a) -> Size b) -> a -> SizeCap b
- cap :: Type a => Size a -> SizeCap a
- notAbove :: (Type a, Bounded a, Size a ~ Range a) => Data a -> SizeCap a
- notBelow :: (Type a, Bounded a, Size a ~ Range a) => Data a -> SizeCap a
- between :: (Type a, Bounded a, Size a ~ Range a) => Data a -> Data a -> SizeCap a

# Documentation

type SizeCap a = Data a -> Data aSource

An identity function affecting the abstract size information used during
optimization. The application of a `SizeCap`

is a *guarantee* (by the caller)
that the argument is within a certain size (determined by the creator of the
`SizeCap`

, e.g. `sizeProp`

).

*Warning: If the guarantee is not fulfilled, optimizations become unsound!*

In general, the size of the resulting value is the intersection of the cap
size and the size obtained by ordinary size inference. That is, a `SizeCap`

can only make the size more precise, not less precise.

sizeProp :: (Syntax a, Type b) => (Size (Internal a) -> Size b) -> a -> SizeCap bSource

`sizeProp prop a b`

: A guarantee that `b`

is within the size `(prop sa)`

,
where `sa`

is the size of `a`

.

notAbove :: (Type a, Bounded a, Size a ~ Range a) => Data a -> SizeCap aSource

`notAbove a b`

: A guarantee that `b <= a`

holds