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


-- | Generic Programming with Mutually Recursive Sums of Products.
--   
--   A library that supports generic programming for mutually recursive
--   families in the sum-of-products style.
--   
--   A couple usage examples can be found under
--   <a>Generics.MRSOP.Examples</a>
@package generics-mrsop
@version 1.2.2


-- | Useful utilities we need accross multiple modules.
module Generics.MRSOP.Util

-- | Fanout: send the input to both argument arrows and combine their
--   output.
--   
--   The default definition may be overridden with a more efficient version
--   if desired.
(&&&) :: Arrow a => a b c -> a b c' -> a b (c, c')
infixr 3 &&&

-- | Split the input between the two argument arrows and combine their
--   output. Note that this is in general not a functor.
--   
--   The default definition may be overridden with a more efficient version
--   if desired.
(***) :: Arrow a => a b c -> a b' c' -> a (b, b') (c, c')
infixr 3 ***

-- | Natural transformations
type f :-> g = forall n. f n -> g n

-- | Kleisli Composition
(<.>) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c
infixr 8 <.>

-- | Poly-kind-indexed product
data (:*:) (f :: k -> *) (g :: k -> *) (x :: k)
(:*:) :: f x -> g x -> (:*:)

-- | Lifted curry
curry' :: ((f :*: g) x -> a) -> f x -> g x -> a

-- | Lifted uncurry
uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a

-- | Distributes the index over the product
delta' :: (f :*: g) x -> (f x, g x)

-- | Type-level Peano Naturals
data Nat
S :: Nat -> Nat
Z :: Nat
proxyUnsuc :: Proxy (S n) -> Proxy n

-- | Singleton Term-level natural
data SNat :: Nat -> *
[SZ] :: SNat Z
[SS] :: SNat n -> SNat (S n)
snat2int :: SNat n -> Integer

-- | And their conversion to term-level integers.
class IsNat (n :: Nat)
getSNat :: IsNat n => Proxy n -> SNat n
getNat :: IsNat n => Proxy n -> Integer
getSNat' :: forall (n :: Nat). IsNat n => SNat n

-- | An inhabitant of <tt>ListPrf ls</tt> is *not* a singleton! It only
--   proves that <tt>ls</tt> is, in fact, a type level list. This is useful
--   since it enables us to pattern match on type-level lists whenever we
--   see fit.
data ListPrf :: [k] -> *
[Nil] :: ListPrf '[]
[Cons] :: ListPrf l -> ListPrf (x : l)

-- | The <tt>IsList</tt> class allows us to construct <a>ListPrf</a>s in a
--   straight forward fashion.
class IsList (xs :: [k])
listPrf :: IsList xs => ListPrf xs

-- | Convenient constraint synonyms
type L1 xs = (IsList xs)
type L2 xs ys = (IsList xs, IsList ys)
type L3 xs ys zs = (IsList xs, IsList ys, IsList zs)
type L4 xs ys zs as = (IsList xs, IsList ys, IsList zs, IsList as)

-- | Appending type-level lists
type family (:++:) (txs :: [k]) (tys :: [k]) :: [k]

-- | Concatenation of lists is also a list.
appendIsListLemma :: ListPrf xs -> ListPrf ys -> ListPrf (xs :++: ys)

-- | Type-level list lookup
type family Lkup (n :: Nat) (ks :: [k]) :: k

-- | Type-level list index
type family Idx (ty :: k) (xs :: [k]) :: Nat

-- | Also list lookup, but for kind * only.
data El :: [*] -> Nat -> *
[El] :: IsNat ix => {unEl :: Lkup ix fam} -> El fam ix

-- | Convenient way to cast an <a>El</a> index to term-level.
getElSNat :: forall ix ls. El ls ix -> SNat ix

-- | Smart constructor into <a>El</a>
into :: forall fam ty ix. (ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix) => ty -> El fam ix

-- | Higher order version of <a>Eq</a>
class Eq1 (f :: k -> *)
eq1 :: forall k. Eq1 f => f k -> f k -> Bool

