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

Copyright | (c) Galois Inc 2014-2019
Maintainer | Joe Hendrix <jhendrix@galois.com>
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 `Assignment`s 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 `Assignment`s 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

- (!) :: 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
- 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)
- 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
- data Diff (l :: Ctx k) (r :: Ctx k)
- 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)
- 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)
- extend :: forall {k} f (ctx :: Ctx k) (x :: k). Assignment f ctx -> f x -> Assignment f (ctx ::> x)
- 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

(!) :: 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 Source # show :: Size ctx -> String Source # showList :: [Size ctx] -> ShowS Source #

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

Return number of elements in assignment.

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) Source #
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 Source # show :: Index ctx tp -> String Source # showList :: [Index ctx tp] -> ShowS Source #
Eq (Index ctx tp) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods (==) :: Index ctx tp -> Index ctx tp -> Bool Source # (/=) :: Index ctx tp -> Index ctx tp -> Bool Source #
Ord (Index ctx tp) Source # |

Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

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

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

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

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

max :: Index ctx tp -> Index ctx tp -> Index ctx tp Source #

min :: Index ctx tp -> Index ctx tp -> Index ctx tp Source #

Hashable (Index ctx tp) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods hashWithSalt :: Int -> Index ctx tp -> Int Source # hash :: Index ctx tp -> Int Source #

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 Source # (.) :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k). Diff b c -> Diff a b -> Diff a c Source #
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) Source #
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 #

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 Source # (.) :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k). Diff b c -> Diff a b -> Diff a c 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 Source # show :: IndexView ctx tp -> String Source # showList :: [IndexView ctx tp] -> ShowS Source #

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) Source #
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 -> () Source #
ShowF f => Show (Assignment f ctx) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods showsPrec :: Int -> Assignment f ctx -> ShowS Source # show :: Assignment f ctx -> String Source # showList :: [Assignment f ctx] -> ShowS Source #
TestEquality f => Eq (Assignment f ctx) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods (==) :: Assignment f ctx -> Assignment f ctx -> Bool Source # (/=) :: Assignment f ctx -> Assignment f ctx -> Bool Source #
OrdF f => Ord (Assignment f ctx) Source # |

Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

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

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

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

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

max :: Assignment f ctx -> Assignment f ctx -> Assignment f ctx Source #

min :: Assignment f ctx -> Assignment f ctx -> Assignment f ctx Source #

(HashableF f, TestEquality f) => Hashable (Assignment f ctx) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods hashWithSalt :: Int -> Assignment f ctx -> Int Source # hash :: Assignment f ctx -> Int Source #
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

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

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.

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 #