Data.Parameterized.Context.Unsafe

Documentation

module Data.Parameterized.Ctx

data Size (ctx :: Ctx k)

Represents the size of a context.

Instances

Show (Size k ctx)

Methods

showsPrec :: Int -> Size k ctx -> ShowS

show :: Size k ctx -> String

showList :: [Size k ctx] -> ShowS

sizeInt :: Size ctx -> Int

zeroSize :: Size EmptyCtx

The size of an empty context.

incSize :: Size ctx -> Size (ctx ::> tp)

Increment the size to the next value.

decSize :: Size (ctx ::> tp) -> Size ctx

extSize :: Size l -> Diff l r -> Size r

Extend the size by a given difference.

addSize :: Size x -> Size y -> Size (x <+> y)

The total size of two concatenated contexts.

data SizeView (ctx :: Ctx k) where

Allows interpreting a size.

Constructors

ZeroSize :: SizeView EmptyCtx

IncSize :: !(Size ctx) -> SizeView (ctx ::> tp)

viewSize :: Size ctx -> SizeView ctx

Project a size

class KnownContext (ctx :: Ctx k) where

A context that can be determined statically at compiler time.

Minimal complete definition

knownSize

Methods

knownSize :: Size ctx

Instances

KnownContext k (EmptyCtx k)

Methods

knownSize :: Size (EmptyCtx k) ctx

KnownContext k ctx => KnownContext k ((::>) k ctx tp)

Methods

knownSize :: Size ((k ::> ctx) tp) ctx

Diff

data Diff (l :: Ctx k) (r :: Ctx k)

Difference in number of elements between two contexts. The first context must be a sub-context of the other.

Instances

Category (Ctx k) (Diff k)

Methods

id :: cat a a

(.) :: cat b c -> cat a b -> cat a c

noDiff :: Diff l l

The identity difference.

extendRight :: Diff l r -> Diff l (r ::> tp)

Extend the difference to a sub-context of the right side.

class KnownDiff (l :: Ctx k) (r :: Ctx k) where

A difference that can be automatically inferred at compile time.

Minimal complete definition

knownDiff

Methods

knownDiff :: Diff l r

Instances

KnownDiff k l l

Methods

knownDiff :: Diff l l r

KnownDiff k l r => KnownDiff k l ((::>) k r tp)

Methods

knownDiff :: Diff l ((k ::> r) tp) r

data DiffView a b where

Constructors

NoDiff :: DiffView a a

ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)

viewDiff :: Diff a b -> DiffView a b

Indexing

data Index (ctx :: Ctx k) (tp :: k)

An index is a reference to a position with a particular type in a context.

Instances

ExtendContext' k' k' (Index k')

Methods

extendContext' :: Diff (Index k') ctx ctx' -> f ctx v -> f ctx' v

ApplyEmbedding' k' k' (Index k')

Methods

applyEmbedding' :: CtxEmbedding (Index k') ctx ctx' -> f ctx v -> f ctx' v

TestEquality k (Index k ctx)

Methods

testEquality :: f a -> f b -> Maybe ((Index k ctx :~: a) b)

HashableF k (Index k ctx)

Methods

hashWithSaltF :: Int -> f tp -> Int

hashF :: f tp -> Int

ShowF k (Index k ctx)

Methods

withShow :: p f -> q tp -> (Show (f tp) -> a) -> a

showF :: f tp -> String

showsF :: f tp -> String -> String

OrdF k (Index k ctx)

Methods

compareF :: ktp x -> ktp y -> OrderingF (Index k ctx) x y

leqF :: ktp x -> ktp y -> Bool

ltF :: ktp x -> ktp y -> Bool

geqF :: ktp x -> ktp y -> Bool

gtF :: ktp x -> ktp y -> Bool

Eq (Index k ctx tp)

Methods

(==) :: Index k ctx tp -> Index k ctx tp -> Bool

(/=) :: Index k ctx tp -> Index k ctx tp -> Bool

Ord (Index k ctx tp)

Methods

compare :: Index k ctx tp -> Index k ctx tp -> Ordering

(<) :: Index k ctx tp -> Index k ctx tp -> Bool

(<=) :: Index k ctx tp -> Index k ctx tp -> Bool

(>) :: Index k ctx tp -> Index k ctx tp -> Bool

(>=) :: Index k ctx tp -> Index k ctx tp -> Bool

max :: Index k ctx tp -> Index k ctx tp -> Index k ctx tp

min :: Index k ctx tp -> Index k ctx tp -> Index k ctx tp

Show (Index k ctx tp)

Methods

showsPrec :: Int -> Index k ctx tp -> ShowS

show :: Index k ctx tp -> String

