Copyright	(c) Galois Inc 2014-2019
Maintainer	Joe Hendrix <[email protected]>
Safe Haskell	Trustworthy
Language	Haskell2010

Data.Parameterized.Context

Contents

Context extension and embedding utilities
Static indexing and lenses for assignments
Currying and uncurrying for assignments
Size and Index values

Description

This module reexports either Data.Parameterized.Context.Safe or Data.Parameterized.Context.Unsafe depending on the the unsafe-operations compile-time flag.

It also defines some utility typeclasses for transforming between curried and uncurried versions of functions over contexts.

The Assignment type is isomorphic to the List type, except Assignments construct lists from the right-hand side, and instead of using type-level '[]-style lists, an Assignment is indexed by a type-level Ctx. The implementation of Assignments is also more efficent than List for lists of many elements, as it uses a balanced binary tree representation rather than a linear-time list. For a motivating example, see List.

Synopsis

data Diff (l :: Ctx k) (r :: Ctx k)
(!) :: forall {k} f (ctx :: Ctx k) (tp :: k). Assignment f ctx -> Index ctx tp -> f tp
empty :: forall {k} (f :: k -> Type). Assignment f (EmptyCtx :: Ctx k)
replicate :: forall {k} (ctx :: Ctx k) f. Size ctx -> (forall (tp :: k). f tp) -> Assignment f ctx
zipWith :: forall {k} f g h (a :: Ctx k). (forall (x :: k). f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a
adjust :: forall {k} f (tp :: k) (ctx :: Ctx k). (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
zipWithM :: forall {k} m f g h (a :: Ctx k). Applicative m => (forall (x :: k). f x -> g x -> m (h x)) -> Assignment f a -> Assignment g a -> m (Assignment h a)
type family (x :: Ctx k) <+> (y :: Ctx k) :: Ctx k where ...
data Size (ctx :: Ctx k)
size :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> Size ctx
extend :: forall {k} f (ctx :: Ctx k) (x :: k). Assignment f ctx -> f x -> Assignment f (ctx ::> x)
update :: forall {k} (ctx :: Ctx k) (tp :: k) f. Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
traverseWithIndex :: forall {k} m (ctx :: Ctx k) f g. Applicative m => (forall (tp :: k). Index ctx tp -> f tp -> m (g tp)) -> Assignment f ctx -> m (Assignment g ctx)
data Index (ctx :: Ctx k) (tp :: k)
generate :: forall {k} (ctx :: Ctx k) f. Size ctx -> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generateM :: forall {k} m (ctx :: Ctx k) f. Applicative m => Size ctx -> (forall (tp :: k). Index ctx tp -> m (f tp)) -> m (Assignment f ctx)
data Ctx k
- = EmptyCtx
- | (Ctx k) ::> k
sizeInt :: forall {k} (ctx :: Ctx k). Size ctx -> Int
zeroSize :: Size ('EmptyCtx :: Ctx k)
incSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
decSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
extSize :: forall {k} (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r
addSize :: forall {k} (x :: Ctx k) (y :: Ctx k). Size x -> Size y -> Size (x <+> y)
data SizeView (ctx :: Ctx k) where
- ZeroSize :: forall {k}. SizeView ('EmptyCtx :: Ctx k)
- IncSize :: forall {k} (ctx1 :: Ctx k) (tp :: k). !(Size ctx1) -> SizeView (ctx1 '::> tp)
viewSize :: forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
sizeToNatRepr :: forall {k} (items :: Ctx k). Size items -> NatRepr (CtxSize items)
class KnownContext (ctx :: Ctx k) where
- knownSize :: Size ctx
noDiff :: forall {k} (l :: Ctx k). Diff l l
addDiff :: forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k). Diff a b -> Diff b c -> Diff a c
extendRight :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Diff l r -> Diff l (r '::> tp)
appendDiff :: forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
data DiffView (a :: Ctx k) (b :: Ctx k) where
- NoDiff :: forall {k} (a :: Ctx k). DiffView a a
- ExtendRightDiff :: forall {k} (a :: Ctx k) (b1 :: Ctx k) (r :: k). Diff a b1 -> DiffView a (b1 '::> r)
viewDiff :: forall {k} (a :: Ctx k) (b :: Ctx k). Diff a b -> DiffView a b
class KnownDiff (l :: Ctx k) (r :: Ctx k) where
- knownDiff :: Diff l r
data IsAppend (l :: Ctx k) (r :: Ctx k) where
- IsAppend :: forall {k} (app :: Ctx k) (l :: Ctx k). Size app -> IsAppend l (l <+> app)
diffIsAppend :: forall {k} (l :: Ctx k) (r :: Ctx k). Diff l r -> IsAppend l r
baseIndex :: forall {k} (tp :: k). Index (('EmptyCtx :: Ctx k) '::> tp) tp
skipIndex :: forall {k} (ctx :: Ctx k) (x :: k) (y :: k). Index ctx x -> Index (ctx '::> y) x
lastIndex :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx ::> tp) -> Index (ctx ::> tp) tp
nextIndex :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Index (ctx ::> tp) tp
leftIndex :: forall {k} (r :: Ctx k) (l :: Ctx k) (tp :: k). Size r -> Index l tp -> Index (l <+> r) tp
rightIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). KnownDiff l r => Index l tp -> Index r tp
extendIndex' :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Diff l r -> Index l tp -> Index r tp
extendIndexAppendLeft :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Size l -> Size r -> Index r tp -> Index (l <+> r) tp
forIndex :: forall {k} (ctx :: Ctx k) r. Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
forIndexRange :: forall {k} (ctx :: Ctx k) r. Int -> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
intIndex :: forall {k} (ctx :: Ctx k). Int -> Size ctx -> Maybe (Some (Index ctx))
data IndexView (ctx :: Ctx k) (tp :: k) where
- IndexViewLast :: forall {k} (ctx1 :: Ctx k) (tp :: k). !(Size ctx1) -> IndexView (ctx1 '::> tp) tp
- IndexViewInit :: forall {k} (ctx1 :: Ctx k) (tp :: k) (u :: k). !(Index ctx1 tp) -> IndexView (ctx1 '::> u) tp
viewIndex :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Index ctx tp -> IndexView ctx tp
data Assignment (f :: k -> Type) (ctx :: Ctx k)
adjustM :: forall {k} m f (tp :: k) (ctx :: Ctx k). Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
data AssignView (f :: k -> Type) (ctx :: Ctx k) where
- AssignEmpty :: forall {k} (f :: k -> Type). AssignView f ('EmptyCtx :: Ctx k)
- AssignExtend :: forall {k} (f :: k -> Type) (ctx1 :: Ctx k) (tp :: k). Assignment f ctx1 -> f tp -> AssignView f (ctx1 '::> tp)
viewAssign :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> AssignView f ctx
(!^) :: forall {k} (l :: Ctx k) (r :: Ctx k) f (tp :: k). KnownDiff l r => Assignment f r -> Index l tp -> f tp
(<++>) :: forall {k} (f :: k -> Type) (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Assignment f (x <+> y)
data IndexRange (ctx :: Ctx k) (sub :: Ctx k)
allRange :: forall {k} (ctx :: Ctx k). Size ctx -> IndexRange ctx ctx
indexOfRange :: forall {k} (ctx :: Ctx k) (e :: k). IndexRange ctx ((EmptyCtx :: Ctx k) ::> e) -> Index ctx e
dropHeadRange :: forall {k} (ctx :: Ctx k) (x :: Ctx k) (y :: Ctx k). IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y
dropTailRange :: forall {k} (ctx :: Ctx k) (x :: Ctx k) (y :: Ctx k). IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x
type EmptyCtx = 'EmptyCtx :: Ctx k
type SingleCtx (x :: k) = (EmptyCtx :: Ctx k) ::> x
type (::>) (c :: Ctx k) (a :: k) = c '::> a
type family CtxSize (a :: Ctx k) :: Nat where ...
type CtxLookup (n :: Nat) (ctx :: Ctx k) = CtxLookupRight (FromLeft ctx n) ctx
type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k) = CtxUpdateRight (FromLeft ctx n) x ctx
type family CtxLookupRight (n :: Nat) (ctx :: Ctx k) :: k where ...
type family CtxUpdateRight (n :: Nat) (x :: k) (ctx :: Ctx k) :: Ctx k where ...
type family CtxFlatten (ctx :: Ctx (Ctx a)) :: Ctx a where ...
type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) where ...
type ValidIx (n :: Nat) (ctx :: Ctx k) = CheckIx ctx n ((n + 1) <=? CtxSize ctx)
type FromLeft (ctx :: Ctx k) (n :: Natural) = (CtxSize ctx - 1) - n
singleton :: forall {k} f (tp :: k). f tp -> Assignment f ((EmptyCtx :: Ctx k) ::> tp)
toVector :: forall {k} f (tps :: Ctx k) e. Assignment f tps -> (forall (tp :: k). f tp -> e) -> Vector e
pattern (:>) :: forall {k} ctx' f ctx (tp :: k). () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'
pattern Empty :: forall {k} ctx f. () => ctx ~ (EmptyCtx :: Ctx k) => Assignment f ctx
decompose :: forall {k} f (ctx :: Ctx k) (tp :: k). Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
null :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> Bool
init :: forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k). Assignment f (ctx '::> tp) -> Assignment f ctx
last :: forall {k} f (ctx :: Ctx k) (tp :: k). Assignment f (ctx '::> tp) -> f tp
view :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> AssignView f ctx
take :: forall {k} (f :: k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
drop :: forall {k} (f :: k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'
forIndexM :: forall {k} (ctx :: Ctx k) m. Applicative m => Size ctx -> (forall (tp :: k). Index ctx tp -> m ()) -> m ()
generateSome :: forall {k} (f :: k -> Type). Int -> (Int -> Some f) -> Some (Assignment f)
generateSomeM :: forall {k} m (f :: k -> Type). Applicative m => Int -> (Int -> m (Some f)) -> m (Some (Assignment f))
fromList :: forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
traverseAndCollect :: forall {k} w m (ctx :: Ctx k) f. (Monoid w, Applicative m) => (forall (tp :: k). Index ctx tp -> f tp -> m w) -> Assignment f ctx -> m w
traverseWithIndex_ :: forall {k} m (ctx :: Ctx k) f. Applicative m => (forall (tp :: k). Index ctx tp -> f tp -> m ()) -> Assignment f ctx -> m ()
dropPrefix :: forall {k} (f :: k -> Type) (xs :: Ctx k) (prefix :: Ctx k) a. TestEquality f => Assignment f xs -> Assignment f prefix -> a -> (forall (addl :: Ctx k). xs ~ (prefix <+> addl) => Assignment f addl -> a) -> a
unzip :: forall {k} (f :: k -> Type) (g :: k -> Type) (ctx :: Ctx k). Assignment (Product f g) ctx -> (Assignment f ctx, Assignment g ctx)
flattenAssignment :: forall {a} (f :: a -> Type) (ctxs :: Ctx (Ctx a)). Assignment (Assignment f) ctxs -> Assignment f (CtxFlatten ctxs)
flattenSize :: forall {k} (ctxs :: Ctx (Ctx k)). Assignment (Size :: Ctx k -> Type) ctxs -> Size (CtxFlatten ctxs)
data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k) = CtxEmbedding {
- _ctxeSize :: Size ctx'
- _ctxeAssignment :: Assignment (Index ctx') ctx
}
class ExtendContext (f :: Ctx k -> Type) where
- extendContext :: forall (ctx :: Ctx k) (ctx' :: Ctx k). Diff ctx ctx' -> f ctx -> f ctx'
class ExtendContext' (f :: Ctx k -> k' -> Type) where
- extendContext' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). Diff ctx ctx' -> f ctx v -> f ctx' v
class ApplyEmbedding (f :: Ctx k -> Type) where
- applyEmbedding :: forall (ctx :: Ctx k) (ctx' :: Ctx k). CtxEmbedding ctx ctx' -> f ctx -> f ctx'
class ApplyEmbedding' (f :: Ctx k -> k' -> Type) where
- applyEmbedding' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
identityEmbedding :: forall {k} (ctx :: Ctx k). Size ctx -> CtxEmbedding ctx ctx
extendEmbeddingRightDiff :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (ctx'' :: Ctx k). Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
extendEmbeddingRight :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k). CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
extendEmbeddingBoth :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k). CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
appendEmbedding :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
appendEmbeddingLeft :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')
ctxeSize :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) f. Functor f => (Size ctx' -> f (Size ctx')) -> CtxEmbedding ctx ctx' -> f (CtxEmbedding ctx ctx')
ctxeAssignment :: forall {k} (ctx1 :: Ctx k) (ctx' :: Ctx k) (ctx2 :: Ctx k) f. Functor f => (Assignment (Index ctx') ctx1 -> f (Assignment (Index ctx') ctx2)) -> CtxEmbedding ctx1 ctx' -> f (CtxEmbedding ctx2 ctx')
type Idx (n :: Nat) (ctx :: Ctx k) (r :: k) = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r)
field :: forall {k} (n :: Nat) (ctx :: Ctx k) (f :: k -> Type) (r :: k). Idx n ctx r => Lens' (Assignment f ctx) (f r)
natIndex :: forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k). Idx n ctx r => Index ctx r
natIndexProxy :: forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k) proxy. Idx n ctx r => proxy n -> Index ctx r
type family CurryAssignment (ctx :: Ctx k) (f :: k -> Type) x where ...
class CurryAssignmentClass (ctx :: Ctx k) where
- curryAssignment :: forall (f :: k -> Type) x. (Assignment f ctx -> x) -> CurryAssignment ctx f x
- uncurryAssignment :: forall (f :: k -> Type) x. CurryAssignment ctx f x -> Assignment f ctx -> x
size1 :: forall {k} (a :: k). Size ((EmptyCtx :: Ctx k) ::> a)
size2 :: forall {k} (a :: k) (b :: k). Size (((EmptyCtx :: Ctx k) ::> a) ::> b)
size3 :: forall {k} (a :: k) (b :: k) (c :: k). Size ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c)
size4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Size (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d)
size5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Size ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e)
size6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Size (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f)
i1of2 :: forall {k} (a :: k) (b :: k). Index (((EmptyCtx :: Ctx k) ::> a) ::> b) a
i2of2 :: forall {k} (a :: k) (b :: k). Index (((EmptyCtx :: Ctx k) ::> a) ::> b) b
i1of3 :: forall {k} (a :: k) (b :: k) (c :: k). Index ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) a
i2of3 :: forall {k} (a :: k) (b :: k) (c :: k). Index ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) b
i3of3 :: forall {k} (a :: k) (b :: k) (c :: k). Index ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) c
i1of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) a
i2of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) b
i3of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) c
i4of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) d
i1of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) a
i2of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) b
i3of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) c
i4of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) d
i5of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) e
i1of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a
i2of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b
i3of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c
i4of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d
i5of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e
i6of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f

