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


-- | Generic programming without too many type classes
--   
--   This library provides a representation build on top of
--   <a>GHC.Generics</a>, which can be used to describe generic operations
--   on a single function, instead of having each case defined in an
--   instance of a type class.
@package simplistic-generics
@version 2.0.0

module Generics.Simplistic.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 <.>

-- | Products: encode multiple arguments to constructors
data ( (f :: k -> Type) :*: (g :: k -> Type) ) (p :: k)
(:*:) :: f p -> g p -> (:*:) (f :: k -> Type) (g :: k -> Type) (p :: k)
infixr 6 :*:
infixr 6 :*:

-- | Diagonal indexed functor
type Delta f = f :*: f

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

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

-- | Duplicates its argument
delta :: f :-> Delta f

-- | Applies the same function to both components of the pair
deltaMap :: (f :-> g) -> Delta f :-> Delta g

-- | Lifted sum of functors.
data Sum (f :: k -> Type) (g :: k -> Type) (a :: k)
InL :: f a -> Sum (f :: k -> Type) (g :: k -> Type) (a :: k)
InR :: g a -> Sum (f :: k -> Type) (g :: k -> Type) (a :: k)

-- | Higher-order sum eliminator
either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r

-- | Just like <a>either'</a>, but the result type is of kind Star
either'' :: (forall x. f x -> a) -> (forall y. g y -> a) -> Sum f g r -> a

-- | Constraint implication
class (c => d) => Implies c d

-- | Trivial constraint
class Trivial c

-- | Higher order , poly kinded, version of <a>Eq</a>
class EqHO (f :: ki -> *)
eqHO :: forall k. EqHO f => f k -> f k -> Bool

-- | Higher order, poly kinded, version of <a>Show</a>; We provide the same
--   <a>showsPrec</a> mechanism. The documentation of <a>Text.Show</a> has
--   a good example of the correct usage of <a>showsPrec</a>:
--   
--   <pre>
--   infixr 5 :^:
--   data Tree a =  Leaf a  |  Tree a :^: Tree a
--   
--   instance (Show a) =&gt; Show (Tree a) where
--     showsPrec d (Leaf m) = showParen (d &gt; app_prec) $
--          showString "Leaf " . showsPrec (app_prec+1) m
--       where app_prec = 10
--   
--     showsPrec d (u :^: v) = showParen (d &gt; up_prec) $
--          showsPrec (up_prec+1) u .
--          showString " :^: "      .
--          showsPrec (up_prec+1) v
--       where up_prec = 5
--   </pre>
class ShowHO (f :: ki -> *)
showHO :: forall k. ShowHO f => f k -> String
showsPrecHO :: forall k. ShowHO f => Int -> f k -> ShowS

-- | Existential type wrapper. This comesin particularly handy when we want
--   to add mrsop terms to some container. See
--   <a>Generics.MRSOP.Holes.Unify</a> for example.
data Exists (f :: k -> *) :: *
[Exists] :: f x -> Exists f

-- | Maps over <a>Exists</a>
exMap :: (forall x. f x -> g x) -> Exists f -> Exists g

-- | Maps a monadic actino over <a>Exists</a>
exMapM :: Monad m => (forall x. f x -> m (g x)) -> Exists f -> m (Exists g)

-- | eliminates an <a>Exists</a>
exElim :: (forall x. f x -> a) -> Exists f -> a

