-- 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 2.0


-- | Utilities for working with <a>Data.Functor.Compose</a>.
--   
--   NB: This module contains an orphan instance. It will be included in
--   GHC 8.10, see
--   <a>https://gitlab.haskell.org/ghc/ghc/merge_requests/273</a>.
module Data.Parameterized.Compose

-- | The deduction (via generativity) that if <tt>g x :~: g y</tt> then
--   <tt>x :~: y</tt>.
--   
--   See <a>https://gitlab.haskell.org/ghc/ghc/merge_requests/273</a>.
testEqualityComposeBare :: forall (f :: k -> *) (g :: l -> k) x y. (forall w z. f w -> f z -> Maybe (w :~: z)) -> Compose f g x -> Compose f g y -> Maybe (x :~: y)
instance forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (Data.Functor.Compose.Compose f g)


-- | 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 -> Type)

-- | 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 -> Type
[Refl] :: forall k (a :: k) (b :: k). () => a :~: a
infix 4 :~:

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

-- | <tt>joinOrderingF x y</tt> first compares on <tt>x</tt>, returning an
--   equivalent value if it is not <a>EQF</a>. If it is <a>EQF</a>, 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

-- | If the "outer" functor has an <a>OrdF</a> instance, then one can be
--   generated for the "inner" functor. The type-level evidence of equality
--   is deduced via generativity of <tt>g</tt>, e.g. the inference <tt>g x
--   ~ g y</tt> implies <tt>x ~ y</tt>.
ordFCompose :: forall (f :: k -> *) (g :: l -> k) x y. (forall w z. f w -> f z -> OrderingF w z) -> Compose f g x -> Compose f g y -> OrderingF x y

-- | 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
type family IndexF (m :: *) :: k -> *
type family IxValueF (m :: *) :: k -> *

-- | 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 forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2). Data.Parameterized.Classes.OrdF f => Data.Parameterized.Classes.OrdF (Data.Functor.Compose.Compose f g)
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.
type family (<+>) (x :: Ctx k) (y :: Ctx k) :: Ctx k

-- | This type family computes the number of elements in a <a>Ctx</a>
type family CtxSize (a :: Ctx k) :: Nat

-- | 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
type family CtxLookupRight (n :: Nat) (ctx :: Ctx k) :: k

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

-- | Helper type family used to generate descriptive error messages when an
--   index is larger than the length of the <a>Ctx</a> being indexed.
type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) :: Constraint

-- | 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 defines a class <tt>DecidableEq</tt>, which represents decidable
--   equality on a type family.
--   
--   This is different from GHC's <tt>TestEquality</tt> in that it provides
--   evidence of non-equality. In fact, it is a superclass of
--   <tt>TestEquality</tt>.
module Data.Parameterized.DecidableEq

-- | Decidable equality.
class DecidableEq f
decEq :: DecidableEq f => f a -> f b -> Either (a :~: b) ((a :~: b) -> Void)


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


-- | Description : a GADT that hides a type parameter
--   
--   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
--   <a>ST</a> 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 repeating.
--   
--   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 :: forall m s k (tp :: k). NonceGenerator m s -> m (Nonce s tp)

-- | The number of nonces generated so far by this generator. Only really
--   useful for profiling.
countNoncesGenerated :: NonceGenerator m s -> m Integer

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

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

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

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

-- | Run a <a>ST</a> computation with a new nonce generator in the
--   <a>ST</a> 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 value <tt>n</tt>. This can be used to help use
--   type-level variables on code with data dependendent types.
--   
--   The <tt>TestEquality</tt> and <tt>DecidableEq</tt> instances for
--   <a>NatRepr</a> are 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 natural value of the number.
natValue :: NatRepr n -> Natural
intValue :: NatRepr n -> Integer

-- | This generates a NatRepr from a type-level context.
knownNat :: forall n. KnownNat n => NatRepr n
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

-- | Every nat is either zero or &gt;= 1.
isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 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 predecessor 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)

-- | Turn an <tt>Integral</tt> value into a <tt>NatRepr</tt>. Returns
--   <tt>Nothing</tt> if the given value is negative.
someNat :: Integral a => a -> Maybe (Some NatRepr)

-- | Turn a <tt>Natural</tt> into the corresponding <tt>NatRepr</tt>
mkNatRepr :: Natural -> Some NatRepr

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

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

