-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Classes and data structures for working with data-kind indexed types
--   
--   This packages contains collection classes and type representations
--   used for working with values that have a single parameter. It's
--   intended for things like expression libraries where one wishes to
--   leverage the Haskell type-checker to improve type-safety by encoding
--   the object language type system into data kinds.
@package parameterized-utils
@version 1.0.1


-- | This module declares classes for working with types with the kind
--   <tt>k -&gt; *</tt> for any kind <tt>k</tt>. These are generalizations
--   of the <a>Data.Functor.Classes</a> types as they work with any kind
--   <tt>k</tt>, and are not restricted to <a>*</a>.
module Data.Parameterized.Classes

-- | This class contains types where you can learn the equality of two
--   types from information contained in <i>terms</i>. Typically, only
--   singleton types should inhabit this class.
class TestEquality (f :: k -> *)

-- | Conditionally prove the equality of <tt>a</tt> and <tt>b</tt>.
testEquality :: TestEquality f => f a -> f b -> Maybe a :~: b

-- | Propositional equality. If <tt>a :~: b</tt> is inhabited by some
--   terminating value, then the type <tt>a</tt> is the same as the type
--   <tt>b</tt>. To use this equality in practice, pattern-match on the
--   <tt>a :~: b</tt> to get out the <tt>Refl</tt> constructor; in the body
--   of the pattern-match, the compiler knows that <tt>a ~ b</tt>.
data (:~:) (a :: k) (b :: k) :: forall k. () => k -> k -> *
[Refl] :: a :~: a

-- | <tt>EqF</tt> provides a method <tt>eqF</tt> for testing whether two
--   parameterized types are equal.
--   
--   Unlike <a>TestEquality</a>, this only works when the type arguments
--   are the same, and does not provide a proof that the types have the
--   same type when they are equal. Thus this can be implemented over
--   parameterized types that are unable to provide evidence that their
--   type arguments are equal.
class EqF (f :: k -> *)
eqF :: EqF f => f a -> f a -> Bool

-- | A polymorphic equality operator that generalizes <a>TestEquality</a>.
class PolyEq u v
polyEqF :: PolyEq u v => u -> v -> Maybe (u :~: v)
polyEq :: PolyEq u v => u -> v -> Bool

-- | A parameterized type that can be compared on distinct instances.
class TestEquality ktp => OrdF (ktp :: k -> *)

-- | compareF compares two keys with different type parameters. Instances
--   must ensure that keys are only equal if the type parameters are equal.
compareF :: OrdF ktp => ktp x -> ktp y -> OrderingF x y
leqF :: OrdF ktp => ktp x -> ktp y -> Bool
ltF :: OrdF ktp => ktp x -> ktp y -> Bool
geqF :: OrdF ktp => ktp x -> ktp y -> Bool
gtF :: OrdF ktp => ktp x -> ktp y -> Bool

-- | Compare two values, and if they are equal compare the next values,
--   otherwise return LTF or GTF
lexCompareF :: forall (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k). OrdF f => f a -> f b -> (a ~ b => OrderingF c d) -> OrderingF c d

-- | Ordering over two distinct types with a proof they are equal.
data OrderingF x y
[LTF] :: OrderingF x y
[EQF] :: OrderingF x x
[GTF] :: OrderingF x y

-- | `joinOrderingF x y` first compares on x, returning an equivalent value
--   if it is not <a>EQF</a>. If it is EQF, it returns <tt>y</tt>.
joinOrderingF :: forall (a :: j) (b :: j) (c :: k) (d :: k). OrderingF a b -> (a ~ b => OrderingF c d) -> OrderingF c d
orderingF_refl :: OrderingF x y -> Maybe (x :~: y)

-- | Convert <a>OrderingF</a> to standard ordering.
toOrdering :: OrderingF x y -> Ordering

-- | Convert standard ordering to <a>OrderingF</a>.
fromOrdering :: Ordering -> OrderingF x x

-- | A parameterized type that can be shown on all instances.
--   
--   To implement <tt><a>ShowF</a> g</tt>, one should implement an instance
--   <tt><a>Show</a> (g tp)</tt> for all argument types <tt>tp</tt>, then
--   write an empty instance <tt>instance <a>ShowF</a> g</tt>.
class ShowF (f :: k -> *)

-- | Provides a show instance for each type.
withShow :: ShowF f => p f -> q tp -> (Show (f tp) => a) -> a

-- | Provides a show instance for each type.
withShow :: (ShowF f, Show (f tp)) => p f -> q tp -> (Show (f tp) => a) -> a
showF :: forall tp. ShowF f => f tp -> String

-- | Like <a>showsPrec</a>, the precedence argument is <i>one more</i> than
--   the precedence of the enclosing context.
showsPrecF :: forall tp. ShowF f => Int -> f tp -> String -> String
showsF :: ShowF f => f tp -> String -> String

-- | A parameterized type that is hashable on all instances.
class HashableF (f :: k -> *)
hashWithSaltF :: HashableF f => Int -> f tp -> Int

-- | Hash with default salt.
hashF :: HashableF f => f tp -> Int

-- | An instance of <a>CoercibleF</a> gives a way to coerce between all the
--   types of a family. We generally use this to witness the fact that the
--   type parameter to <tt>rtp</tt> is a phantom type by giving an
--   implementation in terms of Data.Coerce.coerce.
class CoercibleF (rtp :: k -> *)
coerceF :: CoercibleF rtp => rtp a -> rtp b

-- | Parameterized generalization of the lens <tt>Ixed</tt> class.
class IxedF k m

-- | Given an index into a container, build a traversal that visits the
--   given element in the container, if it exists.
ixF :: forall (x :: k). IxedF k m => IndexF m x -> Traversal' m (IxValueF m x)

-- | Parameterized generalization of the lens <tt>Ixed</tt> class, but with
--   the guarantee that indexes exist in the container.
class IxedF k m => IxedF' k m

-- | Given an index into a container, build a lens that points into the
--   given element in the container.
ixF' :: forall (x :: k). IxedF' k m => IndexF m x -> Lens' m (IxValueF m x)

-- | Parameterized generalization of the lens <tt>At</tt> class.
class IxedF k m => AtF k m

-- | Given an index into a container, build a lens that points into the
--   given position in the container, whether or not it currently exists.
--   Setting values of <tt>atF</tt> to a <tt>Just</tt> value will insert
--   the value if it does not already exist.
atF :: forall (x :: k). AtF k m => IndexF m x -> Lens' m (Maybe (IxValueF m x))

-- | This class is parameterized by a kind <tt>k</tt> (typically a data
--   kind), a type constructor <tt>f</tt> of kind <tt>k -&gt; *</tt>
--   (typically a GADT of singleton types indexed by <tt>k</tt>), and an
--   index parameter <tt>ctx</tt> of kind <tt>k</tt>.
class KnownRepr (f :: k -> *) (ctx :: k)
knownRepr :: KnownRepr f ctx => f ctx

-- | The <a>isJust</a> function returns <a>True</a> iff its argument is of
--   the form <tt>Just _</tt>.
--   
--   <h4><b>Examples</b></h4>
--   
--   Basic usage:
--   
--   <pre>
--   &gt;&gt;&gt; isJust (Just 3)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isJust (Just ())
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isJust Nothing
--   False
--   </pre>
--   
--   Only the outer constructor is taken into consideration:
--   
--   <pre>
--   &gt;&gt;&gt; isJust (Just Nothing)
--   True
--   </pre>
isJust :: () => Maybe a -> Bool
instance Data.Hashable.Class.Hashable a => Data.Parameterized.Classes.HashableF (Data.Functor.Const.Const a)
instance GHC.Show.Show x => Data.Parameterized.Classes.ShowF (Data.Functor.Const.Const x)
instance GHC.Classes.Eq a => Data.Parameterized.Classes.EqF (Data.Functor.Const.Const a)
instance Data.Parameterized.Classes.CoercibleF (Data.Functor.Const.Const x)


-- | This module defines type-level lists used for representing the type of
--   variables in a context.
module Data.Parameterized.Ctx

-- | Kind <tt><a>Ctx</a> k</tt> comprises lists of types of kind
--   <tt>k</tt>.
data Ctx k
EmptyCtx :: Ctx k
(::>) :: Ctx k -> k -> Ctx k
type EmptyCtx =  'EmptyCtx
type SingleCtx x = EmptyCtx ::> x
type (c :: Ctx k) ::> (a :: k) = c ::> a

-- | Append two type-level contexts.

-- | This type family computes the number of elements in a <a>Ctx</a>

-- | Lookup the value in a context by number, from the left. Produce a type
--   error if the index is out of range.
type CtxLookup (n :: Nat) (ctx :: Ctx k) = CtxLookupRight (FromLeft ctx n) ctx

-- | Update the value in a context by number, from the left. If the index
--   is out of range, the context is unchanged.
type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k) = CtxUpdateRight (FromLeft ctx n) x ctx

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

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

-- | Helper type family used to generate descriptive error messages when an
--   index is larger than the length of the <a>Ctx</a> being indexed.

-- | A constraint that checks that the nat <tt>n</tt> is a valid index into
--   the context <tt>ctx</tt>, and raises a type error if not.
type ValidIx (n :: Nat) (ctx :: Ctx k) = CheckIx ctx n (n + 1 <=? CtxSize ctx)

-- | <a>Ctx</a> 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.
type FromLeft ctx n = CtxSize ctx - 1 - n


-- | This reflects type level proofs involving contexts.
module Data.Parameterized.Ctx.Proofs
leftId :: p x -> (EmptyCtx <+> x) :~: x
assoc :: p x -> q y -> r z -> x <+> (y <+> z) :~: (x <+> y) <+> z


-- | This module provides a simple generator of new indexes in the ST
--   monad. It is predictable and not intended for cryptographic purposes.
--   
--   NOTE: the <a>TestEquality</a> and <a>OrdF</a> instances for the
--   <a>Nonce</a> type simply compare the generated nonce values and then
--   assert to the compiler (via <a>unsafeCoerce</a>) that the types
--   ascribed to the nonces are equal if their values are equal. This is
--   only OK because of the discipline by which nonces should be used: they
--   should only be generated from a <a>NonceGenerator</a> (i.e., should
--   not be built directly), and nonces from different generators must
--   never be compared! Arranging to compare Nonces from different origins
--   would allow users to build <a>unsafeCoerce</a> via the
--   <a>testEquality</a> function.
--   
--   A somewhat safer API would be to brand the generated Nonces with the
--   state type variable of the NonceGenerator whence they came, and to
--   only provide NonceGenerators via a Rank-2 continuation-passing API,
--   similar to <a>runST</a>. This would (via a meta-argument involving
--   parametricity) help to prevent nonces of different origin from being
--   compared. However, this would force us to push the <a>ST</a> type
--   brand into a significant number of other structures and APIs.
--   
--   Another alternative would be to use <tt>unsafePerformIO</tt> magic to
--   make a global nonce generator, and make that the only way to generate
--   nonces. It is not clear that this is actually an improvement from a
--   type safety point of view, but an argument could be made.
--   
--   For now, be careful using Nonces, and ensure that you do not mix
--   Nonces from different NonceGenerators.
module Data.Parameterized.Nonce.Unsafe

-- | A simple type that for getting fresh indices in the <a>ST</a> monad.
--   The type parameter <tt>s</tt> is used for the <a>ST</a> monad
--   parameter.
data NonceGenerator s

-- | Create a new counter.
newNonceGenerator :: ST s (NonceGenerator s)

-- | Get a fresh index and increment the counter.
freshNonce :: NonceGenerator s -> ST s (Nonce tp)

-- | Return true if counter has reached the limit, and can't be incremented
--   without risk of error.
atLimit :: NonceGenerator s -> ST s Bool