Documentation

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

Instances details

Category (Diff :: Ctx k -> Ctx k -> Type) Source #	Implemented with `noDiff` and `addDiff`
Instance details Defined in Data.Parameterized.Context.Unsafe Methods id :: forall (a :: Ctx k). Diff a a # (.) :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k). Diff b c -> Diff a b -> Diff a c #

(!) :: forall {k} f (ctx :: Ctx k) (tp :: k). Assignment f ctx -> Index ctx tp -> f tp Source #

Return value of assignment.

empty :: forall {k} (f :: k -> Type). Assignment f (EmptyCtx :: Ctx k) Source #

Return empty assignment

replicate :: forall {k} (ctx :: Ctx k) f. Size ctx -> (forall (tp :: k). f tp) -> Assignment f ctx Source #

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

zipWith :: forall {k} f g h (a :: Ctx k). (forall (x :: k). f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a Source #

adjust :: forall {k} f (tp :: k) (ctx :: Ctx k). (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.

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

type family (x :: Ctx k) <+> (y :: Ctx k) :: Ctx k where ... Source #

Append two type-level contexts.

Equations

(x :: Ctx k) <+> (EmptyCtx :: Ctx k) = x
(x :: Ctx k) <+> (y ::> e :: Ctx k) = (x <+> y) ::> e

data Size (ctx :: Ctx k) Source #

Represents the size of a context.

Instances

Instances details

ShowF (Size :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: Ctx k) a. p (Size :: Ctx k -> Type) -> q tp -> (Show (Size tp) => a) -> a Source # showF :: forall (tp :: Ctx k). Size tp -> String Source # showsPrecF :: forall (tp :: Ctx k). Int -> Size tp -> String -> String Source #
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 #

size :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> Size ctx Source #

Return number of elements in assignment.

extend :: forall {k} f (ctx :: Ctx k) (x :: k). Assignment f ctx -> f x -> Assignment f (ctx ::> x) Source #

Extend an indexed vector with a new entry.

update :: forall {k} (ctx :: Ctx k) (tp :: k) f. 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.

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

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

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

Instances

Instances details

ApplyEmbedding' (Index :: Ctx k' -> k' -> Type) Source #
Instance details Defined in Data.Parameterized.Context Methods applyEmbedding' :: forall (ctx :: Ctx k') (ctx' :: Ctx k') (v :: k'). CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v Source #
ExtendContext' (Index :: Ctx k' -> k' -> Type) Source #
Instance details Defined in Data.Parameterized.Context Methods extendContext' :: forall (ctx :: Ctx k') (ctx' :: Ctx k') (v :: k'). Diff 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 :: forall (a :: k) (b :: k). Index ctx a -> Index ctx b -> Maybe (a :~: b) #
EqF (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods eqF :: forall (a :: k). Index ctx a -> Index ctx a -> Bool Source #
HashableF (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods hashWithSaltF :: forall (tp :: k). Int -> Index ctx tp -> Int Source # hashF :: forall (tp :: k). Index ctx tp -> Int Source #
OrdF (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods compareF :: forall (x :: k) (y :: k). Index ctx x -> Index ctx y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). Index ctx x -> Index ctx y -> Bool Source # ltF :: forall (x :: k) (y :: k). Index ctx x -> Index ctx y -> Bool Source # geqF :: forall (x :: k) (y :: k). Index ctx x -> Index ctx y -> Bool Source # gtF :: forall (x :: k) (y :: k). Index ctx x -> Index ctx y -> Bool Source #
ShowF (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: k) a. p (Index ctx) -> q tp -> (Show (Index ctx tp) => a) -> a Source # showF :: forall (tp :: k). Index ctx tp -> String Source # showsPrecF :: forall (tp :: k). Int -> Index ctx tp -> String -> String Source #
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 #
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 #
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 #

generate :: forall {k} (ctx :: Ctx k) f. Size ctx -> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx Source #

Generate an assignment

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

Generate an assignment in an Applicative context

data Ctx k Source #

Kind Ctx k comprises lists of types of kind k.

Constructors

EmptyCtx
(Ctx k) ::> k

Instances

Instances details

FoldableFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: Ctx k). Assignment f x -> m Source # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source # foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source # foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: Ctx k). Assignment f x -> [a] Source #
FunctorFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: Ctx k). Assignment f x -> Assignment g x Source #
OrdFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: Ctx k) (y :: Ctx k). 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 :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Maybe (x :~: y) Source #
TraversableFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: Ctx k). Assignment f x -> m (Assignment g x) Source #
FoldableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods ifoldMapFC :: forall f m (z :: Ctx k). Monoid m => (forall (x :: k). IndexF (Assignment f z) x -> f x -> m) -> Assignment f z -> m Source # ifoldrFC :: forall (z :: Ctx k) f b. (forall (x :: k). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b Source # ifoldlFC :: forall f b (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> b -> f x -> b) -> b -> Assignment f z -> b Source # ifoldrFC' :: forall f b (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b Source # ifoldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source # itoListFC :: forall f a (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> a) -> Assignment f z -> [a] Source #
FunctorFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods imapFC :: forall f g (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> g x) -> Assignment f z -> Assignment g z Source #
TraversableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods itraverseFC :: forall m (z :: Ctx k) f g. Applicative m => (forall (x :: k). IndexF (Assignment f z) x -> f x -> m (g x)) -> Assignment f z -> m (Assignment g z) Source #
Category (Diff :: Ctx k -> Ctx k -> Type) Source #	Implemented with `noDiff` and `addDiff`
Instance details Defined in Data.Parameterized.Context.Unsafe Methods id :: forall (a :: Ctx k). Diff a a # (.) :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k). Diff b c -> Diff a b -> Diff a c #
ShowF (Size :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: Ctx k) a. p (Size :: Ctx k -> Type) -> q tp -> (Show (Size tp) => a) -> a Source # showF :: forall (tp :: Ctx k). Size tp -> String Source # showsPrecF :: forall (tp :: Ctx k). Int -> Size tp -> String -> String Source #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) #
EqF f => EqF (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods eqF :: forall (a :: Ctx k). Assignment f a -> Assignment f a -> Bool Source #
(HashableF f, TestEquality f) => HashableF (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods hashWithSaltF :: forall (tp :: Ctx k). Int -> Assignment f tp -> Int Source # hashF :: forall (tp :: Ctx k). Assignment f tp -> Int Source #
OrdF f => OrdF (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods compareF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> OrderingF x y Source # leqF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source # ltF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source # geqF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source # gtF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source #
ShowF f => ShowF (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: Ctx k) a. p (Assignment f) -> q tp -> (Show (Assignment f tp) => a) -> a Source # showF :: forall (tp :: Ctx k). Assignment f tp -> String Source # showsPrecF :: forall (tp :: Ctx k). Int -> Assignment f tp -> String -> String Source #
IsRepr f => IsRepr (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Ctx k) r. 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 :: Ctx k) 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 #

sizeInt :: forall {k} (ctx :: Ctx k). Size ctx -> Int Source #

Convert a context size to an Int.

zeroSize :: Size ('EmptyCtx :: Ctx k) Source #

The size of an empty context.

incSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp) Source #

Increment the size to the next value.

decSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx Source #

extSize :: forall {k} (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r Source #

Extend the size by a given difference.

addSize :: forall {k} (x :: Ctx k) (y :: Ctx k). 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 :: forall {k}. SizeView ('EmptyCtx :: Ctx k)
IncSize :: forall {k} (ctx1 :: Ctx k) (tp :: k). !(Size ctx1) -> SizeView (ctx1 '::> tp)

viewSize :: forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx Source #

Project a size

sizeToNatRepr :: forall {k} (items :: Ctx k). Size items -> NatRepr (CtxSize items) Source #

Convert a Size into a NatRepr.

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

A context that can be determined statically at compiler time.

Methods

knownSize :: Size ctx Source #

Instances

Instances details

KnownContext ('EmptyCtx :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods knownSize :: Size ('EmptyCtx :: Ctx k) Source #
KnownContext ctx => KnownContext (ctx '::> tp :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods knownSize :: Size (ctx '::> tp) Source #

noDiff :: forall {k} (l :: Ctx k). Diff l l Source #

The identity difference. Identity element of Category instance.

addDiff :: forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k). Diff a b -> Diff b c -> Diff a c Source #

The addition of differences. Flipped binary operation of Category instance.

extendRight :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Diff l r -> Diff l (r '::> tp) Source #

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

appendDiff :: forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r) Source #

data DiffView (a :: Ctx k) (b :: Ctx k) where Source #

Constructors

NoDiff :: forall {k} (a :: Ctx k). DiffView a a
ExtendRightDiff :: forall {k} (a :: Ctx k) (b1 :: Ctx k) (r :: k). Diff a b1 -> DiffView a (b1 '::> r)

viewDiff :: forall {k} (a :: Ctx k) (b :: Ctx k). 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

Instances details

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 :: Ctx k) (r :: Ctx k) where Source #

Proof that r = l + app for some app

Constructors

IsAppend :: forall {k} (app :: Ctx k) (l :: Ctx k). Size app -> IsAppend l (l <+> app)

diffIsAppend :: forall {k} (l :: Ctx k) (r :: Ctx k). 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

baseIndex :: forall {k} (tp :: k). Index (('EmptyCtx :: Ctx k) '::> tp) tp Source #

Index for first element in context.

skipIndex :: forall {k} (ctx :: Ctx k) (x :: k) (y :: k). Index ctx x -> Index (ctx '::> y) x Source #

Increase context while staying at same index.

lastIndex :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx ::> tp) -> Index (ctx ::> tp) tp Source #

Return the last index of a element.

nextIndex :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Index (ctx ::> tp) tp Source #

Return the index of a element one past the size.

leftIndex :: forall {k} (r :: Ctx k) (l :: Ctx k) (tp :: k). Size r -> Index l tp -> Index (l <+> r) tp Source #

Adapts an index in the left hand context of an append operation.

rightIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Size l -> Size r -> Index r tp -> Index (l <+> r) tp Source #

Adapts an index in the right hand context of an append operation.

extendIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). KnownDiff l r => Index l tp -> Index r tp Source #

extendIndex' :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Diff l r -> Index l tp -> Index r tp Source #

Compute an Index into a context r from an Index into a sub-context l of r.

extendIndexAppendLeft :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Size l -> Size r -> Index r tp -> Index (l <+> r) tp Source #

Compute an Index into an appended context from an Index into its suffix.

forIndex :: forall {k} (ctx :: Ctx k) r. Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r Source #

Given a size n, a function f, and an initial value v0, the expression forIndex n f v0 is equivalent to v0 when n is zero, and f (forIndex (n-1) f v0) n otherwise. Unlike the safe version, which starts from Index 0 and increments Index values, this version starts at Index (n-1) and decrements Index values to Index 0.

forIndexRange :: forall {k} (ctx :: Ctx k) r. Int -> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r Source #

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

intIndex :: forall {k} (ctx :: Ctx k). Int -> Size ctx -> Maybe (Some (Index ctx)) Source #

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

data IndexView (ctx :: Ctx k) (tp :: k) where Source #

View of indexes as pointing to the last element in the index range or pointing to an earlier element in a smaller range.

Constructors

IndexViewLast :: forall {k} (ctx1 :: Ctx k) (tp :: k). !(Size ctx1) -> IndexView (ctx1 '::> tp) tp
IndexViewInit :: forall {k} (ctx1 :: Ctx k) (tp :: k) (u :: k). !(Index ctx1 tp) -> IndexView (ctx1 '::> u) tp

Instances

Instances details

ShowF (IndexView ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: k) a. p (IndexView ctx) -> q tp -> (Show (IndexView ctx tp) => a) -> a Source # showF :: forall (tp :: k). IndexView ctx tp -> String Source # showsPrecF :: forall (tp :: k). Int -> IndexView ctx tp -> String -> String Source #
Show (IndexView ctx tp) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods showsPrec :: Int -> IndexView ctx tp -> ShowS # show :: IndexView ctx tp -> String # showList :: [IndexView ctx tp] -> ShowS #

viewIndex :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Index ctx tp -> IndexView ctx tp Source #

Project an index

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

Instances details

FoldableFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: Ctx k). Assignment f x -> m Source # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source # foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source # foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: Ctx k). Assignment f x -> [a] Source #
FunctorFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: Ctx k). Assignment f x -> Assignment g x Source #
OrdFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: Ctx k) (y :: Ctx k). 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 :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Maybe (x :~: y) Source #
TraversableFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: Ctx k). Assignment f x -> m (Assignment g x) Source #
FoldableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods ifoldMapFC :: forall f m (z :: Ctx k). Monoid m => (forall (x :: k). IndexF (Assignment f z) x -> f x -> m) -> Assignment f z -> m Source # ifoldrFC :: forall (z :: Ctx k) f b. (forall (x :: k). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b Source # ifoldlFC :: forall f b (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> b -> f x -> b) -> b -> Assignment f z -> b Source # ifoldrFC' :: forall f b (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b Source # ifoldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source # itoListFC :: forall f a (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> a) -> Assignment f z -> [a] Source #
FunctorFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods imapFC :: forall f g (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> g x) -> Assignment f z -> Assignment g z Source #
TraversableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods itraverseFC :: forall m (z :: Ctx k) f g. Applicative m => (forall (x :: k). IndexF (Assignment f z) x -> f x -> m (g x)) -> Assignment f z -> m (Assignment g z) Source #
IxedF k (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods ixF :: forall (x :: k). IndexF (Assignment f ctx) x -> Traversal' (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' :: forall (x :: k). IndexF (Assignment f ctx) x -> Lens' (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 :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) #
EqF f => EqF (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods eqF :: forall (a :: Ctx k). Assignment f a -> Assignment f a -> Bool Source #
(HashableF f, TestEquality f) => HashableF (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods hashWithSaltF :: forall (tp :: Ctx k). Int -> Assignment f tp -> Int Source # hashF :: forall (tp :: Ctx k). Assignment f tp -> Int Source #
OrdF f => OrdF (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods compareF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> OrderingF x y Source # leqF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source # ltF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source # geqF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source # gtF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source #
ShowF f => ShowF (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: Ctx k) a. p (Assignment f) -> q tp -> (Show (Assignment f tp) => a) -> a Source # showF :: forall (tp :: Ctx k). Assignment f tp -> String Source # showsPrecF :: forall (tp :: Ctx k). Int -> Assignment f tp -> String -> String Source #
IsRepr f => IsRepr (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Ctx k) r. 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 :: Ctx k) 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 #
NFData (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods rnf :: 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 #
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 #
(HashableF f, TestEquality 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 IndexF (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe type IndexF (Assignment f ctx) = Index ctx
type IxValueF (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe type IxValueF (Assignment f ctx) = f

adjustM :: forall {k} m f (tp :: k) (ctx :: Ctx k). 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 :: k -> Type) (ctx :: Ctx k) where Source #

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

Constructors

AssignEmpty :: forall {k} (f :: k -> Type). AssignView f ('EmptyCtx :: Ctx k)
AssignExtend :: forall {k} (f :: k -> Type) (ctx1 :: Ctx k) (tp :: k). Assignment f ctx1 -> f tp -> AssignView f (ctx1 '::> tp)

viewAssign :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> AssignView f ctx Source #

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

(!^) :: forall {k} (l :: Ctx k) (r :: Ctx k) f (tp :: k). 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.

(<++>) :: forall {k} (f :: k -> Type) (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Assignment f (x <+> y) Source #

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

This represents a contiguous range of indices.

allRange :: forall {k} (ctx :: Ctx k). Size ctx -> IndexRange ctx ctx Source #

Return a range containing all indices in the context.

indexOfRange :: forall {k} (ctx :: Ctx k) (e :: k). IndexRange ctx ((EmptyCtx :: Ctx k) ::> e) -> Index ctx e Source #

indexOfRange returns the only index in a range.

dropHeadRange :: forall {k} (ctx :: Ctx k) (x :: Ctx k) (y :: Ctx k). IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y Source #

dropHeadRange r n drops the first n elements in r.

dropTailRange :: forall {k} (ctx :: Ctx k) (x :: Ctx k) (y :: Ctx k). IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x Source #

dropTailRange r n drops the last n elements in r.

type EmptyCtx = 'EmptyCtx :: Ctx k Source #

type SingleCtx (x :: k) = (EmptyCtx :: Ctx k) ::> x Source #

type (::>) (c :: Ctx k) (a :: k) = c '::> a Source #

type family CtxSize (a :: Ctx k) :: Nat where ... Source #

This type family computes the number of elements in a Ctx

Equations

CtxSize ('EmptyCtx :: Ctx k) = 0
CtxSize (xs '::> x :: Ctx k) = 1 + CtxSize xs

type CtxLookup (n :: Nat) (ctx :: Ctx k) = CtxLookupRight (FromLeft ctx n) ctx Source #

Lookup the value in a context by number, from the left. Produce a type error if the index is out of range.

type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k) = CtxUpdateRight (FromLeft ctx n) x ctx Source #

Update the value in a context by number, from the left. If the index is out of range, the context is unchanged.

type family CtxLookupRight (n :: Nat) (ctx :: Ctx k) :: k where ... Source #

Lookup the value in a context by number, from the right

Equations

CtxLookupRight 0 (ctx '::> r :: Ctx k) = r
CtxLookupRight n (ctx '::> r :: Ctx k) = CtxLookupRight (n - 1) ctx

type family CtxUpdateRight (n :: Nat) (x :: k) (ctx :: Ctx k) :: Ctx k where ... Source #

Update the value in a context by number, from the right. If the index is out of range, the context is unchanged.

Equations

CtxUpdateRight n (x :: k) ('EmptyCtx :: Ctx k) = 'EmptyCtx :: Ctx k
CtxUpdateRight 0 (x :: k) (ctx '::> old :: Ctx k) = ctx '::> x
CtxUpdateRight n (x :: k) (ctx '::> y :: Ctx k) = CtxUpdateRight (n - 1) x ctx '::> y

type family CtxFlatten (ctx :: Ctx (Ctx a)) :: Ctx a where ... Source #

Flatten a nested context

Equations

CtxFlatten (EmptyCtx :: Ctx (Ctx a)) = EmptyCtx :: Ctx a
CtxFlatten (ctxs ::> ctx :: Ctx (Ctx k)) = CtxFlatten ctxs <+> ctx

type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) where ... Source #

Helper type family used to generate descriptive error messages when an index is larger than the length of the Ctx being indexed.

Equations

CheckIx (ctx :: Ctx k) n 'True = ()
CheckIx (ctx :: Ctx k) n 'False = TypeError ((('Text "Index " ':<>: 'ShowType n) ':<>: 'Text " out of range in ") ':<>: 'ShowType ctx) :: Constraint

type ValidIx (n :: Nat) (ctx :: Ctx k) = CheckIx ctx n ((n + 1) <=? CtxSize ctx) Source #

A constraint that checks that the nat n is a valid index into the context ctx, and raises a type error if not.

type FromLeft (ctx :: Ctx k) (n :: Natural) = (CtxSize ctx - 1) - n Source #

Ctx is a snoc-list. In order to use the more intuitive left-to-right ordering of elements the desired index is subtracted from the total number of elements.

singleton :: forall {k} f (tp :: k). f tp -> Assignment f ((EmptyCtx :: Ctx k) ::> tp) Source #

Create a single element context.

toVector :: forall {k} f (tps :: Ctx k) e. Assignment f tps -> (forall (tp :: k). f tp -> e) -> Vector e Source #

Convert the assignment to a vector.

pattern (:>) :: forall {k} ctx' f ctx (tp :: k). () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx' infixl 9 Source #

Pattern synonym for extending an assignment on the right

pattern Empty :: forall {k} ctx f. () => ctx ~ (EmptyCtx :: Ctx k) => Assignment f ctx Source #

Pattern synonym for the empty assignment

decompose :: forall {k} f (ctx :: Ctx k) (tp :: k). Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp) Source #

null :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> Bool Source #

Return true if assignment is empty.

init :: forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k). Assignment f (ctx '::> tp) -> Assignment f ctx Source #

Return assignment with all but the last block.

last :: forall {k} f (ctx :: Ctx k) (tp :: k). Assignment f (ctx '::> tp) -> f tp Source #

Return the last element in the assignment.

view :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> AssignView f ctx Source #

Deprecated: Use viewAssign or the Empty and :> patterns instead.

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

take :: forall {k} (f :: k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx Source #

Return the prefix of an appended Assignment

drop :: forall {k} (f :: k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx' Source #

Return the suffix of an appended Assignment

forIndexM :: forall {k} (ctx :: Ctx k) m. Applicative m => Size ctx -> (forall (tp :: k). Index ctx tp -> m ()) -> m () Source #

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

generateSome :: forall {k} (f :: k -> Type). Int -> (Int -> Some f) -> Some (Assignment f) Source #

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

generateSomeM :: forall {k} m (f :: k -> Type). Applicative m => Int -> (Int -> m (Some f)) -> m (Some (Assignment f)) Source #

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

fromList :: forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f) Source #

Create an assignment from a list of values.

traverseAndCollect :: forall {k} w m (ctx :: Ctx k) f. (Monoid w, Applicative m) => (forall (tp :: k). Index ctx tp -> f tp -> m w) -> Assignment f ctx -> m w Source #

Visit each of the elements in an Assignment in order from left to right and collect the results using the provided Monoid.

traverseWithIndex_ :: forall {k} m (ctx :: Ctx k) f. Applicative m => (forall (tp :: k). Index ctx tp -> f tp -> m ()) -> Assignment f ctx -> m () Source #

Visit each of the elements in an Assignment in order from left to right, executing an action with each.

dropPrefix Source #

Arguments

:: forall {k} (f :: k -> Type) (xs :: Ctx k) (prefix :: Ctx k) a. TestEquality f
=> Assignment f xs	Assignment to split
-> Assignment f prefix	Expected prefix
-> a	error continuation
-> (forall (addl :: Ctx k). xs ~ (prefix <+> addl) => Assignment f addl -> a)	success continuation
-> a

Utility function for testing if xs is an assignment with prefix as a prefix, and computing the tail of xs not in the prefix, if so.

unzip :: forall {k} (f :: k -> Type) (g :: k -> Type) (ctx :: Ctx k). Assignment (Product f g) ctx -> (Assignment f ctx, Assignment g ctx) Source #

Unzip an assignment of pairs into a pair of assignments.

This is the inverse of zipWith Pair.

flattenAssignment :: forall {a} (f :: a -> Type) (ctxs :: Ctx (Ctx a)). Assignment (Assignment f) ctxs -> Assignment f (CtxFlatten ctxs) Source #

Flattens a nested assignment over a context of contexts ctxs :: Ctx (Ctx a) into a flat assignment over the flattened context CtxFlatten ctxs.

flattenSize :: forall {k} (ctxs :: Ctx (Ctx k)). Assignment (Size :: Ctx k -> Type) ctxs -> Size (CtxFlatten ctxs) Source #

Given the size of each context in ctxs, returns the size of CtxFlatten ctxs. You can obtain the former from any nested assignment Assignment (Assignment f) ctxs, by calling fmapFC size.

Context extension and embedding utilities

data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k) Source #

This datastructure contains a proof that the first context is embeddable in the second. This is useful if we want to add extend an existing term under a larger context.

Constructors

CtxEmbedding
Fields _ctxeSize :: Size ctx' _ctxeAssignment :: Assignment (Index ctx') ctx

class ExtendContext (f :: Ctx k -> Type) where Source #

Methods

extendContext :: forall (ctx :: Ctx k) (ctx' :: Ctx k). Diff ctx ctx' -> f ctx -> f ctx' Source #

class ExtendContext' (f :: Ctx k -> k' -> Type) where Source #

Methods

extendContext' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). Diff ctx ctx' -> f ctx v -> f ctx' v Source #

Instances

Instances details

ExtendContext' (Index :: Ctx k' -> k' -> Type) Source #
Instance details Defined in Data.Parameterized.Context Methods extendContext' :: forall (ctx :: Ctx k') (ctx' :: Ctx k') (v :: k'). Diff ctx ctx' -> Index ctx v -> Index ctx' v Source #

class ApplyEmbedding (f :: Ctx k -> Type) where Source #

Methods

applyEmbedding :: forall (ctx :: Ctx k) (ctx' :: Ctx k). CtxEmbedding ctx ctx' -> f ctx -> f ctx' Source #

class ApplyEmbedding' (f :: Ctx k -> k' -> Type) where Source #

Methods

applyEmbedding' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v Source #

Instances

Instances details

ApplyEmbedding' (Index :: Ctx k' -> k' -> Type) Source #
Instance details Defined in Data.Parameterized.Context Methods applyEmbedding' :: forall (ctx :: Ctx k') (ctx' :: Ctx k') (v :: k'). CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v Source #

identityEmbedding :: forall {k} (ctx :: Ctx k). Size ctx -> CtxEmbedding ctx ctx Source #

extendEmbeddingRightDiff :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (ctx'' :: Ctx k). Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx'' Source #

extendEmbeddingRight :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k). CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp) Source #

extendEmbeddingBoth :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k). CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp) Source #

appendEmbedding :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx') Source #

Prove that the prefix of an appended context is embeddable in it

appendEmbeddingLeft :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx') Source #

Prove that the suffix of an appended context is embeddable in it

ctxeSize :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) f. Functor f => (Size ctx' -> f (Size ctx')) -> CtxEmbedding ctx ctx' -> f (CtxEmbedding ctx ctx') Source #

ctxeAssignment :: forall {k} (ctx1 :: Ctx k) (ctx' :: Ctx k) (ctx2 :: Ctx k) f. Functor f => (Assignment (Index ctx') ctx1 -> f (Assignment (Index ctx') ctx2)) -> CtxEmbedding ctx1 ctx' -> f (CtxEmbedding ctx2 ctx') Source #

Static indexing and lenses for assignments

type Idx (n :: Nat) (ctx :: Ctx k) (r :: k) = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r) Source #

Constraint synonym used for getting an Index into a Ctx. n is the zero-based, left-counted index into the list of types ctx which has the type r.

field :: forall {k} (n :: Nat) (ctx :: Ctx k) (f :: k -> Type) (r :: k). Idx n ctx r => Lens' (Assignment f ctx) (f r) Source #

Get a lens for an position in an Assignment by zero-based, left-to-right position. The position must be specified using TypeApplications for the n parameter.

natIndex :: forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k). Idx n ctx r => Index ctx r Source #

Compute an Index value for a particular position in a Ctx. The TypeApplications extension will be needed to disambiguate the choice of the type n.

natIndexProxy :: forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k) proxy. Idx n ctx r => proxy n -> Index ctx r Source #

This version of natIndex is suitable for use without the TypeApplications extension.

Currying and uncurrying for assignments

type family CurryAssignment (ctx :: Ctx k) (f :: k -> Type) x where ... Source #

This type family is used to define currying/uncurrying operations on assignments. It is best understood by seeing its evaluation on several examples:

CurryAssignment EmptyCtx f x = x
CurryAssignment (EmptyCtx ::> a) f x = f a -> x
CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x
CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> x

Equations

CurryAssignment (EmptyCtx :: Ctx k) (f :: k -> Type) x = x
CurryAssignment (ctx ::> a :: Ctx k) (f :: k -> Type) x = CurryAssignment ctx f (f a -> x)

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

This class implements two methods that witness the isomorphism between curried and uncurried functions.

Methods

curryAssignment :: forall (f :: k -> Type) x. (Assignment f ctx -> x) -> CurryAssignment ctx f x Source #

Transform a function that accepts an assignment into one with a separate variable for each element of the assignment.

uncurryAssignment :: forall (f :: k -> Type) x. CurryAssignment ctx f x -> Assignment f ctx -> x Source #

Transform a curried function into one that accepts an assignment value.

Instances

Instances details

CurryAssignmentClass (EmptyCtx :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context Methods curryAssignment :: forall (f :: k -> Type) x. (Assignment f (EmptyCtx :: Ctx k) -> x) -> CurryAssignment (EmptyCtx :: Ctx k) f x Source # uncurryAssignment :: forall (f :: k -> Type) x. CurryAssignment (EmptyCtx :: Ctx k) f x -> Assignment f (EmptyCtx :: Ctx k) -> x Source #
CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context Methods curryAssignment :: forall (f :: k -> Type) x. (Assignment f (ctx ::> a) -> x) -> CurryAssignment (ctx ::> a) f x Source # uncurryAssignment :: forall (f :: k -> Type) x. CurryAssignment (ctx ::> a) f x -> Assignment f (ctx ::> a) -> x Source #

Size and Index values

size1 :: forall {k} (a :: k). Size ((EmptyCtx :: Ctx k) ::> a) Source #

size2 :: forall {k} (a :: k) (b :: k). Size (((EmptyCtx :: Ctx k) ::> a) ::> b) Source #

size3 :: forall {k} (a :: k) (b :: k) (c :: k). Size ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) Source #

size4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Size (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) Source #

size5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Size ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) Source #

size6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Size (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) Source #

i1of2 :: forall {k} (a :: k) (b :: k). Index (((EmptyCtx :: Ctx k) ::> a) ::> b) a Source #

i2of2 :: forall {k} (a :: k) (b :: k). Index (((EmptyCtx :: Ctx k) ::> a) ::> b) b Source #

i1of3 :: forall {k} (a :: k) (b :: k) (c :: k). Index ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) a Source #

i2of3 :: forall {k} (a :: k) (b :: k) (c :: k). Index ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) b Source #

i3of3 :: forall {k} (a :: k) (b :: k) (c :: k). Index ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) c Source #

i1of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) a Source #

i2of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) b Source #

i3of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) c Source #

i4of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) d Source #

i1of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) a Source #

i2of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) b Source #

i3of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) c Source #

i4of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) d Source #

i5of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) e Source #

i1of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a Source #

i2of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b Source #

i3of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c Source #

i4of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d Source #

i5of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e Source #

i6of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f Source #