-- | Strong induction variant of the recursor.
natRecStrong :: forall p f. NatRepr p -> f 0 -> (forall n. NatRepr n -> (forall m. m <= n => NatRepr m -> f m) -> f (n + 1)) -> f p

-- | Bounded recursor for natural numbers.
--   
--   If you can prove: - Base case: f 0 - Inductive step: if n &lt;= h and
--   (f n) then (f (n + 1)) You can conclude: for all n &lt;= h, (f (n +
--   1)).
natRecBounded :: forall m h f. m <= h => NatRepr m -> NatRepr h -> f 0 -> (forall n. n <= h => NatRepr n -> f n -> f (n + 1)) -> f (m + 1)

-- | 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]

-- | Apply a function to each element in a range starting at zero; return
--   the list of values obtained.
natFromZero :: forall h a. NatRepr h -> (forall 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

-- | The strict order (<a>defined by n &lt; m &lt;-</a> n + 1 &lt;= m, is
--   irreflexive.
lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void

-- | The strict order on the naturals is irreflexive.
lessThanAsymmetric :: forall m f n. LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void

-- | 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 two's complement with given
--   width.
minSigned :: 1 <= w => NatRepr w -> Integer

-- | Return maximum value for bitvector in two's 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

-- | (&lt;=) is a decidable relation on nats.
decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void)

-- | <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 <tt>+</tt> is commutative.
plusComm :: forall f m g n. f m -> g n -> (m + n) :~: (n + m)

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

-- | Cancel an add followed by 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)

-- | Used in <tt>Vector</tt>
lemmaMul :: 1 <= n => p w -> q n -> (w + ((n - 1) * w)) :~: (n * w)

-- | Addition of type-level naturals.
type family (+) (a :: Nat) (b :: Nat) :: Nat
infixl 6 +

-- | Subtraction of type-level naturals.
type family (-) (a :: Nat) (b :: Nat) :: Nat
infixl 6 -

-- | Multiplication of type-level naturals.
type family (*) (a :: Nat) (b :: Nat) :: Nat
infixl 7 *

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

-- | 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 -> Type)

-- | 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 -> Type
[Refl] :: forall k (a :: k) (b :: k). () => a :~: a
infix 4 :~:
data Some (f :: k -> *)


-- | This module provides a <a>ST</a>-based hashtable for parameterized
--   keys and values.
--   
--   NOTE: This API makes use of <a>unsafeCoerce</a> to implement the
--   parameterized hashtable abstraction. This should be type-safe provided
--   that 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 :: Type


-- | This module declares classes for working with types with the kind
--   <tt>(k -&gt; *) -&gt; *</tt> for any kind <tt>k</tt>.
--   
--   These classes generally require type-level evidence for operations on
--   their subterms, but don't actually provide it themselves (because
--   their types are not themselves parameterized, unlike those in
--   <a>Data.Parameterized.TraverableFC</a>).
--   
--   Note that there is still some ambiguity around naming conventions, see
--   <a>issue 23</a>.
module Data.Parameterized.ClassesC
class TestEqualityC (t :: (k -> *) -> *)
testEqualityC :: TestEqualityC t => (forall x y. f x -> f y -> Maybe (x :~: y)) -> t f -> t f -> Bool
class TestEqualityC t => OrdC (t :: (k -> *) -> *)
compareC :: OrdC t => (forall x y. f x -> g y -> OrderingF x y) -> t f -> t g -> Ordering
instance Data.Parameterized.ClassesC.OrdC Data.Parameterized.Some.Some
instance Data.Parameterized.ClassesC.TestEqualityC Data.Parameterized.Some.Some

module Data.Parameterized.BoolRepr

data BoolRepr (b :: Bool)
[FalseRepr] :: BoolRepr  'False
[TrueRepr] :: BoolRepr  'True

-- | conditional
ifRepr :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)

-- | negation
notRepr :: BoolRepr b -> BoolRepr (Not b)

-- | Conjunction
(%&&) :: BoolRepr a -> BoolRepr b -> BoolRepr (a && b)
infixr 3 %&&

-- | Disjunction
(%||) :: BoolRepr a -> BoolRepr b -> BoolRepr (a || b)
infixr 2 %||
type KnownBool = KnownRepr BoolRepr
someBool :: Bool -> Some BoolRepr

-- | 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 -> Type)

