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


-- | Classes and data structures for working with data-kind indexed types
--   
--   This package 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.1.11.0


-- | An unsafe module that provides functionality for constructing equality
--   proofs that GHC cannot prove on its own.
module Data.Parameterized.Axiom

-- | Assert a proof of equality between two types. This is unsafe if used
--   improperly, so use this with caution!
unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b

-- | Assert a proof of heterogeneous equality between two types. This is
--   unsafe if used improperly, so use this with caution!
unsafeHeteroAxiom :: forall {k1} {k2} (a :: k1) (b :: k2). a :~~: b


-- | 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> and also
--   https:/<i>github.com</i>haskell-compat<i>base-orphans</i>issues/49.
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 k l f (g :: l -> k) (x :: l) (y :: l). (forall (w :: k) (z :: k). () => f w -> f z -> Maybe (w :~: z)) -> Compose f g x -> Compose f g y -> Maybe (x :~: y)


-- | 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
class TestEquality (f :: k -> Type)
testEquality :: forall (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b)
data (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a

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

-- | The <a>OrdF</a> class is a total ordering over parameterized types so
--   that types with different parameters can be compared.
--   
--   Instances of <a>OrdF</a> are expected to satisfy the following laws:
--   
--   <ul>
--   <li><i><b>Transitivity</b></i> if <tt>leqF x y &amp;&amp; leqF y
--   z</tt> = <a>True</a>, then <tt>leqF x = z</tt> = <tt>True</tt></li>
--   <li><i><b>Reflexivity</b></i> <tt>leqF x x</tt> = <tt>True</tt></li>
--   <li><i><b>Antisymmetry</b></i> if <tt>leqF x y &amp;&amp; leqF y
--   x</tt> = <a>True</a>, then <tt>testEquality x y</tt> = <tt>Just
--   Refl</tt></li>
--   </ul>
--   
--   Note that the following operator interactions are expected to hold:
--   
--   <ul>
--   <li><tt>geqF x y</tt> iff <tt>leqF y x</tt></li>
--   <li><tt>ltF x y</tt> iff <tt>leqF x y &amp;&amp; testEquality x y =
--   Nothing</tt></li>
--   <li><tt>gtF x y</tt> iff <tt>ltF y x</tt></li>
--   <li><tt>ltF x y</tt> iff <tt>compareF x y == LTF</tt></li>
--   <li><tt>gtF x y</tt> iff <tt>compareF x y == GTF</tt></li>
--   <li><tt>isJust (testEquality x y)</tt> iff <tt>compareF x y ==
--   EQF</tt></li>
--   </ul>
--   
--   Furthermore, when <tt>x</tt> and <tt>y</tt> both have type <tt>(k
--   tp)</tt>, we expect:
--   
--   <ul>
--   <li><tt>toOrdering (compareF x y)</tt> equals <tt>compare x y</tt>
--   when <tt>Ord (k tp)</tt> has an instance.</li>
--   <li><tt>isJust (testEquality x y)</tt> equals <tt>x == y</tt> when
--   <tt>Eq (k tp)</tt> has an instance.</li>
--   </ul>
--   
--   Minimal complete definition: either <a>compareF</a> or <a>leqF</a>.
--   Using <a>compareF</a> can be more efficient for complex types.
class TestEquality ktp => OrdF (ktp :: k -> Type)
compareF :: forall (x :: k) (y :: k). OrdF ktp => ktp x -> ktp y -> OrderingF x y
leqF :: forall (x :: k) (y :: k). OrdF ktp => ktp x -> ktp y -> Bool
ltF :: forall (x :: k) (y :: k). OrdF ktp => ktp x -> ktp y -> Bool
geqF :: forall (x :: k) (y :: k). OrdF ktp => ktp x -> ktp y -> Bool
gtF :: forall (x :: k) (y :: k). 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 j k f (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 :: k) (y :: k)
[LTF] :: forall {k} (x :: k) (y :: k). OrderingF x y
[EQF] :: forall {k} (x :: k). OrderingF x x
[GTF] :: forall {k} (x :: k) (y :: k). 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 j k (a :: j) (b :: j) (c :: k) (d :: k). OrderingF a b -> (a ~ b => OrderingF c d) -> OrderingF c d
orderingF_refl :: forall {k} (x :: k) (y :: k). OrderingF x y -> Maybe (x :~: y)

-- | Convert <a>OrderingF</a> to standard ordering.
toOrdering :: forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering

-- | Convert standard ordering to <a>OrderingF</a>.
fromOrdering :: forall {k} (x :: k). 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 k l f (g :: l -> k) (x :: l) (y :: l). (forall (w :: k) (z :: k). () => 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 -> Type)

-- | Provides a show instance for each type.
withShow :: forall p q (tp :: k) a. ShowF f => p f -> q tp -> (Show (f tp) => a) -> a
($dmwithShow) :: forall (tp :: k) p q a. (ShowF f, Show (f tp)) => p f -> q tp -> (Show (f tp) => a) -> a
showF :: forall (tp :: k). 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 :: k). ShowF f => Int -> f tp -> String -> String
showsF :: forall {k} f (tp :: k). ShowF f => f tp -> String -> String

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

-- | Hash with default salt.
hashF :: forall (tp :: k). 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 -> Type)
coerceF :: forall (a :: k) (b :: k). CoercibleF rtp => rtp a -> rtp b

-- | Captures the value obtained from applying a type to a function so that
--   we can use parameterized class instance to provide unparameterized
--   instances for specific types.
--   
--   This is the same as <tt>Ap</tt> from <tt>Control.Applicative</tt>, but
--   we introduce our own new type to avoid orphan instances.
newtype TypeAp (f :: k -> Type) (tp :: k)
TypeAp :: f tp -> TypeAp (f :: k -> Type) (tp :: k)
type family IndexF m :: k -> Type
type family IxValueF m :: k -> Type

-- | 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 -> Type) (ctx :: k)
knownRepr :: KnownRepr f ctx => f ctx
class Eq a => Hashable a
hashWithSalt :: Hashable a => Int -> a -> Int
hash :: Hashable a => a -> Int
isJust :: Maybe a -> Bool
instance Data.Parameterized.Classes.CoercibleF (GHC.Internal.Data.Functor.Const.Const x)
instance GHC.Classes.Eq a => Data.Parameterized.Classes.EqF (GHC.Internal.Data.Functor.Const.Const a)
instance Data.Parameterized.Classes.EqF GHC.Internal.Data.Proxy.Proxy
instance forall k (f :: k -> *) (tp :: k). GHC.Internal.Data.Type.Equality.TestEquality f => GHC.Classes.Eq (Data.Parameterized.Classes.TypeAp f tp)
instance Data.Hashable.Class.Hashable a => Data.Parameterized.Classes.HashableF (GHC.Internal.Data.Functor.Const.Const a)
instance forall k (f :: k -> *) (tp :: k). (Data.Parameterized.Classes.HashableF f, GHC.Internal.Data.Type.Equality.TestEquality f) => Data.Hashable.Class.Hashable (Data.Parameterized.Classes.TypeAp f tp)
instance forall k (ctx :: k). Data.Parameterized.Classes.KnownRepr GHC.Internal.Data.Proxy.Proxy ctx
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> k1). Data.Parameterized.Classes.OrdF f => Data.Parameterized.Classes.OrdF (Data.Functor.Compose.Compose f g)
instance forall k (f :: k -> *) (tp :: k). Data.Parameterized.Classes.OrdF f => GHC.Classes.Ord (Data.Parameterized.Classes.TypeAp f tp)
instance GHC.Internal.Show.Show x => Data.Parameterized.Classes.ShowF (GHC.Internal.Data.Functor.Const.Const x)
instance Data.Parameterized.Classes.ShowF GHC.Internal.Data.Proxy.Proxy
instance forall k (f :: k -> *) (tp :: k). Data.Parameterized.Classes.ShowF f => GHC.Internal.Show.Show (Data.Parameterized.Classes.TypeAp f tp)


-- | This module defines type-level lists used for representing the type of
--   variables in a context.
--   
--   A <a>Ctx</a> is never intended to be manipulated at the value level;
--   it is used purely as a type-level list, just like <tt>'[]</tt>. To see
--   how it is used, see the module header for
--   <a>Data.Parameterized.Context</a>.
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 :: Ctx k
type SingleCtx (x :: k) = EmptyCtx :: Ctx k ::> 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

-- | Flatten a nested context
type family CtxFlatten (ctx :: Ctx Ctx a) :: Ctx a

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

-- | 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 :: Ctx k) (n :: Natural) = CtxSize ctx - 1 - n


-- | This reflects type level proofs involving contexts.
module Data.Parameterized.Ctx.Proofs
leftId :: forall {k} p (x :: Ctx k). p x -> ((EmptyCtx :: Ctx k) <+> x) :~: x
assoc :: forall {k} p (x :: Ctx k) q (y :: Ctx k) r (z :: Ctx k). 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 :: k -> Type)
decEq :: forall (a :: k) (b :: k). 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.
--   
--   This module is deprecated, and should not be used in new code. Clients
--   of this module should migrate to use <a>Data.Parameterized.Nonce</a>.