-- | We will carry constructive information on the constraint. Forcing
--   <a>IsElem</a> to true
type Elem a as = (IsElem a as ~ 'True, HasElem a as)

-- | Negation of <a>Elem</a>
type NotElem a as = IsElem a as ~ 'False
class HasElem a as
hasElem :: HasElem a as => ElemPrf a as
data ElemPrf a as
[Here] :: ElemPrf a (a : as)
[There] :: ElemPrf a as -> ElemPrf a (b : as)
type family IsElem (a :: k) (as :: [k]) :: Bool

-- | Returns whether two types are the same, given that both belong to the
--   same list.
sameTy :: forall fam x y. (Elem x fam, Elem y fam) => Proxy fam -> Proxy x -> Proxy y -> Maybe (x :~: y)
type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint

-- | Carries information about <tt>x</tt> being an instance of <tt>c</tt>
data Witness c x
[Witness] :: c x => Witness c x

-- | Provides the witness that <tt>x</tt> is an instance of <tt>c</tt>
witness :: forall x xs c. (HasElem x xs, All c xs) => Proxy xs -> Witness c x

-- | Provides the witness that <tt>x</tt> is an instance of <tt>c</tt>
witnessPrf :: All c xs => ElemPrf x xs -> Witness c x

-- | Fetches the <a>Eq</a> instance for an element of a list
weq :: forall x xs. (All Eq xs, Elem x xs) => Proxy xs -> x -> x -> Bool

-- | Fetches the <a>Eq</a> instance for an element of a list
wshow :: forall x xs. (All Show xs, Elem x xs) => Proxy xs -> x -> String
instance forall a1 (a2 :: a1) (as :: [a1]). Generics.Simplistic.Util.HasElem a2 (a2 : as)
instance forall a1 (a2 :: a1) (as :: [a1]) (b :: a1). Generics.Simplistic.Util.HasElem a2 as => Generics.Simplistic.Util.HasElem a2 (b : as)
instance forall k (f :: k -> *). Generics.Simplistic.Util.ShowHO f => GHC.Show.Show (Generics.Simplistic.Util.Exists f)
instance GHC.Show.Show a => Generics.Simplistic.Util.ShowHO (Data.Functor.Const.Const a)
instance forall ki (f :: ki -> *) (g :: ki -> *). (Generics.Simplistic.Util.ShowHO f, Generics.Simplistic.Util.ShowHO g) => Generics.Simplistic.Util.ShowHO (f GHC.Generics.:*: g)
instance forall ki (f :: ki -> *) (g :: ki -> *). (Generics.Simplistic.Util.ShowHO f, Generics.Simplistic.Util.ShowHO g) => Generics.Simplistic.Util.ShowHO (Data.Functor.Sum.Sum f g)
instance GHC.Classes.Eq a => Generics.Simplistic.Util.EqHO (Data.Functor.Const.Const a)
instance forall ki (f :: ki -> *) (g :: ki -> *). (Generics.Simplistic.Util.EqHO f, Generics.Simplistic.Util.EqHO g) => Generics.Simplistic.Util.EqHO (f GHC.Generics.:*: g)
instance forall ki (f :: ki -> *) (g :: ki -> *). (Generics.Simplistic.Util.EqHO f, Generics.Simplistic.Util.EqHO g) => Generics.Simplistic.Util.EqHO (Data.Functor.Sum.Sum f g)
instance Generics.Simplistic.Util.EqHO GHC.Generics.V1
instance Generics.Simplistic.Util.EqHO GHC.Generics.U1
instance forall k (c :: k). Generics.Simplistic.Util.Trivial c
instance (c => d) => Generics.Simplistic.Util.Implies c d


-- | Introduces closed representations functor for <a>GHC.Generics</a>
--   style generics.
module Generics.Simplistic

-- | Representable types of kind <tt>*</tt>. This class is derivable in GHC
--   with the <tt>DeriveGeneric</tt> flag on.
--   
--   A <a>Generic</a> instance must satisfy the following laws:
--   
--   <pre>
--   <a>from</a> . <a>to</a> ≡ <a>id</a>
--   <a>to</a> . <a>from</a> ≡ <a>id</a>
--   </pre>
class Generic a

-- | Generic representation type
type family Rep a :: Type -> Type

-- | Generic representation type
type family Rep1 (f :: k -> Type) :: k -> Type

-- | Used for marking occurrences of the parameter
data Par1 p

-- | Recursive calls of kind <tt>* -&gt; *</tt> (or kind <tt>k -&gt;
--   *</tt>, when <tt>PolyKinds</tt> is enabled)
data Rec1 (f :: k -> Type) (p :: k)

-- | Composition of functors
newtype ( (f :: k2 -> Type) :.: (g :: k1 -> k2) ) (p :: k1)
Comp1 :: f (g p) -> (:.:) (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1)
[unComp1] :: (:.:) (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1) -> f (g p)
infixr 7 :.:

-- | Void: used for datatypes without constructors
data V1 (p :: k)

-- | Unit: used for constructors without arguments
data U1 (p :: k)
U1 :: U1 (p :: k)

-- | Sums: encode choice between constructors
data ( (f :: k -> Type) :+: (g :: k -> Type) ) (p :: k)
L1 :: f p -> (:+:) (f :: k -> Type) (g :: k -> Type) (p :: k)
R1 :: g p -> (:+:) (f :: k -> Type) (g :: k -> Type) (p :: k)
infixr 5 :+:

-- | Products: encode multiple arguments to constructors
data ( (f :: k -> Type) :*: (g :: k -> Type) ) (p :: k)
(:*:) :: f p -> g p -> (:*:) (f :: k -> Type) (g :: k -> Type) (p :: k)
infixr 6 :*:
infixr 6 :*:

-- | Constants, additional parameters and recursion of kind <tt>*</tt>
newtype K1 i c (p :: k)
K1 :: c -> K1 i c (p :: k)
[unK1] :: K1 i c (p :: k) -> c

-- | Meta-information (constructor names, etc.)
newtype M1 i (c :: Meta) (f :: k -> Type) (p :: k)
M1 :: f p -> M1 i (c :: Meta) (f :: k -> Type) (p :: k)
[unM1] :: M1 i (c :: Meta) (f :: k -> Type) (p :: k) -> f p

-- | Constraints: used to represent constraints in a constructor.
--   
--   <pre>
--   data Showable a = Show a =&gt; a -&gt; X a
--   
--   instance Generic (Showable a) where
--     type Rep (Showable a) = (Show a) :=&gt;: (K1 R a)
--   </pre>
data ( c :=>: (f :: k -> Type) ) (a :: k)
[SuchThat] :: forall k c (f :: k -> Type) (a :: k). c => f a -> (c :=>: f) a

-- | Tag for K1: recursion (of kind <tt>Type</tt>)
data R

-- | Singletons for metainformation
class GMeta i c
smeta :: GMeta i c => SMeta i c
data SMeta i t
[SM_D] :: Datatype d => SMeta D d
[SM_C] :: Constructor c => SMeta C c
[SM_S] :: Selector s => SMeta S s
data SMetaI d f x
SMetaI :: SMetaI d f x

-- | Given some <tt>a</tt>, a value of type <tt>SRep w (Rep a)</tt> is a
--   closed representation of a generic value of type <tt>a</tt>.
data SRep w f
[S_U1] :: SRep w U1
[S_L1] :: SRep w f -> SRep w (f :+: g)
[S_R1] :: SRep w g -> SRep w (f :+: g)
[:**:] :: SRep w f -> SRep w g -> SRep w (f :*: g)
[S_K1] :: w a -> SRep w (K1 i a)
[S_M1] :: SMeta i t -> SRep w f -> SRep w (M1 i t f)
[S_ST] :: c => SRep w f -> SRep w (c :=>: f)
infixr 5 :**:

-- | Identity functor
newtype I x
I :: x -> I x
[unI] :: I x -> x

-- | All types supported by <a>GHC.Generics</a> are <i>simplistic</i>, this
--   constraint just couples their necessary together.
type Simplistic a = (Generic a, GShallow (Rep a))

-- | Computes the constraint that corresponds to ensuring all leaves of a
--   representation satisfy a given constraint. For example,
--   
--   <pre>
--   OnLeaves Eq (Rep (Either a b)) = (Eq a , Eq b)
--   </pre>
type family OnLeaves (c :: * -> Constraint) (f :: * -> *) :: Constraint

-- | Maps a simple functino over the representation
repMap :: (forall y. f y -> g y) -> SRep f rep -> SRep g rep

-- | Maps a monadic function over the representation
repMapM :: Monad m => (forall y. f y -> m (g y)) -> SRep f rep -> m (SRep g rep)

-- | Maps a function over a representation taking into account that the
--   leaves of the representation satisfy a given constraint.
repMapCM :: (Monad m, OnLeaves c rep) => Proxy c -> (forall y. c y => f y -> m (g y)) -> SRep f rep -> m (SRep g rep)

-- | Zips two representations together if they are made up of the same
--   constructor. For example,
--   
--   <pre>
--   zipSRep (fromS (: 1 [])) (fromS (: 2 (: 3 [])))
--    == Just (fromS (: (1 , 2) ([] , [3])))
--   
--   zipSRep (fromS (: 1 [])) (fromS [])
--    == Nothing
--   </pre>
zipSRep :: SRep w f -> SRep z f -> Maybe (SRep (w :*: z) f)

-- | Performs a <i>crush</i> over the leaves of a <a>SRep</a>
repLeaves :: (forall x. w x -> r) -> (r -> r -> r) -> r -> SRep w rep -> r

-- | Performs a <i>crush</i> over the leaves of a <a>SRep</a> carrying a
--   constraint around.
repLeavesC :: OnLeaves c rep => Proxy c -> (forall x. c x => w x -> r) -> (r -> r -> r) -> r -> SRep w rep -> r

-- | Example of <a>repLeaves</a> that places the values of <tt>w</tt>
--   inside a list.
repLeavesList :: SRep w rep -> [Exists w]
getDatatypeName :: SMeta D d -> String
getConstructorName :: SMeta C c -> String

-- | Retrieves the datatype name for a representation. <i>WARNING;
--   UNSAFE</i> this function only works if <tt>f</tt> is the
--   representation of a type constructed with <a>GHC.Generics</a> builtin
--   mechanisms.
repDatatypeName :: SRep w f -> String

-- | Retrieves the constructor name for a representation. <i>WARNING;
--   UNSAFE</i> this function only works if <tt>f</tt> is the
--   representation of a type constructed with <a>GHC.Generics</a> builtin
--   mechanisms.
repConstructorName :: SRep w f -> String

-- | Converts a value of a generic type directly to its (shallow)
--   simplistic representation.
fromS :: Simplistic a => a -> SRep I (Rep a)

-- | Converts a simplistic representation back to its corresponding value
--   of type <tt>a</tt>.
toS :: Simplistic a => SRep I (Rep a) -> a

-- | Shallow conversion between <a>GHC.Generics</a> representation and
--   <a>SRep</a>; The <a>fromS</a> and <a>toS</a> functions provide the
--   toplevel api.
class GShallow f
sfrom :: GShallow f => f x -> SRep I f
sto :: GShallow f => SRep I f -> f x

-- | Similar to <a>SRep</a>, but is indexed over the functors that make up
--   a <a>Rep1</a>, used to explicitely encode types with one parameter.
data SRep1 f x
[S1_U1] :: SRep1 U1 x
[S1_L1] :: SRep1 f x -> SRep1 (f :+: g) x
[S1_R1] :: SRep1 g x -> SRep1 (f :+: g) x
[:***:] :: SRep1 f x -> SRep1 g x -> SRep1 (f :*: g) x
[S1_K1] :: a -> SRep1 (K1 i a) x
[S1_M1] :: SMeta i t -> SRep1 f x -> SRep1 (M1 i t f) x
[S1_ST] :: c => SRep1 f x -> SRep1 (c :=>: f) x
[S1_Par] :: x -> SRep1 Par1 x
[S1_Rec] :: f x -> SRep1 (Rec1 f) x
[S1_Comp] :: f (SRep1 g x) -> SRep1 (f :.: g) x
infixr 5 :***:
type family OnLeaves1 (c :: * -> Constraint) (r :: (* -> *) -> Constraint) (f :: * -> *) :: Constraint

-- | Converts a value of a generic type directly to its (shallow)
--   simplistic1 representation with a parameter.
fromS1 :: Simplistic1 f => f x -> SRep1 (Rep1 f) x

-- | Converts a simplistic1 representation back to its corresponding value
--   of type <tt>a</tt>.
toS1 :: Simplistic1 f => SRep1 (Rep1 f) x -> f x
class GShallow1 f
sfrom1 :: GShallow1 f => f a -> SRep1 f a
sto1 :: GShallow1 f => SRep1 f a -> f a
type Simplistic1 f = (Generic1 f, GShallow1 (Rep1 f))

-- | Constraint implication
class (c => d) => Implies c d

-- | Trivial constraint
class Trivial c
instance GHC.Classes.Eq x => GHC.Classes.Eq (Generics.Simplistic.I x)
instance forall k i (t :: k). GHC.Show.Show (Generics.Simplistic.SMeta i t)
instance forall k i (t :: k). GHC.Classes.Eq (Generics.Simplistic.SMeta i t)
instance forall k (w :: * -> *) (f :: k -> *). (forall a. GHC.Show.Show (w a)) => GHC.Show.Show (Generics.Simplistic.SRep w f)
instance forall k (w :: * -> *) (f :: k -> *). (forall a. GHC.Classes.Eq (w a)) => GHC.Classes.Eq (Generics.Simplistic.SRep w f)
instance Generics.Simplistic.GShallow1 GHC.Generics.V1
instance Generics.Simplistic.GShallow1 GHC.Generics.U1
instance (Generics.Simplistic.GShallow1 f, Generics.Simplistic.GShallow1 g) => Generics.Simplistic.GShallow1 (f GHC.Generics.:+: g)
instance (Generics.Simplistic.GShallow1 f, Generics.Simplistic.GShallow1 g) => Generics.Simplistic.GShallow1 (f GHC.Generics.:*: g)
instance Generics.Simplistic.GShallow1 (GHC.Generics.K1 i a)
instance (Generics.Simplistic.GMeta i t, Generics.Simplistic.GShallow1 f) => Generics.Simplistic.GShallow1 (GHC.Generics.M1 i t f)
instance (c => Generics.Simplistic.GShallow1 f) => Generics.Simplistic.GShallow1 (c GHC.Generics.Extra.:=>: f)
instance Generics.Simplistic.GShallow1 GHC.Generics.Par1
instance Generics.Simplistic.GShallow1 (GHC.Generics.Rec1 f)
instance (GHC.Base.Functor f, Generics.Simplistic.GShallow1 g) => Generics.Simplistic.GShallow1 (f GHC.Generics.:.: g)
instance Generics.Simplistic.GShallow GHC.Generics.U1
instance forall k (f :: k -> *) (g :: k -> *). (Generics.Simplistic.GShallow f, Generics.Simplistic.GShallow g) => Generics.Simplistic.GShallow (f GHC.Generics.:+: g)
instance forall k (f :: k -> *) (g :: k -> *). (Generics.Simplistic.GShallow f, Generics.Simplistic.GShallow g) => Generics.Simplistic.GShallow (f GHC.Generics.:*: g)
instance forall k (f :: k -> *) i (c :: GHC.Generics.Meta). (Generics.Simplistic.GShallow f, Generics.Simplistic.GMeta i c) => Generics.Simplistic.GShallow (GHC.Generics.M1 i c f)
instance Generics.Simplistic.GShallow (GHC.Generics.K1 GHC.Generics.R x)
instance GHC.Show.Show x => GHC.Show.Show (Generics.Simplistic.I x)
instance GHC.Base.Functor Generics.Simplistic.I
instance GHC.Base.Applicative Generics.Simplistic.I
instance GHC.Base.Monad Generics.Simplistic.I
instance forall k (w :: * -> *) (f :: k -> *). (forall x. Control.DeepSeq.NFData (w x)) => Control.DeepSeq.NFData (Generics.Simplistic.SRep w f)
instance forall k (c :: k). GHC.Generics.Constructor c => Generics.Simplistic.GMeta GHC.Generics.C c
instance forall k (d :: k). GHC.Generics.Datatype d => Generics.Simplistic.GMeta GHC.Generics.D d
instance forall k (s :: k). GHC.Generics.Selector s => Generics.Simplistic.GMeta GHC.Generics.S s


-- | Derives a generic show, for example
--   
--   <pre>
--   data MyList a = MyNil | MyCons { hd :: a, tl :: MyList a } deriving Generic
--   
--   myListValue :: MyList Integer
--   myListValue = MyCons 1 (MyCons 2 (MyCons 3 MyNil))
--   
--   instance Show a =&gt; Show (MyList a) where
--     show = gshow
--   </pre>
--   
--   The code here was adapted from `generic-deriving`
--   <a>https://github.com/dreixel/generic-deriving/blob/master/src/Generics/Deriving/Show.hs</a>
module Generics.Simplistic.Derive.Show
gshow :: (Generic t, GShallow (Rep t), OnLeaves Show (Rep t)) => t -> String
gshowsPrec :: (Generic t, GShallow (Rep t), OnLeaves Show (Rep t)) => Type -> Int -> t -> ShowS

module Generics.Simplistic.Derive.Functor

-- | <a>SRep1</a> is a functor
gfmap' :: OnLeaves1 Trivial Functor f => (a -> b) -> SRep1 f a -> SRep1 f b

-- | The action of f over arrows can be obtained by translating into the
--   generic representation, using the generic <a>gfmap'</a> and
--   translating back to regular representation.
gfmap :: (Simplistic1 f, OnLeaves1 Trivial Functor (Rep1 f)) => (a -> b) -> f a -> f b

module Generics.Simplistic.Derive.Eq
geq' :: OnLeaves Eq f => SRep I f -> SRep I f -> Bool
geq :: (Generic a, GShallow (Rep a), OnLeaves Eq (Rep a)) => a -> a -> Bool


-- | Deep representation for <a>SRep</a>
module Generics.Simplistic.Deep

-- | The cofree comonad and free monad on the same type; this allows us to
--   use the same recursion operator for everything.
data HolesAnn kappa fam ann h a
[Hole'] :: ann a -> h a -> HolesAnn kappa fam ann h a
[Prim'] :: PrimCnstr kappa fam a => ann a -> a -> HolesAnn kappa fam ann h a
[Roll'] :: CompoundCnstr kappa fam a => ann a -> SRep (HolesAnn kappa fam ann h) (Rep a) -> HolesAnn kappa fam ann h a

-- | Deep representations are easily achieved by forbiding the <a>Hole'</a>
--   constructor and providing unit annotations.
type SFix kappa fam = HolesAnn kappa fam U1 V1
pattern SFix :: () => CompoundCnstr kappa fam a => SRep (SFix kappa fam) (Rep a) -> SFix kappa fam a
pattern Prim :: () => PrimCnstr kappa fam a => a -> Holes kappa fam h a

-- | Annotated fixpoints are also easy; forbid the <a>Hole'</a> constructor
--   but add something to every <a>Roll</a> of the representation.
type SFixAnn kappa fam ann = HolesAnn kappa fam ann V1
pattern SFixAnn :: () => CompoundCnstr kappa fam a => ann a -> SRep (SFixAnn kappa fam ann) (Rep a) -> SFixAnn kappa fam ann a
pattern PrimAnn :: () => PrimCnstr kappa fam a => ann a -> a -> SFixAnn kappa fam ann a

-- | A tree with holes has unit annotations
type Holes kappa fam = HolesAnn kappa fam U1
pattern Roll :: () => CompoundCnstr kappa fam a => SRep (Holes kappa fam h) (Rep a) -> Holes kappa fam h a
pattern Hole :: h a -> Holes kappa fam h a
type CompoundCnstr kappa fam a = (Elem a fam, NotElem a kappa, Generic a)
type PrimCnstr kappa fam b = (Elem b kappa, NotElem b fam)
holesToSFix :: Holes kappa fam V1 at -> SFix kappa fam at
sfixToHoles :: SFix kappa fam at -> Holes kappa fam h at

-- | Maps over holes and annotations in a <a>HolesAnn</a>
holesMapAnn :: (forall x. f x -> g x) -> (forall x. ann x -> phi x) -> HolesAnn kappa fam ann f a -> HolesAnn kappa fam phi g a

-- | Maps over the holes in a <a>HolesAnn</a>
holesMap :: (forall x. f x -> g x) -> HolesAnn kappa fam ann f a -> HolesAnn kappa fam ann g a

-- | Maps over <a>HolesAnn</a> maintaining annotations intact.
holesMapM :: Monad m => (forall x. f x -> m (g x)) -> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)

-- | Maps over a <a>HolesAnn</a> treating annotations and holes
--   independently.
holesMapAnnM :: Monad m => (forall x. f x -> m (g x)) -> (forall x. ann x -> m (psi x)) -> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam psi g a)

-- | Retrieves the annotation inside a <a>HolesAnn</a>; this is the counit
--   of the comonad.
getAnn :: HolesAnn kappa fam ann h a -> ann a

-- | Monadic multiplication
holesJoin :: HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a -> HolesAnn kappa fam ann f a

-- | Counts how many <a>Prim</a>s and <a>Roll</a>s are inside a
--   <a>HolesAnn</a>.
holesSize :: HolesAnn kappa fam ann h a -> Int

-- | Computes the list of holes in a <a>HolesAnn</a>
holesHolesList :: HolesAnn kappa fam ann f a -> [Exists f]

-- | Refine holes and primitives
holesRefineM :: Monad m => (forall b. f b -> m (Holes kappa fam g b)) -> (forall b. PrimCnstr kappa fam b => b -> m (Holes kappa fam g b)) -> Holes kappa fam f a -> m (Holes kappa fam g a)

-- | Refine holes with a simple action
holesRefineHoles :: (forall b. f b -> Holes kappa fam g b) -> Holes kappa fam f a -> Holes kappa fam g a

-- | Refines holes using a monadic action
holesRefineHolesM :: Monad m => (forall b. f b -> m (Holes kappa fam g b)) -> Holes kappa fam f a -> m (Holes kappa fam g a)

-- | Simpler version of <a>synthesizeM</a> working over the <i>Identity</i>
--   monad.
synthesize :: (forall b. CompoundCnstr kappa fam b => ann b -> SRep phi (Rep b) -> phi b) -> (forall b. PrimCnstr kappa fam b => ann b -> b -> phi b) -> (forall b. ann b -> h b -> phi b) -> HolesAnn kappa fam ann h a -> HolesAnn kappa fam phi h a

-- | Synthetization of attributes
synthesizeM :: Monad m => (forall b. CompoundCnstr kappa fam b => ann b -> SRep phi (Rep b) -> m (phi b)) -> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)) -> (forall b. ann b -> h b -> m (phi b)) -> HolesAnn kappa fam ann h a -> m (HolesAnn kappa fam phi h a)