-- | 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 -> Type
[Refl] :: forall k (a :: k) (b :: k). () => a :~: a
infix 4 :~:
data Some (f :: k -> *)
instance Data.Hashable.Class.Hashable (Data.Parameterized.BoolRepr.BoolRepr n)
instance GHC.Classes.Eq (Data.Parameterized.BoolRepr.BoolRepr m)
instance Data.Type.Equality.TestEquality Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.DecidableEq.DecidableEq Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.Classes.OrdF Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.Classes.PolyEq (Data.Parameterized.BoolRepr.BoolRepr m) (Data.Parameterized.BoolRepr.BoolRepr n)
instance GHC.Show.Show (Data.Parameterized.BoolRepr.BoolRepr m)
instance Data.Parameterized.Classes.ShowF Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.Classes.HashableF Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.Classes.KnownRepr Data.Parameterized.BoolRepr.BoolRepr 'GHC.Types.True
instance Data.Parameterized.Classes.KnownRepr Data.Parameterized.BoolRepr.BoolRepr 'GHC.Types.False


-- | Description : a type family for representing a type-level string (AKA
--   symbol) at runtime
--   
--   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


-- | Description : Template Haskell primitives for working with large GADTs
--   
--   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:
--   <tt> forall x y . f x -&gt; f y -&gt; Maybe (x :~: y) </tt>
structuralTypeEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ

-- | <tt>structuralTypeOrd f</tt> returns a function with the type: <tt>
--   forall x y . f x -&gt; f y -&gt; OrderingF x y </tt>
--   
--   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 i'th 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)


-- | Description : Traversing structures having a single parametric type
--   followed by a fixed kind.
--   
--   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 <a>Foldable</a> 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 a) -> 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 a) -> 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


-- | Description : Traversing structures having a single parametric type
--   
--   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 <a>Foldable</a> 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 a) -> 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 the predicate.
allF :: FoldableF t => (forall tp. f tp -> Bool) -> t f -> Bool

-- | Return <a>True</a> if any values satisfy the predicate.
anyF :: FoldableF t => (forall tp. f tp -> Bool) -> t f -> Bool
instance Data.Parameterized.TraversableF.TraversableF (Data.Functor.Const.Const x)
instance forall k l (s :: (k -> *) -> *) (t :: (l -> *) -> k -> *). (Data.Parameterized.TraversableF.TraversableF s, Data.Parameterized.TraversableFC.TraversableFC t) => Data.Parameterized.TraversableF.FoldableF (Data.Functor.Compose.Compose s t)
instance forall k l (s :: (k -> *) -> *) (t :: (l -> *) -> k -> *). (Data.Parameterized.TraversableF.TraversableF s, Data.Parameterized.TraversableFC.TraversableFC t) => Data.Parameterized.TraversableF.TraversableF (Data.Functor.Compose.Compose s t)
instance Data.Parameterized.TraversableF.FoldableF (Data.Functor.Const.Const x)
instance Data.Parameterized.TraversableF.FunctorF (Data.Functor.Const.Const x)
instance forall k l (s :: (k -> *) -> *) (t :: (l -> *) -> k -> *). (Data.Parameterized.TraversableF.FunctorF s, Data.Parameterized.TraversableFC.FunctorFC t) => Data.Parameterized.TraversableF.FunctorF (Data.Functor.Compose.Compose s t)


-- | nDescription : A 2-tuple with identically parameterized elements
--   Copyright : (c) Galois, Inc 2017-2019
--   
--   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 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 <tt>k</tt> 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)
infixr 5 :<

-- | 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)
appendDiff :: Size r -> Diff l (l <+> r)
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

-- | Proof that <tt>r = l <a>+</a> app</tt> for some <tt>app</tt>
data IsAppend l r
[IsAppend] :: Size app -> IsAppend l (l <+> app)

-- | If <tt>l</tt> is a sub-context of <tt>r</tt> then extract out their
--   "contextual difference", i.e., the <tt>app</tt> such that <tt>r = l
--   <a>+</a> app</tt>
diffIsAppend :: Diff l r -> IsAppend 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>, the expression <tt>forIndex n v0 f</tt> is equivalent to
--   <tt>v0</tt> when <tt>n</tt> is zero, and <tt>f (forIndex (n-1) v0)
--   (n-1)</tt> 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>, the expression
--   <tt>forIndex i n f v</tt> is equivalent to <tt>v</tt> when <tt>i &gt;=
--   sizeInt n</tt>, and <tt>f i (forIndexRange (i+1) n v)</tt> 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

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