-- | <i>Deprecated: Migrate to use Data.Parameterized.Nonce instead, this
--   module will be removed soon.</i>
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 :: forall {k} s (tp :: k). 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 Data.Parameterized.Classes.EqF Data.Parameterized.Nonce.Unsafe.Nonce
instance forall k (tp :: k). GHC.Classes.Eq (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance Data.Parameterized.Classes.HashableF Data.Parameterized.Nonce.Unsafe.Nonce
instance forall k (tp :: k). Data.Hashable.Class.Hashable (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance Data.Parameterized.Classes.OrdF Data.Parameterized.Nonce.Unsafe.Nonce
instance forall k (tp :: k). GHC.Classes.Ord (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance Data.Parameterized.Classes.ShowF Data.Parameterized.Nonce.Unsafe.Nonce
instance forall k (tp :: k). GHC.Internal.Show.Show (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance GHC.Internal.Data.Type.Equality.TestEquality Data.Parameterized.Nonce.Unsafe.Nonce


-- | 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.
--   
--   All arguments use <tt>hashable</tt>, and <a>structuralHashWithSalt</a>
--   can be used instead as it allows user-definable patterns to be used at
--   specific types.

-- | <i>Deprecated: Use structuralHashWithSalt</i>
structuralHash :: TypeQ -> ExpQ

-- | <tt>structuralHashWithSalt tp</tt> generates a function with the type
--   <tt>Int -&gt; tp -&gt; Int</tt> that hashes type.
--   
--   The second arguments is for generating user-defined patterns to
--   replace <a>hashWithSalt</a> for specific types.
structuralHashWithSalt :: TypeQ -> [(TypePat, ExpQ)] -> 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

-- | Generate a "repr" or singleton type from a data kind. For nullary
--   constructors, this works as follows:
--   
--   <pre>
--   data T1 = A | B | C
--   $(mkRepr ''T1)
--   ======&gt;
--   data T1Repr (tp :: T1)
--     where
--       ARepr :: T1Repr 'A
--       BRepr :: T1Repr 'B
--       CRepr :: T1Repr 'C
--   </pre>
--   
--   For constructors with fields, we assume each field type <tt>T</tt>
--   already has a corresponding repr type <tt>TRepr :: T -&gt; *</tt>.
--   
--   <pre>
--   data T2 = T2_1 T1 | T2_2 T1
--   $(mkRepr ''T2)
--   ======&gt;
--   data T2Repr (tp :: T2)
--     where
--       T2_1Repr :: T1Repr tp -&gt; T2Repr ('T2_1 tp)
--       T2_2Repr :: T1Repr tp -&gt; T2Repr ('T2_2 tp)
--   </pre>
--   
--   Constructors with multiple fields work fine as well:
--   
--   <pre>
--   data T3 = T3 T1 T2
--   $(mkRepr ''T3)
--   ======&gt;
--   data T3Repr (tp :: T3)
--     where
--       T3Repr :: T1Repr tp1 -&gt; T2Repr tp2 -&gt; T3Repr ('T3 tp1 tp2)
--   </pre>
--   
--   This is generally compatible with other "repr" types provided by
--   <tt>parameterized-utils</tt>, such as <tt>NatRepr</tt> and
--   <tt>PeanoRepr</tt>:
--   
--   <pre>
--   data T4 = T4_1 Nat | T4_2 Peano
--   $(mkRepr ''T4)
--   ======&gt;
--   data T4Repr (tp :: T4)
--     where
--       T4Repr :: NatRepr tp1 -&gt; PeanoRepr tp2 -&gt; T4Repr ('T4 tp1 tp2)
--   </pre>
--   
--   The data kind must be "simple", i.e. it must be monomorphic and only
--   contain user-defined data constructors (no lists, tuples, etc.). For
--   example, the following will not work:
--   
--   <pre>
--   data T5 a = T5 a
--   $(mkRepr ''T5)
--   ======&gt;
--   Foo.hs:1:1: error:
--       Exception when trying to run compile-time code:
--         mkRepr cannot be used on polymorphic data kinds.
--   </pre>
--   
--   Similarly, this will not work:
--   
--   <pre>
--   data T5 = T5 [Nat]
--   $(mkRepr ''T5)
--   ======&gt;
--   Foo.hs:1:1: error:
--       Exception when trying to run compile-time code:
--         mkRepr cannot be used on this data kind.
--   </pre>
--   
--   Note that at a minimum, you will need the following extensions to use
--   this macro:
--   
--   <pre>
--   {-# LANGUAGE DataKinds #-}
--   {-# LANGUAGE GADTs #-}
--   {-# LANGUAGE KindSignatures #-}
--   {-# LANGUAGE TemplateHaskell #-}
--   </pre>
mkRepr :: Name -> DecsQ

-- | Generate <tt>KnownRepr</tt> instances for each constructor of a data
--   kind. Given a data kind <tt>T</tt>, we assume a repr type <tt>TRepr (t
--   :: T)</tt> is in scope with structure that perfectly matches
--   <tt>T</tt> (using <a>mkRepr</a> to generate the repr type will
--   guarantee this).
--   
--   Given data kinds <tt>T1</tt>, <tt>T2</tt>, and <tt>T3</tt> from the
--   documentation of <a>mkRepr</a>, and the associated repr types
--   <tt>T1Repr</tt>, <tt>T2Repr</tt>, and <tt>T3Repr</tt>, we can use
--   <a>mkKnownReprs</a> to generate these instances like so:
--   
--   <pre>
--   $(mkKnownReprs ''T1)
--   ======&gt;
--   instance KnownRepr T1Repr 'A where
--     knownRepr = ARepr
--   instance KnownRepr T1Repr 'B where
--     knownRepr = BRepr
--   instance KnownRepr T1Repr 'C where
--     knownRepr = CRepr
--   </pre>
--   
--   <pre>
--   $(mkKnownReprs ''T2)
--   ======&gt;
--   instance KnownRepr T1Repr tp =&gt;
--            KnownRepr T2Repr ('T2_1 tp) where
--     knownRepr = T2_1Repr knownRepr
--   </pre>
--   
--   <pre>
--   $(mkKnownReprs ''T3)
--   ======&gt;
--   instance (KnownRepr T1Repr tp1, KnownRepr T2Repr tp2) =&gt;
--            KnownRepr T3Repr ('T3_1 tp1 tp2) where
--     knownRepr = T3_1Repr knownRepr knownRepr
--   </pre>
--   
--   The same restrictions that apply to <a>mkRepr</a> also apply to
--   <a>mkKnownReprs</a>. The data kind must be "simple", i.e. it must be
--   monomorphic and only contain user-defined data constructors (no lists,
--   tuples, etc.).
--   
--   Note that at a minimum, you will need the following extensions to use
--   this macro:
--   
--   <pre>
--   {-# LANGUAGE DataKinds #-}
--   {-# LANGUAGE GADTs #-}
--   {-# LANGUAGE KindSignatures #-}
--   {-# LANGUAGE MultiParamTypeClasses #-}
--   {-# LANGUAGE TemplateHaskell #-}
--   </pre>
--   
--   Also, <a>mkKnownReprs</a> must be used in the same module as the
--   definition of the repr type (not necessarily for the data kind).
mkKnownReprs :: Name -> DecsQ
type DataD = DatatypeInfo
lookupDataType' :: Name -> Q DatatypeInfo
asTypeCon :: String -> Type -> Q 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

-- | The dataParamTypes function returns the list of Type arguments for the
--   constructor. For example, if passed the DatatypeInfo for a <tt>newtype
--   Id a = MkId a</tt> then this would return <tt>[<a>SigT</a>
--   (<a>VarT</a> a) <a>StarT</a>]</tt>. Note that there may be type
--   *variables* not referenced in the returned array; this simply returns
--   the type *arguments*.
dataParamTypes :: DatatypeInfo -> [Type]

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

module Data.Parameterized.DataKind
data PairRepr (f :: k1 -> Type) (g :: k2 -> Type) (p :: (k1, k2))
[PairRepr] :: forall {k1} {k2} (f :: k1 -> Type) (a :: k1) (g :: k2 -> Type) (b :: k2). f a -> g b -> PairRepr f g '(a, b)
type family Fst (pair :: (k1, k2)) :: k1
type family Snd (pair :: (k1, k2)) :: k2
fst :: forall {k1} {k2} f (g :: k2 -> Type) (p :: (k1, k2)). PairRepr f g p -> f (Fst p)
snd :: forall {k1} {k2} (f :: k1 -> Type) g (p :: (k1, k2)). PairRepr f g p -> g (Snd p)
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> *). (Data.Parameterized.Classes.EqF f, Data.Parameterized.Classes.EqF g) => Data.Parameterized.Classes.EqF (Data.Parameterized.DataKind.PairRepr f g)
instance forall k1 k2 (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2). (GHC.Classes.Eq (f a), GHC.Classes.Eq (g b)) => GHC.Classes.Eq (Data.Parameterized.DataKind.PairRepr f g '(a, b))
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> *). (Data.Parameterized.Classes.OrdF f, Data.Parameterized.Classes.OrdF g) => Data.Parameterized.Classes.OrdF (Data.Parameterized.DataKind.PairRepr f g)
instance forall k1 k2 (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2). (GHC.Classes.Ord (f a), GHC.Classes.Ord (g b)) => GHC.Classes.Ord (Data.Parameterized.DataKind.PairRepr f g '(a, b))
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> *). (Data.Parameterized.Classes.ShowF f, Data.Parameterized.Classes.ShowF g) => Data.Parameterized.Classes.ShowF (Data.Parameterized.DataKind.PairRepr f g)
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> *) (p :: (k1, k2)). (Data.Parameterized.Classes.ShowF f, Data.Parameterized.Classes.ShowF g) => GHC.Internal.Show.Show (Data.Parameterized.DataKind.PairRepr f g p)
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> *). (GHC.Internal.Data.Type.Equality.TestEquality f, GHC.Internal.Data.Type.Equality.TestEquality g) => GHC.Internal.Data.Type.Equality.TestEquality (Data.Parameterized.DataKind.PairRepr f g)


-- | 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 -> Type -> l -> Type)
testEqualityFC :: TestEqualityFC t => (forall (x :: k) (y :: k). () => f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). () => 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 -> Type -> l -> Type)
compareFC :: OrdFC t => (forall (x :: k) (y :: k). () => f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). () => 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 -> Type -> l -> Type)
showFC :: ShowFC t => (forall (x :: k). () => f x -> String) -> forall (x :: l). () => t f x -> String
showsPrecFC :: ShowFC t => (forall (x :: k). () => Int -> f x -> ShowS) -> forall (x :: l). () => 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 -> Type -> l -> Type)
hashWithSaltFC :: HashableFC t => (forall (x :: k). () => Int -> f x -> Int) -> forall (x :: l). () => Int -> t f x -> Int

-- | A parameterized type that is a functor on all instances.
--   
--   Laws:
--   
--   <ul>
--   <li><i>Identity</i> <tt><a>fmapFC</a> <a>id</a> == <a>id</a></tt></li>
--   <li><i>Composition</i> <tt><a>fmapFC</a> (f . g) == <a>fmapFC</a> f .
--   <a>fmapFC</a> g</tt></li>
--   </ul>
class FunctorFC (t :: k -> Type -> l -> Type)
fmapFC :: FunctorFC t => (forall (x :: k). () => f x -> g x) -> forall (x :: l). () => 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 -> Type -> l -> Type)

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

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

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

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

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

-- | Convert structure to list.
toListFC :: FoldableFC t => (forall (x :: k). () => f x -> a) -> forall (x :: l). () => t f x -> [a]

-- | Monadic fold over the elements of a structure from left to right.
foldlMFC :: forall {k} {l} t m b f (c :: l). (FoldableFC t, Monad m) => (forall (x :: k). () => b -> f x -> m b) -> b -> t f c -> m b

-- | Monadic strict fold over the elements of a structure from left to
--   right.
foldlMFC' :: forall {k} {l} t m b f (c :: l). (FoldableFC t, Monad m) => (forall (x :: k). () => b -> f x -> m b) -> b -> t f c -> m b

-- | Monadic fold over the elements of a structure from right to left.
foldrMFC :: forall {k} {l} t m f b (c :: l). (FoldableFC t, Monad m) => (forall (x :: k). () => f x -> b -> m b) -> b -> t f c -> m b

-- | Monadic strict fold over the elements of a structure from right to
--   left.
foldrMFC' :: forall {k} {l} t m f b (c :: l). (FoldableFC t, Monad m) => (forall (x :: k). () => f x -> b -> m b) -> b -> t f c -> m b
class (FunctorFC t, FoldableFC t) => TraversableFC (t :: k -> Type -> l -> Type)
traverseFC :: forall f g m. (TraversableFC t, Applicative m) => (forall (x :: k). () => f x -> m (g x)) -> forall (x :: l). () => 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 :: k). () => f x -> m a) -> forall (x :: l). () => t f x -> m ()

-- | Map each element of a structure to an action, evaluate these actions
--   from left to right, and ignore the results.

-- | <i>Deprecated: Use forFC_</i>
forMFC_ :: forall {k} {l} t m f (c :: l) a. (FoldableFC t, Applicative m) => t f c -> (forall (x :: k). () => f x -> m a) -> m ()

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

-- | Flipped <a>traverseFC</a>
forFC :: forall {k} {l} t m f (x :: l) g. (TraversableFC t, Applicative m) => t f x -> (forall (y :: k). () => f y -> m (g y)) -> m (t g x)

-- | This function may be used as a value for <tt>fmapF</tt> in a
--   <tt>FunctorF</tt> instance.
fmapFCDefault :: TraversableFC t => forall (f :: k -> Type) (g :: k -> Type). () => (forall (x :: k). () => f x -> g x) -> forall (x :: l). () => 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 :: k). () => f x -> m) -> forall (x :: l). () => t f x -> m

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

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

-- | Return number of elements that we fold over.
lengthFC :: forall {k} {l} t (f :: k -> Type) (x :: l). FoldableFC t => t f x -> Int
instance Data.Parameterized.TraversableFC.FoldableFC GHC.Internal.Data.Semigroup.Internal.Alt
instance Data.Parameterized.TraversableFC.FoldableFC GHC.Internal.Data.Monoid.Ap
instance Data.Parameterized.TraversableFC.FoldableFC Data.Parameterized.Classes.TypeAp
instance Data.Parameterized.TraversableFC.FunctorFC GHC.Internal.Data.Semigroup.Internal.Alt
instance Data.Parameterized.TraversableFC.FunctorFC GHC.Internal.Data.Monoid.Ap
instance Data.Parameterized.TraversableFC.FunctorFC Data.Parameterized.Classes.TypeAp
instance Data.Parameterized.TraversableFC.TraversableFC GHC.Internal.Data.Semigroup.Internal.Alt
instance Data.Parameterized.TraversableFC.TraversableFC GHC.Internal.Data.Monoid.Ap
instance Data.Parameterized.TraversableFC.TraversableFC Data.Parameterized.Classes.TypeAp


-- | 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 :: k -> Type -> Type)
fmapF :: FunctorF m => (forall (x :: k). () => 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 -> Type -> Type)

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

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

-- | Left-associative fold of a structure.
foldlF :: FoldableF t => (forall (s :: k). () => 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 :: k). () => e s -> b -> b) -> b -> t e -> b

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

-- | Convert structure to list.
toListF :: FoldableF t => (forall (tp :: k). () => f tp -> a) -> t f -> [a]

-- | Monadic fold over the elements of a structure from left to right.
foldlMF :: (FoldableF t, Monad m) => (forall (x :: k). () => b -> f x -> m b) -> b -> t f -> m b

-- | Monadic strict fold over the elements of a structure from left to
--   right.
foldlMF' :: (FoldableF t, Monad m) => (forall (x :: k). () => b -> f x -> m b) -> b -> t f -> m b

-- | Monadic fold over the elements of a structure from right to left.
foldrMF :: (FoldableF t, Monad m) => (forall (x :: k). () => f x -> b -> m b) -> b -> t f -> m b

-- | Monadic strict fold over the elements of a structure from right to
--   left.
foldrMF' :: (FoldableF t, Monad m) => (forall (x :: k). () => f x -> b -> m b) -> b -> t f -> m b
class (FunctorF t, FoldableF t) => TraversableF (t :: k -> Type -> Type)
traverseF :: (TraversableF t, Applicative m) => (forall (s :: k). () => 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 :: k). () => e s -> f a) -> t e -> f ()

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

-- | Flipped <a>traverseF</a>
forF :: (TraversableF t, Applicative m) => t e -> (forall (s :: k). () => e s -> m (f s)) -> m (t f)

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

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

-- | Return <a>True</a> if any values satisfy the predicate.
anyF :: FoldableF t => (forall (tp :: k). () => f tp -> Bool) -> t f -> Bool

-- | Return number of elements that we fold over.
lengthF :: forall {k} t (f :: k -> Type). FoldableF t => t f -> Int
instance Data.Parameterized.TraversableF.FoldableF (GHC.Internal.Data.Functor.Const.Const x)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Data.Parameterized.TraversableF.FoldableF f, Data.Parameterized.TraversableF.FoldableF g) => Data.Parameterized.TraversableF.FoldableF (Data.Functor.Product.Product f g)
instance Data.Parameterized.TraversableF.FoldableF GHC.Internal.Data.Proxy.Proxy
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Data.Parameterized.TraversableF.FoldableF f, Data.Parameterized.TraversableF.FoldableF g) => Data.Parameterized.TraversableF.FoldableF (Data.Functor.Sum.Sum f g)
instance forall k (s :: (k -> *) -> *) l (t :: (l -> *) -> k -> *). (Data.Parameterized.TraversableF.TraversableF s, Data.Parameterized.TraversableFC.TraversableFC t) => Data.Parameterized.TraversableF.FoldableF (Data.Functor.Compose.Compose s t)
instance Data.Parameterized.TraversableF.FunctorF (GHC.Internal.Data.Functor.Const.Const x)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Data.Parameterized.TraversableF.FunctorF f, Data.Parameterized.TraversableF.FunctorF g) => Data.Parameterized.TraversableF.FunctorF (Data.Functor.Product.Product f g)
instance Data.Parameterized.TraversableF.FunctorF GHC.Internal.Data.Proxy.Proxy
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Data.Parameterized.TraversableF.FunctorF f, Data.Parameterized.TraversableF.FunctorF g) => Data.Parameterized.TraversableF.FunctorF (Data.Functor.Sum.Sum f g)
instance forall k (s :: (k -> *) -> *) l (t :: (l -> *) -> k -> *). (Data.Parameterized.TraversableF.FunctorF s, Data.Parameterized.TraversableFC.FunctorFC t) => Data.Parameterized.TraversableF.FunctorF (Data.Functor.Compose.Compose s t)
instance Data.Parameterized.TraversableF.TraversableF (GHC.Internal.Data.Functor.Const.Const x)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Data.Parameterized.TraversableF.TraversableF f, Data.Parameterized.TraversableF.TraversableF g) => Data.Parameterized.TraversableF.TraversableF (Data.Functor.Product.Product f g)
instance Data.Parameterized.TraversableF.TraversableF GHC.Internal.Data.Proxy.Proxy
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Data.Parameterized.TraversableF.TraversableF f, Data.Parameterized.TraversableF.TraversableF g) => Data.Parameterized.TraversableF.TraversableF (Data.Functor.Sum.Sum f g)
instance forall k (s :: (k -> *) -> *) l (t :: (l -> *) -> k -> *). (Data.Parameterized.TraversableF.TraversableF s, Data.Parameterized.TraversableFC.TraversableFC t) => Data.Parameterized.TraversableF.TraversableF (Data.Functor.Compose.Compose s t)


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

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

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

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