-- | Catamorphism over <a>HolesAnn</a>
cataM :: Monad m => (forall b. CompoundCnstr kappa fam b => ann b -> SRep phi (Rep b) -> m (phi b)) -> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)) -> (forall b. ann b -> h b -> m (phi b)) -> HolesAnn kappa fam ann h a -> m (phi a)

-- | Computes the <i>least general generalization</i> of two trees.
lgg :: forall kappa fam h i a. All Eq kappa => Holes kappa fam h a -> Holes kappa fam i a -> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
class (CompoundCnstr kappa fam a) => Deep kappa fam a
dfrom :: Deep kappa fam a => a -> SFix kappa fam a
dfrom :: (Deep kappa fam a, GDeep kappa fam (Rep a)) => a -> SFix kappa fam a
dto :: Deep kappa fam a => SFix kappa fam a -> a
dto :: (Deep kappa fam a, GDeep kappa fam (Rep a)) => SFix kappa fam a -> a
class GDeep kappa fam f
gdfrom :: GDeep kappa fam f => f x -> SRep (SFix kappa fam) f
gdto :: GDeep kappa fam f => SRep (SFix kappa fam) f -> f x
instance (Generics.Simplistic.Deep.CompoundCnstr kappa fam a, Generics.Simplistic.Deep.Deep kappa fam a) => Generics.Simplistic.Deep.GDeepAtom kappa fam 'GHC.Types.False a
instance Generics.Simplistic.Deep.PrimCnstr kappa fam a => Generics.Simplistic.Deep.GDeepAtom kappa fam 'GHC.Types.True a
instance Generics.Simplistic.Deep.GDeepAtom kappa fam (Generics.Simplistic.Util.IsElem a kappa) a => Generics.Simplistic.Deep.GDeep kappa fam (GHC.Generics.K1 GHC.Generics.R a)
instance Generics.Simplistic.Deep.GDeep kappa fam GHC.Generics.U1
instance forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (g :: k -> *). (Generics.Simplistic.Deep.GDeep kappa fam f, Generics.Simplistic.Deep.GDeep kappa fam g) => Generics.Simplistic.Deep.GDeep kappa fam (f GHC.Generics.:*: g)
instance forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (g :: k -> *). (Generics.Simplistic.Deep.GDeep kappa fam f, Generics.Simplistic.Deep.GDeep kappa fam g) => Generics.Simplistic.Deep.GDeep kappa fam (f GHC.Generics.:+: g)
instance forall k i (c :: GHC.Generics.Meta) (kappa :: [*]) (fam :: [*]) (f :: k -> *). (Generics.Simplistic.GMeta i c, Generics.Simplistic.Deep.GDeep kappa fam f) => Generics.Simplistic.Deep.GDeep kappa fam (GHC.Generics.M1 i c f)
instance (Generics.Simplistic.Util.All GHC.Classes.Eq kappa, Generics.Simplistic.Util.EqHO h) => Generics.Simplistic.Util.EqHO (Generics.Simplistic.Deep.Holes kappa fam h)
instance (Generics.Simplistic.Util.All GHC.Classes.Eq kappa, Generics.Simplistic.Util.EqHO h) => GHC.Classes.Eq (Generics.Simplistic.Deep.Holes kappa fam h t)
instance (forall x. Control.DeepSeq.NFData (ann x), forall x. Control.DeepSeq.NFData (h x)) => Control.DeepSeq.NFData (Generics.Simplistic.Deep.HolesAnn kappa fam ann h f)
instance forall k (x :: k). Control.DeepSeq.NFData (GHC.Generics.V1 x)
instance forall k (x :: k). Control.DeepSeq.NFData (GHC.Generics.U1 x)


