Data.Parameterized.Context.Unsafe

Documentation

module Data.Parameterized.Ctx

class KnownContext (ctx :: Ctx k) where

A context that can be determined statically at compiler time.

Methods

knownSize :: Size ctx

Instances

KnownContext (EmptyCtx :: Ctx k)

Defined in Data.Parameterized.Context.Unsafe

Methods

knownSize :: Size EmptyCtx

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

Defined in Data.Parameterized.Context.Unsafe

Methods

knownSize :: Size (ctx ::> tp)

Size

data Size (ctx :: Ctx k)

Represents the size of a context.

Instances

Show (Size ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

showsPrec :: Int -> Size ctx -> ShowS

show :: Size ctx -> String

showList :: [Size ctx] -> ShowS

sizeInt :: Size ctx -> Int

Convert a context size to an 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

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 (Diff :: Ctx k -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

id :: Diff a a

(.) :: Diff b c -> Diff a b -> Diff 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.

appendDiff :: Size r -> Diff l (l <+> 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

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

A difference that can be automatically inferred at compile time.

Methods

knownDiff :: Diff l r

Instances

KnownDiff (l :: Ctx k) (l :: Ctx k)

Defined in Data.Parameterized.Context.Unsafe

Methods

knownDiff :: Diff l l

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

Defined in Data.Parameterized.Context.Unsafe

Methods

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

data IsAppend l r where

Proof that r = l + app for some app

Constructors

IsAppend :: Size app -> IsAppend l (l <+> app)

diffIsAppend :: Diff l r -> IsAppend l r

If l is a sub-context of r then extract out their "contextual difference", i.e., the app such that r = l + app

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' (Index :: Ctx k' -> k' -> Type)

Defined in Data.Parameterized.Context

Methods

extendContext' :: Diff ctx ctx' -> Index ctx v -> Index ctx' v

ApplyEmbedding' (Index :: Ctx k' -> k' -> Type)

Defined in Data.Parameterized.Context

Methods

applyEmbedding' :: CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v

TestEquality (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

HashableF (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSaltF :: Int -> Index ctx tp -> Int

hashF :: Index ctx tp -> Int

ShowF (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: p (Index ctx) -> q tp -> (Show (Index ctx tp) -> a) -> a

showF :: Index ctx tp -> String

showsPrecF :: Int -> Index ctx tp -> String -> String

OrdF (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

compareF :: Index ctx x -> Index ctx y -> OrderingF x y

leqF :: Index ctx x -> Index ctx y -> Bool

ltF :: Index ctx x -> Index ctx y -> Bool

geqF :: Index ctx x -> Index ctx y -> Bool

gtF :: Index ctx x -> Index ctx y -> Bool

Eq (Index ctx tp)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

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

Ord (Index ctx tp)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

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

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

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

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

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

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

Show (Index ctx tp)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

show :: Index ctx tp -> String

showList :: [Index ctx tp] -> ShowS

Hashable (Index ctx tp)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

hash :: Index ctx tp -> Int

indexVal :: Index ctx tp -> Int

baseIndex :: Index (EmptyCtx ::> tp) tp

Index for first element in context.

skipIndex :: 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, the expression 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, the expression forIndex i n f v is equivalent to v when i >= sizeInt n, and f i (forIndexRange (i+1) n v) otherwise.

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 -> Type) (ctx :: Ctx k)

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

This assignment implementation uses a binomial tree implementation that offers lookups and updates in time and space logarithmic with respect to the number of elements in the context.

Instances

TraversableFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

traverseFC :: Applicative m => (forall (x :: k0). f x -> m (g x)) -> forall (x :: l). Assignment f x -> m (Assignment g x)

FoldableFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

foldMapFC :: Monoid m => (forall (x :: k0). f x -> m) -> forall (x :: l). Assignment f x -> m

foldrFC :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> Assignment f x -> b

foldlFC :: (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> Assignment f x -> b

foldrFC' :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> Assignment f x -> b

foldlFC' :: (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> Assignment f x -> b

toListFC :: (forall (x :: k0). f x -> a) -> forall (x :: l). Assignment f x -> [a]

OrdFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

TestEqualityFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

FunctorFC (Assignment :: (k -> Type) -> Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

fmapFC :: (forall (x :: k0). f x -> g x) -> forall (x :: l). Assignment f x -> Assignment g x

IxedF' k (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

IxedF k (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

TestEquality f => TestEquality (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

HashableF f => HashableF (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSaltF :: Int -> Assignment f tp -> Int

hashF :: Assignment f tp -> Int

ShowF f => ShowF (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

showF :: Assignment f tp -> String

showsPrecF :: Int -> Assignment f tp -> String -> String

OrdF f => OrdF (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

compareF :: Assignment f x -> Assignment f y -> OrderingF x y

leqF :: Assignment f x -> Assignment f y -> Bool

ltF :: Assignment f x -> Assignment f y -> Bool

geqF :: Assignment f x -> Assignment f y -> Bool

gtF :: Assignment f x -> Assignment f y -> Bool

IsRepr f => IsRepr (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: Assignment f a -> (KnownRepr (Assignment f) a -> r) -> r

KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k)

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f EmptyCtx

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

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f (ctx ::> bt)

TestEquality f => Eq (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

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

OrdF f => Ord (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

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

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

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

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

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

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

ShowF f => Show (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

show :: Assignment f ctx -> String

showList :: [Assignment f ctx] -> ShowS

NFData (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

rnf :: Assignment f ctx -> ()

HashableF f => Hashable (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

hash :: Assignment f ctx -> Int

type IxValueF (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

type IxValueF (Assignment f ctx) = f

type IndexF (Assignment f ctx)

Defined in Data.Parameterized.Context.Unsafe

type IndexF (Assignment f ctx) = Index 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 in an Applicative context

empty :: Assignment f EmptyCtx

Return empty assignment

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

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

Deprecated: Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead.

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

Deprecated: Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead.

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.

data AssignView f ctx where

Represent 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)

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

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

(!) :: 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)