-- | <tt>dropTailRange r n</tt> 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 <tt>f tp</tt>.
--   
--   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 in an <a>Applicative</a> context
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)

-- | Represent 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)
appendDiff :: Size r -> Diff l (l <+> r)
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

-- | Proof that <tt>r = l <a>+</a> app</tt> for some <tt>app</tt>
data IsAppend l r
[IsAppend] :: Size app -> IsAppend l (l <+> app)

-- | If <tt>l</tt> is a sub-context of <tt>r</tt> then extract out their
--   "contextual difference", i.e., the <tt>app</tt> such that <tt>r = l
--   <a>+</a> app</tt>
diffIsAppend :: Diff l r -> IsAppend 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>, the expression <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>, the expression
--   <tt>forIndexRange i n f v</tt> is equivalent to <tt>v</tt> when <tt>i
--   &gt;= sizeInt n</tt>, and <tt>f i (forIndexRange (i+1) n v)</tt>
--   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 indexed 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
pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'
infixl 9 :>

-- | Pattern synonym for the empty assignment
pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx
decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)

-- | 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
take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment 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)

-- | Visit each of the elements in an <tt>Assignment</tt> in order from
--   left to right and collect the results using the provided
--   <tt>Monoid</tt>.
traverseAndCollect :: (Monoid w, Applicative m) => (forall tp. Index ctx tp -> f tp -> m w) -> Assignment f ctx -> m w

-- | This datastructure contains a proof that the first context is
--   embeddable in the second. This is useful if we want to add extend an
--   existing term under a larger context.
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)
appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
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>
type family CurryAssignment (ctx :: Ctx k) (f :: k -> *) (x :: *) :: *

-- | 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 forall k (m :: k -> *) (w :: k). GHC.Base.Functor (Data.Parameterized.Context.Collector m w)
instance (GHC.Base.Applicative m, GHC.Base.Monoid w) => GHC.Base.Applicative (Data.Parameterized.Context.Collector m w)
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


-- | This defines a type <a>Peano</a> and <a>PeanoRepr</a> for representing
--   a type-level natural at runtime. These type-level numbers are defined
--   inductively instead of using GHC.TypeLits.
--   
--   As a result, type-level computation defined recursively over these
--   numbers works more smoothly. (For example, see the type-level function
--   <a>Repeat</a> below.)
--   
--   Note: as in <a>NatRepr</a>, in UNSAFE mode, the runtime representation
--   of these type-level natural numbers is <a>Word64</a>.
module Data.Parameterized.Peano

-- | Unary representation for natural numbers
data Peano

-- | Peano zero
type Z =  'Z

-- | Peano successor
type S =  'S

-- | Addition
type family Plus (a :: Peano) (b :: Peano) :: Peano

-- | Subtraction
type family Minus (a :: Peano) (b :: Peano) :: Peano

-- | Multiplication
type family Mul (a :: Peano) (b :: Peano) :: Peano

-- | Maximum
type family Max (a :: Peano) (b :: Peano) :: Peano

-- | Minimum
type family Min (a :: Peano) (b :: Peano) :: Peano

-- | Addition
plusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)

-- | Subtraction
minusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)

-- | Multiplication
mulP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)

-- | Maximum
maxP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)

-- | Minimum
minP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)

-- | Zero
zeroP :: PeanoRepr Z

-- | Successor, Increment
succP :: PeanoRepr n -> PeanoRepr (S n)

-- | Get the predecessor (decrement)
predP :: PeanoRepr (S n) -> PeanoRepr n

-- | Apply a constructor <tt>f</tt> n-times to an argument <tt>s</tt>
type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k

-- | Calculate the size of a context
type family CtxSizeP (ctx :: Ctx k) :: Peano

-- | Apply a constructor <tt>f</tt> n-times to an argument <tt>s</tt>
repeatP :: PeanoRepr m -> (forall a. repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)

-- | Calculate the size of a context
ctxSizeP :: Assignment f ctx -> PeanoRepr (CtxSizeP ctx)

-- | Less-than-or-equal
type family Le (a :: Peano) (b :: Peano) :: Bool

-- | Less-than
type family Lt (a :: Peano) (b :: Peano) :: Bool

-- | Greater-than
type family Gt (a :: Peano) (b :: Peano) :: Bool

-- | Greater-than-or-equal
type family Ge (a :: Peano) (b :: Peano) :: Bool