-- | Constraint-based unification algorithm for <a>Holes</a>
module Generics.Simplistic.Unify

-- | A substitution is but a map; the existential quantifiers are necessary
--   to ensure we can reuse from <a>Data.Map</a>
--   
--   Note that we must be able to compare <tt>Exists phi</tt>. This
--   comparison needs to work heterogeneously and it must return <a>EQ</a>
--   only when the contents are in fact equal. Even though we only need
--   this instance for <a>Data.Map</a>
--   
--   A typical example for <tt>phi</tt> is <tt>Const Int at</tt>,
--   representing a variable. The <tt>Ord</tt> instance would then be:
--   
--   <pre>
--   instance Ord (Exists (Const Int)) where
--     compare (Exists (Const x)) (Exists (Const y))
--       = compare x y
--   </pre>
type Subst kappa fam phi = Map (Exists phi) (Exists (Holes kappa fam phi))

-- | Empty substitution
substEmpty :: Subst kappa fam phi

-- | Inserts a point in a substitution. Note how the index of <tt>phi</tt>
--   <i>must</i> match the index of the term being inserted. This is
--   important when looking up terms because we must <a>unsafeCoerce</a>
--   the existential type variables to return.
--   
--   Please, always use this insertion function; or, if you insert by hand,
--   ensure thetype indices match.
substInsert :: Ord (Exists phi) => Subst kappa fam phi -> phi at -> Holes kappa fam phi at -> Subst kappa fam phi