-- | An index generated by the counter.
data Nonce (tp :: k)
indexValue :: Nonce tp -> Word64
instance forall k (tp :: k). GHC.Show.Show (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance forall k (tp :: k). Data.Hashable.Class.Hashable (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance forall k (tp :: k). GHC.Classes.Ord (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance forall k (tp :: k). GHC.Classes.Eq (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance Data.Type.Equality.TestEquality Data.Parameterized.Nonce.Unsafe.Nonce
instance Data.Parameterized.Classes.OrdF Data.Parameterized.Nonce.Unsafe.Nonce
instance Data.Parameterized.Classes.HashableF Data.Parameterized.Nonce.Unsafe.Nonce
instance Data.Parameterized.Classes.ShowF Data.Parameterized.Nonce.Unsafe.Nonce


-- | This module provides <a>Some</a>, a GADT that hides a type parameter.
module Data.Parameterized.Some
data Some (f :: k -> *)
Some :: (f x) -> Some

-- | Project out of Some.
viewSome :: (forall tp. f tp -> r) -> Some f -> r

-- | Apply function to inner value.
mapSome :: (forall tp. f tp -> g tp) -> Some f -> Some g

-- | Modify the inner value.
traverseSome :: Functor m => (forall tp. f tp -> m (g tp)) -> Some f -> m (Some g)

-- | Modify the inner value.
traverseSome_ :: Functor m => (forall tp. f tp -> m ()) -> Some f -> m ()
instance forall k (f :: k -> *). Data.Type.Equality.TestEquality f => GHC.Classes.Eq (Data.Parameterized.Some.Some f)
instance forall k (f :: k -> *). Data.Parameterized.Classes.OrdF f => GHC.Classes.Ord (Data.Parameterized.Some.Some f)
instance forall k (f :: k -> *). Data.Parameterized.Classes.HashableF f => Data.Hashable.Class.Hashable (Data.Parameterized.Some.Some f)
instance forall k (f :: k -> *). Data.Parameterized.Classes.ShowF f => GHC.Show.Show (Data.Parameterized.Some.Some f)


-- | This module provides a simple generator of new indexes in the ST
--   monad. It is predictable and not intended for cryptographic purposes.
--   
--   This module also provides a global nonce generator that will generate
--   2^64 nonces before looping.
--   
--   NOTE: The <a>TestEquality</a> and <a>OrdF</a> instances for the
--   <a>Nonce</a> type simply compare the generated nonce values and then
--   assert to the compiler (via <a>unsafeCoerce</a>) that the types
--   ascribed to the nonces are equal if their values are equal.
module Data.Parameterized.Nonce

-- | Provides a monadic action for getting fresh typed names.
--   
--   The first type parameter <tt>m</tt> is the monad used for generating
--   names, and the second parameter <tt>s</tt> is used for the counter.
data NonceGenerator (m :: * -> *) (s :: *)
freshNonce :: NonceGenerator m s -> forall k (tp :: k). m (Nonce s tp)

-- | An index generated by the counter.
data Nonce (s :: *) (tp :: k)
indexValue :: Nonce s tp -> Word64

-- | Create a new nonce generator in the ST monad.
newSTNonceGenerator :: ST t (Some (NonceGenerator (ST t)))

-- | Create a new nonce generator in the ST monad.
newIONonceGenerator :: IO (Some (NonceGenerator IO))

-- | Create a new nonce generator in the IO monad.
withIONonceGenerator :: (forall s. NonceGenerator IO s -> IO r) -> IO r

-- | Run a ST computation with a new nonce generator in the ST monad.
withSTNonceGenerator :: (forall s. NonceGenerator (ST t) s -> (ST t) r) -> ST t r

-- | Create a new counter.
withGlobalSTNonceGenerator :: (forall t. NonceGenerator (ST t) t -> ST t r) -> r
data GlobalNonceGenerator

-- | A nonce generator that uses a globally-defined counter.
globalNonceGenerator :: NonceGenerator IO GlobalNonceGenerator
instance forall s k (tp :: k). GHC.Show.Show (Data.Parameterized.Nonce.Nonce s tp)
instance forall s k (tp :: k). Data.Hashable.Class.Hashable (Data.Parameterized.Nonce.Nonce s tp)
instance forall s k (tp :: k). GHC.Classes.Ord (Data.Parameterized.Nonce.Nonce s tp)
instance forall s k (tp :: k). GHC.Classes.Eq (Data.Parameterized.Nonce.Nonce s tp)
instance Data.Type.Equality.TestEquality (Data.Parameterized.Nonce.Nonce s)
instance Data.Parameterized.Classes.OrdF (Data.Parameterized.Nonce.Nonce s)
instance Data.Parameterized.Classes.HashableF (Data.Parameterized.Nonce.Nonce s)
instance Data.Parameterized.Classes.ShowF (Data.Parameterized.Nonce.Nonce s)


-- | This module provides a typeclass and monad transformers for generating
--   nonces.
module Data.Parameterized.Nonce.Transformers

-- | A <a>MonadNonce</a> is a monad that can generate fresh <a>Nonce</a>s
--   in a given set (where we view the phantom type parameter of
--   <a>Nonce</a> as a designator of the set that the <a>Nonce</a> came
--   from).
class Monad m => MonadNonce m where {
    type family NonceSet m :: *;
}
freshNonceM :: forall (tp :: k). MonadNonce m => m (Nonce (NonceSet m) tp)

-- | This transformer adds a nonce generator to a given monad.
newtype NonceT s m a
NonceT :: ReaderT (NonceGenerator m s) m a -> NonceT s m a
[runNonceT] :: NonceT s m a -> ReaderT (NonceGenerator m s) m a

-- | Helper type to build a <a>MonadNonce</a> from the <a>ST</a> monad.
type NonceST t s = NonceT s (ST t)

-- | Helper type to build a <a>MonadNonce</a> from the <a>IO</a> monad.
type NonceIO s = NonceT s IO

-- | Return the actual <a>NonceGenerator</a> used in an <a>ST</a>
--   computation.
getNonceSTGen :: NonceST t s (NonceGenerator (ST t) s)

-- | Run a <a>NonceST</a> computation with a fresh <a>NonceGenerator</a>.
runNonceST :: (forall t s. NonceST t s a) -> a

-- | Run a <a>NonceIO</a> computation with a fresh <a>NonceGenerator</a>
--   inside <a>IO</a>.
runNonceIO :: (forall s. NonceIO s a) -> IO a
instance GHC.Base.Monad m => GHC.Base.Monad (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance GHC.Base.Applicative m => GHC.Base.Applicative (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance GHC.Base.Functor m => GHC.Base.Functor (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance Control.Monad.Trans.Class.MonadTrans (Data.Parameterized.Nonce.Transformers.NonceT s)
instance GHC.Base.Monad m => Data.Parameterized.Nonce.Transformers.MonadNonce (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance Data.Parameterized.Nonce.Transformers.MonadNonce m => Data.Parameterized.Nonce.Transformers.MonadNonce (Control.Monad.Trans.State.Lazy.StateT s m)


-- | This defines a type <a>NatRepr</a> for representing a type-level
--   natural at runtime. This can be used to branch on a type-level value.
--   For each <tt>n</tt>, <tt>NatRepr n</tt> contains a single value
--   containing the vlaue <tt>n</tt>. This can be used to help use
--   type-level variables on code with data dependendent types.
--   
--   The <a>TestEquality</a> instance for <a>NatRepr</a> is implemented
--   using <a>unsafeCoerce</a>, as is the <a>isZeroNat</a> function. This
--   should be typesafe because we maintain the invariant that the integer
--   value contained in a NatRepr value matches its static type.
module Data.Parameterized.NatRepr

-- | A runtime presentation of a type-level <a>Nat</a>.
--   
--   This can be used for performing dynamic checks on a type-level natural
--   numbers.
data NatRepr (n :: Nat)

-- | The underlying integer value of the number.
natValue :: NatRepr n -> Integer

-- | This generates a NatRepr from a type-level context.
knownNat :: forall n. KnownNat n => NatRepr n

-- | <i>Deprecated: This function is potentially unsafe and is schedueled
--   to be removed.</i>
withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
data IsZeroNat n
[ZeroNat] :: IsZeroNat 0
[NonZeroNat] :: IsZeroNat (n + 1)
isZeroNat :: NatRepr n -> IsZeroNat n

-- | Result of comparing two numbers.
data NatComparison m n
[NatLT] :: x + 1 <= x + (y + 1) => !(NatRepr y) -> NatComparison x (x + (y + 1))
[NatEQ] :: NatComparison x x
[NatGT] :: x + 1 <= x + (y + 1) => !(NatRepr y) -> NatComparison (x + (y + 1)) x
compareNat :: NatRepr m -> NatRepr n -> NatComparison m n

-- | Decrement a <tt>NatRepr</tt>
decNat :: (1 <= n) => NatRepr n -> NatRepr (n - 1)

-- | Get the predicessor of a nat
predNat :: NatRepr (n + 1) -> NatRepr n

-- | Increment a <tt>NatRepr</tt>
incNat :: NatRepr n -> NatRepr (n + 1)
addNat :: NatRepr m -> NatRepr n -> NatRepr (m + n)
subNat :: (n <= m) => NatRepr m -> NatRepr n -> NatRepr (m - n)
divNat :: (1 <= n) => NatRepr (m * n) -> NatRepr n -> NatRepr m
halfNat :: NatRepr (n + n) -> NatRepr n
withDivModNat :: forall n m a. NatRepr n -> NatRepr m -> (forall div mod. (n ~ ((div * m) + mod)) => NatRepr div -> NatRepr mod -> a) -> a
natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)
someNat :: Integer -> Maybe (Some NatRepr)

-- | Return the maximum of two nat representations.
maxNat :: NatRepr m -> NatRepr n -> Some NatRepr

-- | Recursor for natural numbeers.
natRec :: forall m f. NatRepr m -> f 0 -> (forall n. NatRepr n -> f n -> f (n + 1)) -> f m

-- | Apply a function to each element in a range; return the list of values
--   obtained.
natForEach :: forall l h a. NatRepr l -> NatRepr h -> (forall n. (l <= n, n <= h) => NatRepr n -> a) -> [a]
data NatCases m n
[NatCaseLT] :: LeqProof (m + 1) n -> NatCases m n
[NatCaseEQ] :: NatCases m m
[NatCaseGT] :: LeqProof (n + 1) m -> NatCases m n
testNatCases :: forall m n. NatRepr m -> NatRepr n -> NatCases m n

-- | Return the value of the nat representation.
widthVal :: NatRepr n -> Int

-- | Return minimum unsigned value for bitvector with given width (always
--   0).
minUnsigned :: NatRepr w -> Integer

-- | Return maximum unsigned value for bitvector with given width.
maxUnsigned :: NatRepr w -> Integer

-- | Return minimum value for bitvector in 2s complement with given width.
minSigned :: (1 <= w) => NatRepr w -> Integer

-- | Return maximum value for bitvector in 2s complement with given width.
maxSigned :: (1 <= w) => NatRepr w -> Integer

-- | <tt>toUnsigned w i</tt> maps <tt>i</tt> to a <tt>i <a>mod</a>
--   2^w</tt>.
toUnsigned :: NatRepr w -> Integer -> Integer

-- | <tt>toSigned w i</tt> interprets the least-significant <tt>w</tt> bits
--   in <tt>i</tt> as a signed number in two's complement notation and
--   returns that value.
toSigned :: (1 <= w) => NatRepr w -> Integer -> Integer

-- | <tt>unsignedClamp w i</tt> rounds <tt>i</tt> to the nearest value
--   between <tt>0</tt> and <tt>2^w-1</tt> (inclusive).
unsignedClamp :: NatRepr w -> Integer -> Integer

-- | <tt>signedClamp w i</tt> rounds <tt>i</tt> to the nearest value
--   between <tt>-2^(w-1)</tt> and <tt>2^(w-1)-1</tt> (inclusive).
signedClamp :: (1 <= w) => NatRepr w -> Integer -> Integer

-- | <tt>LeqProof m n</tt> is a type whose values are only inhabited when
--   <tt>m</tt> is less than or equal to <tt>n</tt>.
data LeqProof m n
[LeqProof] :: (m <= n) => LeqProof m n

-- | <tt>x <a>testLeq</a> y</tt> checks whether <tt>x</tt> is less than or
--   equal to <tt>y</tt>.
testLeq :: forall m n. NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testStrictLeq :: forall m n. (m <= n) => NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)

-- | Apply reflexivity to LeqProof
leqRefl :: forall f n. f n -> LeqProof n n

-- | Apply transitivity to LeqProof
leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p

-- | Add both sides of two inequalities
leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)

-- | Subtract sides of two inequalities.
leqSub2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)

-- | Congruence rule for multiplication
leqMulCongr :: LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)

-- | Create a leqProof using two proxies
leqProof :: (m <= n) => f m -> g n -> LeqProof m n
withLeqProof :: LeqProof m n -> ((m <= n) => a) -> a

-- | Test whether natural number is positive.
isPosNat :: NatRepr n -> Maybe (LeqProof 1 n)

-- | Produce proof that adding a value to the larger element in an LeqProof
--   is larger
leqAdd :: forall f m n p. LeqProof m n -> f p -> LeqProof m (n + p)

-- | Produce proof that subtracting a value from the smaller element is
--   smaller.
leqSub :: forall m n p. LeqProof m n -> LeqProof p m -> LeqProof (m - p) n

-- | Multiplying two positive numbers results in a positive number.
leqMulPos :: forall p q x y. (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y)
leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)
addIsLeq :: f n -> g m -> LeqProof n (n + m)
withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> ((n <= n + m) => NatRepr (n + m) -> a) -> a
addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n)
withAddPrefixLeq :: NatRepr n -> NatRepr m -> ((m <= n + m) => a) -> a
addIsLeqLeft1 :: forall n n' m. LeqProof (n + n') m -> LeqProof n m
dblPosIsPos :: forall n. LeqProof 1 n -> LeqProof 1 (n + n)
leqMulMono :: (1 <= x) => p x -> q y -> LeqProof y (x * y)