-- | Less-than-or-equal-to
leP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)

-- | Less-than
ltP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)

-- | Greater-than
gtP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b)

-- | Greater-than-or-equal-to
geP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b)

-- | Implicit runtime representation
type KnownPeano = KnownRepr PeanoRepr

-- | The run time value, stored as an Word64 As these are unary numbers, we
--   don't worry about overflow.
data PeanoRepr (n :: Peano)

-- | When we have optimized the runtime representation, we need to have a
--   "view" that decomposes the representation into the standard form.
data PeanoView (n :: Peano)
[ZRepr] :: PeanoView Z
[SRepr] :: PeanoRepr n -> PeanoView (S n)

-- | Test whether a number is Zero or Successor
peanoView :: PeanoRepr n -> PeanoView n

-- | convert the view back to the runtime representation
viewRepr :: PeanoView n -> PeanoRepr n

-- | Convert a <a>Word64</a> to a <a>PeanoRepr</a>
mkPeanoRepr :: Word64 -> Some PeanoRepr
peanoValue :: PeanoRepr n -> Word64

-- | Turn an <tt>Integral</tt> value into a <a>PeanoRepr</a>. Returns
--   <tt>Nothing</tt> if the given value is negative.
somePeano :: Integral a => a -> Maybe (Some PeanoRepr)

-- | Return the maximum of two representations.
maxPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr

-- | Return the minimum of two representations.
minPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr

-- | List length as a Peano number
peanoLength :: [a] -> Some PeanoRepr

-- | Context size commutes with context append
plusCtxSizeAxiom :: forall t1 t2 f. Assignment f t1 -> Assignment f t2 -> CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)

-- | Minus distributes over plus
minusPlusAxiom :: forall n t t'. PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Minus n (Plus t' t) :~: Minus (Minus n t') t

-- | We can reshuffle minus with less than
ltMinusPlusAxiom :: forall n t t'. Lt t (Minus n t') ~  'True => PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Lt (Plus t' t) n :~:  '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 -> Type)

-- | 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 -> Type
[Refl] :: forall k (a :: k) (b :: k). () => a :~: a
infix 4 :~:
data Some (f :: k -> *)
instance Data.Parameterized.Classes.KnownRepr Data.Parameterized.Peano.PeanoRepr Data.Parameterized.Peano.Z
instance Data.Parameterized.Classes.KnownRepr Data.Parameterized.Peano.PeanoRepr n => Data.Parameterized.Classes.KnownRepr Data.Parameterized.Peano.PeanoRepr (Data.Parameterized.Peano.S n)
instance Data.Hashable.Class.Hashable (Data.Parameterized.Peano.PeanoRepr n)
instance GHC.Classes.Eq (Data.Parameterized.Peano.PeanoRepr m)
instance Data.Type.Equality.TestEquality Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.DecidableEq.DecidableEq Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.Classes.OrdF Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.Classes.PolyEq (Data.Parameterized.Peano.PeanoRepr m) (Data.Parameterized.Peano.PeanoRepr n)
instance GHC.Show.Show (Data.Parameterized.Peano.PeanoRepr p)
instance Data.Parameterized.Classes.ShowF Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.Classes.HashableF Data.Parameterized.Peano.PeanoRepr

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

-- | <tt>Updated a</tt> 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

-- | <tt>balanceL p l r</tt> returns a balanced tree for the sequence <tt>l
--   ++ [p] ++ r</tt>.
--   
--   It assumes that <tt>l</tt> and <tt>r</tt> are close to being balanced,
--   and that only <tt>l</tt> may contain too many elements.
balanceL :: IsBinTree c e => e -> c -> c -> c

-- | <tt>balanceR p l r</tt> returns a balanced tree for the sequence <tt>l
--   ++ [p] ++ r</tt>.
--   
--   It assumes that <tt>l</tt> and <tt>r</tt> are close to being balanced,
--   and that only <tt>r</tt> may contain too many elements.
balanceR :: IsBinTree c e => e -> c -> c -> c

-- | <tt>glue l r</tt> 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 discarded.
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

-- | <tt>link</tt> 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 parameter 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
--   equivalent value <tt>old</tt>, and <tt>new</tt> otherwise. It returns
--   an <a>Unchanged</a> value if the map stays the same size and an
--   <a>Updated</a> 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)