-- | Looks a value up in a substitution, see <a>substInsert</a>
substLkup :: Ord (Exists phi) => Subst kappa fam phi -> phi at -> Maybe (Holes kappa fam phi at)

-- | Applies a substitution to a term once; Variables not in the support of
--   the substitution are left untouched.
substApply :: Ord (Exists phi) => Subst kappa fam phi -> Holes kappa fam phi at -> Holes kappa fam phi at

-- | Unification can return succesfully or find either a <a>OccursCheck</a>
--   failure or a <a>SymbolClash</a> failure.
data UnifyErr kappa fam phi :: *

-- | The occurs-check fails when the variable in question occurs within the
--   term its supposed to be unified with.
[OccursCheck] :: [Exists phi] -> UnifyErr kappa fam phi

-- | A symbol-clash is thrown when the head of the two terms is different
--   and neither is a variabe.
[SymbolClash] :: Holes kappa fam phi at -> Holes kappa fam phi at -> UnifyErr kappa fam phi

-- | Attempts to unify two <a>Holes</a>
unify :: (All Eq kappa, Ord (Exists phi), EqHO phi) => Holes kappa fam phi at -> Holes kappa fam phi at -> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)

-- | Attempts to unify two <a>Holes</a>, but ignores which error happened
--   when they could not be unified.
unify_ :: (All Eq kappa, Ord (Exists phi), EqHO phi) => Holes kappa fam phi at -> Holes kappa fam phi at -> Maybe (Subst kappa fam phi)