showList :: [Index k ctx tp] -> ShowS

Hashable (Index k ctx tp)

Methods

hashWithSalt :: Int -> Index k ctx tp -> Int

hash :: Index k ctx tp -> Int

indexVal :: Index ctx tp -> Int

base :: Index (EmptyCtx ::> tp) tp

Index for first element in context.

skip :: Index ctx x -> Index (ctx ::> y) x

Increase context while staying at same index.

lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp

Return the last index of a element.

nextIndex :: Size ctx -> Index (ctx ::> tp) tp

Return the index of a element one past the size.

extendIndex :: KnownDiff l r => Index l tp -> Index r tp

extendIndex' :: Diff l r -> Index l tp -> Index r tp

forIndex :: forall ctx r. Size ctx -> (forall tp. r -> Index ctx tp -> r) -> r -> r

Given a size n, an initial value v0, and a function f, 'forIndex n v0 f' is equivalent to v0 when n is zero, and 'f (forIndex (n-1) v0) (n-1)' otherwise.

forIndexRange :: forall ctx r. Int -> Size ctx -> (forall tp. Index ctx tp -> r -> r) -> r -> r

Given an index i, size n, a function f, value v, and a function f, 'forIndex i n f v' is equivalent to v when 'i >= sizeInt n', and 'f i (forIndexRange (i+1) n v0)' otherwise.

forIndexM :: forall ctx m. Applicative m => Size ctx -> (forall tp. Index ctx tp -> m ()) -> m ()

'forIndexM sz f' calls f on indices '[0..sz-1]'.

intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))

Return index at given integer or nothing if integer is out of bounds.

IndexRange

data IndexRange (ctx :: Ctx k) (sub :: Ctx k)

This represents a contiguous range of indices.

allRange :: Size ctx -> IndexRange ctx ctx

Return a range containing all indices in the context.

indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e

indexOfRange returns the only index in a range.

dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y

`dropHeadRange r n` drops the first n elements in r.

dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x

`dropTailRange r n` drops the last n elements in r.

Assignments

data Assignment (f :: k -> *) (ctx :: Ctx k)

An assignment is a sequence that maps each index with type tp to a value of type 'f tp'.

Instances

TraversableFC k (Ctx k) (Assignment k)

Methods

traverseFC :: Applicative m => (forall (s :: Assignment k). e s -> m (f s)) -> t e c -> m (t f c)

FoldableFC k (Ctx k) (Assignment k)

Methods

foldMapFC :: Monoid m => (forall (s :: Assignment k). e s -> m) -> t e c -> m

foldrFC :: (forall (s :: Assignment k). e s -> b -> b) -> b -> t e c -> b

foldlFC :: (forall (s :: Assignment k). b -> e s -> b) -> b -> t e c -> b

foldrFC' :: (forall (s :: Assignment k). e s -> b -> b) -> b -> t e c -> b

foldlFC' :: (forall (s :: Assignment k). b -> e s -> b) -> b -> t e c -> b

toListFC :: (forall (tp :: Assignment k). f tp -> a) -> t f c -> [a]

OrdFC k (Ctx k) (Assignment k)

Methods

compareFC :: (forall (x :: Assignment k) (y :: Assignment k). f x -> f y -> OrderingF (Assignment k) x y) -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF l x y

TestEqualityFC k (Ctx k) (Assignment k)

Methods

testEqualityFC :: (forall (x :: Assignment k) (y :: Assignment k). f x -> f y -> Maybe ((Assignment k :~: x) y)) -> forall (x :: l) (y :: l). t f x -> t f y -> Maybe ((l :~: x) y)

FunctorFC k (Ctx k) (Assignment k)

Methods

fmapFC :: (forall (x :: Assignment k). f x -> g x) -> forall (x :: k). m f x -> m g x

IxedF' k (Assignment k f ctx)

Methods

ixF' :: IndexF k (Assignment k f ctx) x -> Lens' (Assignment k f ctx) (IxValueF k (Assignment k f ctx) x)

IxedF k (Assignment k f ctx)

Methods

ixF :: IndexF k (Assignment k f ctx) x -> Traversal' (Assignment k f ctx) (IxValueF k (Assignment k f ctx) x)

TestEquality k f => TestEquality (Ctx k) (Assignment k f)

Methods

testEquality :: f a -> f b -> Maybe ((Assignment k f :~: a) b)

HashableF k f => HashableF (Ctx k) (Assignment k f)

Methods

hashWithSaltF :: Int -> f tp -> Int

hashF :: f tp -> Int

ShowF k f => ShowF (Ctx k) (Assignment k f)

Methods