-- | Return entries with values that satisfy a predicate.
filter :: (forall tp. f tp -> Bool) -> MapF k f -> MapF k f

-- | Return key-value pairs that satisfy a predicate.
filterWithKey :: (forall tp. k tp -> f tp -> Bool) -> MapF k f -> MapF k f

-- | <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 left fold with the key also provided.
foldlWithKey :: (forall s. b -> k s -> a s -> b) -> b -> MapF k a -> b

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

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

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

-- | Fold the keys and values using the given monoid.
foldMapWithKey :: Monoid m => (forall s. k s -> a s -> m) -> MapF k a -> m

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

-- | Apply function to all elements in map.
mapWithKey :: (forall tp. ktp tp -> f tp -> g tp) -> MapF ktp f -> MapF ktp g

-- | Map elements and collect <a>Just</a> results.
mapMaybe :: (forall tp. f tp -> Maybe (g tp)) -> MapF ktp f -> MapF ktp g

-- | Map keys and elements and collect <a>Just</a> results.
mapMaybeWithKey :: (forall tp. k tp -> f tp -> Maybe (g tp)) -> MapF k f -> MapF k 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 ()

-- | <a>UpdateRequest</a> tells what to do with a found 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

-- | <tt>Updated a</tt> 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)


module Data.Parameterized.Utils.Endian

-- | Determines the composition of smaller numeric values into larger
--   values.
--   
--   BigEndian = most significant values in the lowest index location /
--   first LittleEndian = least significant values in the lowest index
--   location / first
--   
--   Value: 0x01020304 BigEndian = [ 0x01, 0x02, 0x03, 0x04 ] LittleEndian
--   = [ 0x04, 0x03, 0x02, 0x01 ]
data Endian
LittleEndian :: Endian
BigEndian :: Endian
instance GHC.Classes.Ord Data.Parameterized.Utils.Endian.Endian
instance GHC.Show.Show Data.Parameterized.Utils.Endian.Endian
instance GHC.Classes.Eq Data.Parameterized.Utils.Endian.Endian


-- | A fixed-size vector of typed elements.
--   
--   NB: This module contains an orphan instance. It will be included in
--   GHC 8.10, see
--   <a>https://gitlab.haskell.org/ghc/ghc/merge_requests/273</a>.
module Data.Parameterized.Vector

-- | Fixed-size non-empty vectors.
data Vector n a

-- | Make a vector of the given length and element type. Returns
--   <a>Nothing</a> if the input list does not have the right number of
--   elements. <tt>O(n)</tt>.
fromList :: 1 <= n => NatRepr n -> [a] -> Maybe (Vector n a)

-- | Get the elements of the vector as a list, lowest index first.
toList :: Vector n a -> [a]

-- | Length of the vector. <tt>O(1)</tt>
length :: Vector n a -> NatRepr n

-- | Proof that the length of this vector is not 0.
nonEmpty :: Vector n a -> LeqProof 1 n

-- | The length of the vector as an <a>Int</a>.
lengthInt :: Vector n a -> Int
elemAt :: (i + 1) <= n => NatRepr i -> Vector n a -> a

-- | Get the element at the given index. <tt>O(1)</tt>
elemAtMaybe :: Int -> Vector n a -> Maybe a

-- | Get the element at the given index. Raises an exception if the element
--   is not in the vector's domain. <tt>O(1)</tt>
elemAtUnsafe :: Int -> Vector n a -> a

-- | Insert an element at the given index. <tt>O(n)</tt>.
insertAt :: (i + 1) <= n => NatRepr i -> a -> Vector n a -> Vector n a

-- | Insert an element at the given index. Return <a>Nothing</a> if the
--   element is outside the vector bounds. <tt>O(n)</tt>.
insertAtMaybe :: Int -> a -> Vector n a -> Maybe (Vector n a)

-- | Remove the first element of the vector, and return the rest, if any.
uncons :: forall n a. Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))

-- | Extract a subvector of the given vector.
slice :: ((i + w) <= n, 1 <= w) => NatRepr i -> NatRepr w -> Vector n a -> Vector w a

-- | Take the front (lower-indexes) part of the vector.
take :: forall n x a. 1 <= n => NatRepr n -> Vector (n + x) a -> Vector n a

-- | Zip two vectors, potentially changing types. <tt>O(n)</tt>
zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWithM :: Monad m => (a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c)
zipWithM_ :: Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m ()