-- | Produce evidence that + is commutative.
plusComm :: forall f m g n. f m -> g n -> m + n :~: n + m

-- | Produce evidence that * is commutative.
mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)

-- | Cancel an add followed b a subtract
plusMinusCancel :: forall f m g n. f m -> g n -> (m + n) - n :~: m
minusPlusCancel :: forall f m g n. (n <= m) => f m -> g n -> (m - n) + n :~: m
addMulDistribRight :: forall n m p f g h. f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p -> ((((n * p) + (m * p)) ~ ((n + m) * p)) => a) -> a
withSubMulDistribRight :: forall n m p f g h a. (m <= n) => f n -> g m -> h p -> ((((n * p) - (m * p)) ~ ((n - m) * p)) => a) -> a
mulCancelR :: (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)
mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n)

-- | Addition of type-level naturals.

-- | Subtraction of type-level naturals.

-- | Multiplication of type-level naturals.

-- | Comparison of type-level naturals, as a constraint.
type (<=) (x :: Nat) (y :: Nat) = x <=? y ~ True

-- | This class contains types where you can learn the equality of two
--   types from information contained in <i>terms</i>. Typically, only
--   singleton types should inhabit this class.
class TestEquality (f :: k -> *)

-- | Conditionally prove the equality of <tt>a</tt> and <tt>b</tt>.
testEquality :: TestEquality f => f a -> f b -> Maybe a :~: b

-- | Propositional equality. If <tt>a :~: b</tt> is inhabited by some
--   terminating value, then the type <tt>a</tt> is the same as the type
--   <tt>b</tt>. To use this equality in practice, pattern-match on the
--   <tt>a :~: b</tt> to get out the <tt>Refl</tt> constructor; in the body
--   of the pattern-match, the compiler knows that <tt>a ~ b</tt>.
data (:~:) (a :: k) (b :: k) :: forall k. () => k -> k -> *
[Refl] :: a :~: a
data Some (f :: k -> *)
instance Data.Hashable.Class.Hashable (Data.Parameterized.NatRepr.NatRepr n)
instance Data.Parameterized.Classes.OrdF Data.Parameterized.NatRepr.NatRepr
instance GHC.Classes.Eq (Data.Parameterized.NatRepr.NatRepr m)
instance Data.Type.Equality.TestEquality Data.Parameterized.NatRepr.NatRepr
instance Data.Parameterized.Classes.PolyEq (Data.Parameterized.NatRepr.NatRepr m) (Data.Parameterized.NatRepr.NatRepr n)
instance GHC.Show.Show (Data.Parameterized.NatRepr.NatRepr n)
instance Data.Parameterized.Classes.ShowF Data.Parameterized.NatRepr.NatRepr
instance Data.Parameterized.Classes.HashableF Data.Parameterized.NatRepr.NatRepr
instance GHC.TypeNats.KnownNat n => Data.Parameterized.Classes.KnownRepr Data.Parameterized.NatRepr.NatRepr n


-- | This module provides a ST-based hashtable for parameterized keys and
--   values.
--   
--   NOTE: This API makes use of unsafeCoerce to implement the
--   parameterized hashtable abstraction. This should be typesafe provided
--   the <a>TestEquality</a> instance on the key type is implemented
--   soundly.
module Data.Parameterized.HashTable

-- | A hash table mapping nonces to values.
data HashTable s (key :: k -> *) (val :: k -> *)

-- | Create a new empty table.
new :: ST s (HashTable s key val)

-- | Create a new empty table to hold <tt>n</tt> elements.
newSized :: Int -> ST s (HashTable s k v)

-- | Create a hash table that is a copy of the current one.
clone :: (HashableF key, TestEquality key) => HashTable s key val -> ST s (HashTable s key val)

-- | Lookup value of key in table.
lookup :: (HashableF key, TestEquality key) => HashTable s key val -> key tp -> ST s (Maybe (val tp))

-- | Insert new key and value mapping into table.
insert :: (HashableF key, TestEquality key) => HashTable s (key :: k -> *) (val :: k -> *) -> key tp -> val tp -> ST s ()

-- | Return true if the key is in the hash table.
member :: (HashableF key, TestEquality key) => HashTable s (key :: k -> *) (val :: k -> *) -> key (tp :: k) -> ST s Bool

-- | Delete an element from the hash table.
delete :: (HashableF key, TestEquality key) => HashTable s (key :: k -> *) (val :: k -> *) -> key (tp :: k) -> ST s ()
clear :: (HashableF key, TestEquality key) => HashTable s (key :: k -> *) (val :: k -> *) -> ST s ()

-- | A parameterized type that is hashable on all instances.
class HashableF (f :: k -> *)
hashWithSaltF :: HashableF f => Int -> f tp -> Int

-- | Hash with default salt.
hashF :: HashableF f => f tp -> Int

-- | <tt>RealWorld</tt> is deeply magical. It is <i>primitive</i>, but it
--   is not <i>unlifted</i> (hence <tt>ptrArg</tt>). We never manipulate
--   values of type <tt>RealWorld</tt>; it's only used in the type system,
--   to parameterise <tt>State#</tt>.
data RealWorld


-- | This defines a type family <a>SymbolRepr</a> for representing a
--   type-level string (AKA symbol) at runtime. This can be used to branch
--   on a type-level value.
--   
--   The <a>TestEquality</a> and <a>OrdF</a> instances for
--   <a>SymbolRepr</a> are implemented using <a>unsafeCoerce</a>. This
--   should be typesafe because we maintain the invariant that the string
--   value contained in a SymbolRepr value matches its static type.
--   
--   At the type level, symbols have very few operations, so SymbolRepr
--   correspondingly has very few functions that manipulate them.
module Data.Parameterized.SymbolRepr

-- | A runtime representation of a GHC type-level symbol.
data SymbolRepr (nm :: Symbol)

-- | The underlying text representation of the symbol
symbolRepr :: SymbolRepr nm -> Text

-- | Generate a value representative for the type level symbol.
knownSymbol :: KnownSymbol s => SymbolRepr s

-- | Generate a symbol representative at runtime. The type-level symbol
--   will be abstract, as it is hidden by the <a>Some</a> constructor.
someSymbol :: Text -> Some SymbolRepr

-- | (Kind) This is the kind of type-level symbols. Declared here because
--   class IP needs it
data Symbol

-- | This class gives the string associated with a type-level symbol. There
--   are instances of the class for every concrete literal: "hello", etc.
class KnownSymbol (n :: Symbol)
instance GHC.TypeLits.KnownSymbol s => Data.Parameterized.Classes.KnownRepr Data.Parameterized.SymbolRepr.SymbolRepr s
instance Data.Type.Equality.TestEquality Data.Parameterized.SymbolRepr.SymbolRepr
instance Data.Parameterized.Classes.OrdF Data.Parameterized.SymbolRepr.SymbolRepr
instance GHC.Classes.Eq (Data.Parameterized.SymbolRepr.SymbolRepr x)
instance GHC.Classes.Ord (Data.Parameterized.SymbolRepr.SymbolRepr x)
instance Data.Parameterized.Classes.HashableF Data.Parameterized.SymbolRepr.SymbolRepr
instance Data.Hashable.Class.Hashable (Data.Parameterized.SymbolRepr.SymbolRepr nm)
instance GHC.Show.Show (Data.Parameterized.SymbolRepr.SymbolRepr nm)
instance Data.Parameterized.Classes.ShowF Data.Parameterized.SymbolRepr.SymbolRepr


-- | This module declares template Haskell primitives so that it is easier
--   to work with GADTs that have many constructors.
module Data.Parameterized.TH.GADT

-- | <tt>structuralEquality</tt> declares a structural equality predicate.
structuralEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ

-- | <tt>structuralTypeEquality f</tt> returns a function with the type:
--   forall x y . f x -&gt; f y -&gt; Maybe (x :~: y)
structuralTypeEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ

-- | <tt>structuralTypeOrd f</tt> returns a function with the type: forall
--   x y . f x -&gt; f y -&gt; OrderingF x y
--   
--   This implementation avoids matching on both the first and second
--   parameters in a simple case expression in order to avoid stressing
--   GHC's coverage checker. In the case that the first and second
--   parameters have unique constructors, a simple numeric comparison is
--   done to compute the result.
structuralTypeOrd :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ

-- | <tt>structuralTraversal tp</tt> generates a function that applies a
--   traversal <tt>f</tt> to the subterms with free variables in
--   <tt>tp</tt>.
structuralTraversal :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ

-- | <tt>structuralShow tp</tt> generates a function with the type <tt>tp
--   -&gt; ShowS</tt> that shows the constructor.
structuralShowsPrec :: TypeQ -> ExpQ

-- | <tt>structuralHash tp</tt> generates a function with the type <tt>Int
--   -&gt; tp -&gt; Int</tt> that hashes type.
structuralHash :: TypeQ -> ExpQ

-- | A polymorphic equality operator that generalizes <a>TestEquality</a>.
class PolyEq u v
polyEqF :: PolyEq u v => u -> v -> Maybe (u :~: v)
polyEq :: PolyEq u v => u -> v -> Bool
type DataD = DatatypeInfo
lookupDataType' :: Name -> Q DatatypeInfo
asTypeCon :: Monad m => String -> Type -> m Name

-- | Given a constructor and string, this generates a pattern for matching
--   the expression, and the names of variables bound by pattern in order
--   they appear in constructor.
conPat :: ConstructorInfo -> String -> Q (Pat, [Name])

-- | A type used to describe (and match) types appearing in generated
--   pattern matches inside of the TH generators in this module
--   (<a>structuralEquality</a>, <a>structuralTypeEquality</a>,
--   <a>structuralTypeOrd</a>, and <a>structuralTraversal</a>)
data TypePat

-- | The application of a type.
TypeApp :: TypePat -> TypePat -> TypePat

-- | Match any type.
AnyType :: TypePat

-- | Match the ith argument of the data type we are traversing.
DataArg :: Int -> TypePat

-- | Match a ground type.
ConType :: TypeQ -> TypePat
dataParamTypes :: DatatypeInfo -> [Type]

-- | Find value associated with first pattern that matches given pat if
--   any.
assocTypePats :: [Type] -> [(TypePat, v)] -> Type -> Q (Maybe v)


-- | This module declares classes for working with structures that accept a
--   single parametric type parameter.
module Data.Parameterized.TraversableF

-- | A parameterized type that is a functor on all instances.
class FunctorF m
fmapF :: FunctorF m => (forall x. f x -> g x) -> m f -> m g

-- | This is a generalization of the <tt>Foldable</tt> class to structures
--   over parameterized terms.
class FoldableF (t :: (k -> *) -> *)

-- | Map each element of the structure to a monoid, and combine the
--   results.
foldMapF :: (FoldableF t, Monoid m) => (forall s. e s -> m) -> t e -> m

-- | Right-associative fold of a structure.
foldrF :: FoldableF t => (forall s. e s -> b -> b) -> b -> t e -> b

-- | Left-associative fold of a structure.
foldlF :: FoldableF t => (forall s. b -> e s -> b) -> b -> t e -> b

-- | Right-associative fold of a structure, but with strict application of
--   the operator.
foldrF' :: FoldableF t => (forall s. e s -> b -> b) -> b -> t e -> b

-- | Left-associative fold of a parameterized structure with a strict
--   accumulator.
foldlF' :: FoldableF t => (forall s. b -> e s -> b) -> b -> t e -> b

-- | Convert structure to list.
toListF :: FoldableF t => (forall tp. f tp -> a) -> t f -> [a]
class (FunctorF t, FoldableF t) => TraversableF t
traverseF :: (TraversableF t, Applicative m) => (forall s. e s -> m (f s)) -> t e -> m (t f)

-- | Map each element of a structure to an action, evaluate these actions
--   from left to right, and ignore the results.
traverseF_ :: (FoldableF t, Applicative f) => (forall s. e s -> f ()) -> t e -> f ()