withShow :: p f -> q tp -> (Show (f tp) -> a) -> a

showF :: f tp -> String

showsF :: f tp -> String -> String

OrdF k f => OrdF (Ctx k) (Assignment k f)

Methods

compareF :: ktp x -> ktp y -> OrderingF (Assignment k f) x y

leqF :: ktp x -> ktp y -> Bool

ltF :: ktp x -> ktp y -> Bool

geqF :: ktp x -> ktp y -> Bool

gtF :: ktp x -> ktp y -> Bool

KnownRepr (Ctx k) (Assignment k f) (EmptyCtx k)

Methods

knownRepr :: EmptyCtx k ctx

(KnownRepr (Ctx k) (Assignment k f) ctx, KnownRepr k f bt) => KnownRepr (Ctx k) (Assignment k f) ((::>) k ctx bt)

Methods

knownRepr :: (k ::> ctx) bt ctx

TestEquality k f => Eq (Assignment k f ctx)

Methods

(==) :: Assignment k f ctx -> Assignment k f ctx -> Bool

(/=) :: Assignment k f ctx -> Assignment k f ctx -> Bool

OrdF k f => Ord (Assignment k f ctx)

Methods

compare :: Assignment k f ctx -> Assignment k f ctx -> Ordering

(<) :: Assignment k f ctx -> Assignment k f ctx -> Bool

(<=) :: Assignment k f ctx -> Assignment k f ctx -> Bool

(>) :: Assignment k f ctx -> Assignment k f ctx -> Bool

(>=) :: Assignment k f ctx -> Assignment k f ctx -> Bool

max :: Assignment k f ctx -> Assignment k f ctx -> Assignment k f ctx

min :: Assignment k f ctx -> Assignment k f ctx -> Assignment k f ctx

ShowF k f => Show (Assignment k f ctx)

Methods

showsPrec :: Int -> Assignment k f ctx -> ShowS

show :: Assignment k f ctx -> String

showList :: [Assignment k f ctx] -> ShowS

NFData (Assignment k f ctx)

Methods

rnf :: Assignment k f ctx -> ()

HashableF k f => Hashable (Assignment k f ctx)

Methods

hashWithSalt :: Int -> Assignment k f ctx -> Int

hash :: Assignment k f ctx -> Int

type IxValueF k (Assignment k f ctx)

type IxValueF k (Assignment k f ctx) = f

type IndexF k (Assignment k f ctx)

type IndexF k (Assignment k f ctx) = Index k ctx

size :: Assignment f ctx -> Size ctx

Return number of elements in assignment.

replicate :: Size ctx -> (forall tp. f tp) -> Assignment f ctx

replicate n make a context with different copies of the same polymorphic value.

generate :: Size ctx -> (forall tp. Index ctx tp -> f tp) -> Assignment f ctx

Generate an assignment

generateM :: Applicative m => Size ctx -> (forall tp. Index ctx tp -> m (f tp)) -> m (Assignment f ctx)

Generate an assignment

generateSome :: forall f. Int -> (Int -> Some f) -> Some (Assignment f)

Generate an assignment with some context type that is not known.

generateSomeM :: forall m f. Applicative m => Int -> (Int -> m (Some f)) -> m (Some (Assignment f))

Generate an assignment with some context type that is not known.

empty :: Assignment f EmptyCtx

Return empty assignment

null :: Assignment f ctx -> Bool

Return true if assignment is empty.

extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)

update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx

Update the assignment at a particular index.

adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx

Modify the value of an assignment at a particular index.

adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)

Modify the value of an assignment at a particular index.

init :: Assignment f (ctx ::> tp) -> Assignment f ctx

Return assignment with all but the last block.

last :: Assignment f (ctx ::> tp) -> f tp

Return the last element in the assignment.

data AssignView f ctx where

View an assignment as either empty or an assignment with one appended.

Constructors

AssignEmpty :: AssignView f EmptyCtx

AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)

view :: forall f ctx. Assignment f ctx -> AssignView f ctx

View an assignment as either empty or an assignment with one appended.

decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)

fromList :: [Some f] -> Some (Assignment f)

Create an assignment from a list of values.

(!) :: Assignment f ctx -> Index ctx tp -> f tp

Return value of assignment.

(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp

Return value of assignment, where the index is into an initial sequence of the assignment.

zipWith :: (forall x. f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a

zipWithM :: Applicative m => (forall x. f x -> g x -> m (h x)) -> Assignment f a -> Assignment g a -> m (Assignment h a)

(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)

traverseWithIndex :: Applicative m => (forall tp. Index ctx tp -> f tp -> m (g tp)) -> Assignment f ctx -> m (Assignment g ctx)