-- | Higher order version of <a>Show</a>
class Show1 (f :: k -> *)
show1 :: forall k. Show1 f => f k -> String
instance GHC.Show.Show Generics.MRSOP.Util.Nat
instance GHC.Classes.Eq Generics.MRSOP.Util.Nat
instance Generics.MRSOP.Util.IsList '[]
instance forall k (xs :: [k]) (x :: k). Generics.MRSOP.Util.IsList xs => Generics.MRSOP.Util.IsList (x : xs)
instance Generics.MRSOP.Util.IsNat 'Generics.MRSOP.Util.Z
instance Generics.MRSOP.Util.IsNat n => Generics.MRSOP.Util.IsNat ('Generics.MRSOP.Util.S n)
instance Data.Type.Equality.TestEquality Generics.MRSOP.Util.SNat


-- | A curation of base types commonly used by the everyday Haskell
--   programmer.
module Generics.MRSOP.Opaque

-- | Types with kind <a>Kon</a> will be used to index a <a>Singl</a> type
--   with their values inside.
data Kon
KInt :: Kon
KInteger :: Kon
KFloat :: Kon
KDouble :: Kon
KBool :: Kon
KChar :: Kon
KString :: Kon

-- | A singleton GADT for the allowed <a>Kon</a>stants.
data Singl (kon :: Kon) :: *
[SInt] :: Int -> Singl KInt
[SInteger] :: Integer -> Singl KInteger
[SFloat] :: Float -> Singl KFloat
[SDouble] :: Double -> Singl KDouble
[SBool] :: Bool -> Singl KBool
[SChar] :: Char -> Singl KChar
[SString] :: String -> Singl KString

-- | Equality over singletons
eqSingl :: Singl k -> Singl k -> Bool
instance GHC.Show.Show Generics.MRSOP.Opaque.Kon
instance GHC.Classes.Eq Generics.MRSOP.Opaque.Kon
instance GHC.Show.Show (Generics.MRSOP.Opaque.Singl k)
instance GHC.Classes.Eq (Generics.MRSOP.Opaque.Singl k)
instance Generics.MRSOP.Util.Eq1 Generics.MRSOP.Opaque.Singl
instance Generics.MRSOP.Util.Show1 Generics.MRSOP.Opaque.Singl
instance Data.Type.Equality.TestEquality Generics.MRSOP.Opaque.Singl


-- | Standard representation of n-ary sums.
module Generics.MRSOP.Base.NS

-- | Indexed n-ary sums. This is analogous to the <tt>Any</tt> datatype in
--   <tt>Agda</tt>. Combinations of <a>Here</a> and <a>There</a>s are also
--   called injections.
data NS :: (k -> *) -> [k] -> *
[There] :: NS p xs -> NS p (x : xs)
[Here] :: p x -> NS p (x : xs)

-- | Maps over a sum
mapNS :: (f :-> g) -> NS f ks -> NS g ks

-- | Maps a monadic function over a sum
mapNSM :: Monad m => (forall x. f x -> m (g x)) -> NS f ks -> m (NS g ks)

-- | Eliminates a sum
elimNS :: (forall x. f x -> a) -> NS f ks -> a

-- | Combines two sums. Note that we have to fail if they are constructed
--   from different injections.
zipNS :: MonadPlus m => NS ki xs -> NS kj xs -> m (NS (ki :*: kj) xs)

-- | Consumes a value of type <a>NS</a>
cataNS :: (forall x xs. f x -> r (x : xs)) -> (forall x xs. r xs -> r (x : xs)) -> NS f xs -> r xs

-- | Compares two values of type <a>NS</a> using the provided function in
--   case they are made of the same injection.
eqNS :: (forall x. p x -> p x -> Bool) -> NS p xs -> NS p xs -> Bool
instance forall k (ki :: k -> *). Generics.MRSOP.Util.Eq1 ki => Generics.MRSOP.Util.Eq1 (Generics.MRSOP.Base.NS.NS ki)


-- | Standard representation of n-ary products.
module Generics.MRSOP.Base.NP

-- | Indexed n-ary products. This is analogous to the <tt>All</tt> datatype
--   in Agda.
data NP :: (k -> *) -> [k] -> *
[NP0] :: NP p '[]
[:*] :: p x -> NP p xs -> NP p (x : xs)
infixr 5 :*

-- | Append two values of type <a>NP</a>
appendNP :: NP p xs -> NP p ys -> NP p (xs :++: ys)

-- | Proves that the index of a value of type <a>NP</a> is a list. This is
--   useful for pattern matching on said list without having to carry the
--   product around.
listPrfNP :: NP p xs -> ListPrf xs

-- | Maps a natural transformation over a n-ary product
mapNP :: (f :-> g) -> NP f ks -> NP g ks

-- | Maps a monadic natural transformation over a n-ary product
mapNPM :: Monad m => (forall x. f x -> m (g x)) -> NP f ks -> m (NP g ks)

-- | Eliminates the product using a provided function.
elimNP :: (forall x. f x -> a) -> NP f ks -> [a]

-- | Monadic eliminator
elimNPM :: Monad m => (forall x. f x -> m a) -> NP f ks -> m [a]

-- | Combines two products into one.
zipNP :: NP f xs -> NP g xs -> NP (f :*: g) xs

-- | Unzips a combined product into two separate products
unzipNP :: NP (f :*: g) xs -> (NP f xs, NP g xs)

-- | Consumes a value of type <a>NP</a>.
cataNP :: (forall x xs. f x -> r xs -> r (x : xs)) -> r '[] -> NP f xs -> r xs

-- | Consumes a value of type <a>NP</a>.
cataNPM :: Monad m => (forall x xs. f x -> r xs -> m (r (x : xs))) -> m (r '[]) -> NP f xs -> m (r xs)

-- | Compares two <a>NP</a>s pairwise with the provided function and return
--   the conjunction of the results.
eqNP :: (forall x. p x -> p x -> Bool) -> NP p xs -> NP p xs -> Bool
instance forall k (ki :: k -> *). Generics.MRSOP.Util.Eq1 ki => Generics.MRSOP.Util.Eq1 (Generics.MRSOP.Base.NP.NP ki)


-- | Wraps the definitions of <a>NP</a> and <a>NS</a> into Representations
--   (<a>Rep</a>), essentially providing the universe view over
--   sums-of-products.
module Generics.MRSOP.Base.Universe

-- | Atoms can be either opaque types, <tt>kon</tt>, or type variables,
--   <tt>Nat</tt>.
data Atom kon
K :: kon -> Atom kon
I :: Nat -> Atom kon

-- | <tt>NA ki phi a</tt> provides an interpretation for an atom
--   <tt>a</tt>, using either <tt>ki</tt> or <tt>phi</tt> to interpret the
--   type variable or opaque type.
data NA :: (kon -> *) -> (Nat -> *) -> Atom kon -> *
[NA_I] :: IsNat k => phi k -> NA ki phi (I k)
[NA_K] :: ki k -> NA ki phi (K k)

-- | Maps a natural transformation over an atom interpretation
mapNA :: (forall k. ki k -> kj k) -> (forall ix. IsNat ix => f ix -> g ix) -> NA ki f a -> NA kj g a

-- | Maps a monadic natural transformation over an atom interpretation
mapNAM :: Monad m => (forall k. ki k -> m (kj k)) -> (forall ix. IsNat ix => f ix -> m (g ix)) -> NA ki f a -> m (NA kj g a)

-- | Eliminates an atom interpretation
elimNA :: (forall k. ki k -> b) -> (forall k. IsNat k => phi k -> b) -> NA ki phi a -> b

-- | Combines two atoms into one
zipNA :: NA ki f a -> NA kj g a -> NA (ki :*: kj) (f :*: g) a

-- | Compares atoms provided we know how to compare the leaves, both
--   recursive and constant.
eqNA :: (forall k. ki k -> ki k -> Bool) -> (forall ix. fam ix -> fam ix -> Bool) -> NA ki fam l -> NA ki fam l -> Bool

-- | Representation of codes.
newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])
Rep :: NS (PoA ki phi) code -> Rep
[unRep] :: Rep -> NS (PoA ki phi) code

-- | Product of Atoms is a handy synonym to have.
type PoA (ki :: kon -> *) (phi :: Nat -> *) = NP (NA ki phi)

-- | Maps over a representation.
mapRep :: (forall ix. IsNat ix => f ix -> g ix) -> Rep ki f c -> Rep ki g c

-- | Maps a monadic function over a representation.
mapRepM :: Monad m => (forall ix. IsNat ix => f ix -> m (g ix)) -> Rep ki f c -> m (Rep ki g c)

-- | Maps over both indexes of a representation.
bimapRep :: (forall k. ki k -> kj k) -> (forall ix. IsNat ix => f ix -> g ix) -> Rep ki f c -> Rep kj g c

-- | Monadic version of <a>bimapRep</a>
bimapRepM :: Monad m => (forall k. ki k -> m (kj k)) -> (forall ix. IsNat ix => f ix -> m (g ix)) -> Rep ki f c -> m (Rep kj g c)

-- | Zip two representations together, in case they are made with the same
--   constructor.
--   
--   <pre>
--   zipRep (Here (NA_I x :* NP0)) (Here (NA_I y :* NP0))
--     = return $ Here (NA_I (x :*: y) :* NP0)
--   </pre>
--   
--   <pre>
--   zipRep (Here (NA_I x :* NP0)) (There (Here ...))
--     = mzero
--   </pre>
zipRep :: MonadPlus m => Rep ki f c -> Rep kj g c -> m (Rep (ki :*: kj) (f :*: g) c)

-- | Monadic eliminator; This is just the cannonical combination of
--   <a>elimNS</a>, <a>elimNPM</a> and <a>elimNA</a>.
elimRepM :: Monad m => (forall k. ki k -> m a) -> (forall k. IsNat k => f k -> m a) -> ([a] -> m b) -> Rep ki f c -> m b