-- | This function may be used as a value for <a>fmapF</a> in a
--   <a>FunctorF</a> instance.
fmapFDefault :: TraversableF t => (forall s. e s -> f s) -> t e -> t f

-- | This function may be used as a value for <a>foldMap</a> in a
--   <a>Foldable</a> instance.
foldMapFDefault :: (TraversableF t, Monoid m) => (forall s. e s -> m) -> t e -> m

-- | Return <a>True</a> if all values satisfy predicate.
allF :: FoldableF t => (forall tp. f tp -> Bool) -> t f -> Bool

-- | Return <a>True</a> if any values satisfy predicate.
anyF :: FoldableF t => (forall tp. f tp -> Bool) -> t f -> Bool
instance Data.Parameterized.TraversableF.TraversableF (Data.Functor.Const.Const x)
instance Data.Parameterized.TraversableF.FoldableF (Data.Functor.Const.Const x)
instance Data.Parameterized.TraversableF.FunctorF (Data.Functor.Const.Const x)


-- | This module defines a 2-tuple where both elements are parameterized
--   over the same existentially quantified parameter.
module Data.Parameterized.Pair

-- | Like a 2-tuple, but with an existentially quantified parameter that
--   both of the elements share.
data Pair (a :: k -> *) (b :: k -> *)
[Pair] :: !(a tp) -> !(b tp) -> Pair a b

-- | Extract the first element of a pair.
fstPair :: Pair a b -> Some a

-- | Extract the second element of a pair.
sndPair :: Pair a b -> Some b

-- | Project out of Pair.
viewPair :: (forall tp. a tp -> b tp -> c) -> Pair a b -> c
instance forall k (a :: k -> *) (b :: k -> *). (Data.Type.Equality.TestEquality a, Data.Parameterized.Classes.EqF b) => GHC.Classes.Eq (Data.Parameterized.Pair.Pair a b)
instance forall k (a :: k -> *). Data.Parameterized.TraversableF.FunctorF (Data.Parameterized.Pair.Pair a)
instance forall k (a :: k -> *). Data.Parameterized.TraversableF.FoldableF (Data.Parameterized.Pair.Pair a)


-- | This module declares classes for working with structures that accept a
--   parametric type parameter followed by some fixed kind.
module Data.Parameterized.TraversableFC

-- | A parameterized class for types which can be tested for parameterized
--   equality, when given an equality test for subterms.
class TestEqualityFC (t :: (k -> *) -> l -> *)
testEqualityFC :: forall f. TestEqualityFC t => (forall x y. f x -> f y -> (Maybe (x :~: y))) -> (forall x y. t f x -> t f y -> (Maybe (x :~: y)))

-- | A parameterized class for types which can be tested for parameterized
--   ordering, when given an comparison test for subterms.
class TestEqualityFC t => OrdFC (t :: (k -> *) -> l -> *)
compareFC :: forall f. OrdFC t => (forall x y. f x -> f y -> OrderingF x y) -> (forall x y. t f x -> t f y -> OrderingF x y)

-- | A parameterized class for types which can be shown, when given
--   functions to show parameterized subterms.
class ShowFC (t :: (k -> *) -> l -> *)
showFC :: forall f. ShowFC t => (forall x. f x -> String) -> (forall x. t f x -> String)
showsPrecFC :: forall f. ShowFC t => (forall x. Int -> f x -> ShowS) -> (forall x. Int -> t f x -> ShowS)

-- | A parameterized class for types which can be hashed, when given
--   functions to hash parameterized subterms.
class HashableFC (t :: (k -> *) -> l -> *)
hashWithSaltFC :: forall f. HashableFC t => (forall x. Int -> f x -> Int) -> (forall x. Int -> t f x -> Int)

-- | A parameterized type that is a function on all instances.
class FunctorFC (t :: (k -> *) -> l -> *)
fmapFC :: forall f g. FunctorFC t => (forall x. f x -> g x) -> (forall x. t f x -> t g x)

-- | This is a generalization of the <tt>Foldable</tt> class to structures
--   over parameterized terms.
class FoldableFC (t :: (k -> *) -> l -> *)

-- | Map each element of the structure to a monoid, and combine the
--   results.
foldMapFC :: forall f m. (FoldableFC t, Monoid m) => (forall x. f x -> m) -> (forall x. t f x -> m)

-- | Right-associative fold of a structure.
foldrFC :: forall f b. FoldableFC t => (forall x. f x -> b -> b) -> (forall x. b -> t f x -> b)

-- | Left-associative fold of a structure.
foldlFC :: forall f b. FoldableFC t => (forall x. b -> f x -> b) -> (forall x. b -> t f x -> b)

-- | Right-associative fold of a structure, but with strict application of
--   the operator.
foldrFC' :: forall f b. FoldableFC t => (forall x. f x -> b -> b) -> (forall x. b -> t f x -> b)

-- | Left-associative fold of a parameterized structure with a strict
--   accumulator.
foldlFC' :: forall f b. FoldableFC t => (forall x. b -> f x -> b) -> (forall x. b -> t f x -> b)

-- | Convert structure to list.
toListFC :: forall f a. FoldableFC t => (forall x. f x -> a) -> (forall x. t f x -> [a])
class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> *) -> l -> *)
traverseFC :: forall f g m. (TraversableFC t, Applicative m) => (forall x. f x -> m (g x)) -> (forall x. t f x -> m (t g x))

-- | Map each element of a structure to an action, evaluate these actions
--   from left to right, and ignore the results.
traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m ()) -> (forall x. t f x -> m ())

-- | Map each element of a structure to an action, evaluate these actions
--   from left to right, and ignore the results.
forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m ()) -> m ()

-- | This function may be used as a value for <tt>fmapF</tt> in a
--   <tt>FunctorF</tt> instance.
fmapFCDefault :: TraversableFC t => forall f g. (forall x. f x -> g x) -> (forall x. t f x -> t g x)

-- | This function may be used as a value for <a>foldMap</a> in a
--   <a>Foldable</a> instance.
foldMapFCDefault :: (TraversableFC t, Monoid m) => (forall x. f x -> m) -> (forall x. t f x -> m)

-- | Return <a>True</a> if all values satisfy predicate.
allFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool)

-- | Return <a>True</a> if any values satisfy predicate.
anyFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool)

-- | Return number of elements in list.
lengthFC :: FoldableFC t => t f x -> Int


-- | This module defines a list over two parameters. The first is a fixed
--   type-level function <tt>k -&gt; *</tt> for some kind <tt>k</tt>, and
--   the second is a list of types with kind k that provide the indices for
--   the values in the list.
--   
--   This type is closely related to the <tt>Context</tt> type in
--   <tt>Data.Parameterized.Context</tt>.
module Data.Parameterized.List

-- | Parameterized list of elements.
data List :: (k -> *) -> [k] -> *
[Nil] :: List f '[]
[:<] :: f tp -> List f tps -> List f (tp : tps)

-- | Represents an index into a type-level list. Used in place of integers
--   to 1. ensure that the given index *does* exist in the list 2.
--   guarantee that it has the given kind
data Index :: [k] -> k -> *
[IndexHere] :: Index (x : r) x
[IndexThere] :: !(Index r y) -> Index (x : r) y

-- | Return the index as an integer.
indexValue :: Index l tp -> Integer

-- | Return the value in a list at a given index
(!!) :: List f l -> Index l x -> f x

-- | Update the <a>List</a> at an index
update :: List f l -> Index l s -> (f s -> f s) -> List f l

-- | Provides a lens for manipulating the element at the given index.
indexed :: Index l x -> Simple Lens (List f l) (f x)

-- | Map over the elements in the list, and provide the index into each
--   element along with the element itself.
imap :: forall f g l. (forall x. Index l x -> f x -> g x) -> List f l -> List g l

-- | Right-fold with an additional index.
ifoldr :: forall sh a b. (forall tp. Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b

-- | Zip up two lists with a zipper function, which can use the index.
izipWith :: forall a b c sh. (forall tp. Index sh tp -> a tp -> b tp -> c tp) -> List a sh -> List b sh -> List c sh

-- | Traverse with an additional index.
itraverse :: forall a b sh t. Applicative t => (forall tp. Index sh tp -> a tp -> t (b tp)) -> List a sh -> t (List b sh)

-- | Index 0
index0 :: Index (x : r) x

-- | Index 1
index1 :: Index (x0 : x1 : r) x1

-- | Index 2
index2 :: Index (x0 : x1 : x2 : r) x2

-- | Index 3
index3 :: Index (x0 : x1 : x2 : x3 : r) x3
instance forall k (l :: [k]) (x :: k). GHC.Classes.Eq (Data.Parameterized.List.Index l x)
instance forall k (l :: [k]) (x :: k). GHC.Show.Show (Data.Parameterized.List.Index l x)
instance forall k (l :: [k]). Data.Parameterized.Classes.ShowF (Data.Parameterized.List.Index l)
instance forall k (l :: [k]). Data.Type.Equality.TestEquality (Data.Parameterized.List.Index l)
instance forall k (l :: [k]). Data.Parameterized.Classes.OrdF (Data.Parameterized.List.Index l)
instance forall k (sh :: [k]) (x :: k). GHC.Classes.Ord (Data.Parameterized.List.Index sh x)
instance forall k (f :: k -> *) (sh :: [k]). Data.Parameterized.Classes.ShowF f => GHC.Show.Show (Data.Parameterized.List.List f sh)
instance forall k (f :: k -> *). Data.Parameterized.Classes.ShowF f => Data.Parameterized.Classes.ShowF (Data.Parameterized.List.List f)
instance Data.Parameterized.TraversableFC.FunctorFC Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.FoldableFC Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.TraversableFC Data.Parameterized.List.List
instance forall k (f :: k -> *). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (Data.Parameterized.List.List f)
instance forall k (f :: k -> *). Data.Parameterized.Classes.OrdF f => Data.Parameterized.Classes.OrdF (Data.Parameterized.List.List f)
instance forall k (f :: k -> *). Data.Parameterized.Classes.KnownRepr (Data.Parameterized.List.List f) '[]
instance forall a (f :: a -> *) (s :: a) (sh :: [a]). (Data.Parameterized.Classes.KnownRepr f s, Data.Parameterized.Classes.KnownRepr (Data.Parameterized.List.List f) sh) => Data.Parameterized.Classes.KnownRepr (Data.Parameterized.List.List f) (s : sh)

module Data.Parameterized.Context.Unsafe

-- | A context that can be determined statically at compiler time.
class KnownContext (ctx :: Ctx k)
knownSize :: KnownContext ctx => Size ctx

-- | Represents the size of a context.
data Size (ctx :: Ctx k)

-- | Convert a context size to an <a>Int</a>.
sizeInt :: Size ctx -> Int

-- | The size of an empty context.
zeroSize :: Size  'EmptyCtx

-- | Increment the size to the next value.
incSize :: Size ctx -> Size (ctx ::> tp)
decSize :: Size (ctx ::> tp) -> Size ctx

-- | Extend the size by a given difference.
extSize :: Size l -> Diff l r -> Size r

-- | The total size of two concatenated contexts.
addSize :: Size x -> Size y -> Size (x <+> y)

-- | Allows interpreting a size.
data SizeView (ctx :: Ctx k)
[ZeroSize] :: SizeView  'EmptyCtx
[IncSize] :: !(Size ctx) -> SizeView (ctx ::> tp)

-- | Project a size
viewSize :: Size ctx -> SizeView ctx

-- | Difference in number of elements between two contexts. The first
--   context must be a sub-context of the other.
data Diff (l :: Ctx k) (r :: Ctx k)

-- | The identity difference.
noDiff :: Diff l l

-- | Extend the difference to a sub-context of the right side.
extendRight :: Diff l r -> Diff l (r ::> tp)
data DiffView a b
[NoDiff] :: DiffView a a
[ExtendRightDiff] :: Diff a b -> DiffView a (b ::> r)
viewDiff :: Diff a b -> DiffView a b

-- | A difference that can be automatically inferred at compile time.
class KnownDiff (l :: Ctx k) (r :: Ctx k)
knownDiff :: KnownDiff l r => Diff l r

-- | An index is a reference to a position with a particular type in a
--   context.
data Index (ctx :: Ctx k) (tp :: k)
indexVal :: Index ctx tp -> Int

-- | Index for first element in context.
baseIndex :: Index ( 'EmptyCtx ::> tp) tp

-- | Increase context while staying at same index.
skipIndex :: Index ctx x -> Index (ctx ::> y) x

-- | Return the last index of a element.
lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp

-- | Return the index of a element one past the size.
nextIndex :: Size ctx -> Index (ctx ::> tp) tp
extendIndex :: KnownDiff l r => Index l tp -> Index r tp
extendIndex' :: Diff l r -> Index l tp -> Index r tp

-- | Given a size <tt>n</tt>, an initial value <tt>v0</tt>, and a function
--   <tt>f</tt>, 'forIndex n v0 f' is equivalent to <tt>v0</tt> when
--   <tt>n</tt> is zero, and 'f (forIndex (n-1) v0) (n-1)' otherwise.
forIndex :: forall ctx r. Size ctx -> (forall tp. r -> Index ctx tp -> r) -> r -> r

-- | Given an index <tt>i</tt>, size <tt>n</tt>, a function <tt>f</tt>,
--   value <tt>v</tt>, and a function <tt>f</tt>, 'forIndex i n f v' is
--   equivalent to <tt>v</tt> when 'i &gt;= sizeInt n', and 'f i
--   (forIndexRange (i+1) n v0)' otherwise.
forIndexRange :: forall ctx r. Int -> Size ctx -> (forall tp. Index ctx tp -> r -> r) -> r -> r

-- | Return index at given integer or nothing if integer is out of bounds.
intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))

