Safe Haskell	Trustworthy
Language	Haskell98

Data.Parameterized.Context.Unsafe

Contents

Size
Diff
Indexing
- IndexRange
Assignments

Synopsis

module Data.Parameterized.Ctx
class KnownContext (ctx :: Ctx k) where
- knownSize :: Size ctx
data Size (ctx :: Ctx k)
sizeInt :: Size ctx -> Int
zeroSize :: Size EmptyCtx
incSize :: Size ctx -> Size (ctx ::> tp)
decSize :: Size (ctx ::> tp) -> Size ctx
extSize :: Size l -> Diff l r -> Size r
addSize :: Size x -> Size y -> Size (x <+> y)
data SizeView (ctx :: Ctx k) where
- ZeroSize :: SizeView EmptyCtx
- IncSize :: !(Size ctx) -> SizeView (ctx ::> tp)
viewSize :: Size ctx -> SizeView ctx
data Diff (l :: Ctx k) (r :: Ctx k)
noDiff :: Diff l l
extendRight :: Diff l r -> Diff l (r ::> tp)
appendDiff :: Size r -> Diff l (l <+> r)
data DiffView a b where
- 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
- knownDiff :: Diff l r
data IsAppend l r where
- IsAppend :: Size app -> IsAppend l (l <+> app)
diffIsAppend :: Diff l r -> IsAppend l r
data Index (ctx :: Ctx k) (tp :: k)
indexVal :: Index ctx tp -> Int
baseIndex :: Index (EmptyCtx ::> tp) tp
skipIndex :: Index ctx x -> Index (ctx ::> y) x
lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp
nextIndex :: Size ctx -> Index (ctx ::> tp) tp
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
forIndexRange :: forall ctx r. Int -> Size ctx -> (forall tp. Index ctx tp -> r -> r) -> r -> r
intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))
data IndexRange (ctx :: Ctx k) (sub :: Ctx k)
allRange :: Size ctx -> IndexRange ctx ctx
indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e
dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y
dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x
data Assignment (f :: k -> Type) (ctx :: Ctx k)
size :: Assignment f ctx -> Size ctx
replicate :: Size ctx -> (forall tp. f tp) -> Assignment f ctx
generate :: Size ctx -> (forall tp. Index ctx tp -> f tp) -> Assignment f ctx
generateM :: Applicative m => Size ctx -> (forall tp. Index ctx tp -> m (f tp)) -> m (Assignment f ctx)
empty :: Assignment f EmptyCtx
extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)
adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
data AssignView f ctx where
- AssignEmpty :: AssignView f EmptyCtx
- AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)
viewAssign :: forall f ctx. Assignment f ctx -> AssignView f ctx
(!) :: Assignment f ctx -> Index ctx tp -> f tp
(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp
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)

Documentation

module Data.Parameterized.Ctx

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 Methods knownSize :: Size EmptyCtx Source #
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 Methods compareF :: Assignment f x -> Assignment f y -> OrderingF x y Source # leqF :: Assignment f x -> Assignment f y -> Bool Source # ltF :: Assignment f x -> Assignment f y -> Bool Source # geqF :: Assignment f x -> Assignment f y -> Bool Source # gtF :: Assignment f x -> Assignment f y -> Bool Source #
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 Methods knownRepr :: Assignment f EmptyCtx Source #
(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 #