-- | Pure eliminator.
elimRep :: (forall k. ki k -> a) -> (forall k. IsNat k => f k -> a) -> ([a] -> b) -> Rep ki f c -> b

-- | Compares two <a>Rep</a> for equality; again, cannonical combination of
--   <a>eqNS</a>, <a>eqNP</a> and <a>eqNA</a>
eqRep :: (forall k. ki k -> ki k -> Bool) -> (forall ix. fam ix -> fam ix -> Bool) -> Rep ki fam c -> Rep ki fam c -> Bool

-- | A value <tt>c :: Constr ks n</tt> specifies a position in a type-level
--   list. It is, in fact, isomorphic to <tt>Fin (length ks)</tt>.
data Constr :: [k] -> Nat -> *
[CS] :: Constr xs n -> Constr (x : xs) (S n)
[CZ] :: Constr (x : xs) Z

-- | We can define injections into an n-ary sum from its
--   <a>Constr</a>uctors
injNS :: Constr sum n -> PoA ki fam (Lkup n sum) -> NS (NP (NA ki fam)) sum

-- | Wrap it in a <a>Rep</a> for convenience.
inj :: Constr sum n -> PoA ki fam (Lkup n sum) -> Rep ki fam sum

-- | Inverse of <a>injNS</a>. Given some Constructor, see if Rep is of this
--   constructor
matchNS :: Constr sum c -> NS (NP (NA ki fam)) sum -> Maybe (PoA ki fam (Lkup c sum))

-- | Inverse of <a>inj</a>. Given some Constructor, see if Rep is of this
--   constructor
match :: Constr sum c -> Rep ki fam sum -> Maybe (PoA ki fam (Lkup c sum))

-- | Finally, we can view a sum-of-products as a constructor and a
--   product-of-atoms.
data View :: (kon -> *) -> (Nat -> *) -> [[Atom kon]] -> *
[Tag] :: IsNat n => Constr sum n -> PoA ki fam (Lkup n sum) -> View ki fam sum

-- | Unwraps a <a>Rep</a> into a <a>View</a>
sop :: Rep ki fam sum -> View ki fam sum

-- | Wraps a <a>View</a> into a <a>Rep</a>
fromView :: View ki fam sum -> Rep ki fam sum

-- | Indexed least fixpoints
--   
--   Annotated version of Fix. This is basically the <tt>Cofree</tt>
--   datatype, but for n-ary functors
data AnnFix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (phi :: Nat -> *) (n :: Nat)
AnnFix :: phi n -> Rep ki (AnnFix ki codes phi) (Lkup n codes) -> AnnFix
type Fix ki codes = AnnFix ki codes (Const ())
pattern Fix :: forall kon (ki :: kon -> Type) (codes :: [[[Atom kon]]]) (n :: Nat). () => () => Rep ki (AnnFix ki codes (Const () :: Nat -> Type)) (Lkup n codes) -> AnnFix ki codes (Const () :: Nat -> Type) n
unFix :: Fix ki codes ix -> Rep ki (Fix ki codes) (Lkup ix codes)

-- | Catamorphism over fixpoints
cata :: IsNat ix => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) -> Fix ki codes ix -> phi ix
getAnn :: AnnFix ki codes ann ix -> ann ix
annCata :: (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -> AnnFix ki codes chi ix -> phi ix

-- | Forget the annotations
forgetAnn :: AnnFix ki codes a ix -> Fix ki codes ix

-- | Retrieves the index of a <a>Fix</a>
proxyFixIdx :: phi ix -> Proxy ix
sNatFixIdx :: IsNat ix => phi ix -> SNat ix

-- | Maps over the values of opaque types within the fixpoint.
mapFixM :: Monad m => (forall k. ki k -> m (kj k)) -> Fix ki fam ix -> m (Fix kj fam ix)

-- | Compare two values of a same fixpoint for equality.
eqFix :: (forall k. ki k -> ki k -> Bool) -> Fix ki fam ix -> Fix ki fam ix -> Bool

-- | Compare two indexes of two fixpoints Note we can't use a
--   <a>testEquality</a> instance because of the <a>IsNat</a> constraint.
heqFixIx :: (IsNat ix, IsNat ix') => Fix ki fam ix -> Fix ki fam ix' -> Maybe (ix :~: ix')
instance GHC.Show.Show kon => GHC.Show.Show (Generics.MRSOP.Base.Universe.Atom kon)
instance GHC.Classes.Eq kon => GHC.Classes.Eq (Generics.MRSOP.Base.Universe.Atom kon)
instance forall kon (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]). Generics.MRSOP.Util.Eq1 ki => Generics.MRSOP.Util.Eq1 (Generics.MRSOP.Base.Universe.Fix ki codes)
instance forall kon (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]) (ix :: Generics.MRSOP.Util.Nat). Generics.MRSOP.Util.Eq1 ki => GHC.Classes.Eq (Generics.MRSOP.Base.Universe.Fix ki codes ix)
instance forall k (codes :: [k]). Data.Type.Equality.TestEquality (Generics.MRSOP.Base.Universe.Constr codes)
instance forall k (n :: Generics.MRSOP.Util.Nat) (xs :: [k]). Generics.MRSOP.Util.IsNat n => GHC.Show.Show (Generics.MRSOP.Base.Universe.Constr xs n)
instance forall kon (phi :: Generics.MRSOP.Util.Nat -> *) (ki :: kon -> *). (Generics.MRSOP.Util.Eq1 phi, Generics.MRSOP.Util.Eq1 ki) => Generics.MRSOP.Util.Eq1 (Generics.MRSOP.Base.Universe.Rep ki phi)
instance forall kon (phi :: Generics.MRSOP.Util.Nat -> *) (ki :: kon -> *). (Generics.MRSOP.Util.Eq1 phi, Generics.MRSOP.Util.Eq1 ki) => Generics.MRSOP.Util.Eq1 (Generics.MRSOP.Base.Universe.NA ki phi)
instance forall kon (ki :: kon -> *) (phi :: Generics.MRSOP.Util.Nat -> *). Data.Type.Equality.TestEquality ki => Data.Type.Equality.TestEquality (Generics.MRSOP.Base.Universe.NA ki phi)


-- | Implements a rudimentary show instance for our representations. We
--   keep this isolated because the instance for <tt>Show (Rep ki phi
--   code)</tt> requires undecidable instances. Isolating this allows us to
--   turn on this extension for this module only.
module Generics.MRSOP.Base.Show
showNA :: (Show1 phi, Show1 ki) => NA ki (AnnFix ki codes phi) a -> String
showNP :: (Show1 phi, Show1 ki) => PoA ki (AnnFix ki codes phi) xs -> String
showRep :: (Show1 phi, Show1 ki) => Rep ki (AnnFix ki codes phi) xs -> String
showFix :: (Show1 phi, Show1 ki) => AnnFix ki codes phi ix -> String
instance forall kon (phi :: Generics.MRSOP.Util.Nat -> *) (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]) (a :: Generics.MRSOP.Base.Universe.Atom kon). (Generics.MRSOP.Util.Show1 phi, Generics.MRSOP.Util.Show1 ki) => GHC.Show.Show (Generics.MRSOP.Base.Universe.NA ki (Generics.MRSOP.Base.Universe.AnnFix ki codes phi) a)
instance forall kon (phi :: Generics.MRSOP.Util.Nat -> *) (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]) (xs :: [Generics.MRSOP.Base.Universe.Atom kon]). (Generics.MRSOP.Util.Show1 phi, Generics.MRSOP.Util.Show1 ki) => GHC.Show.Show (Generics.MRSOP.Base.Universe.PoA ki (Generics.MRSOP.Base.Universe.AnnFix ki codes phi) xs)
instance forall kon (phi :: Generics.MRSOP.Util.Nat -> *) (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]) (xs :: [[Generics.MRSOP.Base.Universe.Atom kon]]). (Generics.MRSOP.Util.Show1 phi, Generics.MRSOP.Util.Show1 ki) => GHC.Show.Show (Generics.MRSOP.Base.Universe.Rep ki (Generics.MRSOP.Base.Universe.AnnFix ki codes phi) xs)
instance forall kon (phi :: Generics.MRSOP.Util.Nat -> *) (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]) (ix :: Generics.MRSOP.Util.Nat). (Generics.MRSOP.Util.Show1 phi, Generics.MRSOP.Util.Show1 ki) => GHC.Show.Show (Generics.MRSOP.Base.Universe.AnnFix ki codes phi ix)