-- | This represents a contiguous range of indices.
data IndexRange (ctx :: Ctx k) (sub :: Ctx k)

-- | Return a range containing all indices in the context.
allRange :: Size ctx -> IndexRange ctx ctx

-- | <a>indexOfRange</a> returns the only index in a range.
indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e

-- | `dropHeadRange r n` drops the first <tt>n</tt> elements in <tt>r</tt>.
dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y

-- | `dropTailRange r n` drops the last <tt>n</tt> elements in <tt>r</tt>.
dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x

-- | An assignment is a sequence that maps each index with type <tt>tp</tt>
--   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.
data Assignment (f :: k -> Type) (ctx :: Ctx k)

-- | Return number of elements in assignment.
size :: Assignment f ctx -> Size ctx

-- | <tt>replicate n</tt> make a context with different copies of the same
--   polymorphic value.
replicate :: Size ctx -> (forall tp. f tp) -> Assignment f ctx

-- | Generate an assignment
generate :: Size ctx -> (forall tp. Index ctx tp -> f tp) -> Assignment f ctx

-- | Generate an assignment
generateM :: Applicative m => Size ctx -> (forall tp. Index ctx tp -> m (f tp)) -> m (Assignment f ctx)

-- | Return empty assignment
empty :: Assignment f EmptyCtx
extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)

-- | <i>Deprecated: Replace 'adjust f i asgn' with 'Lens.over (ixF i) f
--   asgn' instead.</i>
adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx

-- | <i>Deprecated: Replace 'update idx val asgn' with 'Lens.set (ixF idx)
--   val asgn' instead.</i>
update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx

-- | Modify the value of an assignment at a particular index.
adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)

-- | View an assignment as either empty or an assignment with one appended.
data AssignView f ctx
[AssignEmpty] :: AssignView f EmptyCtx
[AssignExtend] :: Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)

-- | View an assignment as either empty or an assignment with one appended.
viewAssign :: forall f ctx. Assignment f ctx -> AssignView f ctx

-- | Return value of assignment.
(!) :: Assignment f ctx -> Index ctx tp -> f tp