-- | Interleave two vectors. The elements of the first vector are at even
--   indexes in the result, the elements of the second are at odd indexes.
interleave :: forall n a. 1 <= n => Vector n a -> Vector n a -> Vector (2 * n) a

-- | Move the elements around, as specified by the given function. * Note:
--   the reindexing function says where each of the elements in the new
--   vector come from. * Note: it is OK for the same input element to end
--   up in mulitple places in the result. <tt>O(n)</tt>
shuffle :: (Int -> Int) -> Vector n a -> Vector n a

-- | Reverse the vector.
reverse :: forall a n. 1 <= n => Vector n a -> Vector n a

-- | Rotate "left". The first element of the vector is on the "left", so
--   rotate left moves all elemnts toward the corresponding smaller index.
--   Elements that fall off the beginning end up at the end.
rotateL :: Int -> Vector n a -> Vector n a

-- | Rotate "right". The first element of the vector is on the "left", so
--   rotate right moves all elemnts toward the corresponding larger index.
--   Elements that fall off the end, end up at the beginning.
rotateR :: Int -> Vector n a -> Vector n a

-- | Move all elements towards smaller indexes. Elements that fall off the
--   front are ignored. Empty slots are filled in with the given element.
--   <tt>O(n)</tt>.
shiftL :: Int -> a -> Vector n a -> Vector n a

-- | Move all elements towards the larger indexes. Elements that "fall" off
--   the end are ignored. Empty slots are filled in with the given element.
--   <tt>O(n)</tt>.
shiftR :: Int -> a -> Vector n a -> Vector n a

-- | Vector with exactly one element
singleton :: forall a. a -> Vector 1 a

-- | Add an element to the head of a vector
cons :: forall n a. a -> Vector n a -> Vector (n + 1) a

-- | Add an element to the tail of a vector
snoc :: forall n a. Vector n a -> a -> Vector (n + 1) a

-- | Apply a function to each element in a range starting at zero; return
--   the a vector of values obtained. cf. both <tt>natFromZero</tt> and
--   <tt>Data.Vector.generate</tt>
generate :: forall h a. NatRepr h -> (forall n. n <= h => NatRepr n -> a) -> Vector (h + 1) a

-- | Since <tt>Vector</tt> is traversable, we can pretty trivially sequence
--   <tt>natFromZeroVec</tt> inside a monad.
generateM :: forall m h a. Monad m => NatRepr h -> (forall n. n <= h => NatRepr n -> m a) -> m (Vector (h + 1) a)

-- | Monadically join a vector of values, using the given function. This
--   functionality can sometimes be reproduced by creating a newtype
--   wrapper and using <tt>joinWith</tt>, this implementation is provided
--   for convenience.
joinWithM :: forall m f n w. (1 <= w, Monad m) => (forall l. 1 <= l => NatRepr l -> f w -> f l -> m (f (w + l))) -> NatRepr w -> Vector n (f w) -> m (f (n * w))

-- | Join a vector of vectors, using the given function to combine the
--   sub-vectors.
joinWith :: forall f n w. 1 <= w => (forall l. 1 <= l => NatRepr l -> f w -> f l -> f (w + l)) -> NatRepr w -> Vector n (f w) -> f (n * w)

-- | Split a vector into a vector of vectors.
--   
--   The <a>Endian</a> parameter determines the ordering of the inner
--   vectors. If <a>LittleEndian</a>, then less significant bits go into
--   smaller indexes. If <a>BigEndian</a>, then less significant bits go
--   into larger indexes. See the documentation for <a>split</a> for more
--   details.
splitWith :: forall f w n. (1 <= w, 1 <= n) => Endian -> (forall i. (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w) -> NatRepr n -> NatRepr w -> f (n * w) -> Vector n (f w)

-- | An applicative version of <tt>splitWith</tt>.
splitWithA :: forall f g w n. (Applicative f, 1 <= w, 1 <= n) => Endian -> (forall i. (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w)) -> NatRepr n -> NatRepr w -> g (n * w) -> f (Vector n (g w))

-- | Split a vector into a vector of vectors. The default ordering of the
--   outer result vector is <a>LittleEndian</a>.
--   
--   For example: <tt> let wordsize = knownNat :: NatRepr 3 vecsize =
--   knownNat :: NatRepr 12 numwords = knownNat :: NatRepr 4 (12 / 3) Just
--   inpvec = fromList vecsize [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ] in
--   show (split numwords wordsize inpvec) == "[ [1,2,3], [4,5,6], [7,8,9],
--   [10,11,12] ]" </tt> whereas a BigEndian result would have been <tt> [
--   [10,11,12], [7,8,9], [4,5,6], [1,2,3] ] </tt>
split :: (1 <= w, 1 <= n) => NatRepr n -> NatRepr w -> Vector (n * w) a -> Vector n (Vector w a)