-- | Modify the inner value.
traverseSome_ :: forall {k} m f. Functor m => (forall (tp :: k). () => f tp -> m ()) -> Some f -> m ()

-- | A lens that is polymorphic in the index may be used on a value with an
--   existentially-quantified index.
someLens :: forall {k} f a. (forall (tp :: k) (f1 :: Type -> Type). Functor f1 => (a -> f1 a) -> f tp -> f1 (f tp)) -> Lens' (Some f) a
instance forall k (f :: k -> *). GHC.Internal.Data.Type.Equality.TestEquality f => GHC.Classes.Eq (Data.Parameterized.Some.Some f)
instance Data.Parameterized.TraversableF.FoldableF Data.Parameterized.Some.Some
instance Data.Parameterized.TraversableF.FunctorF Data.Parameterized.Some.Some
instance forall k (f :: k -> *). (Data.Parameterized.Classes.HashableF f, GHC.Internal.Data.Type.Equality.TestEquality f) => Data.Hashable.Class.Hashable (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.ShowF f => GHC.Internal.Show.Show (Data.Parameterized.Some.Some f)
instance Data.Parameterized.TraversableF.TraversableF Data.Parameterized.Some.Some


-- | 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 :: forall (s :: Symbol). 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

-- | The SomeSym hides a Symbol parameter but preserves a KnownSymbol
--   constraint on the hidden parameter.
data SomeSym (c :: Symbol -> Type)
SomeSym :: c s -> SomeSym (c :: Symbol -> Type)

-- | Projects a value out of a SomeSym into a function, re-ifying the
--   Symbol type parameter to the called function, along with the
--   KnownSymbol constraint on that Symbol value.
viewSomeSym :: (forall (s :: Symbol). KnownSymbol s => c s -> r) -> SomeSym c -> r
data Symbol
class KnownSymbol (n :: Symbol)
instance Data.Parameterized.Classes.EqF Data.Parameterized.SymbolRepr.SymbolRepr
instance GHC.Classes.Eq (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.Internal.TypeLits.KnownSymbol s => Data.Parameterized.Classes.KnownRepr Data.Parameterized.SymbolRepr.SymbolRepr s
instance Data.Parameterized.Classes.OrdF Data.Parameterized.SymbolRepr.SymbolRepr
instance GHC.Classes.Ord (Data.Parameterized.SymbolRepr.SymbolRepr x)
instance Data.Parameterized.Classes.ShowF Data.Parameterized.SymbolRepr.SymbolRepr
instance GHC.Internal.Show.Show (Data.Parameterized.SymbolRepr.SymbolRepr nm)
instance GHC.Internal.Data.Type.Equality.TestEquality Data.Parameterized.SymbolRepr.SymbolRepr


-- | 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 :: Type -> Type) 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>IO</a> monad.
newIONonceGenerator :: IO (Some (NonceGenerator IO))

-- | Run an <a>IO</a> computation with a new nonce generator in the
--   <a>IO</a> monad.
withIONonceGenerator :: (forall s. () => NonceGenerator IO s -> IO r) -> IO r

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

-- | This combines <a>runST</a> and <a>newSTNonceGenerator</a> to create a
--   nonce generator that shares the same phantom type parameter as the
--   <tt>ST</tt> monad.
--   
--   This can be used to reduce the number of type parameters when we know
--   a ST computation only needs a single <a>NonceGenerator</a>.
runSTNonceGenerator :: (forall s. () => NonceGenerator (ST s) s -> ST s a) -> a

-- | 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 Data.Parameterized.Classes.EqF (Data.Parameterized.Nonce.Nonce s)
instance forall s k (tp :: k). GHC.Classes.Eq (Data.Parameterized.Nonce.Nonce s tp)
instance Data.Parameterized.Classes.HashableF (Data.Parameterized.Nonce.Nonce s)
instance forall s k (tp :: k). Data.Hashable.Class.Hashable (Data.Parameterized.Nonce.Nonce s tp)
instance Data.Parameterized.Classes.OrdF (Data.Parameterized.Nonce.Nonce s)
instance forall s k (tp :: k). GHC.Classes.Ord (Data.Parameterized.Nonce.Nonce s tp)
instance Data.Parameterized.Classes.ShowF (Data.Parameterized.Nonce.Nonce s)
instance forall s k (tp :: k). GHC.Internal.Show.Show (Data.Parameterized.Nonce.Nonce s tp)
instance GHC.Internal.Data.Type.Equality.TestEquality (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 :: Type -> Type) where {
    type NonceSet (m :: Type -> Type);
}
freshNonceM :: forall k (tp :: k). MonadNonce m => m (Nonce (NonceSet m) tp)

-- | This transformer adds a nonce generator to a given monad.
newtype NonceT s (m :: Type -> Type) a
NonceT :: ReaderT (NonceGenerator m s) m a -> NonceT s (m :: Type -> Type) a
[runNonceT] :: NonceT s (m :: Type -> Type) 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.Internal.Base.Applicative m => GHC.Internal.Base.Applicative (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance GHC.Internal.Base.Functor m => GHC.Internal.Base.Functor (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance GHC.Internal.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)
instance GHC.Internal.Base.Monad m => GHC.Internal.Base.Monad (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance Control.Monad.Trans.Class.MonadTrans (Data.Parameterized.Nonce.Transformers.NonceT s)


-- | 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 :: forall (n :: Nat). NatRepr n -> Integer

-- | This generates a NatRepr from a type-level context.
knownNat :: forall (n :: Nat). KnownNat n => NatRepr n
withKnownNat :: forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
data IsZeroNat (n :: Natural)
[ZeroNat] :: IsZeroNat 0
[NonZeroNat] :: forall (n1 :: Natural). IsZeroNat (n1 + 1)
isZeroNat :: forall (n :: Nat). NatRepr n -> IsZeroNat n

-- | Every nat is either zero or &gt;= 1.
isZeroOrGT1 :: forall (n :: Nat). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)

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

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

-- | Get the predecessor of a nat
predNat :: forall (n :: Natural). NatRepr (n + 1) -> NatRepr n

-- | Increment a <tt>NatRepr</tt>
incNat :: forall (n :: Nat). NatRepr n -> NatRepr (n + 1)
addNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatRepr (m + n)
subNat :: forall (n :: Nat) (m :: Nat). n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n)
divNat :: forall (n :: Natural) (m :: Natural). 1 <= n => NatRepr (m * n) -> NatRepr n -> NatRepr m
halfNat :: forall (n :: Natural). NatRepr (n + n) -> NatRepr n
withDivModNat :: forall (n :: Nat) (m :: Nat) a. NatRepr n -> NatRepr m -> (forall (div :: Natural) (mod :: Natural). n ~ ((div * m) + mod) => NatRepr div -> NatRepr mod -> a) -> a
natMultiply :: forall (n :: Nat) (m :: Nat). 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 :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> Some NatRepr

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

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

-- | A version of <a>natRecBounded</a> which doesn't require the type index
--   of the result to be greater than <tt>0</tt> and provides a strict
--   inequality constraint.
natRecStrictlyBounded :: forall (m :: Nat) f. NatRepr m -> f 0 -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> f n -> f (n + 1)) -> f m

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

-- | The strict order (&lt;), defined by n &lt; m &lt;-&gt; 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 asymmetric
lessThanAsymmetric :: forall (m :: Nat) f (n :: Natural). LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void

-- | Return the value of the nat representation.
widthVal :: forall (n :: Nat). NatRepr n -> Int

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

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

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

-- | Return maximum value for bitvector in two's complement with given
--   width.
maxSigned :: forall (w :: Natural). 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 :: forall (w :: Nat). 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 :: forall (w :: Natural). 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 :: forall (w :: Nat). 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 :: forall (w :: Natural). 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 :: Nat) (n :: Nat)
[LeqProof] :: forall (m :: Nat) (n :: Nat). m <= n => LeqProof m n

-- | (&lt;=) is a decidable relation on nats.
decideLeq :: forall (a :: Nat) (b :: Nat). 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 :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testStrictLeq :: forall (m :: Nat) (n :: Nat). m <= n => NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)

-- | Apply reflexivity to LeqProof
leqRefl :: forall f (n :: Nat). f n -> LeqProof n n
leqSucc :: forall f (z :: Nat). f z -> LeqProof z (z + 1)

-- | Apply transitivity to LeqProof
leqTrans :: forall (m :: Nat) (n :: Nat) (p :: Nat). LeqProof m n -> LeqProof n p -> LeqProof m p

-- | Zero is less than or equal to any <a>Nat</a>.
leqZero :: forall (n :: Nat). LeqProof 0 n

-- | Add both sides of two inequalities
leqAdd2 :: forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat). 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 :: forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat). LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)

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

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

-- | Test whether natural number is positive.
isPosNat :: forall (n :: Nat). 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 :: Nat) (n :: Nat) (p :: Natural). LeqProof m n -> f p -> LeqProof m (n + p)

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

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

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

-- | Produce evidence that <tt>+</tt> is associative.
plusAssoc :: forall f (m :: Natural) g (n :: Natural) h (o :: Natural). f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o)

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

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

-- | Used in <tt>Vector</tt>
lemmaMul :: forall (n :: Natural) p (w :: Natural) q. 1 <= n => p w -> q n -> (w + ((n - 1) * w)) :~: (n * w)
type family (a :: Natural) + (b :: Natural) :: Natural
type family (a :: Natural) - (b :: Natural) :: Natural
type family (a :: Natural) * (b :: Natural) :: Natural
type (x :: t) <= (y :: t) = Assert x <=? y LeErrMsg x y :: Constraint
class TestEquality (f :: k -> Type)
testEquality :: forall (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b)
data (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a
data Some (f :: k -> Type)


-- | <tt><a>Fin</a> n</tt> is a finite type with exactly <tt>n</tt>
--   elements. Essentially, they bundle a <a>NatRepr</a> that has an
--   existentially-quantified type parameter with a proof that its
--   parameter is less than some fixed natural.
--   
--   They are useful in combination with types of a fixed size. For example
--   <a>Fin</a> is used as the index in the <a>FunctorWithIndex</a>
--   instance for <a>Vector</a>. As another example, a <tt>Map (<a>Fin</a>
--   n) a</tt> is a <tt>Map</tt> that naturally has a fixed size bound of
--   <tt>n</tt>.
module Data.Parameterized.Fin

-- | The type <tt><a>Fin</a> n</tt> has exactly <tt>n</tt> inhabitants.
data Fin (n :: Natural)
mkFin :: forall (i :: Natural) (n :: Natural). (i + 1) <= n => NatRepr i -> Fin n
buildFin :: forall (m :: Nat). NatRepr m -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1)) -> Fin (m + 1)