-- | Return value of assignment, where the index is into an initial
--   sequence of the assignment.
(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp
zipWith :: (forall x. f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a
zipWithM :: Applicative m => (forall x. f x -> g x -> m (h x)) -> Assignment f a -> Assignment g a -> m (Assignment h a)
(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)
traverseWithIndex :: Applicative m => (forall tp. Index ctx tp -> f tp -> m (g tp)) -> Assignment f ctx -> m (Assignment g ctx)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Unsafe.Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9) (Data.Parameterized.Context.Unsafe.Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Unsafe.Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9) (Data.Parameterized.Context.Unsafe.Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9) (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9) (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (t :: k) (x6 :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field5 (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9) (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (t :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field6 (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9) (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (t :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field7 (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9) (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (t :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field8 (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9) (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field9 (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t) (Data.Parameterized.Context.Unsafe.Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Unsafe.Assignment8 f t x2 x3 x4 x5 x6 x7 x8) (Data.Parameterized.Context.Unsafe.Assignment8 f u x2 x3 x4 x5 x6 x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Unsafe.Assignment8 f x1 t x3 x4 x5 x6 x7 x8) (Data.Parameterized.Context.Unsafe.Assignment8 f x1 u x3 x4 x5 x6 x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 t x4 x5 x6 x7 x8) (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 u x4 x5 x6 x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 x3 t x5 x6 x7 x8) (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 x3 u x5 x6 x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (t :: k) (x6 :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field5 (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 x3 x4 t x6 x7 x8) (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 x3 x4 u x6 x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (t :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field6 (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 x3 x4 x5 t x7 x8) (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 x3 x4 x5 u x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (t :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field7 (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 x3 x4 x5 x6 t x8) (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 x3 x4 x5 x6 u x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field8 (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 x3 x4 x5 x6 x7 t) (Data.Parameterized.Context.Unsafe.Assignment8 f x1 x2 x3 x4 x5 x6 x7 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Unsafe.Assignment7 f t x2 x3 x4 x5 x6 x7) (Data.Parameterized.Context.Unsafe.Assignment7 f u x2 x3 x4 x5 x6 x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Unsafe.Assignment7 f x1 t x3 x4 x5 x6 x7) (Data.Parameterized.Context.Unsafe.Assignment7 f x1 u x3 x4 x5 x6 x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Unsafe.Assignment7 f x1 x2 t x4 x5 x6 x7) (Data.Parameterized.Context.Unsafe.Assignment7 f x1 x2 u x4 x5 x6 x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (x5 :: k) (x6 :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Unsafe.Assignment7 f x1 x2 x3 t x5 x6 x7) (Data.Parameterized.Context.Unsafe.Assignment7 f x1 x2 x3 u x5 x6 x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (t :: k) (x6 :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field5 (Data.Parameterized.Context.Unsafe.Assignment7 f x1 x2 x3 x4 t x6 x7) (Data.Parameterized.Context.Unsafe.Assignment7 f x1 x2 x3 x4 u x6 x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (t :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field6 (Data.Parameterized.Context.Unsafe.Assignment7 f x1 x2 x3 x4 x5 t x7) (Data.Parameterized.Context.Unsafe.Assignment7 f x1 x2 x3 x4 x5 u x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field7 (Data.Parameterized.Context.Unsafe.Assignment7 f x1 x2 x3 x4 x5 x6 t) (Data.Parameterized.Context.Unsafe.Assignment7 f x1 x2 x3 x4 x5 x6 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Unsafe.Assignment6 f t x2 x3 x4 x5 x6) (Data.Parameterized.Context.Unsafe.Assignment6 f u x2 x3 x4 x5 x6) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Unsafe.Assignment6 f x1 t x3 x4 x5 x6) (Data.Parameterized.Context.Unsafe.Assignment6 f x1 u x3 x4 x5 x6) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (x5 :: k) (x6 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Unsafe.Assignment6 f x1 x2 t x4 x5 x6) (Data.Parameterized.Context.Unsafe.Assignment6 f x1 x2 u x4 x5 x6) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (x5 :: k) (x6 :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Unsafe.Assignment6 f x1 x2 x3 t x5 x6) (Data.Parameterized.Context.Unsafe.Assignment6 f x1 x2 x3 u x5 x6) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (t :: k) (x6 :: k) (u :: k). Control.Lens.Tuple.Field5 (Data.Parameterized.Context.Unsafe.Assignment6 f x1 x2 x3 x4 t x6) (Data.Parameterized.Context.Unsafe.Assignment6 f x1 x2 x3 x4 u x6) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field6 (Data.Parameterized.Context.Unsafe.Assignment6 f x1 x2 x3 x4 x5 t) (Data.Parameterized.Context.Unsafe.Assignment6 f x1 x2 x3 x4 x5 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Unsafe.Assignment5 f t x2 x3 x4 x5) (Data.Parameterized.Context.Unsafe.Assignment5 f u x2 x3 x4 x5) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (x5 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Unsafe.Assignment5 f x1 t x3 x4 x5) (Data.Parameterized.Context.Unsafe.Assignment5 f x1 u x3 x4 x5) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (x5 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Unsafe.Assignment5 f x1 x2 t x4 x5) (Data.Parameterized.Context.Unsafe.Assignment5 f x1 x2 u x4 x5) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (x5 :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Unsafe.Assignment5 f x1 x2 x3 t x5) (Data.Parameterized.Context.Unsafe.Assignment5 f x1 x2 x3 u x5) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field5 (Data.Parameterized.Context.Unsafe.Assignment5 f x1 x2 x3 x4 t) (Data.Parameterized.Context.Unsafe.Assignment5 f x1 x2 x3 x4 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Unsafe.Assignment4 f t x2 x3 x4) (Data.Parameterized.Context.Unsafe.Assignment4 f u x2 x3 x4) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Unsafe.Assignment4 f x1 t x3 x4) (Data.Parameterized.Context.Unsafe.Assignment4 f x1 u x3 x4) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Unsafe.Assignment4 f x1 x2 t x4) (Data.Parameterized.Context.Unsafe.Assignment4 f x1 x2 u x4) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Unsafe.Assignment4 f x1 x2 x3 t) (Data.Parameterized.Context.Unsafe.Assignment4 f x1 x2 x3 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Unsafe.Assignment3 f t x2 x3) (Data.Parameterized.Context.Unsafe.Assignment3 f u x2 x3) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Unsafe.Assignment3 f x1 t x3) (Data.Parameterized.Context.Unsafe.Assignment3 f x1 u x3) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Unsafe.Assignment3 f x1 x2 t) (Data.Parameterized.Context.Unsafe.Assignment3 f x1 x2 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Unsafe.Assignment2 f t x2) (Data.Parameterized.Context.Unsafe.Assignment2 f u x2) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Unsafe.Assignment2 f x1 t) (Data.Parameterized.Context.Unsafe.Assignment2 f x1 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Unsafe.Assignment1 f t) (Data.Parameterized.Context.Unsafe.Assignment1 f u) (f t) (f u)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Control.DeepSeq.NFData (Data.Parameterized.Context.Unsafe.Assignment f ctx)
instance Data.Parameterized.TraversableFC.TestEqualityFC Data.Parameterized.Context.Unsafe.Assignment
instance forall k (f :: k -> *). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (Data.Parameterized.Context.Unsafe.Assignment f)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Type.Equality.TestEquality f => GHC.Classes.Eq (Data.Parameterized.Context.Unsafe.Assignment f ctx)
instance Data.Parameterized.TraversableFC.OrdFC Data.Parameterized.Context.Unsafe.Assignment
instance forall k (f :: k -> *). Data.Parameterized.Classes.OrdF f => Data.Parameterized.Classes.OrdF (Data.Parameterized.Context.Unsafe.Assignment f)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.OrdF f => GHC.Classes.Ord (Data.Parameterized.Context.Unsafe.Assignment f ctx)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.HashableF f => Data.Hashable.Class.Hashable (Data.Parameterized.Context.Unsafe.Assignment f ctx)
instance forall k (f :: k -> *). Data.Parameterized.Classes.HashableF f => Data.Parameterized.Classes.HashableF (Data.Parameterized.Context.Unsafe.Assignment f)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.ShowF f => GHC.Show.Show (Data.Parameterized.Context.Unsafe.Assignment f ctx)
instance forall k (f :: k -> *). Data.Parameterized.Classes.ShowF f => Data.Parameterized.Classes.ShowF (Data.Parameterized.Context.Unsafe.Assignment f)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.IxedF' k (Data.Parameterized.Context.Unsafe.Assignment f ctx)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.IxedF k (Data.Parameterized.Context.Unsafe.Assignment f ctx)
instance Data.Parameterized.TraversableFC.FunctorFC Data.Parameterized.Context.Unsafe.Assignment
instance Data.Parameterized.TraversableFC.FoldableFC Data.Parameterized.Context.Unsafe.Assignment
instance Data.Parameterized.TraversableFC.TraversableFC Data.Parameterized.Context.Unsafe.Assignment
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k) (bt :: k). (Data.Parameterized.Classes.KnownRepr (Data.Parameterized.Context.Unsafe.Assignment f) ctx, Data.Parameterized.Classes.KnownRepr f bt) => Data.Parameterized.Classes.KnownRepr (Data.Parameterized.Context.Unsafe.Assignment f) (ctx Data.Parameterized.Ctx.::> bt)
instance forall k (f :: k -> *). Data.Parameterized.Classes.KnownRepr (Data.Parameterized.Context.Unsafe.Assignment f) Data.Parameterized.Ctx.EmptyCtx
instance Data.Parameterized.TraversableFC.TestEqualityFC (Data.Parameterized.Context.Unsafe.BinomialTree h)
instance Data.Parameterized.TraversableFC.OrdFC (Data.Parameterized.Context.Unsafe.BinomialTree h)
instance forall k (f :: k -> *) (h :: Data.Parameterized.Context.Unsafe.Height). Data.Parameterized.Classes.HashableF f => Data.Parameterized.Classes.HashableF (Data.Parameterized.Context.Unsafe.BinomialTree h f)
instance Data.Parameterized.TraversableFC.TestEqualityFC (Data.Parameterized.Context.Unsafe.BalancedTree h)
instance Data.Parameterized.TraversableFC.OrdFC (Data.Parameterized.Context.Unsafe.BalancedTree h)
instance forall k (f :: k -> *) (h :: Data.Parameterized.Context.Unsafe.Height). Data.Parameterized.Classes.HashableF f => Data.Parameterized.Classes.HashableF (Data.Parameterized.Context.Unsafe.BalancedTree h f)
instance forall k (f :: k -> *) (h :: Data.Parameterized.Context.Unsafe.Height) (tp :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.ShowF f => GHC.Show.Show (Data.Parameterized.Context.Unsafe.BalancedTree h f tp)
instance forall k (f :: k -> *) (h :: Data.Parameterized.Context.Unsafe.Height). Data.Parameterized.Classes.ShowF f => Data.Parameterized.Classes.ShowF (Data.Parameterized.Context.Unsafe.BalancedTree h f)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (tp :: k). GHC.Classes.Eq (Data.Parameterized.Context.Unsafe.Index ctx tp)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Type.Equality.TestEquality (Data.Parameterized.Context.Unsafe.Index ctx)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (tp :: k). GHC.Classes.Ord (Data.Parameterized.Context.Unsafe.Index ctx tp)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.OrdF (Data.Parameterized.Context.Unsafe.Index ctx)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (tp :: k). GHC.Show.Show (Data.Parameterized.Context.Unsafe.Index ctx tp)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.ShowF (Data.Parameterized.Context.Unsafe.Index ctx)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.HashableF (Data.Parameterized.Context.Unsafe.Index ctx)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (tp :: k). Data.Hashable.Class.Hashable (Data.Parameterized.Context.Unsafe.Index ctx tp)
instance forall k (l :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Context.Unsafe.KnownDiff l l
instance forall k (l :: Data.Parameterized.Ctx.Ctx k) (r :: Data.Parameterized.Ctx.Ctx k) (tp :: k). Data.Parameterized.Context.Unsafe.KnownDiff l r => Data.Parameterized.Context.Unsafe.KnownDiff l (r 'Data.Parameterized.Ctx.::> tp)
instance Control.Category.Category Data.Parameterized.Context.Unsafe.Diff
instance Data.Parameterized.Context.Unsafe.KnownContext 'Data.Parameterized.Ctx.EmptyCtx
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (tp :: k). Data.Parameterized.Context.Unsafe.KnownContext ctx => Data.Parameterized.Context.Unsafe.KnownContext (ctx 'Data.Parameterized.Ctx.::> tp)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k). GHC.Show.Show (Data.Parameterized.Context.Unsafe.Size ctx)


-- | This module defines type contexts as a data-kind that consists of a
--   list of types. Indexes are defined with respect to these contexts. In
--   addition, finite dependent products (Assignments) are defined over
--   type contexts. The elements of an assignment can be accessed using
--   appropriately-typed indexes.
--   
--   This module is intended to export exactly the same API as module
--   <a>Data.Parameterized.Context.Unsafe</a>, so that they can be used
--   interchangeably.
--   
--   This implementation is entirely typesafe, and provides a proof that
--   the signature implemented by this module is consistent. Contexts,
--   indexes, and assignments are represented naively by linear sequences.
--   
--   Compared to the implementation in
--   <a>Data.Parameterized.Context.Unsafe</a>, this one suffers from the
--   fact that the operation of extending an the context of an index is
--   <i>not</i> a no-op. We therefore cannot use <a>coerce</a> to
--   understand indexes in a new context without actually breaking things.
module Data.Parameterized.Context.Safe

-- | An indexed singleton type representing the size of a context.
data Size (ctx :: Ctx k)

-- | Convert a context size to an <a>Int</a>.
sizeInt :: Size ctx -> Int

-- | The size of an empty context.
zeroSize :: Size  'EmptyCtx

-- | Increment the size to the next value.
incSize :: Size ctx -> Size (ctx ::> tp)
decSize :: Size (ctx ::> tp) -> Size ctx

-- | Extend the size by a given difference.
extSize :: Size l -> Diff l r -> Size r

-- | The total size of two concatenated contexts.
addSize :: Size x -> Size y -> Size (x <+> y)

-- | Allows interpreting a size.
data SizeView (ctx :: Ctx k)
[ZeroSize] :: SizeView  'EmptyCtx
[IncSize] :: !(Size ctx) -> SizeView (ctx ::> tp)

-- | View a size as either zero or a smaller size plus one.
viewSize :: Size ctx -> SizeView ctx

-- | A context that can be determined statically at compiler time.
class KnownContext (ctx :: Ctx k)
knownSize :: KnownContext ctx => Size ctx

-- | Difference in number of elements between two contexts. The first
--   context must be a sub-context of the other.
data Diff (l :: Ctx k) (r :: Ctx k)

-- | The identity difference.
noDiff :: Diff l l

-- | Extend the difference to a sub-context of the right side.
extendRight :: Diff l r -> Diff l (r ::> tp)
data DiffView a b
[NoDiff] :: DiffView a a
[ExtendRightDiff] :: Diff a b -> DiffView a (b ::> r)
viewDiff :: Diff a b -> DiffView a b

-- | A difference that can be automatically inferred at compile time.
class KnownDiff (l :: Ctx k) (r :: Ctx k)
knownDiff :: KnownDiff l r => Diff l r

-- | An index is a reference to a position with a particular type in a
--   context.
data Index (ctx :: Ctx k) (tp :: k)

-- | Convert an index to an <a>Int</a>, where the index of the left-most
--   type in the context is 0.
indexVal :: Index ctx tp -> Int

-- | Index for first element in context.
baseIndex :: Index ( 'EmptyCtx ::> tp) tp

-- | Increase context while staying at same index.
skipIndex :: Index ctx x -> Index (ctx ::> y) x

-- | Return the last index of a element.
lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp

-- | Return the index of an element one past the size.
nextIndex :: Size ctx -> Index (ctx ::> tp) tp
extendIndex :: KnownDiff l r => Index l tp -> Index r tp
extendIndex' :: Diff l r -> Index l tp -> Index r tp

-- | Given a size <tt>n</tt>, an initial value <tt>v0</tt>, and a function
--   <tt>f</tt>, <tt>forIndex n v0 f</tt> calls <tt>f</tt> on each index
--   less than <tt>n</tt> starting from <tt>0</tt> and <tt>v0</tt>, with
--   the value <tt>v</tt> obtained from the last call.
forIndex :: forall ctx r. Size ctx -> (forall tp. r -> Index ctx tp -> r) -> r -> r

-- | Given an index <tt>i</tt>, size <tt>n</tt>, a function <tt>f</tt>,
--   value <tt>v</tt>, and a function <tt>f</tt>, 'forIndex i n f v' is
--   equivalent to <tt>v</tt> when 'i &gt;= sizeInt n', and 'f i
--   (forIndexRange (i+1) n v0)' otherwise.
forIndexRange :: Int -> Size ctx -> (forall tp. Index ctx tp -> r -> r) -> r -> r

-- | Return index at given integer or nothing if integer is out of bounds.
intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))

-- | An assignment is a sequence that maps each index with type <tt>tp</tt>
--   to a value of type 'f tp'.
data Assignment (f :: k -> Type) (ctx :: Ctx k)

-- | Return number of elements in assignment.
size :: Assignment f ctx -> Size ctx

-- | <tt>replicate n</tt> make a context with different copies of the same
--   polymorphic value.
replicate :: Size ctx -> (forall tp. f tp) -> Assignment f ctx

-- | Generate an assignment
generate :: forall ctx f. Size ctx -> (forall tp. Index ctx tp -> f tp) -> Assignment f ctx

-- | Generate an assignment
generateM :: forall ctx m f. Applicative m => Size ctx -> (forall tp. Index ctx tp -> m (f tp)) -> m (Assignment f ctx)

-- | Create empty indexec vector.
empty :: Assignment f  'EmptyCtx
extend :: Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)

-- | <i>Deprecated: Replace 'adjust f i asgn' with 'Lens.over (ixF i) f
--   asgn' instead.</i>
adjust :: forall f ctx tp. (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx

-- | <i>Deprecated: Replace 'update idx val asgn' with 'Lens.set (ixF idx)
--   val asgn' instead.</i>
update :: forall f ctx tp. Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
adjustM :: forall m f ctx tp. Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)

-- | View an assignment as either empty or an assignment with one appended.
data AssignView (f :: k -> Type) (ctx :: Ctx k)
[AssignEmpty] :: AssignView f EmptyCtx
[AssignExtend] :: Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)
viewAssign :: forall f ctx. Assignment f ctx -> AssignView f ctx

-- | Return value of assignment.
(!) :: Assignment f ctx -> Index ctx tp -> f tp

-- | Return value of assignment, where the index is into an initial
--   sequence of the assignment.
(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp
zipWith :: (forall x. f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a
zipWithM :: Applicative m => (forall tp. f tp -> g tp -> m (h tp)) -> Assignment f c -> Assignment g c -> m (Assignment h c)
(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)
traverseWithIndex :: Applicative m => (forall tp. Index ctx tp -> f tp -> m (g tp)) -> Assignment f ctx -> m (Assignment g ctx)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Safe.Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9) (Data.Parameterized.Context.Safe.Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Safe.Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9) (Data.Parameterized.Context.Safe.Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9) (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9) (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (t :: k) (x6 :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field5 (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9) (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (t :: k) (x7 :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field6 (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9) (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (t :: k) (x8 :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field7 (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9) (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (t :: k) (x9 :: k) (u :: k). Control.Lens.Tuple.Field8 (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9) (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field9 (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t) (Data.Parameterized.Context.Safe.Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Safe.Assignment8 f t x2 x3 x4 x5 x6 x7 x8) (Data.Parameterized.Context.Safe.Assignment8 f u x2 x3 x4 x5 x6 x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Safe.Assignment8 f x1 t x3 x4 x5 x6 x7 x8) (Data.Parameterized.Context.Safe.Assignment8 f x1 u x3 x4 x5 x6 x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 t x4 x5 x6 x7 x8) (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 u x4 x5 x6 x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (x5 :: k) (x6 :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 x3 t x5 x6 x7 x8) (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 x3 u x5 x6 x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (t :: k) (x6 :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field5 (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 x3 x4 t x6 x7 x8) (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 x3 x4 u x6 x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (t :: k) (x7 :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field6 (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 x3 x4 x5 t x7 x8) (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 x3 x4 x5 u x7 x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (t :: k) (x8 :: k) (u :: k). Control.Lens.Tuple.Field7 (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 x3 x4 x5 x6 t x8) (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 x3 x4 x5 x6 u x8) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field8 (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 x3 x4 x5 x6 x7 t) (Data.Parameterized.Context.Safe.Assignment8 f x1 x2 x3 x4 x5 x6 x7 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Safe.Assignment7 f t x2 x3 x4 x5 x6 x7) (Data.Parameterized.Context.Safe.Assignment7 f u x2 x3 x4 x5 x6 x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Safe.Assignment7 f x1 t x3 x4 x5 x6 x7) (Data.Parameterized.Context.Safe.Assignment7 f x1 u x3 x4 x5 x6 x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (x5 :: k) (x6 :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Safe.Assignment7 f x1 x2 t x4 x5 x6 x7) (Data.Parameterized.Context.Safe.Assignment7 f x1 x2 u x4 x5 x6 x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (x5 :: k) (x6 :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Safe.Assignment7 f x1 x2 x3 t x5 x6 x7) (Data.Parameterized.Context.Safe.Assignment7 f x1 x2 x3 u x5 x6 x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (t :: k) (x6 :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field5 (Data.Parameterized.Context.Safe.Assignment7 f x1 x2 x3 x4 t x6 x7) (Data.Parameterized.Context.Safe.Assignment7 f x1 x2 x3 x4 u x6 x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (t :: k) (x7 :: k) (u :: k). Control.Lens.Tuple.Field6 (Data.Parameterized.Context.Safe.Assignment7 f x1 x2 x3 x4 x5 t x7) (Data.Parameterized.Context.Safe.Assignment7 f x1 x2 x3 x4 x5 u x7) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field7 (Data.Parameterized.Context.Safe.Assignment7 f x1 x2 x3 x4 x5 x6 t) (Data.Parameterized.Context.Safe.Assignment7 f x1 x2 x3 x4 x5 x6 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Safe.Assignment6 f t x2 x3 x4 x5 x6) (Data.Parameterized.Context.Safe.Assignment6 f u x2 x3 x4 x5 x6) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (x5 :: k) (x6 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Safe.Assignment6 f x1 t x3 x4 x5 x6) (Data.Parameterized.Context.Safe.Assignment6 f x1 u x3 x4 x5 x6) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (x5 :: k) (x6 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Safe.Assignment6 f x1 x2 t x4 x5 x6) (Data.Parameterized.Context.Safe.Assignment6 f x1 x2 u x4 x5 x6) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (x5 :: k) (x6 :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Safe.Assignment6 f x1 x2 x3 t x5 x6) (Data.Parameterized.Context.Safe.Assignment6 f x1 x2 x3 u x5 x6) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (t :: k) (x6 :: k) (u :: k). Control.Lens.Tuple.Field5 (Data.Parameterized.Context.Safe.Assignment6 f x1 x2 x3 x4 t x6) (Data.Parameterized.Context.Safe.Assignment6 f x1 x2 x3 x4 u x6) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field6 (Data.Parameterized.Context.Safe.Assignment6 f x1 x2 x3 x4 x5 t) (Data.Parameterized.Context.Safe.Assignment6 f x1 x2 x3 x4 x5 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (x5 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Safe.Assignment5 f t x2 x3 x4 x5) (Data.Parameterized.Context.Safe.Assignment5 f u x2 x3 x4 x5) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (x5 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Safe.Assignment5 f x1 t x3 x4 x5) (Data.Parameterized.Context.Safe.Assignment5 f x1 u x3 x4 x5) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (x5 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Safe.Assignment5 f x1 x2 t x4 x5) (Data.Parameterized.Context.Safe.Assignment5 f x1 x2 u x4 x5) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (x5 :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Safe.Assignment5 f x1 x2 x3 t x5) (Data.Parameterized.Context.Safe.Assignment5 f x1 x2 x3 u x5) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (x4 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field5 (Data.Parameterized.Context.Safe.Assignment5 f x1 x2 x3 x4 t) (Data.Parameterized.Context.Safe.Assignment5 f x1 x2 x3 x4 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (x4 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Safe.Assignment4 f t x2 x3 x4) (Data.Parameterized.Context.Safe.Assignment4 f u x2 x3 x4) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (x4 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Safe.Assignment4 f x1 t x3 x4) (Data.Parameterized.Context.Safe.Assignment4 f x1 u x3 x4) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (x4 :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Safe.Assignment4 f x1 x2 t x4) (Data.Parameterized.Context.Safe.Assignment4 f x1 x2 u x4) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (x3 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field4 (Data.Parameterized.Context.Safe.Assignment4 f x1 x2 x3 t) (Data.Parameterized.Context.Safe.Assignment4 f x1 x2 x3 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (x3 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Safe.Assignment3 f t x2 x3) (Data.Parameterized.Context.Safe.Assignment3 f u x2 x3) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (x3 :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Safe.Assignment3 f x1 t x3) (Data.Parameterized.Context.Safe.Assignment3 f x1 u x3) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (x2 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field3 (Data.Parameterized.Context.Safe.Assignment3 f x1 x2 t) (Data.Parameterized.Context.Safe.Assignment3 f x1 x2 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (x2 :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Safe.Assignment2 f t x2) (Data.Parameterized.Context.Safe.Assignment2 f u x2) (f t) (f u)
instance forall k (f :: k -> *) (x1 :: k) (t :: k) (u :: k). Control.Lens.Tuple.Field2 (Data.Parameterized.Context.Safe.Assignment2 f x1 t) (Data.Parameterized.Context.Safe.Assignment2 f x1 u) (f t) (f u)
instance forall k (f :: k -> *) (t :: k) (u :: k). Control.Lens.Tuple.Field1 (Data.Parameterized.Context.Safe.Assignment1 f t) (Data.Parameterized.Context.Safe.Assignment1 f u) (f t) (f u)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Control.DeepSeq.NFData (Data.Parameterized.Context.Safe.Assignment f ctx)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.IxedF k (Data.Parameterized.Context.Safe.Assignment f ctx)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.IxedF' k (Data.Parameterized.Context.Safe.Assignment f ctx)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Type.Equality.TestEquality f => GHC.Classes.Eq (Data.Parameterized.Context.Safe.Assignment f ctx)
instance Data.Parameterized.TraversableFC.TestEqualityFC Data.Parameterized.Context.Safe.Assignment
instance forall k (f :: k -> *). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (Data.Parameterized.Context.Safe.Assignment f)
instance forall k (f :: k -> *) (x :: Data.Parameterized.Ctx.Ctx k) (y :: Data.Parameterized.Ctx.Ctx k). Data.Type.Equality.TestEquality f => Data.Parameterized.Classes.PolyEq (Data.Parameterized.Context.Safe.Assignment f x) (Data.Parameterized.Context.Safe.Assignment f y)
instance Data.Parameterized.TraversableFC.OrdFC Data.Parameterized.Context.Safe.Assignment
instance forall k (f :: k -> *). Data.Parameterized.Classes.OrdF f => Data.Parameterized.Classes.OrdF (Data.Parameterized.Context.Safe.Assignment f)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.OrdF f => GHC.Classes.Ord (Data.Parameterized.Context.Safe.Assignment f ctx)
instance forall k (f :: k -> *). Data.Parameterized.Classes.HashableF f => Data.Parameterized.Classes.HashableF (Data.Parameterized.Context.Safe.Assignment f)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.HashableF f => Data.Hashable.Class.Hashable (Data.Parameterized.Context.Safe.Assignment f ctx)
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.ShowF f => GHC.Show.Show (Data.Parameterized.Context.Safe.Assignment f ctx)
instance forall k (f :: k -> *). Data.Parameterized.Classes.ShowF f => Data.Parameterized.Classes.ShowF (Data.Parameterized.Context.Safe.Assignment f)
instance Data.Parameterized.TraversableFC.FunctorFC Data.Parameterized.Context.Safe.Assignment
instance Data.Parameterized.TraversableFC.FoldableFC Data.Parameterized.Context.Safe.Assignment
instance Data.Parameterized.TraversableFC.TraversableFC Data.Parameterized.Context.Safe.Assignment
instance forall k (f :: k -> *) (ctx :: Data.Parameterized.Ctx.Ctx k) (bt :: k). (Data.Parameterized.Classes.KnownRepr (Data.Parameterized.Context.Safe.Assignment f) ctx, Data.Parameterized.Classes.KnownRepr f bt) => Data.Parameterized.Classes.KnownRepr (Data.Parameterized.Context.Safe.Assignment f) (ctx Data.Parameterized.Ctx.::> bt)
instance forall k (f :: k -> *). Data.Parameterized.Classes.KnownRepr (Data.Parameterized.Context.Safe.Assignment f) Data.Parameterized.Ctx.EmptyCtx
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (tp :: k). GHC.Classes.Eq (Data.Parameterized.Context.Safe.Index ctx tp)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Type.Equality.TestEquality (Data.Parameterized.Context.Safe.Index ctx)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (tp :: k). GHC.Classes.Ord (Data.Parameterized.Context.Safe.Index ctx tp)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.OrdF (Data.Parameterized.Context.Safe.Index ctx)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (tp :: k). GHC.Show.Show (Data.Parameterized.Context.Safe.Index ctx tp)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.ShowF (Data.Parameterized.Context.Safe.Index ctx)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (tp :: k). Data.Hashable.Class.Hashable (Data.Parameterized.Context.Safe.Index ctx tp)
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Classes.HashableF (Data.Parameterized.Context.Safe.Index ctx)
instance forall k (l :: Data.Parameterized.Ctx.Ctx k). Data.Parameterized.Context.Safe.KnownDiff l l
instance forall k (l :: Data.Parameterized.Ctx.Ctx k) (r :: Data.Parameterized.Ctx.Ctx k) (tp :: k). Data.Parameterized.Context.Safe.KnownDiff l r => Data.Parameterized.Context.Safe.KnownDiff l (r 'Data.Parameterized.Ctx.::> tp)
instance Control.Category.Category Data.Parameterized.Context.Safe.Diff
instance Data.Parameterized.Context.Safe.KnownContext 'Data.Parameterized.Ctx.EmptyCtx
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (tp :: k). Data.Parameterized.Context.Safe.KnownContext ctx => Data.Parameterized.Context.Safe.KnownContext (ctx 'Data.Parameterized.Ctx.::> tp)


-- | This module reexports either <a>Data.Parameterized.Context.Safe</a> or
--   <a>Data.Parameterized.Context.Unsafe</a> 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.
module Data.Parameterized.Context

-- | Create a single element context.
singleton :: f tp -> Assignment f (EmptyCtx ::> tp)

-- | Convert the assignment to a vector.
toVector :: Assignment f tps -> (forall tp. f tp -> e) -> Vector e

-- | Pattern synonym for extending an assignment on the right
infixl 9 :>

-- | Pattern synonym for the empty assignment
decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)

-- | Views
--   
--   Return true if assignment is empty.
null :: Assignment f ctx -> Bool

-- | Return assignment with all but the last block.
init :: Assignment f (ctx ::> tp) -> Assignment f ctx

-- | Return the last element in the assignment.
last :: Assignment f (ctx ::> tp) -> f tp

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

-- | <i>Deprecated: Use viewAssign or the Empty and :&gt; patterns
--   instead.</i>
view :: forall f ctx. Assignment f ctx -> AssignView f ctx

-- | 'forIndexM sz f' calls <tt>f</tt> on indices '[0..sz-1]'.
forIndexM :: forall ctx m. Applicative m => Size ctx -> (forall tp. Index ctx tp -> m ()) -> m ()

-- | Generate an assignment with some context type that is not known.
generateSome :: forall f. Int -> (Int -> Some f) -> Some (Assignment f)

-- | Generate an assignment with some context type that is not known.
generateSomeM :: forall m f. Applicative m => Int -> (Int -> m (Some f)) -> m (Some (Assignment f))

-- | Create an assignment from a list of values.
fromList :: [Some f] -> Some (Assignment f)

-- | Context embedding.
data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k)
CtxEmbedding :: Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding
[_ctxeSize] :: CtxEmbedding -> Size ctx'
[_ctxeAssignment] :: CtxEmbedding -> Assignment (Index ctx') ctx
class ExtendContext (f :: Ctx k -> *)
extendContext :: ExtendContext f => Diff ctx ctx' -> f ctx -> f ctx'
class ExtendContext' (f :: Ctx k -> k' -> *)
extendContext' :: ExtendContext' f => Diff ctx ctx' -> f ctx v -> f ctx' v
class ApplyEmbedding (f :: Ctx k -> *)
applyEmbedding :: ApplyEmbedding f => CtxEmbedding ctx ctx' -> f ctx -> f ctx'
class ApplyEmbedding' (f :: Ctx k -> k' -> *)
applyEmbedding' :: ApplyEmbedding' f => CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
identityEmbedding :: Size ctx -> CtxEmbedding ctx ctx
extendEmbeddingRightDiff :: forall ctx ctx' ctx''. Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx')
ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx') (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2)

-- | Constraint synonym used for getting an <a>Index</a> into a <a>Ctx</a>.
--   <tt>n</tt> is the zero-based, left-counted index into the list of
--   types <tt>ctx</tt> which has the type <tt>r</tt>.
type Idx n ctx r = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r)

-- | Get a lens for an position in an <a>Assignment</a> by zero-based,
--   left-to-right position. The position must be specified using
--   <tt>TypeApplications</tt> for the <tt>n</tt> parameter.
field :: forall n ctx f r. Idx n ctx r => Lens' (Assignment f ctx) (f r)

-- | Compute an <a>Index</a> value for a particular position in a
--   <a>Ctx</a>. The <tt>TypeApplications</tt> extension will be needed to
--   disambiguate the choice of the type <tt>n</tt>.
natIndex :: forall n ctx r. Idx n ctx r => Index ctx r

-- | This version of <a>natIndex</a> is suitable for use without the
--   <tt>TypeApplications</tt> extension.
natIndexProxy :: forall n ctx r proxy. Idx n ctx r => proxy n -> Index ctx r

-- | This type family is used to define currying/uncurrying operations on
--   assignments. It is best understood by seeing its evaluation on several
--   examples:
--   
--   <pre>
--   CurryAssignment EmptyCtx f x = x
--   CurryAssignment (EmptyCtx ::&gt; a) f x = f a -&gt; x
--   CurryAssignment (EmptyCtx ::&gt; a ::&gt; b) f x = f a -&gt; f b -&gt; x
--   CurryAssignment (EmptyCtx ::&gt; a ::&gt; b ::&gt; c) f x = f a -&gt; f b -&gt; f c -&gt; x
--   </pre>

-- | This class implements two methods that witness the isomorphism between
--   curried and uncurried functions.
class CurryAssignmentClass (ctx :: Ctx k)

-- | Transform a function that accepts an assignment into one with a
--   separate variable for each element of the assignment.
curryAssignment :: CurryAssignmentClass ctx => (Assignment f ctx -> x) -> CurryAssignment ctx f x

-- | Transform a curried function into one that accepts an assignment
--   value.
uncurryAssignment :: CurryAssignmentClass ctx => CurryAssignment ctx f x -> (Assignment f ctx -> x)
size1 :: Size (EmptyCtx ::> a)
size2 :: Size (EmptyCtx ::> a ::> b)
size3 :: Size (EmptyCtx ::> a ::> b ::> c)
size4 :: Size (EmptyCtx ::> a ::> b ::> c ::> d)
size5 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e)
size6 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f)
i1of2 :: Index (EmptyCtx ::> a ::> b) a
i2of2 :: Index (EmptyCtx ::> a ::> b) b
i1of3 :: Index (EmptyCtx ::> a ::> b ::> c) a
i2of3 :: Index (EmptyCtx ::> a ::> b ::> c) b
i3of3 :: Index (EmptyCtx ::> a ::> b ::> c) c
i1of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) a
i2of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) b
i3of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) c
i4of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) d
i1of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) a
i2of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) b
i3of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) c
i4of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) d
i5of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) e
i1of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) a
i2of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) b
i3of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) c
i4of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) d
i5of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) e
i6of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) f
instance Data.Parameterized.Context.CurryAssignmentClass Data.Parameterized.Ctx.EmptyCtx
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (a :: k). Data.Parameterized.Context.CurryAssignmentClass ctx => Data.Parameterized.Context.CurryAssignmentClass (ctx Data.Parameterized.Ctx.::> a)
instance forall k (xs :: Data.Parameterized.Ctx.Ctx k) (x :: k). Data.Parameterized.Context.Unsafe.KnownContext xs => Data.Parameterized.Context.Idx' 0 (xs 'Data.Parameterized.Ctx.::> x) x
instance forall k (xs :: Data.Parameterized.Ctx.Ctx k) (n :: GHC.Types.Nat) (r :: k) (x :: k). (Data.Parameterized.Context.Unsafe.KnownContext xs, Data.Parameterized.Context.Idx' (n GHC.TypeNats.- 1) xs r) => Data.Parameterized.Context.Idx' n (xs 'Data.Parameterized.Ctx.::> x) r
instance Data.Parameterized.Context.ExtendContext' Data.Parameterized.Context.Unsafe.Index
instance Data.Parameterized.Context.ApplyEmbedding' Data.Parameterized.Context.Unsafe.Index

module Data.Parameterized


module Data.Parameterized.Utils.BinTree

-- | A strict version of <a>Maybe</a>
data MaybeS v
JustS :: !v -> MaybeS v
NothingS :: MaybeS v
fromMaybeS :: a -> MaybeS a -> a

-- | Updated a contains a value that has been flagged on whether it was
--   modified by an operation.
data Updated a
Updated :: !a -> Updated a
Unchanged :: !a -> Updated a
updatedValue :: Updated a -> a
data TreeApp e t
BinTree :: !e -> !t -> !t -> TreeApp e t
TipTree :: TreeApp e t
class IsBinTree t e | t -> e
asBin :: IsBinTree t e => t -> TreeApp e t
tip :: IsBinTree t e => t
bin :: IsBinTree t e => e -> t -> t -> t
size :: IsBinTree t e => t -> Int
balanceL :: (IsBinTree c e) => e -> c -> c -> c
balanceR :: (IsBinTree c e) => e -> c -> c -> c

-- | 'glue l r' concatenates <tt>l</tt> and <tt>r</tt>.
--   
--   It assumes that <tt>l</tt> and <tt>r</tt> are already balanced with
--   respect to each other.
glue :: IsBinTree c e => c -> c -> c

-- | Concatenate two trees that are ordered with respect to each other.
merge :: IsBinTree c e => c -> c -> c

-- | Returns only entries that are less than predicate with respect to the
--   ordering and Nothing if no elements are discared.
filterGt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c

-- | <tt>filterLt' k m</tt> returns submap of <tt>m</tt> that only contains
--   entries that are smaller than <tt>k</tt>. If no entries are deleted
--   then return Nothing.
filterLt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c

-- | <tt>insert p m</tt> inserts the binding into <tt>m</tt>. It returns an
--   Unchanged value if the map stays the same size and an updated value if
--   a new entry was inserted.
insert :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> Updated c
delete :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c

-- | Union two sets
union :: (IsBinTree c e) => (e -> e -> Ordering) -> c -> c -> c

-- | link is called to insert a key and value between two disjoint
--   subtrees.
link :: IsBinTree c e => e -> c -> c -> c

-- | A Strict pair
data PairS f s
PairS :: !f -> !s -> PairS f s
instance GHC.Base.Functor Data.Parameterized.Utils.BinTree.MaybeS
instance GHC.Base.Alternative Data.Parameterized.Utils.BinTree.MaybeS
instance GHC.Base.Applicative Data.Parameterized.Utils.BinTree.MaybeS


-- | This module defines finite maps where the key and value types are
--   parameterized by an arbitrary kind.
--   
--   Some code was adapted from containers.
module Data.Parameterized.Map

-- | A map from parameterized keys to values with the same paramter type.
data MapF (k :: v -> Type) (a :: v -> Type)

-- | Return empty map
empty :: MapF k a

-- | Return map containing a single element
singleton :: k tp -> a tp -> MapF k a

-- | Insert a binding into the map, replacing the existing binding if
--   needed.
insert :: OrdF k => k tp -> a tp -> MapF k a -> MapF k a

-- | <tt>insertWith f new m</tt> inserts the binding into <tt>m</tt>.
--   
--   It inserts <tt>f new old</tt> if <tt>m</tt> already contains an
--   equivaltn value <tt>old</tt>, and <tt>new</tt> otherwise. It returns
--   an Unchanged value if the map stays the same size and an updated value
--   if a new entry was inserted.
insertWith :: OrdF k => (a tp -> a tp -> a tp) -> k tp -> a tp -> MapF k a -> MapF k a

-- | Delete a value from the map if present.
delete :: OrdF k => k tp -> MapF k a -> MapF k a

-- | Union two sets
union :: OrdF k => MapF k a -> MapF k a -> MapF k a

-- | Return true if map is empty
null :: MapF k a -> Bool

-- | Lookup value in map.
lookup :: OrdF k => k tp -> MapF k a -> Maybe (a tp)

-- | Return true if key is bound in map.
member :: OrdF k => k tp -> MapF k a -> Bool

-- | Return true if key is not bound in map.
notMember :: OrdF k => k tp -> MapF k a -> Bool
size :: IsBinTree t e => t -> Int

-- | Return all keys of the map in ascending order.
keys :: MapF k a -> [Some k]

-- | Return all elements of the map in the ascending order of their keys.
elems :: MapF k a -> [Some a]

-- | Create a Map from a list of pairs.
fromList :: OrdF k => [Pair k a] -> MapF k a
toList :: MapF k a -> [Pair k a]

-- | Generate a map from a foldable collection of keys and a function from
--   keys to values.
fromKeys :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type). (Monad m, Foldable t, OrdF a) => (forall tp. a tp -> m (v tp)) -> t (Some a) -> m (MapF a v)

-- | Generate a map from a foldable collection of keys and a monadic
--   function from keys to values.
fromKeysM :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type). (Monad m, Foldable t, OrdF a) => (forall tp. a tp -> m (v tp)) -> t (Some a) -> m (MapF a v)

-- | <tt>filterGt k m</tt> returns submap of <tt>m</tt> that only contains
--   entries that are larger than <tt>k</tt>.
filterGt :: OrdF k => k tp -> MapF k v -> MapF k v

-- | <tt>filterLt k m</tt> returns submap of <tt>m</tt> that only contains
--   entries that are smaller than <tt>k</tt>.
filterLt :: OrdF k => k tp -> MapF k v -> MapF k v

-- | Perform a fold with the key also provided.
foldrWithKey :: (forall s. k s -> a s -> b -> b) -> b -> MapF k a -> b

-- | Modify elements in a map
map :: (forall tp. f tp -> g tp) -> MapF ktp f -> MapF ktp g

-- | Run partial map over elements.
mapMaybe :: (forall tp. f tp -> Maybe (g tp)) -> MapF ktp f -> MapF ktp g

-- | Traverse elements in a map
traverseWithKey :: Applicative m => (forall tp. ktp tp -> f tp -> m (g tp)) -> MapF ktp f -> m (MapF ktp g)

-- | Traverse elements in a map without returning result.
traverseWithKey_ :: Applicative m => (forall tp. ktp tp -> f tp -> m ()) -> MapF ktp f -> m ()

-- | Update request tells when to do with value
data UpdateRequest v

-- | Keep the current value.
Keep :: UpdateRequest v

-- | Set the value to a new value.
Set :: !v -> UpdateRequest v

-- | Delete a value.
Delete :: UpdateRequest v

-- | Updated a contains a value that has been flagged on whether it was
--   modified by an operation.
data Updated a
Updated :: !a -> Updated a
Unchanged :: !a -> Updated a
updatedValue :: Updated a -> a

-- | Log-time algorithm that allows a value at a specific key to be added,
--   replaced, or deleted.
updateAtKey :: (OrdF k, Functor f) => k tp -> f (Maybe (a tp)) -> (a tp -> f (UpdateRequest (a tp))) -> MapF k a -> f (Updated (MapF k a))

-- | Merge bindings in two maps to get a third.
mergeWithKeyM :: forall k a b c m. (Applicative m, OrdF k) => (forall tp. k tp -> a tp -> b tp -> m (Maybe (c tp))) -> (MapF k a -> m (MapF k c)) -> (MapF k b -> m (MapF k c)) -> MapF k a -> MapF k b -> m (MapF k c)

-- | Like a 2-tuple, but with an existentially quantified parameter that
--   both of the elements share.
data Pair (a :: k -> *) (b :: k -> *)
[Pair] :: !(a tp) -> !(b tp) -> Pair a b
instance forall a (k :: a -> *) (v :: a -> *). Data.Parameterized.Classes.OrdF k => Data.Parameterized.Classes.IxedF a (Data.Parameterized.Map.MapF k v)
instance forall a (k :: a -> *) (v :: a -> *). Data.Parameterized.Classes.OrdF k => Data.Parameterized.Classes.AtF a (Data.Parameterized.Map.MapF k v)
instance forall k1 (k2 :: k1 -> *) (a :: k1 -> *). Data.Parameterized.Utils.BinTree.IsBinTree (Data.Parameterized.Map.MapF k2 a) (Data.Parameterized.Pair.Pair k2 a)
instance forall v (k :: v -> *) (a :: v -> *). (Data.Type.Equality.TestEquality k, Data.Parameterized.Classes.EqF a) => GHC.Classes.Eq (Data.Parameterized.Map.MapF k a)
instance forall k (ktp :: k -> *). Data.Parameterized.TraversableF.FunctorF (Data.Parameterized.Map.MapF ktp)
instance forall k (ktp :: k -> *). Data.Parameterized.TraversableF.FoldableF (Data.Parameterized.Map.MapF ktp)
instance forall k (ktp :: k -> *). Data.Parameterized.TraversableF.TraversableF (Data.Parameterized.Map.MapF ktp)
instance forall v (ktp :: v -> *) (rtp :: v -> *). (Data.Parameterized.Classes.ShowF ktp, Data.Parameterized.Classes.ShowF rtp) => GHC.Show.Show (Data.Parameterized.Map.MapF ktp rtp)