{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

-- 
-- This file provides functorial syntax -- versions of standard functors for
-- use in parametric syntax.

module Cubix.Language.Parametric.Syntax.Functor
  (
    -- * Functorial syntax
    MaybeF(..)
  , ListF(..)
  , PairF(..)
  , TripleF(..)
  , EitherF(..)

  , pattern Just'
  , pattern Nothing'

  , pattern JustA'

  , pattern ConsF'
  , pattern NilF'
  , pattern SingletonF'

  , pattern ConsFA'
  , pattern NilFA'
  , pattern SingletonFA'

  , pattern PairF'
  , pattern TripleF'

  , pattern Left'
  , pattern Right'

    -- ** Smart constructors
  , riNothingF
  , iJustF
  , jJustF
  , riNilF
  , iConsF
  , jConsF
  , riPairF
  , riTripleF
  , riLeftF
  , riRightF

    -- ** Converting functorial syntax
  , ExtractF(..)
  , KExtractF(..)
  , KExtractF'(..)
  , ExtractF2(..)
  , KExtractF2(..)
  , KExtractF2'(..)
  , ExtractF3(..)
  , KExtractF3(..)
  , KExtractF3'(..)
  , InsertF(..)

  , insertFHole
  , liftF
  , mapF
  ) where

import Data.Comp.Multi ( HFunctor, (:<:), Sum, (:&:), Cxt(..), Context, K(..), unK, inject, project, project', RemA(..), NotSum, HFix, caseCxt, All, CxtS, (:-<:) )
import Data.Comp.Multi.Derive ( derive, makeConstrNameHF, makeHFunctor, makeHTraversable, makeHFoldable, makeEqHF, makeShowHF, makeOrdHF )

import Data.Comp.Multi.Strategy.Classification

import Data.Typeable ( Typeable, eqT )

import Cubix.Language.Parametric.InjF


--------------------------------------------------------------------------------
-- Higher-order versions of standard functors
--------------------------------------------------------------------------------

-- | A higher-order functor version of Maybe, for use with
-- multi-sorted compositional data types
-- 
-- @e@ : a functor mapping labels to terms of the corresponding sort
-- 
-- @l@ : the label. Will have the form @Maybe l'@
data MaybeF e l where
  NothingF :: Typeable l => MaybeF e (Maybe l)
  JustF    :: Typeable l => e l -> MaybeF e (Maybe l)

type instance IsSortInjection MaybeF = False

-- | A higher-order functor version of [], for use with
-- multi-sorted compositional data types
-- 
-- @e@ : a functor mapping labels to terms of the corresponding sort
-- 
-- @l@ : the label. Will have the form [l]
data ListF e l where
  NilF  :: Typeable l => ListF e [l]
  ConsF :: Typeable l => e l -> e [l] -> ListF e [l]

type instance IsSortInjection ListF = False

-- | A higher-order functor version of (,), for use with
-- multi-sorted compositional data types
-- 
-- @e@ : a functor mapping labels to terms of the corresponding sort
-- 
-- @l@ : the label . Will have the form (l1,l2)

data PairF e l where
  PairF :: (Typeable i, Typeable j) => e i -> e j -> PairF e (i, j)

type instance IsSortInjection PairF = False

data TripleF e l where
  TripleF :: (Typeable i, Typeable j, Typeable k) => e i -> e j -> e k -> TripleF e (i, j, k)

type instance IsSortInjection TripleF = False

-- | A higher-order functor version of Either, for use with
-- multi-sorted compositional data types
-- 
-- @e@ : a functor mapping labels to terms of the corresponding sort
-- 
-- @l@ : the label . Will have the form (Either l1 l2)
data EitherF e l where
  LeftF  :: (Typeable i, Typeable j) => e i -> EitherF e (Either i j)
  RightF :: (Typeable i, Typeable j) => e j -> EitherF e (Either i j)

type instance IsSortInjection EitherF = False

--------------------------------------------------------------------------------
-- Instances of Generic
--------------------------------------------------------------------------------

{-
instance G.Generic (MaybeF e (Maybe l)) where
  type Rep (MaybeF e (Maybe l)) = G.U1 G.:+: (G.Rec0 (e l))
  from NothingF      = G.L1 G.U1
  from (JustF x)     = G.R1 $ G.K1 x
  to (G.L1 G.U1)     = NothingF
  to (G.R1 (G.K1 x)) = JustF x

instance G.Generic (ListF e [l]) where
  type Rep (ListF e [l]) = G.U1 G.:+: (G.Rec0 (e l) G.:*: G.Rec0 (e [l]))
  from NilF                        = G.L1 G.U1
  from (ConsF x xs)                = G.R1 $ G.K1 x G.:*: G.K1 xs
  to (G.L1 G.U1)                   = NilF
  to (G.R1 (G.K1 x G.:*: G.K1 xs)) = ConsF x xs


instance G.Generic (PairF e (i,j)) where
  type Rep (PairF e (i,j)) = G.Rec0 (e i) G.:*: G.Rec0 (e j)
  from (PairF x y)         = G.K1 x G.:*: G.K1 y
  to (G.K1 x G.:*: G.K1 y) = PairF x y

instance G.Generic (TripleF e (i,j,k)) where
  type Rep (TripleF e (i,j,k))           = G.Rec0 (e i) G.:*: G.Rec0 (e j) G.:*: G.Rec0 (e k)
  from (TripleF x y z)                   = G.K1 x G.:*: G.K1 y G.:*: G.K1 z
  to (G.K1 x G.:*: G.K1 y G.:*: G.K1 z)  = TripleF x y z

instance G.Generic (EitherF e (Either i j)) where
  type Rep (EitherF e (Either i j)) = G.Rec0 (e i) G.:+: G.Rec0 (e j)
  from (LeftF x)     = G.L1 $ G.K1 x
  from (RightF x)    = G.R1 $ G.K1 x
  to (G.L1 (G.K1 x)) = LeftF x
  to (G.R1 (G.K1 x)) = RightF x

--------------------------------------------------------------------------------
-- Trivial instances of Generic
--------------------------------------------------------------------------------

instance G.Generic (MaybeF e [l]) where
  type Rep (MaybeF e [l]) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (MaybeF e (i,j)) where
  type Rep (MaybeF e (i,j)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (MaybeF e (i,j,k)) where
  type Rep (MaybeF e (i,j,k)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (MaybeF e (Either i j)) where
  type Rep (MaybeF e (Either i j)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (ListF e (Maybe l)) where
  type Rep (ListF e (Maybe l)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (ListF e (i,j)) where
  type Rep (ListF e (i,j)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (ListF e (i,j,k)) where
  type Rep (ListF e (i,j,k)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (ListF e (Either i j)) where
  type Rep (ListF e (Either i j)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (PairF e (Maybe l)) where
  type Rep (PairF e (Maybe l)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (PairF e [l]) where
  type Rep (PairF e [l]) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (PairF e (i,j,k)) where
  type Rep (PairF e (i,j,k)) = G.V1
  from = undefined
  to  = undefined

instance G.Generic (PairF e (Either i j)) where
  type Rep (PairF e (Either i j)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (TripleF e (Maybe l)) where
  type Rep (TripleF e (Maybe l)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (TripleF e [l]) where
  type Rep (TripleF e [l]) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (TripleF e (i,j)) where
  type Rep (TripleF e (i,j)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (TripleF e (Either i j)) where
  type Rep (TripleF e (Either i j)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (EitherF e (Maybe l)) where
  type Rep (EitherF e (Maybe l)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (EitherF e [l]) where
  type Rep (EitherF e [l]) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (EitherF e (i,j)) where
  type Rep (EitherF e (i,j)) = G.V1
  from = undefined
  to   = undefined

instance G.Generic (EitherF e (i,j,k)) where
  type Rep (EitherF e (i,j,k)) = G.V1
  from = undefined
  to   = undefined

-}

--------------------------------------------------------------------------------

-- DynCase instances are usually generated by TH,
-- but the TH currently does not handle higher-kinded labels
--
-- These currently have some unfortunate coupling with KDynCaseC
-- in compstrat. Still better than what we had before (actually able
-- to give us all the instances we want)

instance (Typeable l) => KDynCase MaybeF (Maybe l) where
  kdyncase :: forall (e :: Family) b. MaybeF e b -> Maybe (b :~: Maybe l)
kdyncase MaybeF e b
NothingF  = Maybe (b :~: Maybe l)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  kdyncase (JustF e l
_) = Maybe (b :~: Maybe l)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

instance (Typeable l) => KDynCase ListF [l] where
  kdyncase :: forall (e :: Family) b. ListF e b -> Maybe (b :~: [l])
kdyncase ListF e b
NilF        = Maybe (b :~: [l])
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  kdyncase (ConsF e l
_ e [l]
_) = Maybe (b :~: [l])
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

instance (Typeable l, Typeable l') => KDynCase PairF (l, l') where
  kdyncase :: forall (e :: Family) b. PairF e b -> Maybe (b :~: (l, l'))
kdyncase (PairF e i
_ e j
_) = Maybe (b :~: (l, l'))
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

instance (Typeable l, Typeable l', Typeable l'') => KDynCase TripleF (l, l', l'') where
  kdyncase :: forall (e :: Family) b. TripleF e b -> Maybe (b :~: (l, l', l''))
kdyncase (TripleF e i
_ e j
_ e k
_) = Maybe (b :~: (l, l', l''))
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

instance (Typeable l, Typeable l') => KDynCase EitherF (Either l l') where
  kdyncase :: forall (e :: Family) b. EitherF e b -> Maybe (b :~: Either l l')
kdyncase (LeftF e i
_)  = Maybe (b :~: Either l l')
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  kdyncase (RightF e j
_) = Maybe (b :~: Either l l')
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

-- You cannot write a (KDynCase EitherF (Either l l')) instance. That
-- can be used to write unsafe casts. The best you could do is a (KDynCase EitherF (exists l'. Either l l'))
-- instance; not sure how to write that in Haskell

--------------------------------------------------------------------------------

-- Fully smart constructors for NothingF and NilF do not
-- typecheck because of unconstrained label

-- | Smart constructor for NothingF. Restricted; cannot be lifted through a sort injection
riNothingF :: forall h f a l. (MaybeF :<: f, Typeable l) => Cxt h f a (Maybe l)
riNothingF :: forall h (f :: Node) (a :: Family) l.
(MaybeF :<: f, Typeable l) =>
Cxt h f a (Maybe l)
riNothingF = MaybeF (Cxt h f a) (Maybe l) -> Cxt h f a (Maybe l)
MaybeF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject MaybeF (Cxt h f a) (Maybe l)
forall i (e :: Family). Typeable i => MaybeF e (Maybe i)
NothingF

iJustF :: (MaybeF :-<: fs, InjF fs (Maybe l) l', Typeable l) => CxtS h fs a l -> CxtS h fs a l'
iJustF :: forall (fs :: Signature) l l' h (a :: Family).
(MaybeF :-<: fs, InjF fs (Maybe l) l', Typeable l) =>
CxtS h fs a l -> CxtS h fs a l'
iJustF = CxtS h fs a (Maybe l) -> CxtS h fs a l'
forall (fs :: Signature) l l' h (a :: Family).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: Family). CxtS h fs a (Maybe l) -> CxtS h fs a l'
injF (CxtS h fs a (Maybe l) -> CxtS h fs a l')
-> (CxtS h fs a l -> CxtS h fs a (Maybe l))
-> CxtS h fs a l
-> CxtS h fs a l'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h fs a l -> CxtS h fs a (Maybe l)
forall (f :: Node) l h (a :: Family).
(MaybeF :<: f, Typeable l) =>
Cxt h f a l -> Cxt h f a (Maybe l)
jJustF

jJustF :: (MaybeF :<: f, Typeable l) => Cxt h f a l -> Cxt h f a (Maybe l)
jJustF :: forall (f :: Node) l h (a :: Family).
(MaybeF :<: f, Typeable l) =>
Cxt h f a l -> Cxt h f a (Maybe l)
jJustF = MaybeF (Cxt h f a) (Maybe l) -> Cxt h f a (Maybe l)
MaybeF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (MaybeF (Cxt h f a) (Maybe l) -> Cxt h f a (Maybe l))
-> (Cxt h f a l -> MaybeF (Cxt h f a) (Maybe l))
-> Cxt h f a l
-> Cxt h f a (Maybe l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt h f a l -> MaybeF (Cxt h f a) (Maybe l)
forall i (e :: Family). Typeable i => e i -> MaybeF e (Maybe i)
JustF

-- | Smart constructor for NilF. Restricted; cannot be lifted through a sort injection
riNilF :: forall h f a l. (ListF :<: f, Typeable l) => Cxt h f a [l]
riNilF :: forall h (f :: Node) (a :: Family) l.
(ListF :<: f, Typeable l) =>
Cxt h f a [l]
riNilF = ListF (Cxt h f a) [l] -> Cxt h f a [l]
ListF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject ListF (Cxt h f a) [l]
forall i (e :: Family). Typeable i => ListF e [i]
NilF

iConsF :: (ListF :-<: fs, InjF fs [l] l', Typeable l) => CxtS h fs a l -> CxtS h fs a [l] -> CxtS h fs a l'
iConsF :: forall (fs :: Signature) l l' h (a :: Family).
(ListF :-<: fs, InjF fs [l] l', Typeable l) =>
CxtS h fs a l -> CxtS h fs a [l] -> CxtS h fs a l'
iConsF CxtS h fs a l
x CxtS h fs a [l]
y = CxtS h fs a [l] -> CxtS h fs a l'
forall (fs :: Signature) l l' h (a :: Family).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: Family). CxtS h fs a [l] -> CxtS h fs a l'
injF (CxtS h fs a l -> CxtS h fs a [l] -> CxtS h fs a [l]
forall (f :: Node) l h (a :: Family).
(ListF :<: f, Typeable l) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
jConsF CxtS h fs a l
x CxtS h fs a [l]
y)

jConsF :: (ListF :<: f, Typeable l) => Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
jConsF :: forall (f :: Node) l h (a :: Family).
(ListF :<: f, Typeable l) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
jConsF Cxt h f a l
x Cxt h f a [l]
y = ListF (Cxt h f a) [l] -> Cxt h f a [l]
ListF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (Cxt h f a l -> Cxt h f a [l] -> ListF (Cxt h f a) [l]
forall i (e :: Family). Typeable i => e i -> e [i] -> ListF e [i]
ConsF Cxt h f a l
x Cxt h f a [l]
y)

-- | Smart constructor for PairF. Restricted; cannot be lifted through a sort injection
riPairF :: (PairF :<: f, Typeable i, Typeable j) => Cxt h f a i -> Cxt h f a j -> Cxt h f a (i, j)
riPairF :: forall (f :: Node) i j h (a :: Family).
(PairF :<: f, Typeable i, Typeable j) =>
Cxt h f a i -> Cxt h f a j -> Cxt h f a (i, j)
riPairF Cxt h f a i
x Cxt h f a j
y = PairF (Cxt h f a) (i, j) -> Cxt h f a (i, j)
PairF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (Cxt h f a i -> Cxt h f a j -> PairF (Cxt h f a) (i, j)
forall i j (e :: Family).
(Typeable i, Typeable j) =>
e i -> e j -> PairF e (i, j)
PairF Cxt h f a i
x Cxt h f a j
y)

riTripleF :: (TripleF :<: f, Typeable i, Typeable j, Typeable k) => Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> Cxt h f a (i, j, k)
riTripleF :: forall (f :: Node) i j k h (a :: Family).
(TripleF :<: f, Typeable i, Typeable j, Typeable k) =>
Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> Cxt h f a (i, j, k)
riTripleF Cxt h f a i
x Cxt h f a j
y Cxt h f a k
z = TripleF (Cxt h f a) (i, j, k) -> Cxt h f a (i, j, k)
TripleF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (Cxt h f a i
-> Cxt h f a j -> Cxt h f a k -> TripleF (Cxt h f a) (i, j, k)
forall i j k (e :: Family).
(Typeable i, Typeable j, Typeable k) =>
e i -> e j -> e k -> TripleF e (i, j, k)
TripleF Cxt h f a i
x Cxt h f a j
y Cxt h f a k
z)

riLeftF :: (EitherF :<: f, Typeable i, Typeable j) => Cxt h f a i -> Cxt h f a (Either i j)
riLeftF :: forall (f :: Node) i j h (a :: Family).
(EitherF :<: f, Typeable i, Typeable j) =>
Cxt h f a i -> Cxt h f a (Either i j)
riLeftF = EitherF (Cxt h f a) (Either i j) -> Cxt h f a (Either i j)
EitherF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (EitherF (Cxt h f a) (Either i j) -> Cxt h f a (Either i j))
-> (Cxt h f a i -> EitherF (Cxt h f a) (Either i j))
-> Cxt h f a i
-> Cxt h f a (Either i j)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt h f a i -> EitherF (Cxt h f a) (Either i j)
forall i j (e :: Family).
(Typeable i, Typeable j) =>
e i -> EitherF e (Either i j)
LeftF

riRightF :: (EitherF :<: f, Typeable i, Typeable j) => Cxt h f a j -> Cxt h f a (Either i j)
riRightF :: forall (f :: Node) i j h (a :: Family).
(EitherF :<: f, Typeable i, Typeable j) =>
Cxt h f a j -> Cxt h f a (Either i j)
riRightF = EitherF (Cxt h f a) (Either i j) -> Cxt h f a (Either i j)
EitherF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (EitherF (Cxt h f a) (Either i j) -> Cxt h f a (Either i j))
-> (Cxt h f a j -> EitherF (Cxt h f a) (Either i j))
-> Cxt h f a j
-> Cxt h f a (Either i j)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt h f a j -> EitherF (Cxt h f a) (Either i j)
forall i j (e :: Family).
(Typeable i, Typeable j) =>
e j -> EitherF e (Either i j)
RightF

$(derive [makeHFunctor, makeHTraversable, makeHFoldable, makeEqHF, makeShowHF,
                    makeOrdHF, makeConstrNameHF ]
       [''MaybeF, ''ListF, ''PairF, ''TripleF, ''EitherF])

--------------------------------------------------------------------------------
-- Dealing with functorial syntax
--------------------------------------------------------------------------------

-- We should be able to make this safe using OrderedOverlappingTypeFamilies.
--
-- This is an instance of a distributive law, and likely can (and should)
-- be replaced with such.
class ExtractF f e where
  -- | Pulls a functor out of a label.
  -- 
  -- Example:
  -- 
  -- @
  -- 'extractF' :: 'JavaProj' ['SourceFileL'] -> ['JavaProj' 'SourceFileL']
  -- @
  --
  -- Beware that this function unsafely assumes that e.g.: a term of sort
  -- @[l]@ is a `ListF` node (and similar for Maybe, etc).
  -- If you define a custom node that has sort @[l]@ for any @l@, and
  -- do not define a corresponding `ExtractF` instance, then `extractF`
  -- may give an error.
  extractF :: e (f l) -> f (e l)

-- | Inductive form of ExtractF.
-- An instance @KExtract f g@ gives rise to an instance @ExtractF f (Term g)@
class KExtractF f g where
  kextractF :: ExtractF f e => g e (f l) -> f (e l)

class KExtractF' f g where
  kextractF' :: g e (f l) -> f (e l)

instance {-# OVERLAPPABLE #-} KExtractF' f g => KExtractF f g where
  kextractF :: forall (e :: Family) l. ExtractF f e => g e (f l) -> f (e l)
kextractF = g e (f l) -> f (e l)
forall (e :: Family) l. g e (f l) -> f (e l)
forall (f :: Family) (g :: Node) (e :: Family) l.
KExtractF' f g =>
g e (f l) -> f (e l)
kextractF'

instance {-# OVERLAPPING #-} (All (KExtractF f) gs) => KExtractF f (Sum gs) where
  kextractF :: forall (e :: Family) l. ExtractF f e => Sum gs e (f l) -> f (e l)
kextractF = forall (cxt :: Node -> Constraint) (fs :: Signature) (a :: Family)
       e b.
All cxt fs =>
(forall (f :: Node). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @(KExtractF f) f e (f l) -> f (e l)
forall (e :: Family) l. ExtractF f e => f e (f l) -> f (e l)
forall (f :: Family) (g :: Node) (e :: Family) l.
(KExtractF f g, ExtractF f e) =>
g e (f l) -> f (e l)
forall (f :: Node). KExtractF f f => f e (f l) -> f (e l)
kextractF

instance {-# OVERLAPPING #-} (All (KExtractF' f) gs) => KExtractF' f (Sum gs) where
  kextractF' :: forall (e :: Family) l. Sum gs e (f l) -> f (e l)
kextractF' = forall (cxt :: Node -> Constraint) (fs :: Signature) (a :: Family)
       e b.
All cxt fs =>
(forall (f :: Node). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @(KExtractF' f) f e (f l) -> f (e l)
forall (e :: Family) l. f e (f l) -> f (e l)
forall (f :: Family) (g :: Node) (e :: Family) l.
KExtractF' f g =>
g e (f l) -> f (e l)
forall (f :: Node). KExtractF' f f => f e (f l) -> f (e l)
kextractF'

instance {-# OVERLAPPING #-}  (KExtractF f g) => KExtractF f (g :&: a) where
  kextractF :: forall (e :: Family) l.
ExtractF f e =>
(:&:) g a e (f l) -> f (e l)
kextractF = g e (f l) -> f (e l)
forall (e :: Family) l. ExtractF f e => g e (f l) -> f (e l)
forall (f :: Family) (g :: Node) (e :: Family) l.
(KExtractF f g, ExtractF f e) =>
g e (f l) -> f (e l)
kextractF (g e (f l) -> f (e l))
-> ((:&:) g a e (f l) -> g e (f l)) -> (:&:) g a e (f l) -> f (e l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) g a e (f l) -> g e (f l)
forall (a :: Family). (:&:) g a a :-> g a
forall (s :: Node) (s' :: Node) (a :: Family).
RemA s s' =>
s a :-> s' a
remA

instance {-# OVERLAPPING #-} (KExtractF' f g) => KExtractF' f (g :&: a) where
  kextractF' :: forall (e :: Family) l. (:&:) g a e (f l) -> f (e l)
kextractF' = g e (f l) -> f (e l)
forall (e :: Family) l. g e (f l) -> f (e l)
forall (f :: Family) (g :: Node) (e :: Family) l.
KExtractF' f g =>
g e (f l) -> f (e l)
kextractF' (g e (f l) -> f (e l))
-> ((:&:) g a e (f l) -> g e (f l)) -> (:&:) g a e (f l) -> f (e l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) g a e (f l) -> g e (f l)
forall (a :: Family). (:&:) g a a :-> g a
forall (s :: Node) (s' :: Node) (a :: Family).
RemA s s' =>
s a :-> s' a
remA

instance (Applicative f) => ExtractF f (K a) where
  extractF :: forall l. K a (f l) -> f (K a l)
extractF = K a l -> f (K a l)
forall a. a -> f a
forall (f :: Family) a. Applicative f => a -> f a
pure (K a l -> f (K a l))
-> (K a (f l) -> K a l) -> K a (f l) -> f (K a l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> K a l
forall a i. a -> K a i
K (a -> K a l) -> (K a (f l) -> a) -> K a (f l) -> K a l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K a (f l) -> a
forall a i. K a i -> a
unK

instance (KExtractF f g, ExtractF f a, Functor f) => ExtractF f (Cxt h g a) where
  extractF :: forall l. Cxt h g a (f l) -> f (Cxt h g a l)
extractF (Term g (Cxt h g a) (f l)
x) = g (Cxt h g a) (f l) -> f (Cxt h g a l)
forall (e :: Family) l. ExtractF f e => g e (f l) -> f (e l)
forall (f :: Family) (g :: Node) (e :: Family) l.
(KExtractF f g, ExtractF f e) =>
g e (f l) -> f (e l)
kextractF g (Cxt h g a) (f l)
x
  extractF (Hole a (f l)
x) = (a l -> Cxt h g a l) -> f (a l) -> f (Cxt h g a l)
forall a b. (a -> b) -> f a -> f b
forall (f :: Family) a b. Functor f => (a -> b) -> f a -> f b
fmap a l -> Cxt h g a l
a l -> Cxt Hole g a l
forall (a :: Family) i (f :: Node). a i -> Cxt Hole f a i
Hole (f (a l) -> f (Cxt h g a l)) -> f (a l) -> f (Cxt h g a l)
forall a b. (a -> b) -> a -> b
$ a (f l) -> f (a l)
forall l. a (f l) -> f (a l)
forall (f :: Family) (e :: Family) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF a (f l)
x

instance {-# OVERLAPPABLE #-} (NotSum g) => KExtractF' f g where
  kextractF' :: forall (e :: Family) l. g e (f l) -> f (e l)
kextractF' = String -> g e (f l) -> f (e l)
forall a. HasCallStack => String -> a
error String
"Undefined use of extractF"

--------------------------------------------------------------------------------

instance {-# OVERLAPPING #-} KExtractF [] ListF where
  kextractF :: forall (e :: Family) l. ExtractF [] e => ListF e [l] -> [e l]
kextractF ListF e [l]
NilF = []
  kextractF (ConsF e l
x e [l]
xs) = e l
e l
x e l -> [e l] -> [e l]
forall a. a -> [a] -> [a]
: (e [l] -> [e l]
forall l. e [l] -> [e l]
forall (f :: Family) (e :: Family) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF e [l]
e [l]
xs)

instance {-# OVERLAPPING #-} KExtractF' Maybe MaybeF where
  kextractF' :: forall (e :: Family) l. MaybeF e (Maybe l) -> Maybe (e l)
kextractF' MaybeF e (Maybe l)
NothingF = Maybe (e l)
forall a. Maybe a
Nothing
  kextractF' (JustF e l
x) = e l -> Maybe (e l)
forall a. a -> Maybe a
Just e l
e l
x

--------------------------------------------------------------------------------

class ExtractF2 f e where
  extractF2 :: e (f l l') -> f (e l) (e l')

class KExtractF2 f g where
  kextractF2 :: ExtractF2 f e => g e (f l l') -> f (e l) (e l')

class KExtractF2' f g where
  kextractF2' :: g e (f l l') -> f (e l) (e l')

instance {-# OVERLAPPABLE #-} KExtractF2' f g => KExtractF2 f g where
  kextractF2 :: forall (e :: Family) l l'.
ExtractF2 f e =>
g e (f l l') -> f (e l) (e l')
kextractF2 = g e (f l l') -> f (e l) (e l')
forall (e :: Family) l l'. g e (f l l') -> f (e l) (e l')
forall (f :: * -> Family) (g :: Node) (e :: Family) l l'.
KExtractF2' f g =>
g e (f l l') -> f (e l) (e l')
kextractF2'

instance {-# OVERLAPPING #-} (All (KExtractF2 f) gs) => KExtractF2 f (Sum gs) where
  kextractF2 :: forall (e :: Family) l l'.
ExtractF2 f e =>
Sum gs e (f l l') -> f (e l) (e l')
kextractF2 = forall (cxt :: Node -> Constraint) (fs :: Signature) (a :: Family)
       e b.
All cxt fs =>
(forall (f :: Node). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @(KExtractF2 f) f e (f l l') -> f (e l) (e l')
forall (e :: Family) l l'.
ExtractF2 f e =>
f e (f l l') -> f (e l) (e l')
forall (f :: * -> Family) (g :: Node) (e :: Family) l l'.
(KExtractF2 f g, ExtractF2 f e) =>
g e (f l l') -> f (e l) (e l')
forall (f :: Node).
KExtractF2 f f =>
f e (f l l') -> f (e l) (e l')
kextractF2

instance {-# OVERLAPPING #-} (All (KExtractF2' f) gs) => KExtractF2' f (Sum gs) where
  kextractF2' :: forall (e :: Family) l l'. Sum gs e (f l l') -> f (e l) (e l')
kextractF2' = forall (cxt :: Node -> Constraint) (fs :: Signature) (a :: Family)
       e b.
All cxt fs =>
(forall (f :: Node). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @(KExtractF2' f) f e (f l l') -> f (e l) (e l')
forall (e :: Family) l l'. f e (f l l') -> f (e l) (e l')
forall (f :: * -> Family) (g :: Node) (e :: Family) l l'.
KExtractF2' f g =>
g e (f l l') -> f (e l) (e l')
forall (f :: Node).
KExtractF2' f f =>
f e (f l l') -> f (e l) (e l')
kextractF2'

instance {-# OVERLAPPING #-} (KExtractF2 f g) => KExtractF2 f (g :&: a) where
  kextractF2 :: forall (e :: Family) l l'.
ExtractF2 f e =>
(:&:) g a e (f l l') -> f (e l) (e l')
kextractF2 = g e (f l l') -> f (e l) (e l')
forall (e :: Family) l l'.
ExtractF2 f e =>
g e (f l l') -> f (e l) (e l')
forall (f :: * -> Family) (g :: Node) (e :: Family) l l'.
(KExtractF2 f g, ExtractF2 f e) =>
g e (f l l') -> f (e l) (e l')
kextractF2 (g e (f l l') -> f (e l) (e l'))
-> ((:&:) g a e (f l l') -> g e (f l l'))
-> (:&:) g a e (f l l')
-> f (e l) (e l')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) g a e (f l l') -> g e (f l l')
forall (a :: Family). (:&:) g a a :-> g a
forall (s :: Node) (s' :: Node) (a :: Family).
RemA s s' =>
s a :-> s' a
remA

instance {-# OVERLAPPING #-} (KExtractF2' f g) => KExtractF2' f (g :&: a) where
  kextractF2' :: forall (e :: Family) l l'. (:&:) g a e (f l l') -> f (e l) (e l')
kextractF2' = g e (f l l') -> f (e l) (e l')
forall (e :: Family) l l'. g e (f l l') -> f (e l) (e l')
forall (f :: * -> Family) (g :: Node) (e :: Family) l l'.
KExtractF2' f g =>
g e (f l l') -> f (e l) (e l')
kextractF2' (g e (f l l') -> f (e l) (e l'))
-> ((:&:) g a e (f l l') -> g e (f l l'))
-> (:&:) g a e (f l l')
-> f (e l) (e l')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) g a e (f l l') -> g e (f l l')
forall (a :: Family). (:&:) g a a :-> g a
forall (s :: Node) (s' :: Node) (a :: Family).
RemA s s' =>
s a :-> s' a
remA

instance (KExtractF2 f g) => ExtractF2 f (HFix g) where
  extractF2 :: forall l l'. HFix g (f l l') -> f (HFix g l) (HFix g l')
extractF2 (Term g (HFix g) (f l l')
x) = g (HFix g) (f l l')
-> f (Cxt NoHole g (K ()) l) (Cxt NoHole g (K ()) l')
forall (e :: Family) l l'.
ExtractF2 f e =>
g e (f l l') -> f (e l) (e l')
forall (f :: * -> Family) (g :: Node) (e :: Family) l l'.
(KExtractF2 f g, ExtractF2 f e) =>
g e (f l l') -> f (e l) (e l')
kextractF2 g (HFix g) (f l l')
x

instance {-# OVERLAPPABLE #-} (NotSum g) => KExtractF2' f g where
  kextractF2' :: forall (e :: Family) l l'. g e (f l l') -> f (e l) (e l')
kextractF2' = String -> g e (f l l') -> f (e l) (e l')
forall a. HasCallStack => String -> a
error String
"Undefined use of extractF2"

--------------------------------------------------------------------------------

instance {-# OVERLAPPING #-} KExtractF2' (,) PairF where
  kextractF2' :: forall (e :: Family) l l'. PairF e (l, l') -> (e l, e l')
kextractF2' (PairF e i
a e j
b) = (e l
e i
a, e l'
e j
b)

instance {-# OVERLAPPING #-} KExtractF2' Either EitherF where
  kextractF2' :: forall (e :: Family) l l'.
EitherF e (Either l l') -> Either (e l) (e l')
kextractF2' (LeftF  e i
a) = e l -> Either (e l) (e l')
forall a b. a -> Either a b
Left e l
e i
a
  kextractF2' (RightF e j
a) = e l' -> Either (e l) (e l')
forall a b. b -> Either a b
Right e l'
e j
a

--------------------------------------------------------------------------------

class ExtractF3 f e where
  extractF3 :: e (f l l' l'') -> f (e l) (e l') (e l'')

class KExtractF3 f g where
  kextractF3 :: ExtractF3 f e => g e (f l l' l'') -> f (e l) (e l') (e l'')

class KExtractF3' f g where
  kextractF3' :: g e (f l l' l'') -> f (e l) (e l') (e l'')

instance {-# OVERLAPPABLE #-} KExtractF3' f g => KExtractF3 f g where
  kextractF3 :: forall (e :: Family) l l' l''.
ExtractF3 f e =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3 = g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (e :: Family) l l' l''.
g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (f :: * -> * -> Family) (g :: Node) (e :: Family) l l' l''.
KExtractF3' f g =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3'

instance {-# OVERLAPPING #-} (All (KExtractF3 f) gs) => KExtractF3 f (Sum gs) where
  kextractF3 :: forall (e :: Family) l l' l''.
ExtractF3 f e =>
Sum gs e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3 = forall (cxt :: Node -> Constraint) (fs :: Signature) (a :: Family)
       e b.
All cxt fs =>
(forall (f :: Node). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @(KExtractF3 f) f e (f l l' l'') -> f (e l) (e l') (e l'')
forall (e :: Family) l l' l''.
ExtractF3 f e =>
f e (f l l' l'') -> f (e l) (e l') (e l'')
forall (f :: * -> * -> Family) (g :: Node) (e :: Family) l l' l''.
(KExtractF3 f g, ExtractF3 f e) =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (f :: Node).
KExtractF3 f f =>
f e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3

instance {-# OVERLAPPING #-} (All (KExtractF3' f) gs) => KExtractF3' f (Sum gs) where
  kextractF3' :: forall (e :: Family) l l' l''.
Sum gs e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3' = forall (cxt :: Node -> Constraint) (fs :: Signature) (a :: Family)
       e b.
All cxt fs =>
(forall (f :: Node). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @(KExtractF3' f) f e (f l l' l'') -> f (e l) (e l') (e l'')
forall (e :: Family) l l' l''.
f e (f l l' l'') -> f (e l) (e l') (e l'')
forall (f :: * -> * -> Family) (g :: Node) (e :: Family) l l' l''.
KExtractF3' f g =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (f :: Node).
KExtractF3' f f =>
f e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3'

instance {-# OVERLAPPING #-} (KExtractF3 f g) => KExtractF3 f (g :&: a) where
  kextractF3 :: forall (e :: Family) l l' l''.
ExtractF3 f e =>
(:&:) g a e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3 = g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (e :: Family) l l' l''.
ExtractF3 f e =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (f :: * -> * -> Family) (g :: Node) (e :: Family) l l' l''.
(KExtractF3 f g, ExtractF3 f e) =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3 (g e (f l l' l'') -> f (e l) (e l') (e l''))
-> ((:&:) g a e (f l l' l'') -> g e (f l l' l''))
-> (:&:) g a e (f l l' l'')
-> f (e l) (e l') (e l'')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) g a e (f l l' l'') -> g e (f l l' l'')
forall (a :: Family). (:&:) g a a :-> g a
forall (s :: Node) (s' :: Node) (a :: Family).
RemA s s' =>
s a :-> s' a
remA

instance {-# OVERLAPPING #-} (KExtractF3' f g) => KExtractF3' f (g :&: a) where
  kextractF3' :: forall (e :: Family) l l' l''.
(:&:) g a e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3' = g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (e :: Family) l l' l''.
g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (f :: * -> * -> Family) (g :: Node) (e :: Family) l l' l''.
KExtractF3' f g =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3' (g e (f l l' l'') -> f (e l) (e l') (e l''))
-> ((:&:) g a e (f l l' l'') -> g e (f l l' l''))
-> (:&:) g a e (f l l' l'')
-> f (e l) (e l') (e l'')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) g a e (f l l' l'') -> g e (f l l' l'')
forall (a :: Family). (:&:) g a a :-> g a
forall (s :: Node) (s' :: Node) (a :: Family).
RemA s s' =>
s a :-> s' a
remA

instance (KExtractF3 f g) => ExtractF3 f (HFix g) where
  extractF3 :: forall l l' l''.
HFix g (f l l' l'') -> f (HFix g l) (HFix g l') (HFix g l'')
extractF3 (Term g (HFix g) (f l l' l'')
x) = g (HFix g) (f l l' l'')
-> f (Cxt NoHole g (K ()) l)
     (Cxt NoHole g (K ()) l')
     (Cxt NoHole g (K ()) l'')
forall (e :: Family) l l' l''.
ExtractF3 f e =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (f :: * -> * -> Family) (g :: Node) (e :: Family) l l' l''.
(KExtractF3 f g, ExtractF3 f e) =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3 g (HFix g) (f l l' l'')
x

instance {-# OVERLAPPABLE #-} (NotSum g) => KExtractF3' f g where
  kextractF3' :: forall (e :: Family) l l' l''.
g e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3' = String -> g e (f l l' l'') -> f (e l) (e l') (e l'')
forall a. HasCallStack => String -> a
error String
"Undefined use of extractF3"

--------------------------------------------------------------------------------

instance KExtractF3' (,,) TripleF where
  kextractF3' :: forall (e :: Family) l l' l''.
TripleF e (l, l', l'') -> (e l, e l', e l'')
kextractF3' (TripleF e i
a e j
b e k
c) = (e l
e i
a, e l'
e j
b, e l''
e k
c)

--------------------------------------------------------------------------------

-- This is an instance of a distributive law, and can probably be replaced with such.
class (Functor f) => InsertF f e where
  -- | Inverse of extractF. Pushes a functor into a label.
  -- 
  -- Example:
  -- 
  -- @
  -- 'insertF' :: ['JavaProj' 'SourceFileL'] -> 'JavaProj' ['SourceFileL']
  -- @
  -- 
  -- Note that this cannot be used on a labeled tree, as the insertion operation will
  -- require generating additional labels.
  insertF :: (Typeable l) => f (e l) -> e (f l)


insertFHole :: (InsertF e (Context f (HFix g)), Typeable l) => e (HFix g l) -> Context f (HFix g) (e l)
insertFHole :: forall (e :: Family) (f :: Node) (g :: Node) l.
(InsertF e (Context f (HFix g)), Typeable l) =>
e (HFix g l) -> Context f (HFix g) (e l)
insertFHole = e (Cxt Hole f (HFix g) l) -> Cxt Hole f (HFix g) (e l)
forall l.
Typeable l =>
e (Cxt Hole f (HFix g) l) -> Cxt Hole f (HFix g) (e l)
forall (f :: Family) (e :: Family) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF (e (Cxt Hole f (HFix g) l) -> Cxt Hole f (HFix g) (e l))
-> (e (HFix g l) -> e (Cxt Hole f (HFix g) l))
-> e (HFix g l)
-> Cxt Hole f (HFix g) (e l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HFix g l -> Cxt Hole f (HFix g) l)
-> e (HFix g l) -> e (Cxt Hole f (HFix g) l)
forall a b. (a -> b) -> e a -> e b
forall (f :: Family) a b. Functor f => (a -> b) -> f a -> f b
fmap HFix g l -> Cxt Hole f (HFix g) l
forall (a :: Family) i (f :: Node). a i -> Cxt Hole f a i
Hole

instance (ListF :<: e, HFunctor e) => InsertF [] (Cxt h e a) where
  insertF :: forall l. Typeable l => [Cxt h e a l] -> Cxt h e a [l]
insertF [] = Cxt h e a [l]
forall h (f :: Node) (a :: Family) l.
(ListF :<: f, Typeable l) =>
Cxt h f a [l]
riNilF
  insertF (Cxt h e a l
x : [Cxt h e a l]
xs) = Cxt h e a l
x Cxt h e a l -> Cxt h e a [l] -> Cxt h e a [l]
forall (f :: Node) l h (a :: Family).
(ListF :<: f, Typeable l) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
`jConsF` ([Cxt h e a l] -> Cxt h e a [l]
forall l. Typeable l => [Cxt h e a l] -> Cxt h e a [l]
forall (f :: Family) (e :: Family) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF [Cxt h e a l]
xs)

instance (MaybeF :<: e, HFunctor e) => InsertF Maybe (Cxt h e a) where
  insertF :: forall l. Typeable l => Maybe (Cxt h e a l) -> Cxt h e a (Maybe l)
insertF Maybe (Cxt h e a l)
Nothing = Cxt h e a (Maybe l)
forall h (f :: Node) (a :: Family) l.
(MaybeF :<: f, Typeable l) =>
Cxt h f a (Maybe l)
riNothingF
  insertF (Just Cxt h e a l
x) = Cxt h e a l -> Cxt h e a (Maybe l)
forall (f :: Node) l h (a :: Family).
(MaybeF :<: f, Typeable l) =>
Cxt h f a l -> Cxt h f a (Maybe l)
jJustF Cxt h e a l
x


liftF :: (InsertF f h, ExtractF f g, Functor f, Typeable b) => (f (g a) -> f (h b)) -> g (f a) -> h (f b)
liftF :: forall (f :: Family) (h :: Family) (g :: Family) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(f (g a) -> f (h b)) -> g (f a) -> h (f b)
liftF f (g a) -> f (h b)
f = f (h b) -> h (f b)
forall l. Typeable l => f (h l) -> h (f l)
forall (f :: Family) (e :: Family) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF (f (h b) -> h (f b)) -> (g (f a) -> f (h b)) -> g (f a) -> h (f b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (g a) -> f (h b)
f (f (g a) -> f (h b)) -> (g (f a) -> f (g a)) -> g (f a) -> f (h b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g (f a) -> f (g a)
forall l. g (f l) -> f (g l)
forall (f :: Family) (e :: Family) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF

mapF :: (InsertF f h, ExtractF f g, Functor f, Typeable b) => (g a -> h b) -> g (f a) -> h (f b)
mapF :: forall (f :: Family) (h :: Family) (g :: Family) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(g a -> h b) -> g (f a) -> h (f b)
mapF g a -> h b
f = (f (g a) -> f (h b)) -> g (f a) -> h (f b)
forall (f :: Family) (h :: Family) (g :: Family) b a.
(InsertF f h, ExtractF f g, Functor f, Typeable b) =>
(f (g a) -> f (h b)) -> g (f a) -> h (f b)
liftF ((g a -> h b) -> f (g a) -> f (h b)
forall a b. (a -> b) -> f a -> f b
forall (f :: Family) a b. Functor f => (a -> b) -> f a -> f b
fmap g a -> h b
f)

pattern Just' :: (MaybeF :<: f, Typeable l, HFunctor f) => Cxt h f a l -> Cxt h f a (Maybe l)
pattern $mJust' :: forall {r} {f :: Node} {l} {h} {a :: Family}.
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l) -> (Cxt h f a l -> r) -> ((# #) -> r) -> r
$bJust' :: forall (f :: Node) l h (a :: Family).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a (Maybe l)
Just' x <- (project -> (Just (JustF x))) where
  Just' Cxt h f a l
x = MaybeF (Cxt h f a) (Maybe l) -> Cxt h f a (Maybe l)
MaybeF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (MaybeF (Cxt h f a) (Maybe l) -> Cxt h f a (Maybe l))
-> MaybeF (Cxt h f a) (Maybe l) -> Cxt h f a (Maybe l)
forall a b. (a -> b) -> a -> b
$ Cxt h f a l -> MaybeF (Cxt h f a) (Maybe l)
forall i (e :: Family). Typeable i => e i -> MaybeF e (Maybe i)
JustF Cxt h f a l
x

pattern Nothing' :: (MaybeF :<: f, Typeable l, HFunctor f) => Cxt h f a (Maybe l)
pattern $mNothing' :: forall {r} {f :: Node} {l} {h} {a :: Family}.
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l) -> ((# #) -> r) -> ((# #) -> r) -> r
$bNothing' :: forall (f :: Node) l h (a :: Family).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l)
Nothing' <- (project -> Just NothingF) where
  Nothing' = MaybeF (Cxt h f a) (Maybe l) -> Cxt h f a (Maybe l)
MaybeF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject MaybeF (Cxt h f a) (Maybe l)
forall i (e :: Family). Typeable i => MaybeF e (Maybe i)
NothingF


pattern NilF' :: (ListF :<: f, Typeable l, HFunctor f) => Cxt h f a [l]
pattern $mNilF' :: forall {r} {f :: Node} {l} {h} {a :: Family}.
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l] -> ((# #) -> r) -> ((# #) -> r) -> r
$bNilF' :: forall (f :: Node) l h (a :: Family).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
NilF' <- (project -> Just NilF) where
  NilF' = ListF (Cxt h f a) [l] -> Cxt h f a [l]
ListF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject ListF (Cxt h f a) [l]
forall i (e :: Family). Typeable i => ListF e [i]
NilF

pattern ConsF' :: (ListF :<: f, Typeable l, HFunctor f) => Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
pattern $mConsF' :: forall {r} {f :: Node} {l} {h} {a :: Family}.
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
-> (Cxt h f a l -> Cxt h f a [l] -> r) -> ((# #) -> r) -> r
$bConsF' :: forall (f :: Node) l h (a :: Family).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
ConsF' x xs <- (project -> (Just (ConsF x xs))) where
  ConsF' Cxt h f a l
x Cxt h f a [l]
xs = ListF (Cxt h f a) [l] -> Cxt h f a [l]
ListF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (ListF (Cxt h f a) [l] -> Cxt h f a [l])
-> ListF (Cxt h f a) [l] -> Cxt h f a [l]
forall a b. (a -> b) -> a -> b
$ Cxt h f a l -> Cxt h f a [l] -> ListF (Cxt h f a) [l]
forall i (e :: Family). Typeable i => e i -> e [i] -> ListF e [i]
ConsF Cxt h f a l
x Cxt h f a [l]
xs

pattern SingletonF' :: (ListF :<: f, Typeable l, HFunctor f) => Cxt h f a l -> Cxt h f a [l]
pattern $mSingletonF' :: forall {r} {f :: Node} {l} {h} {a :: Family}.
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l] -> (Cxt h f a l -> r) -> ((# #) -> r) -> r
$bSingletonF' :: forall (f :: Node) l h (a :: Family).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a l -> Cxt h f a [l]
SingletonF' x = ConsF' x NilF'

pattern PairF' :: (PairF :<: f, Typeable l, Typeable l', HFunctor f) => Cxt h f a l -> Cxt h f a l' -> Cxt h f a (l, l')
pattern $mPairF' :: forall {r} {f :: Node} {l} {l'} {h} {a :: Family}.
(PairF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a (l, l')
-> (Cxt h f a l -> Cxt h f a l' -> r) -> ((# #) -> r) -> r
$bPairF' :: forall (f :: Node) l l' h (a :: Family).
(PairF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l -> Cxt h f a l' -> Cxt h f a (l, l')
PairF' x y <- (project -> (Just (PairF x y))) where
  PairF' Cxt h f a l
x Cxt h f a l'
y = PairF (Cxt h f a) (l, l') -> Cxt h f a (l, l')
PairF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (PairF (Cxt h f a) (l, l') -> Cxt h f a (l, l'))
-> PairF (Cxt h f a) (l, l') -> Cxt h f a (l, l')
forall a b. (a -> b) -> a -> b
$ Cxt h f a l -> Cxt h f a l' -> PairF (Cxt h f a) (l, l')
forall i j (e :: Family).
(Typeable i, Typeable j) =>
e i -> e j -> PairF e (i, j)
PairF Cxt h f a l
x Cxt h f a l'
y

pattern TripleF' :: (TripleF :<: f, Typeable i, Typeable j, Typeable k, HFunctor f) => Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> Cxt h f a (i,j,k)
pattern $mTripleF' :: forall {r} {f :: Node} {i} {j} {k} {h} {a :: Family}.
(TripleF :<: f, Typeable i, Typeable j, Typeable k, HFunctor f) =>
Cxt h f a (i, j, k)
-> (Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> r)
-> ((# #) -> r)
-> r
$bTripleF' :: forall (f :: Node) i j k h (a :: Family).
(TripleF :<: f, Typeable i, Typeable j, Typeable k, HFunctor f) =>
Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> Cxt h f a (i, j, k)
TripleF' x y z <- (project -> Just (TripleF x y z)) where
  TripleF' Cxt h f a i
x Cxt h f a j
y Cxt h f a k
z = TripleF (Cxt h f a) (i, j, k) -> Cxt h f a (i, j, k)
TripleF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (TripleF (Cxt h f a) (i, j, k) -> Cxt h f a (i, j, k))
-> TripleF (Cxt h f a) (i, j, k) -> Cxt h f a (i, j, k)
forall a b. (a -> b) -> a -> b
$ Cxt h f a i
-> Cxt h f a j -> Cxt h f a k -> TripleF (Cxt h f a) (i, j, k)
forall i j k (e :: Family).
(Typeable i, Typeable j, Typeable k) =>
e i -> e j -> e k -> TripleF e (i, j, k)
TripleF Cxt h f a i
x Cxt h f a j
y Cxt h f a k
z

pattern Left'  :: (EitherF :<: f, Typeable l, Typeable l', HFunctor f) => Cxt h f a l  -> Cxt h f a (Either l l')
pattern $mLeft' :: forall {r} {f :: Node} {l} {l'} {h} {a :: Family}.
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a (Either l l') -> (Cxt h f a l -> r) -> ((# #) -> r) -> r
$bLeft' :: forall (f :: Node) l l' h (a :: Family).
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l -> Cxt h f a (Either l l')
Left'  x <- (project -> (Just (LeftF x))) where
  Left'  Cxt h f a l
x = EitherF (Cxt h f a) (Either l l') -> Cxt h f a (Either l l')
EitherF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (EitherF (Cxt h f a) (Either l l') -> Cxt h f a (Either l l'))
-> EitherF (Cxt h f a) (Either l l') -> Cxt h f a (Either l l')
forall a b. (a -> b) -> a -> b
$ Cxt h f a l -> EitherF (Cxt h f a) (Either l l')
forall i j (e :: Family).
(Typeable i, Typeable j) =>
e i -> EitherF e (Either i j)
LeftF Cxt h f a l
x

pattern Right' :: (EitherF :<: f, Typeable l, Typeable l', HFunctor f) => Cxt h f a l' -> Cxt h f a (Either l l')
pattern $mRight' :: forall {r} {f :: Node} {l} {l'} {h} {a :: Family}.
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a (Either l l') -> (Cxt h f a l' -> r) -> ((# #) -> r) -> r
$bRight' :: forall (f :: Node) l l' h (a :: Family).
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a l' -> Cxt h f a (Either l l')
Right' x <- (project -> (Just (RightF x))) where
  Right' Cxt h f a l'
x = EitherF (Cxt h f a) (Either l l') -> Cxt h f a (Either l l')
EitherF (Cxt h f a) :-> Cxt h f a
forall (g :: Node) (f :: Node) h (a :: Family).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (EitherF (Cxt h f a) (Either l l') -> Cxt h f a (Either l l'))
-> EitherF (Cxt h f a) (Either l l') -> Cxt h f a (Either l l')
forall a b. (a -> b) -> a -> b
$ Cxt h f a l' -> EitherF (Cxt h f a) (Either l l')
forall i j (e :: Family).
(Typeable i, Typeable j) =>
e j -> EitherF e (Either i j)
RightF Cxt h f a l'
x

--------------------------------------------------------------------------------

-- |
-- I really don't like having to copy variants for annotated versions, but must with current design

pattern JustA' :: (MaybeF :<: f, Typeable l, HFunctor f) => Cxt h (f :&: p) a l -> Cxt h (f :&: p) a (Maybe l)
pattern $mJustA' :: forall {r} {f :: Node} {l} {h} {p} {a :: Family}.
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h (f :&: p) a (Maybe l)
-> (Cxt h (f :&: p) a l -> r) -> ((# #) -> r) -> r
JustA' x <- (project' -> (Just (JustF x)))

pattern NilFA' :: (ListF :<: f, Typeable l, HFunctor f) => Cxt h (f :&: p) a [l]
pattern $mNilFA' :: forall {r} {f :: Node} {l} {h} {p} {a :: Family}.
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h (f :&: p) a [l] -> ((# #) -> r) -> ((# #) -> r) -> r
NilFA' <- (project' -> Just NilF)

pattern ConsFA' :: (ListF :<: f, Typeable l, HFunctor f) => Cxt h (f :&: p) a l -> Cxt h (f :&: p) a [l] -> Cxt h (f :&: p) a [l]
pattern $mConsFA' :: forall {r} {f :: Node} {l} {h} {p} {a :: Family}.
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h (f :&: p) a [l]
-> (Cxt h (f :&: p) a l -> Cxt h (f :&: p) a [l] -> r)
-> ((# #) -> r)
-> r
ConsFA' x xs <- (project' -> (Just (ConsF x xs)))

pattern SingletonFA' :: (ListF :<: f, Typeable l, HFunctor f) => Cxt h (f :&: p) a l -> Cxt h (f :&: p) a [l]
pattern $mSingletonFA' :: forall {r} {f :: Node} {l} {h} {p} {a :: Family}.
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h (f :&: p) a [l]
-> (Cxt h (f :&: p) a l -> r) -> ((# #) -> r) -> r
SingletonFA' x <- (ConsFA' x NilFA')