parameterized-utils-2.0: Classes and data structures for working with data-kind indexed types

Safe HaskellTrustworthy
LanguageHaskell98

Data.Parameterized.Context.Unsafe

Contents

Synopsis

Documentation

class KnownContext (ctx :: Ctx k) where Source #

A context that can be determined statically at compiler time.

Methods

knownSize :: Size ctx Source #

Instances
KnownContext (EmptyCtx :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

KnownContext ctx => KnownContext (ctx ::> tp :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

knownSize :: Size (ctx ::> tp) Source #

Size

data Size (ctx :: Ctx k) Source #

Represents the size of a context.

Instances
Show (Size ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

show :: Size ctx -> String #

showList :: [Size ctx] -> ShowS #

sizeInt :: Size ctx -> Int Source #

Convert a context size to an Int.

zeroSize :: Size EmptyCtx Source #

The size of an empty context.

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

Increment the size to the next value.

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

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

Extend the size by a given difference.

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

The total size of two concatenated contexts.

data SizeView (ctx :: Ctx k) where Source #

Allows interpreting a size.

Constructors

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

viewSize :: Size ctx -> SizeView ctx Source #

Project a size

Diff

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

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) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

id :: Diff a a #

(.) :: Diff b c -> Diff a b -> Diff a c #

noDiff :: Diff l l Source #

The identity difference.

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

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

appendDiff :: Size r -> Diff l (l <+> r) Source #

data DiffView a b where Source #

Constructors

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

viewDiff :: Diff a b -> DiffView a b Source #

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

A difference that can be automatically inferred at compile time.

Methods

knownDiff :: Diff l r Source #

Instances
KnownDiff (l :: Ctx k) (l :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

knownDiff :: Diff l l Source #

KnownDiff l r => KnownDiff (l :: Ctx k) (r ::> tp :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

data IsAppend l r where Source #

Proof that r = l + app for some app

Constructors

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

diffIsAppend :: Diff l r -> IsAppend l r Source #

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) Source #

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

Instances
ExtendContext' (Index :: Ctx k' -> k' -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context

Methods

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

ApplyEmbedding' (Index :: Ctx k' -> k' -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context

Methods

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

TestEquality (Index ctx :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

HashableF (Index ctx :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

hashF :: Index ctx tp -> Int Source #

ShowF (Index ctx :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

showF :: Index ctx tp -> String Source #

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

OrdF (Index ctx :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

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

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

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

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

Eq (Index ctx tp) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

hash :: Index ctx tp -> Int #

indexVal :: Index ctx tp -> Int Source #

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

Index for first element in context.

skipIndex :: Index ctx x -> Index (ctx ::> y) x Source #

Increase context while staying at same index.

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

Return the last index of a element.

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

Return the index of a element one past the size.

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

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

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

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 Source #

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)) Source #

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

IndexRange

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

This represents a contiguous range of indices.

allRange :: Size ctx -> IndexRange ctx ctx Source #

Return a range containing all indices in the context.

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

indexOfRange returns the only index in a range.

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

dropHeadRange r n drops the first n elements in r.

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

dropTailRange r n drops the last n elements in r.

Assignments

data Assignment (f :: k -> Type) (ctx :: Ctx k) Source #

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) Source # 
Instance details

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) Source #

FoldableFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

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

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

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

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

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

OrdFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # 
Instance details

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 Source #

TestEqualityFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # 
Instance details

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) Source #

FunctorFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

IxedF' k (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

IxedF k (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

hashF :: Assignment f tp -> Int Source #

ShowF f => ShowF (Assignment f :: Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

showF :: Assignment f tp -> String Source #

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

OrdF f => OrdF (Assignment f :: Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

IsRepr f => IsRepr (Assignment f :: Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.WithRepr

Methods

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

KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

(KnownRepr (Assignment f) ctx, KnownRepr f bt) => KnownRepr (Assignment f :: Ctx k -> Type) (ctx ::> bt :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

TestEquality f => Eq (Assignment f ctx) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

rnf :: Assignment f ctx -> () #

HashableF f => Hashable (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

hash :: Assignment f ctx -> Int #

type IxValueF (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

type IxValueF (Assignment f ctx) = f
type IndexF (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

type IndexF (Assignment f ctx) = Index ctx

size :: Assignment f ctx -> Size ctx Source #

Return number of elements in assignment.

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

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 Source #

Generate an assignment

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

Generate an assignment in an Applicative context

empty :: Assignment f EmptyCtx Source #

Return empty assignment

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

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

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 Source #

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) Source #

Modify the value of an assignment at a particular index.

data AssignView f ctx where Source #

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 Source #

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

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

Return value of assignment.

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

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 Source #

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

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

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