-- | Attempts to unify two <a>Holes</a> with an already existing
--   substitution
unifyWith :: (All Eq kappa, Ord (Exists phi), EqHO phi) => Subst kappa fam phi -> Holes kappa fam phi at -> Holes kappa fam phi at -> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)

-- | The minimization step performs the <i>occurs check</i> and removes
--   unecessary steps, returning an idempodent substitution when
--   successful. For example;
--   
--   <pre>
--   sigma = fromList
--             [ (0 , bin 1 2)
--             , (1 , bin 4 4) ]
--   </pre>
--   
--   Then, <tt>minimize sigma</tt> will return <tt>fromList [(0 , bin (bin
--   4 4) 2) , (1 , bin 4 4)]</tt> This returns <tt>Left vs</tt> if
--   occurs-check fail for variables <tt>vs</tt>.
minimize :: forall kappa fam phi. Ord (Exists phi) => Subst kappa fam phi -> Either [Exists phi] (Subst kappa fam phi)


-- | This module provides some Template Haskell functionality to help out
--   the declaration of <a>Deep</a> instances.
--   
--   Note that we chose to not automate the whole process on purpose.
--   Sometimes the user will need to define standalone <tt>Generic</tt>
--   instances for some select types in the family, some other times the
--   user might want better control over naming, for example. Consequently,
--   the most adaptable option is to provide two TH utilities:
--   
--   <ol>
--   <li>Unfolding a family into a list of types until a fixpoint is
--   reached, given in <a>unfoldFamilyInto</a></li>
--   <li>Declaring <a>Deep</a> for a list of types, given in
--   <tt>declareDeepFor</tt></li>
--   </ol>
--   
--   The stepts in between unfolding the family and declaring <a>Deep</a>
--   vary too much from case to case and hence, must be manually executed.
--   Let us run through a simple example, which involves mutual recursion
--   and type synonyms in the AST of a pseudo-language.
--   
--   <pre>
--   data Stmt var
--     = SAssign var (Exp var)
--     | SIf     (Exp var) (Stmt var) (Stmt var)
--     | SSeq    (Stmt var) (Stmt var)
--     | SReturn (Exp var)
--     | SDecl (Decl var)
--     | SSkip
--     deriving (Show, Generic)
--   
--   data ODecl var
--     = DVar var
--     | DFun var var (Stmt var)
--     deriving (Show, Generic)
--   
--   type Decl x = TDecl x
--   type TDecl x = ODecl x
--   
--   data Exp var
--     = EVar  var
--     | ECall var (Exp var)
--     | EAdd (Exp var) (Exp var)
--     | ESub (Exp var) (Exp var)
--     | ELit Int
--     deriving (Show, Generic)
--   </pre>
--   
--   Now say we want to use some code written with
--   <i>generics-simplistic</i> over these datatypes above. We must declare
--   the <a>Deep</a> instances for the types in the family and
--   <a>GHC.Generics</a> takes care of the rest.
--   
--   The first step is in defining <tt>Prim</tt> and <tt>Fam</tt>, which
--   will be type-level lists with the primitive types and the
--   non-primitive, or compound, types.
--   
--   An easy way to gather <i>all</i> types involved in the family is with
--   <a>unfoldFamilyInto</a>, like:
--   
--   <pre>
--   unfoldFamilyInto "stmtFam" [t| Stmt Int |]
--   </pre>
--   
--   The call above will be expanded into:
--   
--   <pre>
--   stmtFam :: [String]
--   stmtFam = ["Generics.Simplistic.Example.Exp Int"
--             ,"Generics.Simplistic.Example.ODecl Int"
--             ,"Generics.Simplistic.Example.Stmt Int"
--             ,"Int"
--             ]
--   </pre>
--   
--   Which can then be inspected with GHCi and, with some elbow-grease (or
--   test-editting macros!) we can easily generate the necessary type-level
--   lists:
--   
--   <pre>
--   type Fam = '[Generics.Simplistic.Example.Exp Int
--               ,Generics.Simplistic.Example.ODecl Int
--               ,Generics.Simplistic.Example.Stmt Int
--               ]
--   
--   type Prim = '[Int]
--   </pre>
--   
--   Finally, we are ready to call <a>deriveDeepFor</a> and get the
--   instances declared.
--   
--   <pre>
--   deriveDeepFor ''Prim ''Fam
--   </pre>
--   
--   The TH code above expands to:
--   
--   <pre>
--   instance Deep Prim Fam (Exp Int)
--   instance Deep Prim Fam (ODecl Int)
--   instance Deep Prim Fam (Stmt Int)
--   </pre>
--   
--   This workflow is crucial to be able to work with large mutually
--   recursive families, and it becomes especially easy if coupled with a
--   text editor with good macro support (read emacs and vim).
module Generics.Simplistic.Deep.TH