-- | Join a vector of vectors into a single vector. Assumes an
--   append/<a>LittleEndian</a> join strategy: the order of the inner
--   vectors is preserved in the result vector.
--   
--   <pre>
--   let innersize = knownNat :: NatRepr 4
--       Just inner1 = fromList innersize [ 1, 2, 3, 4 ]
--       Just inner2 = fromList innersize [ 5, 6, 7, 8 ]
--       Just inner3 = fromList innersize [ 9, 10, 11, 12 ]
--       outersize = knownNat :: NatRepr 3
--       Just outer = fromList outersize [ inner1, inner2, inner3 ]
--   in show (join innersize outer) = [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]
--   </pre>
--   
--   a prepend/<a>BigEndian</a> join strategy would have the result: <tt> [
--   9, 10, 11, 12, 5, 6, 7, 8, 1, 2, 3, 4 ] </tt>
join :: 1 <= w => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a

-- | Append two vectors. The first one is at lower indexes in the result.
append :: Vector m a -> Vector n a -> Vector (m + n) a
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Parameterized.Vector.Vector n a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Parameterized.Vector.Vector n a)
instance GHC.Base.Functor (Data.Parameterized.Vector.Vector n)
instance Data.Foldable.Foldable (Data.Parameterized.Vector.Vector n)
instance Data.Traversable.Traversable (Data.Parameterized.Vector.Vector n)


-- | This module declares a class with a single method that can be used to
--   derive a <a>KnownRepr</a> constraint from an explicit <tt>Repr</tt>
--   argument. Clients of this method need only create an empty instance.
--   The default implementation suffices.
--   
--   For example, suppose we have defined a <tt>Repr</tt> type for
--   <tt>Peano</tt> numbers:
--   
--   <pre>
--   data Peano = Z | S Peano
--   
--   data PeanoRepr p where
--       ZRepr :: PeanoRepr Z
--       SRepr :: PeanoRepr p -&gt; PeanoRepr (S p)
--   
--   -- KnownRepr instances
--   </pre>
--   
--   Then the instance for this class <tt> instance IsRepr PeanoRepr </tt>
--   
--   means that functions with <a>KnownRepr</a> constraints can be used
--   after pattern matching.
--   
--   <pre>
--   f :: KnownRepr PeanoRepr a =&gt; ...
--   
--   example :: PeanoRepr n -&gt; ...
--   example ZRepr = ...
--   example (SRepr (pm::PeanoRepr m)) = ... withRepr pm f ...
--   </pre>
--   
--   NOTE: The type <tt>f</tt> must be a *singleton* type--- i.e. for a
--   given type <tt>a</tt> there should be only one value that inhabits 'f
--   a'. If that is not the case, this operation can be used to subvert
--   coherence.
--   
--   Credit: the unsafe implementation of <a>withRepr</a> is taken from the
--   <tt>withSingI</tt> function in the singletons library
--   <a>http://hackage.haskell.org/package/singletons-2.5.1/</a>. Packaging
--   this method in a class here makes it more flexible---we do not have to
--   define a dedicated <tt>Sing</tt> type, but can use any convenient
--   singleton as a <tt>Repr</tt>.
--   
--   NOTE: if this module is compiled without 1, the default method will
--   not be available.
module Data.Parameterized.WithRepr

-- | Turn an explicit Repr value into an implict KnownRepr constraint
class IsRepr (f :: k -> *)
withRepr :: IsRepr f => f a -> (KnownRepr f a => r) -> r
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.NatRepr.Internal.NatRepr
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.SymbolRepr.SymbolRepr
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.BoolRepr.BoolRepr
instance forall k (f :: k -> *). Data.Parameterized.WithRepr.IsRepr f => Data.Parameterized.WithRepr.IsRepr (Data.Parameterized.List.List f)
instance forall k (f :: k -> *). Data.Parameterized.WithRepr.IsRepr f => Data.Parameterized.WithRepr.IsRepr (Data.Parameterized.Context.Unsafe.Assignment f)