-- | Provides the main class of the library, <a>Family</a>.
module Generics.MRSOP.Base.Class

-- | A Family consists of a list of types and a list of codes of the same
--   length. The idea is that the code of <tt>Lkup n fam</tt> is <tt>Lkup n
--   code</tt>. We also parametrize on the interpretation of constants. The
--   class family provides primitives for performing a shallow conversion.
--   The <a>deep</a> conversion is easy to obtain: <tt>deep = map deep .
--   shallow</tt>
class Family (ki :: kon -> *) (fam :: [*]) (codes :: [[[Atom kon]]]) | fam -> ki codes, ki codes -> fam
sfrom' :: Family ki fam codes => SNat ix -> El fam ix -> Rep ki (El fam) (Lkup ix codes)
sto' :: Family ki fam codes => SNat ix -> Rep ki (El fam) (Lkup ix codes) -> El fam ix

-- | A Smarter variant of <a>sfrom'</a>, since <a>El</a> is a GADT, we can
--   extract the term-level rep of <tt>ix</tt> from there.
sfrom :: forall fam ki codes ix. Family ki fam codes => El fam ix -> Rep ki (El fam) (Lkup ix codes)

-- | For <a>sto'</a> there is a similar more general combinator. If
--   <tt>ix</tt> implements <a>IsNat</a> we can cast it.
sto :: forall fam ki codes ix. (Family ki fam codes, IsNat ix) => Rep ki (El fam) (Lkup ix codes) -> El fam ix

-- | Converts an entire element of our family into
dfrom :: forall ix ki fam codes. Family ki fam codes => El fam ix -> Fix ki codes ix

-- | Converts an element back from a deep encoding. This is the dual of
--   <a>dfrom</a>.
--   
--   <pre>
--   dto = sto . map dto
--   </pre>
dto :: forall ix ki fam codes. (Family ki fam codes, IsNat ix) => Rep ki (Fix ki codes) (Lkup ix codes) -> El fam ix

-- | Converts a type into its shallow representation.
shallow :: forall fam ty ki codes ix. (Family ki fam codes, ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix) => ty -> Rep ki (El fam) (Lkup ix codes)

-- | Converts a type into its deep representation.
deep :: forall fam ty ki codes ix. (Family ki fam codes, ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix) => ty -> AnnFix ki codes (Const ()) ix


-- | Metadata maintenance; usefull for pretty-printing values.
module Generics.MRSOP.Base.Metadata
type ModuleName = String
type FamilyName = String
type ConstructorName = String
type FieldName = String

-- | Since we only handled fully saturated datatypes, a <a>DatatypeName</a>
--   needs to remember what were the arguments applied to a type.
--   
--   The type <tt>[Int]</tt> is represented by <tt>Name "[]" :</tt><tt>:
--   Name <a>Int</a></tt>
data DatatypeName
Name :: String -> DatatypeName
(:@:) :: DatatypeName -> DatatypeName -> DatatypeName
infixl 5 :@:

-- | Provides information about the declaration of a datatype.
data DatatypeInfo :: [[Atom kon]] -> *
[ADT] :: ModuleName -> DatatypeName -> NP ConstructorInfo c -> DatatypeInfo c
[New] :: ModuleName -> DatatypeName -> ConstructorInfo '[c] -> DatatypeInfo '['[c]]
moduleName :: DatatypeInfo code -> ModuleName
datatypeName :: DatatypeInfo code -> DatatypeName
constructorInfo :: DatatypeInfo code -> NP ConstructorInfo code

-- | Associativity information for infix constructors.
data Associativity
LeftAssociative :: Associativity
RightAssociative :: Associativity
NotAssociative :: Associativity

-- | Fixity information for infix constructors.
type Fixity = Int

-- | Constructor metadata.
data ConstructorInfo :: [Atom kon] -> *
[Constructor] :: ConstructorName -> ConstructorInfo xs
[Infix] :: ConstructorName -> Associativity -> Fixity -> ConstructorInfo '[x, y]
[Record] :: ConstructorName -> NP FieldInfo xs -> ConstructorInfo xs
constructorName :: ConstructorInfo con -> ConstructorName

-- | Record fields metadata
data FieldInfo :: Atom kon -> *
[FieldInfo] :: {fieldName :: FieldName} -> FieldInfo k

-- | Given a <a>Family</a>, provides the <a>DatatypeInfo</a> for the type
--   with index <tt>ix</tt> in family <tt>fam</tt>.
class (Family ki fam codes) => HasDatatypeInfo ki fam codes | fam -> codes ki
datatypeInfo :: HasDatatypeInfo ki fam codes => Proxy fam -> SNat ix -> DatatypeInfo (Lkup ix codes)

-- | Sometimes it is more convenient to use a proxy of the type in the
--   family instead of indexes.
datatypeInfoFor :: forall ki fam codes ix ty. (HasDatatypeInfo ki fam codes, ix ~ Idx ty fam, Lkup ix fam ~ ty, IsNat ix) => Proxy fam -> Proxy ty -> DatatypeInfo (Lkup ix codes)

-- | This is essentially a list lookup, but needs significant type
--   information to go through. Returns the name of the <tt>c</tt>th
--   constructor of a sum-type.
constrInfoLkup :: Constr sum c -> DatatypeInfo sum -> ConstructorInfo (Lkup c sum)

-- | Returns the constructor information for a given type in the family.
constrInfoFor :: HasDatatypeInfo ki fam codes => Proxy fam -> SNat ix -> Constr (Lkup ix codes) c -> ConstructorInfo (Lkup c (Lkup ix codes))
instance GHC.Show.Show Generics.MRSOP.Base.Metadata.Associativity
instance GHC.Classes.Eq Generics.MRSOP.Base.Metadata.Associativity
instance GHC.Show.Show Generics.MRSOP.Base.Metadata.DatatypeName
instance GHC.Classes.Eq Generics.MRSOP.Base.Metadata.DatatypeName
instance forall kon (code :: [[Generics.MRSOP.Base.Universe.Atom kon]]). GHC.Show.Show (Generics.MRSOP.Base.NP.NP Generics.MRSOP.Base.Metadata.ConstructorInfo code)
instance forall kon (code :: [Generics.MRSOP.Base.Universe.Atom kon]). GHC.Show.Show (Generics.MRSOP.Base.NP.NP Generics.MRSOP.Base.Metadata.FieldInfo code)
instance forall kon (code :: [Generics.MRSOP.Base.Universe.Atom kon]). GHC.Show.Show (Generics.MRSOP.Base.Metadata.ConstructorInfo code)
instance forall kon (code :: [[Generics.MRSOP.Base.Universe.Atom kon]]). GHC.Show.Show (Generics.MRSOP.Base.Metadata.DatatypeInfo code)
instance forall kon (atom :: Generics.MRSOP.Base.Universe.Atom kon). GHC.Show.Show (Generics.MRSOP.Base.Metadata.FieldInfo atom)


-- | Provides a simple way for the end-user deriving the mechanical, yet
--   long, Element instances for a family.
--   
--   We are borrowing a some code from generic-sop (
--   <a>https://hackage.haskell.org/package/generics-sop-0.3.2.0/docs/src/Generics-SOP-TH.html</a>
--   )
module Generics.MRSOP.TH

-- | Given the name of the first element in the family, derives:
--   
--   <ol>
--   <li>The other types in the family and Konstant types one needs.</li>
--   <li>the SOP code for each of the datatypes involved</li>
--   <li>One <tt>Element</tt> instance per datatype</li>
--   <li>Metadada information for each of the datatypes involved</li>
--   <li>Uses the opaque-type universe provided.</li>
--   </ol>
deriveFamilyWith :: Name -> Q Type -> Q [Dec]
deriveFamilyWithTy :: Q Type -> Q Type -> Q [Dec]
deriveFamily :: Q Type -> Q [Dec]

-- | Generates a bunch of strings for debug purposes.
genFamilyDebug :: STy -> [(STy, Int, DTI IK)] -> Q [Dec]
instance GHC.Show.Show Generics.MRSOP.TH.Idxs
instance GHC.Show.Show Generics.MRSOP.TH.IK
instance GHC.Classes.Eq Generics.MRSOP.TH.IK
instance GHC.Classes.Ord Generics.MRSOP.TH.STy
instance GHC.Show.Show Generics.MRSOP.TH.STy
instance GHC.Classes.Eq Generics.MRSOP.TH.STy
instance GHC.Base.Functor Generics.MRSOP.TH.DTI
instance GHC.Show.Show ty => GHC.Show.Show (Generics.MRSOP.TH.DTI ty)
instance GHC.Classes.Eq ty => GHC.Classes.Eq (Generics.MRSOP.TH.DTI ty)
instance GHC.Base.Functor Generics.MRSOP.TH.CI
instance GHC.Show.Show ty => GHC.Show.Show (Generics.MRSOP.TH.CI ty)
instance GHC.Classes.Eq ty => GHC.Classes.Eq (Generics.MRSOP.TH.CI ty)
instance GHC.Show.Show Generics.MRSOP.TH.OpaqueData
instance GHC.Classes.Eq Generics.MRSOP.TH.OpaqueData


-- | A collection of combinators for operating over sums of products.
module Generics.MRSOP.Base.Combinators

-- | Given a way to compare the constant types within two values, compare
--   the outer values for syntatical equality.
geq :: forall ki fam codes ix. Family ki fam codes => (forall k. ki k -> ki k -> Bool) -> El fam ix -> El fam ix -> Bool

-- | Given a morphism for the <tt>iy</tt> element of the family, applies it
--   everywhere in another element of the family.
composM :: forall ki fam codes ix m. (Monad m, Family ki fam codes, IsNat ix) => (forall iy. IsNat iy => SNat iy -> El fam iy -> m (El fam iy)) -> El fam ix -> m (El fam ix)

-- | Non monadic version from above.
compos :: forall ki fam codes ix. (Family ki fam codes, IsNat ix) => (forall iy. IsNat iy => SNat iy -> El fam iy -> El fam iy) -> El fam ix -> El fam ix

-- | <a>crushM</a> Applies its first parameter to all leaves, combines the
--   results with its second parameter.
crushM :: forall ki fam codes ix r m. (Monad m, Family ki fam codes) => (forall k. ki k -> m r) -> ([r] -> m r) -> El fam ix -> m r

-- | Non-monadic version
crush :: forall ki fam codes ix r. Family ki fam codes => (forall k. ki k -> r) -> ([r] -> r) -> El fam ix -> r


-- | Re-exports everything from under <tt>Generics.MRSOP.Base</tt>
module Generics.MRSOP.Base


-- | Usage example with template haskell support.
module Generics.MRSOP.Examples.RoseTreeTH

-- | Rose trees with redundancy.
data Rose a
(:>:) :: a -> [Rose a] -> Rose a
Leaf :: a -> Rose a

-- | Sample values.
value1 :: Rose Int

-- | Sample values.
value2 :: Rose Int

-- | Sample values.
value3 :: Rose Int
value4 :: Rose Int
type FamRoseInt = '[Rose Int, [Rose Int]]
type CodesRoseInt = '['['[ 'K  'KInt,  'I ( 'S  'Z)], '[ 'K  'KInt]], '['[], '[ 'I  'Z,  'I ( 'S  'Z)]]]
pattern ListRoseInt_Ifx1 :: phi_ayyY  'Z -> phi_ayyY ( 'S  'Z) -> View kon_ayyZ phi_ayyY (Lkup ( 'S  'Z) CodesRoseInt)
pattern ListRoseInt_Ifx0 :: View kon_ayyV phi_ayyU (Lkup ( 'S  'Z) CodesRoseInt)
pattern RoseIntLeaf_ :: kon_ayyT  'KInt -> View kon_ayyT phi_ayyS (Lkup  'Z CodesRoseInt)
pattern RoseInt_Ifx0 :: kon_ayyQ  'KInt -> phi_ayyP ( 'S  'Z) -> View kon_ayyQ phi_ayyP (Lkup  'Z CodesRoseInt)
pattern IdxListRoseInt :: forall (a :: Nat). () => forall (n :: Nat). (a ~# S n, n ~# Z) => SNat a
pattern IdxRoseInt :: forall (a :: Nat). () => a ~# Z => SNat a
tyInfo_1 :: [Char]
tyInfo_0 :: [Char]

-- | Equality test; should return <a>True</a>!
testEq :: Bool

-- | This function removes the redundant <a>Leaf</a> constructor by the
--   means of a <a>compos</a>. Check the source for details.
normalize :: Rose Int -> Rose Int

-- | Sums up the values in a rose tree using a <a>crush</a>
sumTree :: Rose Int -> Int

-- | The sum of a tree should be the same as the sum of a normalized tree;
--   This should return <a>True</a>.
testSum :: Bool
instance Generics.MRSOP.Base.Class.Family Generics.MRSOP.Opaque.Singl Generics.MRSOP.Examples.RoseTreeTH.FamRoseInt Generics.MRSOP.Examples.RoseTreeTH.CodesRoseInt
instance Generics.MRSOP.Base.Metadata.HasDatatypeInfo Generics.MRSOP.Opaque.Singl Generics.MRSOP.Examples.RoseTreeTH.FamRoseInt Generics.MRSOP.Examples.RoseTreeTH.CodesRoseInt
instance GHC.Classes.Eq (Generics.MRSOP.Examples.RoseTreeTH.Rose GHC.Types.Int)
instance GHC.Show.Show a => GHC.Show.Show (Generics.MRSOP.Examples.RoseTreeTH.Rose a)


-- | This module is analogous to <a>RoseTreeTH</a>, but we use no Template
--   Haskell here.
module Generics.MRSOP.Examples.RoseTree
data R a
(:>:) :: a -> [R a] -> R a
Leaf :: a -> R a
value1 :: R Int
value2 :: R Int
value3 :: R Int
type ListCode = '['[], '[I (S Z), I Z]]
type RTCode = '['[K KInt, I Z], '[K KInt]]
type CodesRose = '[ListCode, RTCode]
type FamRose = '[[R Int], R Int]
testEq :: Bool
pattern RInt_ :: forall (a :: Nat). () => forall (n :: Nat). (a ~# S n, n ~# Z) => SNat a
normalize :: R Int -> R Int
sumTree :: R Int -> Int
testSum :: Bool
instance GHC.Show.Show a => GHC.Show.Show (Generics.MRSOP.Examples.RoseTree.R a)
instance Generics.MRSOP.Base.Class.Family Generics.MRSOP.Opaque.Singl Generics.MRSOP.Examples.RoseTree.FamRose Generics.MRSOP.Examples.RoseTree.CodesRose
instance Generics.MRSOP.Base.Metadata.HasDatatypeInfo Generics.MRSOP.Opaque.Singl Generics.MRSOP.Examples.RoseTree.FamRose Generics.MRSOP.Examples.RoseTree.CodesRose
instance GHC.Classes.Eq (Generics.MRSOP.Examples.RoseTree.R GHC.Types.Int)


-- | Provide a generic alpha equality decider for the lambda calculus.
module Generics.MRSOP.Examples.LambdaAlphaEqTH

-- | Standard Lambda Calculus.
data Term
Var :: String -> Term
Abs :: String -> Term -> Term
App :: Term -> Term -> Term
type FamTerm = '[Term]
type CodesTerm = '['['[ 'K  'KString], '[ 'K  'KString,  'I  'Z], '[ 'I  'Z,  'I  'Z]]]
pattern App_ :: phi_aBaP  'Z -> phi_aBaP  'Z -> View kon_aBaQ phi_aBaP (Lkup  'Z CodesTerm)
pattern Abs_ :: kon_aBaM  'KString -> phi_aBaL  'Z -> View kon_aBaM phi_aBaL (Lkup  'Z CodesTerm)
pattern Var_ :: kon_aBaI  'KString -> View kon_aBaI phi_aBaH (Lkup  'Z CodesTerm)
pattern IdxTerm :: forall (a :: Nat). () => a ~# Z => SNat a
tyInfo_0 :: [Char]

-- | Interface needed for deciding alpha equivalence.
class Monad m => MonadAlphaEq m

-- | Runs a computation under a new scope.
onNewScope :: MonadAlphaEq m => m a -> m a

-- | Registers a name equivalence under the current scope.
addRule :: MonadAlphaEq m => String -> String -> m ()

-- | Checks for a name equivalence under all scopes.
(=~=) :: MonadAlphaEq m => String -> String -> m Bool
onHead :: (a -> a) -> [a] -> [a]

-- | Given a list of scopes, which consist in a list of pairs each, checks
--   whether or not two names are equivalent.
onScope :: String -> String -> [[(String, String)]] -> Bool

-- | Runs a computation.
runAlpha :: State [[(String, String)]] a -> a
type FIX = Fix Singl CodesTerm

-- | Decides whether or not two terms are alpha equivalent.
alphaEq :: Term -> Term -> Bool
t1 :: String -> String -> Term
t2 :: String -> String -> String -> Char -> Term
instance Generics.MRSOP.Examples.LambdaAlphaEqTH.MonadAlphaEq (Control.Monad.Trans.State.Lazy.State [[(GHC.Base.String, GHC.Base.String)]])
instance Generics.MRSOP.Base.Class.Family Generics.MRSOP.Opaque.Singl Generics.MRSOP.Examples.LambdaAlphaEqTH.FamTerm Generics.MRSOP.Examples.LambdaAlphaEqTH.CodesTerm
instance Generics.MRSOP.Base.Metadata.HasDatatypeInfo Generics.MRSOP.Opaque.Singl Generics.MRSOP.Examples.LambdaAlphaEqTH.FamTerm Generics.MRSOP.Examples.LambdaAlphaEqTH.CodesTerm


-- | Attribute grammars over mutual recursive datatypes
module Generics.MRSOP.AG
zipAnn :: forall phi1 phi2 phi3 ki codes ix. (forall iy. phi1 iy -> phi2 iy -> phi3 iy) -> AnnFix ki codes phi1 ix -> AnnFix ki codes phi2 ix -> AnnFix ki codes phi3 ix
mapAnn :: (forall iy. chi iy -> phi iy) -> AnnFix ki codes chi ix -> AnnFix ki codes phi ix

-- | Inherited attributes
inheritAnn :: forall ki codes chi phi ix. (forall iy. chi iy -> Rep ki (Const ()) (Lkup iy codes) -> phi iy -> Rep ki phi (Lkup iy codes)) -> phi ix -> AnnFix ki codes chi ix -> AnnFix ki codes phi ix
inherit :: forall ki phi codes ix. (forall iy. Rep ki (Const ()) (Lkup iy codes) -> phi iy -> Rep ki phi (Lkup iy codes)) -> phi ix -> Fix ki codes ix -> AnnFix ki codes phi ix

-- | Synthesized attributes
synthesizeAnn :: forall ki codes chi phi ix. (forall iy. chi iy -> Rep ki phi (Lkup iy codes) -> phi iy) -> AnnFix ki codes chi ix -> AnnFix ki codes phi ix
synthesize :: forall ki phi codes ix. IsNat ix => (forall iy. IsNat iy => Rep ki phi (Lkup iy codes) -> phi iy) -> Fix ki codes ix -> AnnFix ki codes phi ix
monoidAlgebra :: Monoid m => Rep ki (Const m) xs -> Const m iy
sizeAlgebra :: Rep ki (Const (Sum Int)) xs -> Const (Sum Int) iy

-- | Annotate each node with the number of subtrees
sizeGeneric' :: IsNat ix => Fix ki codes ix -> AnnFix ki codes (Const (Sum Int)) ix

-- | Count the number of nodes
sizeGeneric :: IsNat ix => Fix ki codes ix -> Const (Sum Int) ix
instance GHC.Show.Show k2 => Generics.MRSOP.Util.Show1 (Data.Functor.Const.Const k2)
instance forall k (f :: k -> *) (g :: k -> *). (Generics.MRSOP.Util.Show1 f, Generics.MRSOP.Util.Show1 g) => Generics.MRSOP.Util.Show1 (Data.Functor.Product.Product f g)


-- | Provides Zippers (aka One-hole contexts) for our universe.
module Generics.MRSOP.Zipper

-- | In a <tt>Zipper</tt>, a Location is a a pair of a one hole context and
--   whatever was supposed to be there. In a sums of products fashion, it
--   consists of a choice of constructor and a position in the type of that
--   constructor.
data Loc :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> *
[Loc] :: IsNat ix => El fam ix -> Ctxs ki fam cs iy ix -> Loc ki fam cs iy

-- | A <tt>Ctxs ki fam codes ix iy</tt> represents a value of type <tt>El
--   fam ix</tt> with a <tt>El fam iy</tt>-typed hole in it.
data Ctxs :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> Nat -> *
[Nil] :: Ctxs ki fam cs ix ix
[Cons] :: (IsNat ix, IsNat a, IsNat b) => Ctx ki fam (Lkup ix cs) b -> Ctxs ki fam cs a ix -> Ctxs ki fam cs a b

-- | A <tt>Ctx ki fam c ix</tt> is a choice of constructor for <tt>c</tt>
--   with a hole of type <tt>ix</tt> inside.
data Ctx :: (kon -> *) -> [*] -> [[Atom kon]] -> Nat -> *
[Ctx] :: Constr c n -> NPHole ki fam ix (Lkup n c) -> Ctx ki fam c ix

-- | A <tt>NPHole ki fam ix prod</tt> is a recursive position of type
--   <tt>ix</tt> in <tt>prod</tt>.
data NPHole :: (kon -> *) -> [*] -> Nat -> [Atom kon] -> *
[H] :: PoA ki (El fam) xs -> NPHole ki fam ix (I ix : xs)
[T] :: NA ki (El fam) x -> NPHole ki fam ix xs -> NPHole ki fam ix (x : xs)

-- | Existential abstraction; needed for walking the possible holes in a
--   product. We must be able to hide the type.
data NPHoleE :: (kon -> *) -> [*] -> [Atom kon] -> *
[ExistsIX] :: IsNat ix => El fam ix -> NPHole ki fam ix xs -> NPHoleE ki fam xs

-- | Given a <a>PoA</a> (product of atoms), returns a one with a hole in
--   the first seen <a>NA_I</a>. Note that we need the <a>NPHoleE</a> with
--   the existential because we don't know, a priori, what will be the type
--   of such hole.
mkNPHole :: PoA ki (El fam) xs -> Maybe (NPHoleE ki fam xs)

-- | Given a hole and an element, put both together to form the <a>PoA</a>
--   again.
fillNPHole :: IsNat ix => El fam ix -> NPHole ki fam ix xs -> PoA ki (El fam) xs

-- | Given an hole and an element, return the next hole, if any.
walkNPHole :: IsNat ix => El fam ix -> NPHole ki fam ix xs -> Maybe (NPHoleE ki fam xs)

-- | Executes an action in the first hole within the given <a>Rep</a>
--   value, if such hole can be constructed.
first :: (forall ix. IsNat ix => El fam ix -> Ctx ki fam c ix -> a) -> Rep ki (El fam) c -> Maybe a

-- | Fills up a hole.
fill :: IsNat ix => El fam ix -> Ctx ki fam c ix -> Rep ki (El fam) c

-- | Recursively fills a stack of holes however, the Family constraint
--   ain't so nice. so we perhaps want to take zippers over a deep
--   representation
fillCtxs :: forall ix fam iy ki c. (IsNat ix, Family ki fam c) => El fam iy -> Ctxs ki fam c ix iy -> El fam ix

-- | Walks to the next hole and execute an action.
next :: IsNat ix => (forall iy. IsNat iy => El fam iy -> Ctx ki fam c iy -> a) -> El fam ix -> Ctx ki fam c ix -> Maybe a

-- | Move one layer deeper within the recursive structure.
down :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)

-- | Move one layer upwards within the recursive structure
up :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)

-- | More one hole to the right
right :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)

-- | Initializes the zipper
enter :: (Family ki fam codes, IsNat ix) => El fam ix -> Loc ki fam codes ix

-- | Exits the zipper
leave :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> El fam ix

-- | Updates the value in the hole.
update :: (Family ki fam codes, IsNat ix) => (forall ix. SNat ix -> El fam ix -> El fam ix) -> Loc ki fam codes ix -> Loc ki fam codes ix


-- | Uses a more involved example to test some of the functionalities of
--   <tt>generics-mrsop</tt>.
module Generics.MRSOP.Examples.SimpTH
data Stmt var
SAssign :: var -> Exp var -> Stmt var
SIf :: Exp var -> Stmt var -> Stmt var -> Stmt var
SSeq :: Stmt var -> Stmt var -> Stmt var
SReturn :: Exp var -> Stmt var
SDecl :: Decl var -> Stmt var
SSkip :: Stmt var
data Decl var
DVar :: var -> Decl var
DFun :: var -> var -> Stmt var -> Decl var
data Exp var
EVar :: var -> Exp var
ECall :: var -> Exp var -> Exp var
EAdd :: Exp var -> Exp var -> Exp var
ESub :: Exp var -> Exp var -> Exp var
ELit :: Int -> Exp var
type FamStmtString = '[Stmt String, Exp String, Decl String]
type CodesStmtString = '['['[ 'K  'KString,  'I ( 'S  'Z)], '[ 'I ( 'S  'Z),  'I  'Z,  'I  'Z], '[ 'I  'Z,  'I  'Z], '[ 'I ( 'S  'Z)], '[ 'I ( 'S ( 'S  'Z))], '[]], '['[ 'K  'KString], '[ 'K  'KString,  'I ( 'S  'Z)], '[ 'I ( 'S  'Z),  'I ( 'S  'Z)], '[ 'I ( 'S  'Z),  'I ( 'S  'Z)], '[ 'K  'KInt]], '['[ 'K  'KString], '[ 'K  'KString,  'K  'KString,  'I  'Z]]]
pattern DeclStringDFun_ :: kon_aG17  'KString -> kon_aG17  'KString -> phi_aG16  'Z -> View kon_aG17 phi_aG16 (Lkup ( 'S ( 'S  'Z)) CodesStmtString)
pattern DeclStringDVar_ :: kon_aG12  'KString -> View kon_aG12 phi_aG11 (Lkup ( 'S ( 'S  'Z)) CodesStmtString)
pattern ExpStringELit_ :: kon_aG0Z  'KInt -> View kon_aG0Z phi_aG0Y (Lkup ( 'S  'Z) CodesStmtString)
pattern ExpStringESub_ :: phi_aG0V ( 'S  'Z) -> phi_aG0V ( 'S  'Z) -> View kon_aG0W phi_aG0V (Lkup ( 'S  'Z) CodesStmtString)
pattern ExpStringEAdd_ :: phi_aG0R ( 'S  'Z) -> phi_aG0R ( 'S  'Z) -> View kon_aG0S phi_aG0R (Lkup ( 'S  'Z) CodesStmtString)
pattern ExpStringECall_ :: kon_aG0O  'KString -> phi_aG0N ( 'S  'Z) -> View kon_aG0O phi_aG0N (Lkup ( 'S  'Z) CodesStmtString)
pattern ExpStringEVar_ :: kon_aG0K  'KString -> View kon_aG0K phi_aG0J (Lkup ( 'S  'Z) CodesStmtString)
pattern StmtStringSSkip_ :: View kon_aG0H phi_aG0G (Lkup  'Z CodesStmtString)
pattern StmtStringSDecl_ :: phi_aG0E ( 'S ( 'S  'Z)) -> View kon_aG0F phi_aG0E (Lkup  'Z CodesStmtString)
pattern StmtStringSReturn_ :: phi_aG0B ( 'S  'Z) -> View kon_aG0C phi_aG0B (Lkup  'Z CodesStmtString)
pattern StmtStringSSeq_ :: phi_aG0y  'Z -> phi_aG0y  'Z -> View kon_aG0z phi_aG0y (Lkup  'Z CodesStmtString)
pattern StmtStringSIf_ :: phi_aG0u ( 'S  'Z) -> phi_aG0u  'Z -> phi_aG0u  'Z -> View kon_aG0v phi_aG0u (Lkup  'Z CodesStmtString)
pattern StmtStringSAssign_ :: kon_aG0q  'KString -> phi_aG0p ( 'S  'Z) -> View kon_aG0q phi_aG0p (Lkup  'Z CodesStmtString)
pattern IdxDeclString :: forall (a :: Nat). () => forall (n :: Nat) (n1 :: Nat). (a ~# S n, n ~# S n1, n1 ~# Z) => SNat a
pattern IdxExpString :: forall (a :: Nat). () => forall (n :: Nat). (a ~# S n, n ~# Z) => SNat a
pattern IdxStmtString :: forall (a :: Nat). () => a ~# Z => SNat a
tyInfo_2 :: [Char]
tyInfo_1 :: [Char]
tyInfo_0 :: [Char]
type FIX = Fix Singl CodesStmtString
alphaEqD :: Decl String -> Decl String -> Bool
test1 :: String -> String -> String -> Decl String
test2 :: String -> String -> String -> Decl String
test3 :: String -> String -> String -> Decl String
(>>>) :: (a -> b) -> (b -> c) -> a -> c
infixr 4 >>>
test4 :: Int -> Decl String
test5 :: Maybe (Decl String)
instance Generics.MRSOP.Base.Class.Family Generics.MRSOP.Opaque.Singl Generics.MRSOP.Examples.SimpTH.FamStmtString Generics.MRSOP.Examples.SimpTH.CodesStmtString
instance Generics.MRSOP.Base.Metadata.HasDatatypeInfo Generics.MRSOP.Opaque.Singl Generics.MRSOP.Examples.SimpTH.FamStmtString Generics.MRSOP.Examples.SimpTH.CodesStmtString
instance GHC.Show.Show var => GHC.Show.Show (Generics.MRSOP.Examples.SimpTH.Decl var)
instance GHC.Show.Show var => GHC.Show.Show (Generics.MRSOP.Examples.SimpTH.Stmt var)
instance GHC.Show.Show var => GHC.Show.Show (Generics.MRSOP.Examples.SimpTH.Exp var)


-- | Provides one-hole contexts for our universe, but over deep encoded
--   datatypes. These are a bit easier to use computationally.
--   
--   This module follows the very same structure as <a>Zipper</a>. Refer
--   there for further documentation.
module Generics.MRSOP.Zipper.Deep

-- | Analogous to <a>Ctxs</a>
data Ctxs (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> Nat -> *
[Nil] :: Ctxs ki codes ix ix
[Cons] :: (IsNat ix, IsNat a, IsNat b) => Ctx ki codes (Lkup ix codes) b -> Ctxs ki codes a ix -> Ctxs ki codes a b

-- | Analogous to <a>Ctx</a>
data Ctx (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [[Atom kon]] -> Nat -> *
[Ctx] :: Constr c n -> NPHole ki codes ix (Lkup n c) -> Ctx ki codes c ix

-- | Analogous to <a>NPHole</a>, but uses a deep representation for generic
--   values.
data NPHole (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> [Atom kon] -> *
[H] :: PoA ki (Fix ki codes) xs -> NPHole ki codes ix ( 'I ix : xs)
[T] :: NA ki (Fix ki codes) x -> NPHole ki codes ix xs -> NPHole ki codes ix (x : xs)
getCtxsIx :: Ctxs ki codes iy ix -> Proxy ix

-- | Given a product with a hole in it, and an element, get back a product
--   
--   dual of <a>removeNPHole</a>
fillNPHole :: IsNat ix => Fix ki codes ix -> NPHole ki codes ix xs -> PoA ki (Fix ki codes) xs

-- | Given a value that fits in a context, fills the context hole.
fillCtxs :: IsNat ix => Fix ki codes iy -> Ctxs ki codes ix iy -> Fix ki codes ix
fillCtx :: IsNat ix => Fix ki codes ix -> Ctx ki codes c ix -> Rep ki (Fix ki codes) c

-- | Given a value and a context, tries to match to context in the value
--   and, upon success, returns whatever overlaps with the hole.
removeCtxs :: (Eq1 ki, IsNat ix) => Ctxs ki codes ix iy -> Fix ki codes ix -> Maybe (Fix ki codes iy)
removeCtx :: forall ix ki codes c. (Eq1 ki, IsNat ix) => Rep ki (Fix ki codes) c -> Ctx ki codes c ix -> Maybe (Fix ki codes ix)
removeNPHole :: (Eq1 ki, IsNat ix) => NPHole ki codes ix xs -> PoA ki (Fix ki codes) xs -> Maybe (Fix ki codes ix)