-- | Lists all the necessary types that should have <tt>Generic</tt> and
--   <a>Deep</a> instances. For example,
--   
--   <pre>
--   data Rose2 a b = Fork (Either a b) [Rose2 a b]
--   unfoldFamilyInto 'rose2tys [t| Rose2 Int Char |]
--   </pre>
--   
--   Will yield the following code:
--   
--   <pre>
--   rose2tys :: String
--   rose2tys = [ "Rose2 Int Char"
--              , "Either Int Char"
--              , "[Rose2 Int Char]"
--              , "Int"
--              , "Char"
--              ]
--   </pre>
--   
--   You should then use some elbow grease or your favorite text editor and
--   its provided macro functionality to produce:
--   
--   <pre>
--   type Rose2Prim = '[Int , Char]
--   type Rose2Fam  = '[Rose2 Int Char , Either Int Char , [Rose2 Int Char]]
--   deriving instance Generic (Rose2 Int Char)
--   deriving instance Generic (Either Int Char)
--   instance Deep Rose2Prim Rose2Fam (Rose2 Int Char)
--   instance Deep Rose2Prim Rose2Fam (Either Int Char)
--   instance Deep Rose2Prim Rose2Fam [Rose2 Int Char]
--   </pre>
--   
--   Note that types like <tt>Int</tt> will appear fully qualified, this
--   will need some renaming.
unfoldFamilyInto :: String -> Q Type -> Q [Dec]