-- | Count all of the numbers up to <tt>m</tt> that meet some condition.
countFin :: forall (m :: Nat). NatRepr m -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> Fin (n + 1) -> Bool) -> Fin (m + 1)
viewFin :: forall (n :: Natural) r. (forall (i :: Natural). (i + 1) <= n => NatRepr i -> r) -> Fin n -> r
finToNat :: forall (n :: Natural). Fin n -> Natural
embed :: forall (n :: Natural) (m :: Natural). n <= m => Fin n -> Fin m
tryEmbed :: forall (n :: Nat) (m :: Nat). NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m)

-- | The smallest element of <tt><a>Fin</a> n</tt>
minFin :: forall (n :: Natural). 1 <= n => Fin n
incFin :: forall (n :: Natural). Fin n -> Fin (n + 1)
fin0Void :: Iso' (Fin 0) Void
fin1Unit :: Iso' (Fin 1) ()
fin2Bool :: Iso' (Fin 2) Bool
instance (1 GHC.Internal.Data.Type.Ord.<= n, GHC.Internal.TypeNats.KnownNat n) => GHC.Internal.Enum.Bounded (Data.Parameterized.Fin.Fin n)
instance GHC.Classes.Eq (Data.Parameterized.Fin.Fin n)
instance GHC.Classes.Ord (Data.Parameterized.Fin.Fin n)
instance GHC.Internal.Show.Show (Data.Parameterized.Fin.Fin n)


-- | 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 -> Type) (val :: k -> Type)

-- | Create a new empty table.
new :: forall {k} s (key :: k -> Type) (val :: k -> Type). ST s (HashTable s key val)

-- | Create a new empty table to hold <tt>n</tt> elements.
newSized :: forall {k1} s (k2 :: k1 -> Type) (v :: k1 -> Type). Int -> ST s (HashTable s k2 v)

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

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

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

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

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

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

-- | Hash with default salt.
hashF :: forall (tp :: k). HashableF f => f tp -> Int
data RealWorld


-- | 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.TraversableFC</a>).
--   
--   Note that there is still some ambiguity around naming conventions, see
--   <a>issue 23</a>.
module Data.Parameterized.ClassesC
class TestEqualityC (t :: k -> Type -> Type)
testEqualityC :: TestEqualityC t => (forall (x :: k) (y :: k). () => f x -> f y -> Maybe (x :~: y)) -> t f -> t f -> Bool
class TestEqualityC t => OrdC (t :: k -> Type -> Type)
compareC :: OrdC t => (forall (x :: k) (y :: k). () => 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
type family (a :: Bool) && (b :: Bool) :: Bool
type family (a :: Bool) || (b :: Bool) :: Bool
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k
type family Not (a :: Bool) = (res :: Bool) | res -> a

-- | A Boolean flag
data BoolRepr (b :: Bool)
[FalseRepr] :: BoolRepr 'False
[TrueRepr] :: BoolRepr 'True

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

-- | negation
notRepr :: forall (b :: Bool). BoolRepr b -> BoolRepr (Not b)

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

-- | Disjunction
(%||) :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> BoolRepr (a || b)
infixr 2 %||
type KnownBool = KnownRepr BoolRepr
someBool :: Bool -> Some BoolRepr
class TestEquality (f :: k -> Type)
testEquality :: forall (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b)
data (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a
data Some (f :: k -> Type)
instance Data.Parameterized.DecidableEq.DecidableEq Data.Parameterized.BoolRepr.BoolRepr
instance GHC.Classes.Eq (Data.Parameterized.BoolRepr.BoolRepr m)
instance Data.Parameterized.Classes.EqF Data.Parameterized.BoolRepr.BoolRepr
instance Data.Hashable.Class.Hashable (Data.Parameterized.BoolRepr.BoolRepr n)
instance Data.Parameterized.Classes.HashableF Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.Classes.KnownRepr Data.Parameterized.BoolRepr.BoolRepr 'GHC.Types.False
instance Data.Parameterized.Classes.KnownRepr Data.Parameterized.BoolRepr.BoolRepr 'GHC.Types.True
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.Internal.Show.Show (Data.Parameterized.BoolRepr.BoolRepr m)
instance Data.Parameterized.Classes.ShowF Data.Parameterized.BoolRepr.BoolRepr
instance GHC.Internal.Data.Type.Equality.TestEquality Data.Parameterized.BoolRepr.BoolRepr


-- | 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 -> Type) (b :: k -> Type)
[Pair] :: forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type). !a tp -> !b tp -> Pair a b

-- | Extract the first element of a pair.
fstPair :: forall {k} (a :: k -> Type) (b :: k -> Type). Pair a b -> Some a

-- | Extract the second element of a pair.
sndPair :: forall {k} (a :: k -> Type) (b :: k -> Type). Pair a b -> Some b

