indices-1.6.0: Static indices

Data.Index

Description

The indices supplied by this module are static type and value-level linked lists. Since their type gives us information about them, recursion on indices can be unrolled easily.

Indices look like x:.y:.Z :: i:.j:.Z . The value is the actual index used, and the type is the upper-bound on that index.

For instance, one index of a 4x4 matrix is 2:.2:.Z :: 3:.3:.Z , and another index for a 1024x1024x1024 cube is 512:.512:.512:.Z :: 1024:.1024:.1024:.Z

Synopsis

Core

class Ord n => Dim n where Source

Minimal complete definition

each, rank, size, reflect', next, prev, toIndex, fromIndex', correct, correctOnce, lastDim, zipDims, unsafeZipDims, mapDim, unsafeMapDim

Methods

each :: Int -> n Source

each n = an index of all n

rank :: n -> Int Source

The number of dimensions in an index

size :: proxy n -> Int Source

The size of the index

reflect :: n Source

Reify a type-level index into a value-level one

next :: n -> n Source

Increment by one. Wraps around to minBound when maxBound is given.

prev :: n -> n Source

Decrement by one. Wraps around to maxBound when minBound is given.

toIndex :: n -> Int Source

Create an Int index.

fromIndex :: Int -> n Source

Create an index from its Int representation.

correct :: n -> n Source

Ensure an index is within its bounds.

Instances

 Dim Z (KnownNat x, Dim xs) => Dim ((:.) Nat x xs)

zero :: Dim a => a Source

class Rank a b where Source

Methods

setBound :: a -> b Source

Retain the rank, but change the upper bound

Instances

 Rank Z Z Rank xs ys => Rank ((:.) k x xs) ((:.) k y ys) Rank

data a :. b infixr 9 Source

Index constructor, analogous to :

The Applicative and Monad instances multiply in their bind operations, and their 'return'/'pure' creates an index whose first dimension is 1.

Constructors

 !Int :. !b infixr 9

Instances

 KnownNat s => Monad ((:.) Nat s) Functor ((:.) k a) KnownNat s => Applicative ((:.) Nat s) Foldable ((:.) k a) Traversable ((:.) k a) Dim ((:.) k x xs) => Bounded ((:.) k x xs) Dim ((:.) k x xs) => Enum ((:.) k x xs) Eq b => Eq ((:.) k a b) (Integral xs, Dim ((:.) k x xs), Enum ((:.) k x xs)) => Integral ((:.) k x xs) Dim ((:.) k x xs) => Num ((:.) k x xs) Ord b => Ord ((:.) k a b) Read b => Read ((:.) k a b) (Num ((:.) k x xs), Dim ((:.) k x xs)) => Real ((:.) k x xs) Show b => Show ((:.) k a b) (Ranged ((:.) k x xs), Num xs) => Ix ((:.) k x xs) The indices in an Ix instance are always bound by (0, t), where t is the type of the index. Generic ((:.) k a b) (Dim ((:.) k x xs), Monoid xs) => Monoid ((:.) k x xs) (KnownNat x, Dim xs) => Dim ((:.) Nat x xs) Rank xs ys => Rank ((:.) k x xs) ((:.) k y ys) Rank type Rep ((:.) k a b)

data Z Source

The zero index, used to end indices, just as '[]' ends a list.

Constructors

 Z

Instances

 Bounded Z Enum Z Eq Z Integral Z Data Z Num Z Ord Z Read Z Real Z Show Z Ix Z Generic Z Monoid Z Dim Z Typeable * Z Rank Z Z type Rep Z

Selecting whether to unroll loops

data Mode :: * -> * where Source

Select whether to generate an unrolled loop or just the loop at compile-time.

Constructors

 Unroll :: Ranged i => Mode i Roll :: Dim i => Mode i

roll :: Dim a => Proxy a -> Mode a Source

You might prefer to use dimr

unroll :: Ranged a => Proxy a -> Mode a Source

You might prefer to use dimu

Using ranges

foldlRange :: Mode n -> (b -> n -> b) -> b -> b Source

Lazy right fold over a range.

foldrRange :: Mode n -> (n -> b -> b) -> b -> b Source

Lazy right fold over a range.

withRange :: Applicative m => Mode a -> (a -> m ()) -> m () Source

Compute something from a range

Over Int indices

foldlRangeIndices :: Mode n -> (b -> Int -> b) -> b -> b Source

Strict left fold over the raw Int indices under a range

foldrRangeIndices :: Mode n -> (Int -> b -> b) -> b -> b Source

Lazy right fold over the raw Int indices under a range

withRangeIndices :: Applicative m => Mode n -> (Int -> m ()) -> m () Source

Compute something using the raw indices under a range

Range types

class (Dim n, Range (ToPeano (Size n))) => Ranged n Source

Types that support static range operations

Instances

 (Dim n, Range (ToPeano (Size n))) => Ranged n

type family InRange a b :: Bool Source

Equations

 InRange Z Z = True InRange (x :. xs) (y :. ys) = And (x <=? y) (InRange xs ys)

class Range n Source

Minimal complete definition

swithRange_, sfoldrRange_, sfoldlRange_, swithRangeIndices_, sfoldrRangeIndices_, sfoldlRangeIndices_

Instances

 Range Zero Range n => Range (Succ n)

data Peano Source

Peano numbers

Constructors

 Zero Succ Peano

type family ToPeano n :: Peano Source

Convert a Nat to a type-level Peano

Equations

 ToPeano 0 = Zero ToPeano n = Succ (ToPeano (n - 1))

type family Size dim :: Nat Source

Compute the size of an index

Equations

 Size (x :. Z) = x Size (x :. xs) = x * Size xs

Utility

bounds :: (Dim a, Bounded a) => Proxy a -> (a, a) Source

Create a bound for use with e.g. "Data.Array.array"

range :: Mode n -> [n] Source

The range of an index

dimHead :: KnownNat x => (x :. xs) -> Int Source

dimTail :: (x :. xs) -> xs Source

pdimHead :: KnownNat x => proxy (x :. xs) -> Int Source

pdimTail :: proxy (x :. xs) -> Proxy xs Source

cnat :: KnownNat n => proxy (n :: Nat) -> Int Source

fromInteger . natVal

type family And a b :: Bool Source

Equations

 And True True = True And a b = False

Syntax

Expands to a Proxy with the phantom type being the dimension specified. Works in types and expressions.

Examples:

id [dim|3 4 5|] ==> id (Proxy :: Proxy (3:.4:.5:.Z))
Proxy :: [dim|3 4 5|] ==> Proxy :: Proxy (3:.4:.5:.Z)

Same as dim, but create an Unroll instead of a Proxy.

Same as dim, but create a Roll instead of a Proxy.

module Data.Proxy