-- | Given two type-level lists <tt>Prims</tt> and <tt>Fam</tt>, will
--   generate <tt>instance Deep Prim Fam f</tt> for every <tt>f</tt> in
--   <tt>Fam</tt>.
deriveDeepFor :: Name -> Name -> Q [Dec]

-- | Given a function <tt>f</tt> and a type level stored in <tt>fam</tt>,
--   <tt>deriveInstacesWith</tt> will generate:
--   
--   <pre>
--   instance f x
--   </pre>
--   
--   for each <tt>x</tt> in <tt>fam</tt>. This function is mostly internal,
--   please check <a>deriveDeepFor</a> and <tt>deriveGenericFor</tt>.
deriveInstancesWith :: (Type -> Q Type) -> Name -> Q [Dec]
instance GHC.Classes.Ord Generics.Simplistic.Deep.TH.STy
instance GHC.Show.Show Generics.Simplistic.Deep.TH.STy
instance GHC.Classes.Eq Generics.Simplistic.Deep.TH.STy


-- | Provides bare-bones <i>zipper</i> functionality to <a>SRep</a> and
--   <a>Holes</a>.
module Generics.Simplistic.Zipper

-- | A value of type 'SZip ty w f' corresponds to a value of type 'SRep w
--   f' with one of its leaves of type <tt>w ty</tt> absent. This is
--   essentially a zipper for <a>SRep</a>.
data SZip ty w f
[Z_KH] :: SZip ty w (K1 i ty)
[Z_L1] :: SZip ty w f -> SZip ty w (f :+: g)
[Z_R1] :: SZip ty w g -> SZip ty w (f :+: g)
[Z_PairL] :: SZip ty w f -> SRep w g -> SZip ty w (f :*: g)
[Z_PairR] :: SRep w f -> SZip ty w g -> SZip ty w (f :*: g)
[Z_M1] :: SMeta i t -> SZip ty w f -> SZip ty w (M1 i t f)

-- | We can transform a <a>SZip</a> into a <a>SRep</a> given we are
--   provided with a value to <i>plug</i> into the identified position.
plug :: SZip ty phi f -> phi ty -> SRep phi f

-- | Maps over a <a>SZip</a>
zipperMap :: (forall x. h x -> g x) -> SZip ty h f -> SZip ty g f
inr1 :: (x :*: y) t -> (Sum z x :*: y) t

-- | Given a <tt>z :: SZip ty h f</tt> and a <tt>r :: Rep w f</tt>, if
--   <tt>z</tt> and <tt>r</tt> are made with the same constuctor we return
--   a representation that contains both <tt>h</tt>s and <tt>w</tt>s in its
--   leaves, except in one leaf of type <tt>ty</tt>. This is analogous to
--   <a>zipSRep</a>.
zipperRepZip :: SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)

-- | Overlaps two zippers together; only succeeds if both zippers have the
--   same constructor AND hole.
zipSZip :: SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)

-- | Analogous to <a>repLeavesList</a>
zipLeavesList :: SZip ty w f -> [Maybe (Exists w)]

-- | The <a>Zipper</a> datatype packages a <a>SZip</a> in a more standard
--   presentation. A value of type <tt>Zipper c f g t</tt> represents a
--   value of type <tt>SRep f t</tt>, where exactly one recursive leaf (of
--   type <tt>t</tt>) carries a value of type <tt>g t</tt>, moreover, we
--   also carry a proof that the constraint <tt>c</tt> holds.
data Zipper c f g t
[Zipper] :: c => {zipper :: SZip t f (Rep t), sel :: g t} -> Zipper c f g t

-- | Auxiliar type synonym for annotated fixpoints.
type Zipper' kappa fam ann phi t = Zipper (CompoundCnstr kappa fam t) (HolesAnn kappa fam ann phi) (HolesAnn kappa fam ann phi) t

-- | Given a function that checks wheter an arbitrary position is recursive
--   and a value of <tt>t</tt>, returns all possible zippers ove
--   <tt>t</tt>.
zippers :: forall kappa fam ann phi t. (forall a. Elem t fam => phi a -> Maybe (a :~: t)) -> HolesAnn kappa fam ann phi t -> [Zipper' kappa fam ann phi t]

-- | Retrieves the constructor name for a representation. <i>WARNING;
--   UNSAFE</i> this function only works if <tt>f</tt> is the
--   representation of a type constructed with <a>GHC.Generics</a> builtin
--   mechanisms.
zipConstructorName :: SZip h w f -> String
instance forall k (w :: * -> *) h (f :: k -> *). (forall a. GHC.Show.Show (w a)) => GHC.Show.Show (Generics.Simplistic.Zipper.SZip h w f)
instance forall k (w :: * -> *) h (f :: k -> *). (forall a. GHC.Classes.Eq (w a)) => GHC.Classes.Eq (Generics.Simplistic.Zipper.SZip h w f)