-- | Project out of Pair.
viewPair :: (forall (tp :: k). () => a tp -> b tp -> c) -> Pair a b -> c
instance forall k (a :: k -> *) (b :: k -> *). (GHC.Internal.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.FoldableF (Data.Parameterized.Pair.Pair a)
instance forall k (a :: k -> *). Data.Parameterized.TraversableF.FunctorF (Data.Parameterized.Pair.Pair a)


-- | This module provides <a>All</a>, a GADT that encodes universal
--   quantification/parametricity over a type variable.
--   
--   The following is an example of a situation in which it might be
--   necessary to use <a>All</a> (though it is a bit contrived):
--   
--   <pre>
--   {-# LANGUAGE FlexibleInstances #-}
--   {-# LANGUAGE GADTs #-}
--   
--   data F (x :: Bool) where
--     FTrue :: F 'True
--     FFalse :: F 'False
--     FIndeterminate :: F b
--   
--   data Value =
--     VAllF (All F)
--   
--   class Valuable a where
--     valuation :: a -&gt; Value
--   
--   instance Valuable (All F) where
--     valuation = VAllF
--   
--   val1 :: Value
--   val1 = valuation (All FIndeterminate)
--   </pre>
--   
--   For a less contrived but more complex example, see this blog post:
--   <a>http://comonad.com/reader/2008/rotten-bananas/</a>
module Data.Parameterized.All
newtype All (f :: k -> Type)
All :: (forall (x :: k). () => f x) -> All (f :: k -> Type)
[getAll] :: All (f :: k -> Type) -> forall (x :: k). () => f x
allConst :: forall {k} a. a -> All (Const a :: k -> Type)
instance forall k (f :: k -> *). Data.Parameterized.Classes.EqF f => GHC.Classes.Eq (Data.Parameterized.All.All f)
instance Data.Parameterized.TraversableF.FoldableF Data.Parameterized.All.All
instance Data.Parameterized.TraversableF.FunctorF Data.Parameterized.All.All
instance forall k (f :: k -> *). Data.Parameterized.Classes.ShowF f => GHC.Internal.Show.Show (Data.Parameterized.All.All f)

module Data.Parameterized


-- | As in the package indexed-traversable.
module Data.Parameterized.TraversableFC.WithIndex
class FunctorFC t => FunctorFCWithIndex (t :: k -> Type -> l -> Type)

-- | Like <a>fmapFC</a>, but with an index.
--   
--   <pre>
--   <a>fmapFC</a> f ≡ <a>imapFC</a> (<a>const</a> f)
--   </pre>
imapFC :: forall f g (z :: l). FunctorFCWithIndex t => (forall (x :: k). () => IndexF (t f z) x -> f x -> g x) -> t f z -> t g z
class (FoldableFC t, FunctorFCWithIndex t) => FoldableFCWithIndex (t :: k -> Type -> l -> Type)

-- | Like <a>foldMapFC</a>, but with an index.
--   
--   <pre>
--   <a>foldMapFC</a> f ≡ <a>ifoldMapFC</a> (<a>const</a> f)
--   </pre>
ifoldMapFC :: forall f m (z :: l). (FoldableFCWithIndex t, Monoid m) => (forall (x :: k). () => IndexF (t f z) x -> f x -> m) -> t f z -> m

-- | Like <a>foldrFC</a>, but with an index.
ifoldrFC :: forall (z :: l) f b. FoldableFCWithIndex t => (forall (x :: k). () => IndexF (t f z) x -> f x -> b -> b) -> b -> t f z -> b

-- | Like <a>foldlFC</a>, but with an index.
ifoldlFC :: forall f b (z :: l). FoldableFCWithIndex t => (forall (x :: k). () => IndexF (t f z) x -> b -> f x -> b) -> b -> t f z -> b

-- | Like <a>ifoldrFC</a>, but with an index.
ifoldrFC' :: forall f b (z :: l). FoldableFCWithIndex t => (forall (x :: k). () => IndexF (t f z) x -> f x -> b -> b) -> b -> t f z -> b

-- | Like <a>ifoldlFC</a>, but with an index.
ifoldlFC' :: forall f b. FoldableFCWithIndex t => (forall (x :: k). () => b -> f x -> b) -> forall (x :: l). () => b -> t f x -> b

-- | Convert structure to list.
itoListFC :: forall f a (z :: l). FoldableFCWithIndex t => (forall (x :: k). () => IndexF (t f z) x -> f x -> a) -> t f z -> [a]

-- | Like <a>foldlMFC</a>, but with an index.
ifoldlMFC :: forall {k} {l} t m f (z :: l) b. (FoldableFCWithIndex t, Monad m) => (forall (x :: k). () => IndexF (t f z) x -> b -> f x -> m b) -> b -> t f z -> m b

-- | Like <a>foldrMFC</a>, but with an index.
ifoldrMFC :: forall {k} {l} t m f (z :: l) b. (FoldableFCWithIndex t, Monad m) => (forall (x :: k). () => IndexF (t f z) x -> f x -> b -> m b) -> b -> t f z -> m b

-- | Like <a>allFC</a>, but with an index.
iallFC :: forall {k} {l} t f (z :: l). FoldableFCWithIndex t => (forall (x :: k). () => IndexF (t f z) x -> f x -> Bool) -> t f z -> Bool

-- | Like <a>anyFC</a>, but with an index.
ianyFC :: forall {k} {l} t f (z :: l). FoldableFCWithIndex t => (forall (x :: k). () => IndexF (t f z) x -> f x -> Bool) -> t f z -> Bool
class (TraversableFC t, FoldableFCWithIndex t) => TraversableFCWithIndex (t :: k -> Type -> l -> Type)

-- | Like <a>traverseFC</a>, but with an index.
--   
--   <pre>
--   <a>traverseFC</a> f ≡ <a>itraverseFC</a> (<a>const</a> f)
--   </pre>
itraverseFC :: forall m (z :: l) f g. (TraversableFCWithIndex t, Applicative m) => (forall (x :: k). () => IndexF (t f z) x -> f x -> m (g x)) -> t f z -> m (t g z)
imapFCDefault :: forall {k} {l} t f g (z :: l). TraversableFCWithIndex t => (forall (x :: k). () => IndexF (t f z) x -> f x -> g x) -> t f z -> t g z
ifoldMapFCDefault :: forall {k} {l} t m (z :: l) f. (TraversableFCWithIndex t, Monoid m) => (forall (x :: k). () => IndexF (t f z) x -> f x -> m) -> t f z -> m


-- | 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 <a>Assignment</a> type in
--   <a>Data.Parameterized.Context</a>.
--   
--   <h1>Motivating example - the <a>List</a> type</h1>
--   
--   For this example, we need the following extensions:
--   
--   <pre>
--   {-# LANGUAGE DataKinds #-}
--   {-# LANGUAGE GADTs #-}
--   {-# LANGUAGE KindSignatures #-}
--   {-# LANGUAGE TypeOperators #-}
--   </pre>
--   
--   We also require the following imports:
--   
--   <pre>
--   import Data.Parameterized
--   import Data.Parameterized.List
--   import GHC.TypeLits
--   </pre>
--   
--   Suppose we have a bitvector type:
--   
--   <pre>
--   data BitVector (w :: Nat) :: * where
--     BV :: NatRepr w -&gt; Integer -&gt; BitVector w
--   </pre>
--   
--   This type contains a <a>NatRepr</a>, a value-level representative of
--   the vector width, and an <a>Integer</a>, containing the actual value
--   of the bitvector. We can create values of this type as follows:
--   
--   <pre>
--   BV (knownNat @8) 0xAB
--   </pre>
--   
--   We can also create a smart constructor to handle the <a>NatRepr</a>
--   automatically, when the width is known from the type context:
--   
--   <pre>
--   bitVector :: KnownNat w =&gt; Integer -&gt; BitVector w
--   bitVector x = BV knownNat x
--   </pre>
--   
--   Note that this does not check that the value can be represented in the
--   given number of bits; that is not important for this example.
--   
--   If we wish to construct a list of <tt>BitVector</tt>s of a particular
--   length, we can do:
--   
--   <pre>
--   [bitVector 0xAB, bitVector 0xFF, bitVector 0] :: BitVector 8
--   </pre>
--   
--   However, what if we wish to construct a list of <tt>BitVector</tt>s of
--   different lengths? We could try:
--   
--   <pre>
--   [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
--   </pre>
--   
--   However, this gives us an error:
--   
--   <pre>
--   &lt;interactive&gt;:3:33: error:
--       • Couldn't match type ‘16’ with ‘8’
--         Expected type: BitVector 8
--           Actual type: BitVector 16
--       • In the expression: bitVector 0x1234 :: BitVector 16
--         In the expression:
--           [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
--         In an equation for ‘it’:
--             it
--               = [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
--   </pre>
--   
--   A vanilla Haskell list cannot contain two elements of different types,
--   and even though the two elements here are both <tt>BitVector</tt>s,
--   they do not have the same type! One solution is to use the <a>Some</a>
--   type:
--   
--   <pre>
--   [Some (bitVector 0xAB :: BitVector 8), Some (bitVector 0x1234 :: BitVector 16)]
--   </pre>
--   
--   The type of the above expression is <tt>[Some BitVector]</tt>, which
--   may be perfectly acceptable. However, there is nothing in this type
--   that tells us what the widths of the bitvectors are, or what the
--   length of the overall list is. If we want to actually track that
--   information on the type level, we can use the <a>List</a> type from
--   this module.
--   
--   <pre>
--   (bitVector 0xAB :: BitVector 8) :&lt; (bitVector 0x1234 :: BitVector 16) :&lt; Nil
--   </pre>
--   
--   The type of the above expression is <tt>List BitVector '[8, 16]</tt>
--   -- That is, a two-element list of <tt>BitVector</tt>s, where the first
--   element has width 8 and the second has width 16.
--   
--   <h2>Summary</h2>
--   
--   In general, if we have a type constructor <tt>Foo</tt> of kind <tt>k
--   -&gt; *</tt> (in our example, <tt>Foo</tt> is just <tt>BitVector</tt>,
--   and we want to create a list of <tt>Foo</tt>s where the parameter
--   <tt>k</tt> varies, <i>and</i> we wish to keep track of what each value
--   of <tt>k</tt> is inside the list at compile time, we can use the
--   <a>List</a> type for this purpose.
module Data.Parameterized.List

-- | Parameterized list of elements.
data List (a :: k -> Type) (b :: [k])
[Nil] :: forall {k} (a :: k -> Type). List a ('[] :: [k])
[:<] :: forall {k} (a :: k -> Type) (tp :: k) (tps :: [k]). a tp -> List a tps -> List a (tp ': tps)
infixr 5 :<

-- | Map from list of Some to Some list
fromSomeList :: forall {k} (f :: k -> Type). [Some f] -> Some (List f)

-- | Apply function to list to yield a parameterized list.
fromListWith :: forall {k} a (f :: k -> Type). (a -> Some f) -> [a] -> Some (List f)

-- | Apply monadic action to list to yield a parameterized list.
fromListWithM :: forall {k} a (f :: k -> Type) m. Monad m => (a -> m (Some f)) -> [a] -> m (Some (List f))

-- | 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 (a :: [k]) (b :: k)
[IndexHere] :: forall {k} (b :: k) (r :: [k]). Index (b ': r) b
[IndexThere] :: forall {k} (r :: [k]) (b :: k) (x :: k). !Index r b -> Index (x ': r) b

-- | Return the index as an integer.
indexValue :: forall {k} (l :: [k]) (tp :: k). Index l tp -> Integer

-- | Return the value in a list at a given index
(!!) :: forall {k} f (l :: [k]) (x :: k). List f l -> Index l x -> f x

-- | Update the <a>List</a> at an index
update :: forall {k} f (l :: [k]) (s :: k). 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 :: forall {k} (l :: [k]) (x :: k) (f :: k -> Type). Index l x -> 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.
--   
--   This is a specialization of <a>imapFC</a>.
imap :: forall {k} f g (l :: [k]). (forall (x :: k). () => Index l x -> f x -> g x) -> List f l -> List g l

-- | Left fold with an additional index.
ifoldlM :: forall {k} (sh :: [k]) a b m. Monad m => (forall (tp :: k). () => b -> Index sh tp -> a tp -> m b) -> b -> List a sh -> m b

-- | Right-fold with an additional index.
--   
--   This is a specialization of <a>ifoldrFC</a>.
ifoldr :: forall {k} (sh :: [k]) a b. (forall (tp :: k). () => 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 {k} a b c (sh :: [k]). (forall (tp :: k). () => Index sh tp -> a tp -> b tp -> c tp) -> List a sh -> List b sh -> List c sh

-- | Traverse with an additional index.
--   
--   This is a specialization of <a>itraverseFC</a>.
itraverse :: forall {k} a b (sh :: [k]) t. Applicative t => (forall (tp :: k). () => Index sh tp -> a tp -> t (b tp)) -> List a sh -> t (List b sh)

-- | Index 0
index0 :: forall {k} (x :: k) (r :: [k]). Index (x ': r) x

-- | Index 1
index1 :: forall {k} (x0 :: k) (x1 :: k) (r :: [k]). Index (x0 ': (x1 ': r)) x1

-- | Index 2
index2 :: forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (r :: [k]). Index (x0 ': (x1 ': (x2 ': r))) x2

-- | Index 3
index3 :: forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (x3 :: k) (r :: [k]). Index (x0 ': (x1 ': (x2 ': (x3 ': r)))) x3
instance forall k (f :: k -> *). Data.Parameterized.Classes.EqF f => Data.Parameterized.Classes.EqF (Data.Parameterized.List.List f)
instance forall k (l :: [k]) (x :: k). GHC.Classes.Eq (Data.Parameterized.List.Index l x)
instance Data.Parameterized.TraversableFC.WithIndex.FoldableFCWithIndex Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.FoldableFC Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.WithIndex.FunctorFCWithIndex Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.FunctorFC Data.Parameterized.List.List
instance forall k (l :: [k]) (x :: k). Data.Hashable.Class.Hashable (Data.Parameterized.List.Index l x)
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)
instance forall k (f :: k -> *). Data.Parameterized.Classes.KnownRepr (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 (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 -> *). Data.Parameterized.Classes.ShowF f => Data.Parameterized.Classes.ShowF (Data.Parameterized.List.List f)
instance forall k (l :: [k]). Data.Parameterized.Classes.ShowF (Data.Parameterized.List.Index l)
instance forall k (l :: [k]) (x :: k). GHC.Internal.Show.Show (Data.Parameterized.List.Index l x)
instance forall k (f :: k -> *) (sh :: [k]). Data.Parameterized.Classes.ShowF f => GHC.Internal.Show.Show (Data.Parameterized.List.List f sh)
instance forall k (f :: k -> *). GHC.Internal.Data.Type.Equality.TestEquality f => GHC.Internal.Data.Type.Equality.TestEquality (Data.Parameterized.List.List f)
instance forall k (l :: [k]). GHC.Internal.Data.Type.Equality.TestEquality (Data.Parameterized.List.Index l)
instance Data.Parameterized.TraversableFC.WithIndex.TraversableFCWithIndex Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.TraversableFC Data.Parameterized.List.List


-- | 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.
--   
--   The <a>Assignment</a> type is isomorphic to the <a>List</a> type,
--   except <a>Assignment</a>s construct lists from the right-hand side,
--   and instead of using type-level <tt>'[]</tt>-style lists, an
--   <a>Assignment</a> is indexed by a type-level <a>Ctx</a>. The
--   implementation of <a>Assignment</a>s is also more efficent than
--   <a>List</a> for lists of many elements, as it uses a balanced binary
--   tree representation rather than a linear-time list. For a motivating
--   example, see <a>List</a>.
module Data.Parameterized.Context

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

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

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

-- | Convert a context size to an <a>Int</a>.
sizeInt :: forall {k} (ctx :: Ctx k). Size ctx -> Int

-- | The size of an empty context.
zeroSize :: Size ('EmptyCtx :: Ctx k)

-- | Increment the size to the next value.
incSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
decSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx

-- | Extend the size by a given difference.
extSize :: forall {k} (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r

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

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

-- | Project a size
viewSize :: forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx

-- | Convert a <a>Size</a> into a <a>NatRepr</a>.
sizeToNatRepr :: forall {k} (items :: Ctx k). Size items -> NatRepr (CtxSize items)

-- | 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. Identity element of <tt>Category</tt>
--   instance.
noDiff :: forall {k} (l :: Ctx k). Diff l l

-- | The addition of differences. Flipped binary operation of
--   <tt>Category</tt> instance.
addDiff :: forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k). Diff a b -> Diff b c -> Diff a c

-- | Extend the difference to a sub-context of the right side.
extendRight :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Diff l r -> Diff l (r '::> tp)
appendDiff :: forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
data DiffView (a :: Ctx k) (b :: Ctx k)
[NoDiff] :: forall {k} (a :: Ctx k). DiffView a a
[ExtendRightDiff] :: forall {k} (a :: Ctx k) (b1 :: Ctx k) (r :: k). Diff a b1 -> DiffView a (b1 '::> r)
viewDiff :: forall {k} (a :: Ctx k) (b :: Ctx k). Diff a b -> DiffView a b

-- | 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 :: Ctx k) (r :: Ctx k)
[IsAppend] :: forall {k} (app :: Ctx k) (l :: Ctx k). 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 :: forall {k} (l :: Ctx k) (r :: Ctx k). Diff l r -> IsAppend l r

-- | Index for first element in context.
baseIndex :: forall {k} (tp :: k). Index (('EmptyCtx :: Ctx k) '::> tp) tp

-- | Increase context while staying at same index.
skipIndex :: forall {k} (ctx :: Ctx k) (x :: k) (y :: k). Index ctx x -> Index (ctx '::> y) x

-- | Return the last index of a element.
lastIndex :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx ::> tp) -> Index (ctx ::> tp) tp

-- | Return the index of a element one past the size.
nextIndex :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Index (ctx ::> tp) tp

-- | Adapts an index in the left hand context of an append operation.
leftIndex :: forall {k} (r :: Ctx k) (l :: Ctx k) (tp :: k). Size r -> Index l tp -> Index (l <+> r) tp

-- | Adapts an index in the right hand context of an append operation.
rightIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). KnownDiff l r => Index l tp -> Index r tp

-- | Compute an <a>Index</a> into a context <tt>r</tt> from an <a>Index</a>
--   into a sub-context <tt>l</tt> of <tt>r</tt>.
extendIndex' :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Diff l r -> Index l tp -> Index r tp

-- | Compute an <a>Index</a> into an appended context from an <a>Index</a>
--   into its suffix.
extendIndexAppendLeft :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k). Size l -> Size r -> Index r tp -> Index (l <+> r) tp

-- | Given a size <tt>n</tt>, a function <tt>f</tt>, and an initial value
--   <tt>v0</tt>, the expression <tt>forIndex n f v0</tt> is equivalent to
--   <tt>v0</tt> when <tt>n</tt> is zero, and <tt>f (forIndex (n-1) f v0)
--   n</tt> otherwise. Unlike the safe version, which starts from
--   <a>Index</a> <tt>0</tt> and increments <a>Index</a> values, this
--   version starts at <a>Index</a> <tt>(n-1)</tt> and decrements
--   <a>Index</a> values to <a>Index</a> <tt>0</tt>.
forIndex :: forall {k} (ctx :: Ctx k) r. Size ctx -> (forall (tp :: k). () => r -> Index ctx tp -> r) -> r -> r

-- | Given an index <tt>i</tt>, size <tt>n</tt>, a function <tt>f</tt>, and
--   a value <tt>v</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 f v)</tt> otherwise.
forIndexRange :: forall {k} (ctx :: Ctx k) r. Int -> Size ctx -> (forall (tp :: k). () => Index ctx tp -> r -> r) -> r -> r

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

-- | View of indexes as pointing to the last element in the index range or
--   pointing to an earlier element in a smaller range.
data IndexView (ctx :: Ctx k) (tp :: k)
[IndexViewLast] :: forall {k} (ctx1 :: Ctx k) (tp :: k). !Size ctx1 -> IndexView (ctx1 '::> tp) tp
[IndexViewInit] :: forall {k} (ctx1 :: Ctx k) (tp :: k) (u :: k). !Index ctx1 tp -> IndexView (ctx1 '::> u) tp

-- | Project an index
viewIndex :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Index ctx tp -> IndexView ctx tp

-- | 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 :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> Size ctx

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

-- | Generate an assignment
generate :: forall {k} (ctx :: Ctx k) f. Size ctx -> (forall (tp :: k). () => Index ctx tp -> f tp) -> Assignment f ctx

-- | Generate an assignment in an <a>Applicative</a> context
generateM :: forall {k} m (ctx :: Ctx k) f. Applicative m => Size ctx -> (forall (tp :: k). () => Index ctx tp -> m (f tp)) -> m (Assignment f ctx)

-- | Return empty assignment
empty :: forall {k} (f :: k -> Type). Assignment f (EmptyCtx :: Ctx k)

-- | Extend an indexed vector with a new entry.
extend :: forall {k} f (ctx :: Ctx k) (x :: k). 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 :: forall {k} f (tp :: k) (ctx :: Ctx k). (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 {k} (ctx :: Ctx k) (tp :: k) f. Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx

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

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

-- | View an assignment as either empty or an assignment with one appended.
viewAssign :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> AssignView f ctx

-- | Return value of assignment.
(!) :: forall {k} f (ctx :: Ctx k) (tp :: k). Assignment f ctx -> Index ctx tp -> f tp

-- | Return value of assignment, where the index is into an initial
--   sequence of the assignment.
(!^) :: forall {k} (l :: Ctx k) (r :: Ctx k) f (tp :: k). KnownDiff l r => Assignment f r -> Index l tp -> f tp
zipWith :: forall {k} f g h (a :: Ctx k). (forall (x :: k). () => f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a
zipWithM :: forall {k} m f g h (a :: Ctx k). Applicative m => (forall (x :: k). () => f x -> g x -> m (h x)) -> Assignment f a -> Assignment g a -> m (Assignment h a)
(<++>) :: forall {k} (f :: k -> Type) (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Assignment f (x <+> y)
traverseWithIndex :: forall {k} m (ctx :: Ctx k) f g. Applicative m => (forall (tp :: k). () => Index ctx tp -> f tp -> m (g tp)) -> Assignment f ctx -> m (Assignment g ctx)

-- | 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 :: forall {k} (ctx :: Ctx k). Size ctx -> IndexRange ctx ctx

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

-- | <tt>dropHeadRange r n</tt> drops the first <tt>n</tt> elements in
--   <tt>r</tt>.
dropHeadRange :: forall {k} (ctx :: Ctx k) (x :: Ctx k) (y :: Ctx k). 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 :: forall {k} (ctx :: Ctx k) (x :: Ctx k) (y :: Ctx k). IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x
type EmptyCtx = 'EmptyCtx :: Ctx k
type SingleCtx (x :: k) = EmptyCtx :: Ctx k ::> x
type (c :: Ctx k) ::> (a :: k) = c '::> a

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

-- | Flatten a nested context
type family CtxFlatten (ctx :: Ctx Ctx a) :: Ctx a

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

-- | 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 :: Ctx k) (n :: Natural) = CtxSize ctx - 1 - n

-- | Create a single element context.
singleton :: forall {k} f (tp :: k). f tp -> Assignment f ((EmptyCtx :: Ctx k) ::> tp)

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

-- | Pattern synonym for extending an assignment on the right
pattern (:>) :: forall {k} ctx' f ctx (tp :: k). () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'
infixl 9 :>

-- | Pattern synonym for the empty assignment
pattern Empty :: forall {k} ctx f. () => ctx ~ (EmptyCtx :: Ctx k) => Assignment f ctx
decompose :: forall {k} f (ctx :: Ctx k) (tp :: k). Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)

-- | Return true if assignment is empty.
null :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> Bool

-- | Return assignment with all but the last block.
init :: forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k). Assignment f (ctx '::> tp) -> Assignment f ctx

-- | Return the last element in the assignment.
last :: forall {k} f (ctx :: Ctx k) (tp :: k). 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 {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> AssignView f ctx

-- | Return the prefix of an appended <a>Assignment</a>
take :: forall {k} (f :: k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx

-- | Return the suffix of an appended <a>Assignment</a>
drop :: forall {k} (f :: k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k). 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 {k} (ctx :: Ctx k) m. Applicative m => Size ctx -> (forall (tp :: k). () => Index ctx tp -> m ()) -> m ()

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

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

-- | Create an assignment from a list of values.
fromList :: forall {k} (f :: k -> Type). [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 :: forall {k} w m (ctx :: Ctx k) f. (Monoid w, Applicative m) => (forall (tp :: k). () => Index ctx tp -> f tp -> m w) -> Assignment f ctx -> m w

-- | Visit each of the elements in an <tt>Assignment</tt> in order from
--   left to right, executing an action with each.
traverseWithIndex_ :: forall {k} m (ctx :: Ctx k) f. Applicative m => (forall (tp :: k). () => Index ctx tp -> f tp -> m ()) -> Assignment f ctx -> m ()

-- | Utility function for testing if <tt>xs</tt> is an assignment with
--   <tt>prefix</tt> as a prefix, and computing the tail of xs not in the
--   prefix, if so.
dropPrefix :: forall {k} (f :: k -> Type) (xs :: Ctx k) (prefix :: Ctx k) a. TestEquality f => Assignment f xs -> Assignment f prefix -> a -> (forall (addl :: Ctx k). xs ~ (prefix <+> addl) => Assignment f addl -> a) -> a

-- | Unzip an assignment of pairs into a pair of assignments.
--   
--   This is the inverse of <tt><a>zipWith</a> <a>Pair</a></tt>.
unzip :: forall {k} (f :: k -> Type) (g :: k -> Type) (ctx :: Ctx k). Assignment (Product f g) ctx -> (Assignment f ctx, Assignment g ctx)

-- | Flattens a nested assignment over a context of contexts <tt>ctxs ::
--   Ctx (Ctx a)</tt> into a flat assignment over the flattened context
--   <tt>CtxFlatten ctxs</tt>.
flattenAssignment :: forall {a} (f :: a -> Type) (ctxs :: Ctx (Ctx a)). Assignment (Assignment f) ctxs -> Assignment f (CtxFlatten ctxs)

-- | Given the size of each context in <tt>ctxs</tt>, returns the size of
--   <tt>CtxFlatten ctxs</tt>. You can obtain the former from any nested
--   assignment <tt>Assignment (Assignment f) ctxs</tt>, by calling
--   <tt>fmapFC size</tt>.
flattenSize :: forall {k} (ctxs :: Ctx (Ctx k)). Assignment (Size :: Ctx k -> Type) ctxs -> Size (CtxFlatten ctxs)

-- | 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 (ctx :: Ctx k) (ctx' :: Ctx k)
[_ctxeSize] :: CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k) -> Size ctx'
[_ctxeAssignment] :: CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k) -> Assignment (Index ctx') ctx
class ExtendContext (f :: Ctx k -> Type)
extendContext :: forall (ctx :: Ctx k) (ctx' :: Ctx k). ExtendContext f => Diff ctx ctx' -> f ctx -> f ctx'
class ExtendContext' (f :: Ctx k -> k' -> Type)
extendContext' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). ExtendContext' f => Diff ctx ctx' -> f ctx v -> f ctx' v
class ApplyEmbedding (f :: Ctx k -> Type)
applyEmbedding :: forall (ctx :: Ctx k) (ctx' :: Ctx k). ApplyEmbedding f => CtxEmbedding ctx ctx' -> f ctx -> f ctx'
class ApplyEmbedding' (f :: Ctx k -> k' -> Type)
applyEmbedding' :: forall (ctx :: Ctx k) (ctx' :: Ctx k) (v :: k'). ApplyEmbedding' f => CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
identityEmbedding :: forall {k} (ctx :: Ctx k). Size ctx -> CtxEmbedding ctx ctx
extendEmbeddingRightDiff :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (ctx'' :: Ctx k). Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
extendEmbeddingRight :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k). CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
extendEmbeddingBoth :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k). CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)

-- | Prove that the prefix of an appended context is embeddable in it
appendEmbedding :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')

-- | Prove that the suffix of an appended context is embeddable in it
appendEmbeddingLeft :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k). Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')
ctxeSize :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) f. Functor f => (Size ctx' -> f (Size ctx')) -> CtxEmbedding ctx ctx' -> f (CtxEmbedding ctx ctx')
ctxeAssignment :: forall {k} (ctx1 :: Ctx k) (ctx' :: Ctx k) (ctx2 :: Ctx k) f. Functor f => (Assignment (Index ctx') ctx1 -> f (Assignment (Index ctx') ctx2)) -> CtxEmbedding ctx1 ctx' -> f (CtxEmbedding ctx2 ctx')

-- | 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 :: Nat) (ctx :: Ctx k) (r :: k) = (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 {k} (n :: Nat) (ctx :: Ctx k) (f :: k -> Type) (r :: k). 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 {k} (n :: Nat) (ctx :: Ctx k) (r :: k). 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 {k} (n :: Nat) (ctx :: Ctx k) (r :: k) 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 -> Type) 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 :: forall (f :: k -> Type) x. CurryAssignmentClass ctx => (Assignment f ctx -> x) -> CurryAssignment ctx f x

-- | Transform a curried function into one that accepts an assignment
--   value.
uncurryAssignment :: forall (f :: k -> Type) x. CurryAssignmentClass ctx => CurryAssignment ctx f x -> Assignment f ctx -> x
size1 :: forall {k} (a :: k). Size ((EmptyCtx :: Ctx k) ::> a)
size2 :: forall {k} (a :: k) (b :: k). Size (((EmptyCtx :: Ctx k) ::> a) ::> b)
size3 :: forall {k} (a :: k) (b :: k) (c :: k). Size ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c)
size4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Size (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d)
size5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Size ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e)
size6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Size (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f)
i1of2 :: forall {k} (a :: k) (b :: k). Index (((EmptyCtx :: Ctx k) ::> a) ::> b) a
i2of2 :: forall {k} (a :: k) (b :: k). Index (((EmptyCtx :: Ctx k) ::> a) ::> b) b
i1of3 :: forall {k} (a :: k) (b :: k) (c :: k). Index ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) a
i2of3 :: forall {k} (a :: k) (b :: k) (c :: k). Index ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) b
i3of3 :: forall {k} (a :: k) (b :: k) (c :: k). Index ((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) c
i1of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) a
i2of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) b
i3of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) c
i4of4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k). Index (((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) d
i1of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) a
i2of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) b
i3of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) c
i4of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) d
i5of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Index ((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) e
i1of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a
i2of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b
i3of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c
i4of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d
i5of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e
i6of6 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). Index (((((((EmptyCtx :: Ctx k) ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f
instance (GHC.Internal.Base.Applicative m, GHC.Internal.Base.Monoid w) => GHC.Internal.Base.Applicative (Data.Parameterized.Context.Collector m w)
instance Data.Parameterized.Context.ApplyEmbedding' Data.Parameterized.Context.Unsafe.Index
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 Data.Parameterized.Context.CurryAssignmentClass Data.Parameterized.Ctx.EmptyCtx
instance Data.Parameterized.Context.ExtendContext' Data.Parameterized.Context.Unsafe.Index
instance forall k (m :: k -> *) (w :: k). GHC.Internal.Base.Functor (Data.Parameterized.Context.Collector m w)
instance forall k (xs :: Data.Parameterized.Ctx.Ctx k) (n :: GHC.Num.Natural.Natural) (r :: k) (x :: k). (Data.Parameterized.Context.Unsafe.KnownContext xs, Data.Parameterized.Context.Idx' (n GHC.Internal.TypeNats.- 1) xs r) => Data.Parameterized.Context.Idx' n (xs 'Data.Parameterized.Ctx.::> x) r
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


-- | 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 :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)

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

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

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

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

-- | Zero
zeroP :: PeanoRepr Z

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

-- | Get the predecessor (decrement)
predP :: forall (n :: Peano). 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 :: forall {k} (m :: Peano) repr (f :: k -> k) (s :: k). PeanoRepr m -> (forall (a :: k). () => repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)

-- | Calculate the size of a context
ctxSizeP :: forall {k} (f :: k -> Type) (ctx :: Ctx k). 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 :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)

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

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

-- | Greater-than-or-equal-to
geP :: forall (a :: Peano) (b :: Peano). 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] :: forall (n1 :: Peano). PeanoRepr n1 -> PeanoView ('S n1)

-- | Test whether a number is Zero or Successor
peanoView :: forall (n :: Peano). PeanoRepr n -> PeanoView n

-- | convert the view back to the runtime representation
viewRepr :: forall (n :: Peano). 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 :: forall (m :: Peano) (n :: Peano). PeanoRepr m -> PeanoRepr n -> Some PeanoRepr

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

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

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

-- | Minus distributes over plus
minusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano). 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 :: Peano) (t :: Peano) (t' :: Peano). Lt t (Minus n t') ~ 'True => PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Lt (Plus t' t) n :~: 'True
class TestEquality (f :: k -> Type)
testEquality :: forall (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b)
data (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a
data Some (f :: k -> Type)
instance Data.Parameterized.DecidableEq.DecidableEq Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.Classes.EqF Data.Parameterized.Peano.PeanoRepr
instance GHC.Classes.Eq (Data.Parameterized.Peano.PeanoRepr m)
instance Data.Parameterized.Classes.HashableF Data.Parameterized.Peano.PeanoRepr
instance Data.Hashable.Class.Hashable (Data.Parameterized.Peano.PeanoRepr n)
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.Parameterized.Classes.KnownRepr Data.Parameterized.Peano.PeanoRepr Data.Parameterized.Peano.Z
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 Data.Parameterized.Classes.ShowF Data.Parameterized.Peano.PeanoRepr
instance GHC.Internal.Show.Show (Data.Parameterized.Peano.PeanoRepr p)
instance GHC.Internal.Data.Type.Equality.TestEquality Data.Parameterized.Peano.PeanoRepr


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.Internal.Base.Alternative Data.Parameterized.Utils.BinTree.MaybeS
instance GHC.Internal.Base.Applicative Data.Parameterized.Utils.BinTree.MaybeS
instance GHC.Internal.Base.Functor 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 :: forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a

-- | Return map containing a single element
singleton :: forall {v} k (tp :: v) a. k tp -> a tp -> MapF k a

-- | Insert a binding into the map, replacing the existing binding if
--   needed.
insert :: forall {v} k (tp :: v) a. 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 :: forall {v} k a (tp :: v). 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 :: forall {v} k (tp :: v) (a :: v -> Type). OrdF k => k tp -> MapF k a -> MapF k a

-- | Left-biased union of two maps. The resulting map will contain the
--   union of the keys of the two arguments. When a key is contained in
--   both maps the value from the first map will be preserved.
union :: forall {v} (k :: v -> Type) (a :: v -> Type). OrdF k => MapF k a -> MapF k a -> MapF k a

-- | Applies a function to the pairwise common elements of two maps.
--   
--   Formally, we have that <tt>intersectWithKeyMaybe f x y</tt> contains a
--   binding from a key <tt>k</tt> to a value <tt>v</tt> if and only if
--   <tt>x</tt> and <tt>y</tt> bind <tt>k</tt> to <tt>x_k</tt> and
--   <tt>y_k</tt> and <tt>f x_k y_k = Just v</tt>.
intersectWithKeyMaybe :: OrdF k => (forall (tp :: v). () => k tp -> a tp -> b tp -> Maybe (c tp)) -> MapF k a -> MapF k b -> MapF k c

-- | Return true if map is empty
null :: forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a -> Bool

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

-- | <tt>findWithDefault d k m</tt> returns the value bound to <tt>k</tt>
--   in the map <tt>m</tt>, or <tt>d</tt> if <tt>k</tt> is not bound in the
--   map.
findWithDefault :: forall {v} k a (tp :: v). OrdF k => a tp -> k tp -> MapF k a -> a tp

-- | Return true if key is bound in map.
member :: forall {v} k (tp :: v) (a :: v -> Type). OrdF k => k tp -> MapF k a -> Bool

-- | Return true if key is not bound in map.
notMember :: forall {v} k (tp :: v) (a :: v -> Type). OrdF k => k tp -> MapF k a -> Bool
size :: IsBinTree t e => t -> Int

-- | Return all keys of the map in ascending order.
keys :: forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type). MapF k2 a -> [Some k2]

-- | Return all elements of the map in the ascending order of their keys.
elems :: forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type). MapF k2 a -> [Some a]

-- | Create a Map from a list of pairs.
fromList :: forall {v} (k :: v -> Type) (a :: v -> Type). OrdF k => [Pair k a] -> MapF k a

-- | Return list of key-values pairs in map.
toList :: forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type). MapF k2 a -> [Pair k2 a]

-- | Return list of key-values pairs in map in ascending order.
toAscList :: forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type). MapF k2 a -> [Pair k2 a]

-- | Return list of key-values pairs in map in descending order.
toDescList :: forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type). MapF k2 a -> [Pair k2 a]

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

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

-- | Return key-value pairs that satisfy a predicate.
filterWithKey :: (forall (tp :: v). () => 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 :: forall {v1} k (tp :: v1) (v2 :: v1 -> Type). OrdF k => k tp -> MapF k v2 -> MapF k v2

-- | <tt>filterLt k m</tt> returns submap of <tt>m</tt> that only contains
--   entries that are smaller than <tt>k</tt>.
filterLt :: forall {v1} k (tp :: v1) (v2 :: v1 -> Type). OrdF k => k tp -> MapF k v2 -> MapF k v2

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

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

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

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

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

-- | A monadic left-to-right fold over keys and values in the map.
foldlMWithKey :: forall {v} m b k a. Monad m => (forall (s :: v). () => b -> k s -> a s -> m b) -> b -> MapF k a -> m b

-- | A monadic right-to-left fold over keys and values in the map.
foldrMWithKey :: forall {v} m k a b. Monad m => (forall (s :: v). () => k s -> a s -> b -> m b) -> b -> MapF k a -> m b

-- | Modify elements in a map
map :: forall {v} f g (ktp :: v -> Type). (forall (tp :: v). () => f tp -> g tp) -> MapF ktp f -> MapF ktp g

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

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

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

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

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

-- | Traverse keys/values and collect the <a>Just</a> results.
traverseMaybeWithKey :: forall {v} f k a b. Applicative f => (forall (tp :: v). () => k tp -> a tp -> f (Maybe (b tp))) -> MapF k a -> f (MapF k b)

-- | <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 :: forall {v} k f (tp :: v) a. (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.
--   
--   The first function is used to merge elements that occur under the same
--   key in both maps. Return Just to add an entry into the resulting map
--   under this key or Nothing to remove this key from the resulting map.
--   
--   The second function will be applied to submaps of the first map
--   argument where no keys overlap with the second map argument. The
--   result of this function must be a map with a subset of the keys of its
--   argument. This means the function can alter the values of its argument
--   and it can remove key-value pairs from it, but it can break
--   <a>MapF</a> ordering invariants if it introduces new keys.
--   
--   Third function is analogous to the second function except that it
--   applies to the second map argument of <a>mergeWithKeyM</a> instead of
--   the first.
--   
--   Common examples of the two functions include <a>id</a> when
--   constructing a union or <a>const</a> <a>empty</a> when constructing an
--   intersection.
mergeWithKey :: OrdF k => (forall (tp :: v). () => k tp -> a tp -> b tp -> Maybe (c tp)) -> (MapF k a -> MapF k c) -> (MapF k b -> MapF k c) -> MapF k a -> MapF k b -> MapF k c

-- | Merge bindings in two maps using monadic actions to get a third.
--   
--   The first function is used to merge elements that occur under the same
--   key in both maps. Return Just to add an entry into the resulting map
--   under this key or Nothing to remove this key from the resulting map.
--   
--   The second function will be applied to submaps of the first map
--   argument where no keys overlap with the second map argument. The
--   result of this function must be a map with a subset of the keys of its
--   argument. This means the function can alter the values of its argument
--   and it can remove key-value pairs from it, but it can break
--   <a>MapF</a> ordering invariants if it introduces new keys.
--   
--   Third function is analogous to the second function except that it
--   applies to the second map argument of <a>mergeWithKeyM</a> instead of
--   the first.
--   
--   Common examples of the two functions include <a>id</a> when
--   constructing a union or <a>const</a> <a>empty</a> when constructing an
--   intersection.
mergeWithKeyM :: forall {v} k a b c m. (Applicative m, OrdF k) => (forall (tp :: v). () => 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 -> Type) (b :: k -> Type)
[Pair] :: forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type). !a tp -> !b tp -> Pair a b
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 v (k :: v -> *) (a :: v -> *). (GHC.Internal.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.FoldableF (Data.Parameterized.Map.MapF ktp)
instance forall k (ktp :: k -> *). Data.Parameterized.TraversableF.FunctorF (Data.Parameterized.Map.MapF ktp)
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 a (k :: a -> *) (v :: a -> *). Data.Parameterized.Classes.OrdF k => Data.Parameterized.Classes.IxedF a (Data.Parameterized.Map.MapF k v)
instance forall v (ktp :: v -> *) (rtp :: v -> *). (Data.Parameterized.Classes.ShowF ktp, Data.Parameterized.Classes.ShowF rtp) => GHC.Internal.Show.Show (Data.Parameterized.Map.MapF ktp rtp)
instance forall k (ktp :: k -> *). Data.Parameterized.TraversableF.TraversableF (Data.Parameterized.Map.MapF ktp)


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.Eq Data.Parameterized.Utils.Endian.Endian
instance GHC.Classes.Ord Data.Parameterized.Utils.Endian.Endian
instance GHC.Internal.Show.Show 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 :: Natural) 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 :: forall (n :: Natural) a. 1 <= n => NatRepr n -> [a] -> Maybe (Vector n a)

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

-- | Convert a non-empty <a>Assignment</a> to a fixed-size <a>Vector</a>.
--   
--   This function uses the same ordering convention as <a>toVector</a>.
fromAssignment :: forall {k} f (ctx :: Ctx k) (tp :: k) e. (forall (tp' :: k). () => f tp' -> e) -> Assignment f (ctx ::> tp) -> Vector (CtxSize (ctx ::> tp)) e

-- | Convert a <a>Vector</a> into a <a>Assignment</a>.
--   
--   This function uses the same ordering convention as <a>toVector</a>.
toAssignment :: forall {k} (ctx :: Ctx k) e f. Size ctx -> (forall (tp :: k). () => Index ctx tp -> e -> f tp) -> Vector (CtxSize ctx) e -> Assignment f ctx

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

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

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

-- | Get the element at the given index. <tt>O(1)</tt>
elemAtMaybe :: forall (n :: Natural) a. 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 :: forall (n :: Natural) a. Int -> Vector n a -> a
indicesUpTo :: forall (n :: Nat). NatRepr n -> Vector (n + 1) (Fin (n + 1))
indicesOf :: forall (n :: Natural) a. Vector n a -> Vector n (Fin n)

-- | Insert an element at the given index. <tt>O(n)</tt>.
insertAt :: forall (i :: Natural) (n :: Natural) a. (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 :: forall a (n :: Natural). 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 :: Natural) a. Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))

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

-- | Extract a subvector of the given vector.
slice :: forall (i :: Natural) (w :: Natural) (n :: Natural) a. ((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 :: Natural) (x :: Natural) a. 1 <= n => NatRepr n -> Vector (n + x) a -> Vector n a

-- | Replace a sub-section of a vector with the given sub-vector.
replace :: forall (i :: Natural) (w :: Natural) (n :: Natural) a. ((i + w) <= n, 1 <= w) => NatRepr i -> Vector w a -> Vector n a -> Vector n a

-- | Scope a function to a sub-section of the given vector.
mapAt :: forall (i :: Natural) (w :: Natural) (n :: Natural) a. ((i + w) <= n, 1 <= w) => NatRepr i -> NatRepr w -> (Vector w a -> Vector w a) -> Vector n a -> Vector n a

-- | Scope a monadic function to a sub-section of the given vector.
mapAtM :: forall m (i :: Natural) (w :: Natural) (n :: Natural) a. (Monad m, (i + w) <= n, 1 <= w) => NatRepr i -> NatRepr w -> (Vector w a -> m (Vector w a)) -> Vector n a -> m (Vector n a)

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

-- | Reverse the vector.
reverse :: forall a (n :: Natural). 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 :: forall (n :: Natural) a. 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 :: forall (n :: Natural) a. 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 :: forall a (n :: Natural). 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 :: forall a (n :: Natural). Int -> a -> Vector n a -> Vector n a

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

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

-- | Add an element to the tail of a vector
snoc :: forall (n :: Natural) 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 :: Nat) a. NatRepr h -> (forall (n :: Nat). 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 :: Nat) a. Monad m => NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> m a) -> m (Vector (h + 1) a)

-- | Construct a vector with exactly <tt>h + 1</tt> elements by repeatedly
--   applying a generator function to a seed value.
--   
--   c.f. <tt>Data.Vector.unfoldrExactN</tt>
unfoldr :: forall (h :: Nat) a b. NatRepr h -> (b -> (a, b)) -> b -> Vector (h + 1) a

-- | Monadically construct a vector with exactly <tt>h + 1</tt> elements by
--   repeatedly applying a generator function to a seed value.
--   
--   c.f. <tt>Data.Vector.unfoldrExactNM</tt>
unfoldrM :: forall m (h :: Nat) a b. Monad m => NatRepr h -> (b -> m (a, b)) -> b -> m (Vector (h + 1) a)

-- | Unfold a vector, with access to the current index.
--   
--   c.f. <tt>Data.Vector.unfoldrExactN</tt>
unfoldrWithIndex :: forall (h :: Nat) a b. NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> b -> (a, b)) -> b -> Vector (h + 1) a

-- | Monadically unfold a vector, with access to the current index.
--   
--   c.f. <tt>Data.Vector.unfoldrExactNM</tt>
unfoldrWithIndexM :: forall m (h :: Nat) a b. Monad m => NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> b -> m (a, b)) -> b -> m (Vector (h + 1) a)

-- | Build a vector by repeatedly applying a function to a seed value.
--   
--   Compare to <a>iterateN</a>
iterateN :: forall (n :: Nat) a. NatRepr n -> (a -> a) -> a -> Vector (n + 1) a

-- | Build a vector by repeatedly applying a monadic function to a seed
--   value.
--   
--   Compare to <a>iterateNM</a>.
iterateNM :: forall m (n :: Nat) a. Monad m => NatRepr n -> (a -> m a) -> a -> m (Vector (n + 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 :: Natural) (w :: Natural). (1 <= w, Monad m) => (forall (l :: Natural). 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 :: Natural) (w :: Natural). 1 <= w => (forall (l :: Natural). 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 :: Natural) (n :: Natural). (1 <= w, 1 <= n) => Endian -> (forall (i :: Natural). (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 :: Natural) (n :: Natural). (Applicative f, 1 <= w, 1 <= n) => Endian -> (forall (i :: Natural). (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 :: forall (w :: Natural) (n :: Natural) a. (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 :: forall (w :: Natural) (n :: Natural) a. 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 :: forall (m :: Natural) a (n :: Natural). 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.Internal.Data.Foldable.Foldable (Data.Parameterized.Vector.Vector n)
instance WithIndex.FoldableWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.Vector.Vector n)
instance GHC.Internal.Base.Functor (Data.Parameterized.Vector.Vector n)
instance WithIndex.FunctorWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.Vector.Vector n)
instance GHC.Internal.Show.Show a => GHC.Internal.Show.Show (Data.Parameterized.Vector.Vector n a)
instance GHC.Internal.Data.Traversable.Traversable (Data.Parameterized.Vector.Vector n)
instance WithIndex.TraversableWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.Vector.Vector n)


-- | See <a>Data.Parameterized.FinMap</a>.
module Data.Parameterized.FinMap.Unsafe

-- | <tt><a>FinMap</a> n a</tt> is a map with <tt><a>Fin</a> n</tt> keys
--   and <tt>a</tt> values.
data FinMap (n :: Nat) a

-- | <i>O(1)</i>. Is the map empty?
null :: forall (n :: Nat) a. FinMap n a -> Bool

-- | <i>O(min(n,W))</i>. Fetch the value at the given key in the map.
lookup :: forall (n :: Natural) a. Fin n -> FinMap n a -> Maybe a

-- | <i>O(1)</i>. Number of elements in the map.
size :: forall (n :: Nat) a. FinMap n a -> Fin (n + 1)

-- | <i>O(1)</i>. Increase maximum key/size by 1.
--   
--   This does not alter the key-value pairs in the map, but rather
--   increases the maximum number of key-value pairs that the map can hold.
--   See <a>Data.Parameterized.FinMap</a> for more information.
--   
--   Requires <tt>n + 1 &lt; (maxBound :: Int)</tt>.
incMax :: forall (n :: Nat) a. FinMap n a -> FinMap (n + 1) a

-- | <i>O(1)</i>. Increase maximum key/size.
--   
--   Requires <tt>m &lt; (maxBound :: Int)</tt>.
embed :: forall (n :: Nat) (m :: Nat) a. n <= m => NatRepr m -> FinMap n a -> FinMap m a

-- | <i>O(1)</i>. The empty map.
empty :: forall (n :: Nat) a. KnownNat n => FinMap n a

-- | <i>O(1)</i>. A map with one element.
singleton :: a -> FinMap 1 a

-- | <i>O(min(n,W))</i>.
insert :: forall (n :: Natural) a. Fin n -> a -> FinMap n a -> FinMap n a
buildFinMap :: forall (m :: Nat) a. NatRepr m -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> FinMap n a -> FinMap (n + 1) a) -> FinMap m a

-- | <i>O(min(n,W))</i>.
append :: forall (n :: Nat) a. NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
fromVector :: forall (n :: Natural) a. Vector n (Maybe a) -> FinMap n a

-- | <i>O(min(n,W))</i>.
delete :: forall (n :: Natural) a. Fin n -> FinMap n a -> FinMap n a

-- | Decrement the key/size, removing the item at key <tt>n + 1</tt> if
--   present.
decMax :: forall (n :: Nat) a. NatRepr n -> FinMap (n + 1) a -> FinMap n a
mapWithKey :: forall (n :: Natural) a b. (Fin n -> a -> b) -> FinMap n a -> FinMap n b

-- | <i>O(n+m)</i>.
unionWithKey :: forall (n :: Natural) a. (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a

-- | <i>O(n+m)</i>.
unionWith :: forall a (n :: Nat). (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a

-- | <i>O(n+m)</i>. Left-biased union, i.e. (<tt><a>union</a> ==
--   <a>unionWith</a> <a>const</a></tt>).
union :: forall (n :: Nat) a. FinMap n a -> FinMap n a -> FinMap n a
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Parameterized.FinMap.Unsafe.FinMap n a)
instance GHC.Internal.Data.Foldable.Foldable (Data.Parameterized.FinMap.Unsafe.FinMap n)
instance WithIndex.FoldableWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.FinMap.Unsafe.FinMap n)
instance GHC.Internal.Base.Functor (Data.Parameterized.FinMap.Unsafe.FinMap n)
instance WithIndex.FunctorWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.FinMap.Unsafe.FinMap n)
instance GHC.Internal.TypeNats.KnownNat n => GHC.Internal.Base.Monoid (Data.Parameterized.FinMap.Unsafe.FinMap n a)
instance GHC.Internal.Base.Semigroup (Data.Parameterized.FinMap.Unsafe.FinMap n a)
instance GHC.Internal.Show.Show a => GHC.Internal.Show.Show (Data.Parameterized.FinMap.Unsafe.FinMap n a)
instance GHC.Internal.Data.Traversable.Traversable (Data.Parameterized.FinMap.Unsafe.FinMap n)


-- | <tt><a>FinMap</a> n a</tt> conceptually (see NOTE) a map with
--   <tt><a>Fin</a> n</tt> keys, implying a maximum size of <tt>n</tt>.
--   Here's how <a>FinMap</a> compares to other map-like types:
--   
--   <ul>
--   <li><tt><a>FinMap</a> n a</tt> is conceptually isomorphic to a
--   <tt><a>Vector</a> n (<a>Maybe</a> a)</tt>, but can be more
--   space-efficient especially if <tt>n</tt> is large and the vector is
--   populated with a small number of <a>Just</a> values.</li>
--   <li><tt><a>FinMap</a></tt> is less general than <a>Map</a>, because it
--   has a fixed key type (<tt><a>Fin</a> n</tt>).</li>
--   <li><tt><a>FinMap</a> n a</tt> is similar to <tt><a>IntMap</a> a</tt>,
--   but it provides a static guarantee of a maximum size, and its
--   operations (such as <a>size</a>) allow the recovery of more type-level
--   information.</li>
--   <li><tt><a>FinMap</a></tt> is dissimilar from
--   <a>Data.Parameterized.Map.MapF</a> in that neither the key nor value
--   type of <a>FinMap</a> is parameterized.</li>
--   </ul>
--   
--   The type parameter <tt>n</tt> doesn't track the <i>current</i> number
--   of key-value pairs in a <tt><a>FinMap</a> n</tt> (i.e., the size of
--   the map), but rather <i>an upper bound</i>. <a>insert</a> and
--   <a>delete</a> don't alter <tt>n</tt>, whereas <a>incMax</a> does -
--   despite the fact that it has no effect on the keys and values in the
--   <a>FinMap</a>.
--   
--   The <a>FinMap</a> interface has two implementations:
--   
--   <ul>
--   <li>The implementation in <a>Data.Parameterized.FinMap.Unsafe</a> is
--   backed by an <a>IntMap</a>, and must have a size of at most
--   <tt><a>maxBound</a> :: <a>Int</a></tt>. This module uses unsafe
--   operations like <a>unsafeCoerce</a> internally for the sake of time
--   and space efficiency.</li>
--   <li>The implementation in <a>Data.Parameterized.FinMap.Safe</a> is
--   backed by an <tt><a>Map</a> (<a>Fin</a> n)</tt>. All of its functions
--   are implemented using safe operations.</li>
--   </ul>
--   
--   The implementation in <a>FinMap</a> is property tested against that in
--   <a>FinMap</a> to ensure they have the same behavior.
--   
--   In this documentation, <i>W</i> is used in big-O notations the same
--   way as in the <a>Data.IntMap</a> documentation.
--   
--   NOTE: Where the word "conceptually" is used, it implies that this
--   correspondence is not literally true, but is true modulo some details
--   such as differences between bounded types like <a>Int</a> and
--   unbounded types like <a>Integer</a>.
--   
--   Several of the functions in both implementations are marked
--   <tt>INLINE</tt> or <tt>INLINABLE</tt>. There are three reasons for
--   this:
--   
--   <ul>
--   <li>Some of these just have very small definitions and so inlining is
--   likely more beneficial than harmful.</li>
--   <li>Some participate in <tt>RULES</tt> relevant to functions used in
--   their implementations.</li>
--   <li>They are thin wrappers (often just newtype wrappers) around
--   functions marked <tt>INLINE</tt>, which should therefore also be
--   inlined.</li>
--   </ul>
module Data.Parameterized.FinMap


-- | See <a>Data.Parameterized.FinMap</a>.
module Data.Parameterized.FinMap.Safe

-- | <tt><a>FinMap</a> n a</tt> is a map with <tt><a>Fin</a> n</tt> keys
--   and <tt>a</tt> values.
data FinMap (n :: Nat) a

-- | <i>O(1)</i>. Is the map empty?
null :: forall (n :: Nat) a. FinMap n a -> Bool

-- | <i>O(log n)</i>. Fetch the value at the given key in the map.
lookup :: forall (n :: Natural) a. Fin n -> FinMap n a -> Maybe a

-- | <i>O(nlog(n))</i>. Number of elements in the map.
--   
--   This operation is much slower than <a>size</a> because its
--   implementation must provide significant evidence to the type-checker,
--   and the easiest way to do that is fairly inefficient. If speed is a
--   concern, use <a>Data.Parameterized.FinMap.Unsafe</a>.
size :: forall (n :: Nat) a. FinMap n a -> Fin (n + 1)

-- | <i>O(n log n)</i>. Increase maximum key/size by 1.
--   
--   This does not alter the key-value pairs in the map, but rather
--   increases the maximum number of key-value pairs that the map can hold.
--   See <a>Data.Parameterized.FinMap</a> for more information.
--   
--   Requires <tt>n + 1 &lt; (maxBound :: Int)</tt>.
incMax :: forall (n :: Nat) a. FinMap n a -> FinMap (n + 1) a

-- | <i>O(n log n)</i>. Increase maximum key/size.
--   
--   Requires <tt>m &lt; (maxBound :: Int)</tt>.
embed :: forall (n :: Nat) (m :: Nat) a. n <= m => NatRepr m -> FinMap n a -> FinMap m a

-- | <i>O(1)</i>. The empty map.
empty :: forall (n :: Nat) a. KnownNat n => FinMap n a

-- | <i>O(1)</i>. A map with one element.
singleton :: a -> FinMap 1 a

-- | <i>O(log n)</i>.
insert :: forall (n :: Natural) a. Fin n -> a -> FinMap n a -> FinMap n a
buildFinMap :: forall (m :: Nat) a. NatRepr m -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> FinMap n a -> FinMap (n + 1) a) -> FinMap m a

-- | <i>O(min(n,W))</i>.
append :: forall (n :: Nat) a. NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
fromVector :: forall (n :: Natural) a. Vector n (Maybe a) -> FinMap n a

-- | <i>O(log n)</i>.
delete :: forall (n :: Natural) a. Fin n -> FinMap n a -> FinMap n a

-- | Decrement the key/size, removing the item at key <tt>n + 1</tt> if
--   present.
decMax :: forall (n :: Nat) a. NatRepr n -> FinMap (n + 1) a -> FinMap n a
mapWithKey :: forall (n :: Natural) a b. (Fin n -> a -> b) -> FinMap n a -> FinMap n b

-- | <i>O(n+m)</i>.
unionWithKey :: forall (n :: Natural) a. (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a

-- | <i>O(n+m)</i>.
unionWith :: forall a (n :: Nat). (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a

-- | <i>O(n+m)</i>. Left-biased union, i.e. (<tt><a>union</a> ==
--   <a>unionWith</a> <a>const</a></tt>).
union :: forall (n :: Nat) a. FinMap n a -> FinMap n a -> FinMap n a
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Parameterized.FinMap.Safe.FinMap n a)
instance GHC.Internal.Data.Foldable.Foldable (Data.Parameterized.FinMap.Safe.FinMap n)
instance WithIndex.FoldableWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.FinMap.Safe.FinMap n)
instance GHC.Internal.Base.Functor (Data.Parameterized.FinMap.Safe.FinMap n)
instance WithIndex.FunctorWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.FinMap.Safe.FinMap n)
instance GHC.Internal.TypeNats.KnownNat n => GHC.Internal.Base.Monoid (Data.Parameterized.FinMap.Safe.FinMap n a)
instance GHC.Internal.Base.Semigroup (Data.Parameterized.FinMap.Safe.FinMap n a)
instance GHC.Internal.Show.Show a => GHC.Internal.Show.Show (Data.Parameterized.FinMap.Safe.FinMap n a)
instance GHC.Internal.Data.Traversable.Traversable (Data.Parameterized.FinMap.Safe.FinMap 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 -> Type)
withRepr :: forall (a :: k) r. IsRepr f => f a -> (KnownRepr f a => r) -> r
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.Context.Unsafe.Assignment f)
instance forall k (f :: k -> *). Data.Parameterized.WithRepr.IsRepr f => Data.Parameterized.WithRepr.IsRepr (Data.Parameterized.List.List f)
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.NatRepr.Internal.NatRepr
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.SymbolRepr.SymbolRepr
