{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
-- 
-- 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
  , riNilF
  , iConsF
  , 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, makeHFunctor, makeHTraversable, makeHFoldable, makeEqHF, makeShowHF, makeOrdHF )

import Data.Comp.Multi.Strategy.Classification

import Data.Typeable ( Typeable, eqT )
import Data.Proxy

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)

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

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

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


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

--------------------------------------------------------------------------------
-- 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 :: MaybeF e b -> Maybe (b :~: Maybe l)
kdyncase NothingF  = Maybe (b :~: Maybe l)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  kdyncase (JustF _) = 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 :: ListF e b -> Maybe (b :~: [l])
kdyncase NilF        = Maybe (b :~: [l])
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  kdyncase (ConsF _ _) = 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 :: PairF e b -> Maybe (b :~: (l, l'))
kdyncase (PairF _ _) = 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 :: TripleF e b -> Maybe (b :~: (l, l', l''))
kdyncase (TripleF _ _ _) = 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 :: EitherF e b -> Maybe (b :~: Either l l')
kdyncase (LeftF _)  = Maybe (b :~: Either l l')
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  kdyncase (RightF _) = 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 :: Cxt h f a (Maybe l)
riNothingF = MaybeF (Cxt h f a) (Maybe l) -> Cxt h f a (Maybe l)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject MaybeF (Cxt h f a) (Maybe l)
forall l (e :: * -> *). Typeable l => MaybeF e (Maybe l)
NothingF

iJustF :: (MaybeF :-<: fs, InjF fs (Maybe l) l', Typeable l) => CxtS h fs a l -> CxtS h fs a l'
iJustF :: CxtS h fs a l -> CxtS h fs a l'
iJustF = CxtS h fs a (Maybe l) -> CxtS h fs a l'
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a 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 :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l) =>
Cxt h f a l -> Cxt h f a (Maybe l)
iJust

iJust :: (MaybeF :<: f, Typeable l) => Cxt h f a l -> Cxt h f a (Maybe l)
iJust :: Cxt h f a l -> Cxt h f a (Maybe l)
iJust = MaybeF (Cxt h f a) (Maybe l) -> Cxt h f a (Maybe l)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 l (e :: * -> *). Typeable l => e l -> MaybeF e (Maybe l)
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 :: Cxt h f a [l]
riNilF = ListF (Cxt h f a) [l] -> Cxt h f a [l]
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject ListF (Cxt h f a) [l]
forall l (e :: * -> *). Typeable l => ListF e [l]
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 :: CxtS h fs a l -> CxtS h fs a [l] -> CxtS h fs a l'
iConsF x :: CxtS h fs a l
x y :: CxtS h fs a [l]
y = CxtS h fs a [l] -> CxtS h fs a l'
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
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 :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
iCons CxtS h fs a l
x CxtS h fs a [l]
y)

iCons :: (ListF :<: f, Typeable l) => Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
iCons :: Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
iCons x :: Cxt h f a l
x y :: Cxt h f a [l]
y = ListF (Cxt h f a) [l] -> Cxt h f a [l]
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 l (e :: * -> *). Typeable l => e l -> e [l] -> ListF e [l]
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 :: Cxt h f a i -> Cxt h f a j -> Cxt h f a (i, j)
riPairF x :: Cxt h f a i
x y :: Cxt h f a j
y = PairF (Cxt h f a) (i, j) -> Cxt h f a (i, j)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 :: * -> *).
(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 :: Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> Cxt h f a (i, j, k)
riTripleF x :: Cxt h f a i
x y :: Cxt h f a j
y z :: Cxt h f a k
z = TripleF (Cxt h f a) (i, j, k) -> Cxt h f a (i, j, k)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 :: * -> *).
(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 :: 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)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 :: * -> *).
(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 :: 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)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 :: * -> *).
(Typeable i, Typeable j) =>
e j -> EitherF e (Either i j)
RightF

$(derive [makeHFunctor, makeHTraversable, makeHFoldable, makeEqHF, makeShowHF,
                    makeOrdHF ]
       [''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 KExtractF' f g => KExtractF f g where
  kextractF :: g e (f l) -> f (e l)
kextractF = g e (f l) -> f (e l)
forall (f :: * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) l.
KExtractF' f g =>
g e (f l) -> f (e l)
kextractF'

instance (All (KExtractF f) gs) => KExtractF f (Sum gs) where
  kextractF :: Sum gs e (f l) -> f (e l)
kextractF = Proxy (KExtractF f)
-> (forall (f :: (* -> *) -> * -> *).
    KExtractF f f =>
    f e (f l) -> f (e l))
-> Sum gs e (f l)
-> f (e l)
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy (KExtractF f)
forall k (t :: k). Proxy t
Proxy @(KExtractF f)) forall (f :: * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) l.
(KExtractF f g, ExtractF f e) =>
g e (f l) -> f (e l)
forall (f :: (* -> *) -> * -> *).
KExtractF f f =>
f e (f l) -> f (e l)
kextractF

instance (All (KExtractF' f) gs) => KExtractF' f (Sum gs) where
  kextractF' :: Sum gs e (f l) -> f (e l)
kextractF' = Proxy (KExtractF' f)
-> (forall (f :: (* -> *) -> * -> *).
    KExtractF' f f =>
    f e (f l) -> f (e l))
-> Sum gs e (f l)
-> f (e l)
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy (KExtractF' f)
forall k (t :: k). Proxy t
Proxy @(KExtractF' f)) forall (f :: * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) l.
KExtractF' f g =>
g e (f l) -> f (e l)
forall (f :: (* -> *) -> * -> *).
KExtractF' f f =>
f e (f l) -> f (e l)
kextractF'

instance (KExtractF f g) => KExtractF f (g :&: a) where
  kextractF :: (:&:) g a e (f l) -> f (e l)
kextractF = g e (f l) -> f (e l)
forall (f :: * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) 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 (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA

instance (KExtractF' f g) => KExtractF' f (g :&: a) where
  kextractF' :: (:&:) g a e (f l) -> f (e l)
kextractF' = g e (f l) -> f (e l)
forall (f :: * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) 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 (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA

instance (Applicative f) => ExtractF f (K a) where
  extractF :: K a (f l) -> f (K a l)
extractF = K a l -> f (K a l)
forall (f :: * -> *) 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 :: Cxt h g a (f l) -> f (Cxt h g a l)
extractF (Term x :: g (Cxt h g a) (f l)
x) = g (Cxt h g a) (f l) -> f (Cxt h g a l)
forall (f :: * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) 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 x :: a (f l)
x) = (a l -> Cxt Hole g a l) -> f (a l) -> f (Cxt Hole g a l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a l -> Cxt Hole g a l
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
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 (f :: * -> *) (e :: * -> *) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF a (f l)
x

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

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

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

instance KExtractF' Maybe MaybeF where
  kextractF' :: MaybeF e (Maybe l) -> Maybe (e l)
kextractF' NothingF = Maybe (e l)
forall a. Maybe a
Nothing
  kextractF' (JustF x :: e l
x) = e l -> Maybe (e l)
forall a. a -> Maybe a
Just 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 KExtractF2' f g => KExtractF2 f g where
  kextractF2 :: g e (f l l') -> f (e l) (e l')
kextractF2 = g e (f l l') -> f (e l) (e l')
forall (f :: * -> * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) l
       l'.
KExtractF2' f g =>
g e (f l l') -> f (e l) (e l')
kextractF2'

instance (All (KExtractF2 f) gs) => KExtractF2 f (Sum gs) where
  kextractF2 :: Sum gs e (f l l') -> f (e l) (e l')
kextractF2 = Proxy (KExtractF2 f)
-> (forall (f :: (* -> *) -> * -> *).
    KExtractF2 f f =>
    f e (f l l') -> f (e l) (e l'))
-> Sum gs e (f l l')
-> f (e l) (e l')
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy (KExtractF2 f)
forall k (t :: k). Proxy t
Proxy @(KExtractF2 f)) forall (f :: * -> * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) l
       l'.
(KExtractF2 f g, ExtractF2 f e) =>
g e (f l l') -> f (e l) (e l')
forall (f :: (* -> *) -> * -> *).
KExtractF2 f f =>
f e (f l l') -> f (e l) (e l')
kextractF2

instance (All (KExtractF2' f) gs) => KExtractF2' f (Sum gs) where
  kextractF2' :: Sum gs e (f l l') -> f (e l) (e l')
kextractF2' = Proxy (KExtractF2' f)
-> (forall (f :: (* -> *) -> * -> *).
    KExtractF2' f f =>
    f e (f l l') -> f (e l) (e l'))
-> Sum gs e (f l l')
-> f (e l) (e l')
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy (KExtractF2' f)
forall k (t :: k). Proxy t
Proxy @(KExtractF2' f)) forall (f :: * -> * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) l
       l'.
KExtractF2' f g =>
g e (f l l') -> f (e l) (e l')
forall (f :: (* -> *) -> * -> *).
KExtractF2' f f =>
f e (f l l') -> f (e l) (e l')
kextractF2'

instance (KExtractF2 f g) => KExtractF2 f (g :&: a) where
  kextractF2 :: (:&:) g a e (f l l') -> f (e l) (e l')
kextractF2 = g e (f l l') -> f (e l) (e l')
forall (f :: * -> * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) 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 (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA

instance (KExtractF2' f g) => KExtractF2' f (g :&: a) where
  kextractF2' :: (:&:) g a e (f l l') -> f (e l) (e l')
kextractF2' = g e (f l l') -> f (e l) (e l')
forall (f :: * -> * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) 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 (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA

instance (KExtractF2 f g) => ExtractF2 f (HFix g) where
  extractF2 :: HFix g (f l l') -> f (HFix g l) (HFix g l')
extractF2 (Term x :: g (HFix g) (f l l')
x) = g (HFix g) (f l l') -> f (HFix g l) (HFix g l')
forall (f :: * -> * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) 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 (NotSum g) => KExtractF2' f g where
  kextractF2' :: 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 "Undefined use of extractF2"

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

instance KExtractF2' (,) PairF where
  kextractF2' :: PairF e (l, l') -> (e l, e l')
kextractF2' (PairF a :: e i
a b :: e j
b) = (e l
e i
a, e l'
e j
b)

instance KExtractF2' Either EitherF where
  kextractF2' :: EitherF e (Either l l') -> Either (e l) (e l')
kextractF2' (LeftF  a :: e i
a) = e i -> Either (e i) (e l')
forall a b. a -> Either a b
Left e i
a
  kextractF2' (RightF a :: e j
a) = e j -> Either (e l) (e j)
forall a b. b -> Either a b
Right 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 KExtractF3' f g => KExtractF3 f g where
  kextractF3 :: 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 (f :: * -> * -> * -> *) (g :: (* -> *) -> * -> *)
       (e :: * -> *) l l' l''.
KExtractF3' f g =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3'

instance (All (KExtractF3 f) gs) => KExtractF3 f (Sum gs) where
  kextractF3 :: Sum gs e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3 = Proxy (KExtractF3 f)
-> (forall (f :: (* -> *) -> * -> *).
    KExtractF3 f f =>
    f e (f l l' l'') -> f (e l) (e l') (e l''))
-> Sum gs e (f l l' l'')
-> f (e l) (e l') (e l'')
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy (KExtractF3 f)
forall k (t :: k). Proxy t
Proxy @(KExtractF3 f)) forall (f :: * -> * -> * -> *) (g :: (* -> *) -> * -> *)
       (e :: * -> *) l l' l''.
(KExtractF3 f g, ExtractF3 f e) =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (f :: (* -> *) -> * -> *).
KExtractF3 f f =>
f e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3

instance (All (KExtractF3' f) gs) => KExtractF3' f (Sum gs) where
  kextractF3' :: Sum gs e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3' = Proxy (KExtractF3' f)
-> (forall (f :: (* -> *) -> * -> *).
    KExtractF3' f f =>
    f e (f l l' l'') -> f (e l) (e l') (e l''))
-> Sum gs e (f l l' l'')
-> f (e l) (e l') (e l'')
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy (KExtractF3' f)
forall k (t :: k). Proxy t
Proxy @(KExtractF3' f)) forall (f :: * -> * -> * -> *) (g :: (* -> *) -> * -> *)
       (e :: * -> *) l l' l''.
KExtractF3' f g =>
g e (f l l' l'') -> f (e l) (e l') (e l'')
forall (f :: (* -> *) -> * -> *).
KExtractF3' f f =>
f e (f l l' l'') -> f (e l) (e l') (e l'')
kextractF3'

instance (KExtractF3 f g) => KExtractF3 f (g :&: a) where
  kextractF3 :: (:&:) 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 (f :: * -> * -> * -> *) (g :: (* -> *) -> * -> *)
       (e :: * -> *) 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 (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA

instance (KExtractF3' f g) => KExtractF3' f (g :&: a) where
  kextractF3' :: (:&:) 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 (f :: * -> * -> * -> *) (g :: (* -> *) -> * -> *)
       (e :: * -> *) 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 (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA

instance (KExtractF3 f g) => ExtractF3 f (HFix g) where
  extractF3 :: HFix g (f l l' l'') -> f (HFix g l) (HFix g l') (HFix g l'')
extractF3 (Term x :: g (HFix g) (f l l' l'')
x) = g (HFix g) (f l l' l'') -> f (HFix g l) (HFix g l') (HFix g l'')
forall (f :: * -> * -> * -> *) (g :: (* -> *) -> * -> *)
       (e :: * -> *) 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 (NotSum g) => KExtractF3' f g where
  kextractF3' :: 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 "Undefined use of extractF3"

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

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

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

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.
  -- 
  -- This is an instance of a distributive law, and can probably be replaced with such.
  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 :: e (HFix g l) -> Context f (HFix g) (e l)
insertFHole = e (Cxt Hole f (HFix g) l) -> Context f (HFix g) (e l)
forall (f :: * -> *) (e :: * -> *) l.
(InsertF f e, Typeable l) =>
f (e l) -> e (f l)
insertF (e (Cxt Hole f (HFix g) l) -> Context f (HFix g) (e l))
-> (e (HFix g l) -> e (Cxt Hole f (HFix g) l))
-> e (HFix g l)
-> Context 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HFix g l -> Cxt Hole f (HFix g) l
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole

instance (ListF :<: e, HFunctor e) => InsertF [] (Cxt h e a) where
  insertF :: [Cxt h e a l] -> Cxt h e a [l]
insertF [] = Cxt h e a [l]
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) l.
(ListF :<: f, Typeable l) =>
Cxt h f a [l]
riNilF
  insertF (x :: Cxt h e a l
x : xs :: [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 :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l) =>
Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
`iCons` ([Cxt h e a l] -> Cxt h e a [l]
forall (f :: * -> *) (e :: * -> *) 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 :: Maybe (Cxt h e a l) -> Cxt h e a (Maybe l)
insertF Nothing = Cxt h e a (Maybe l)
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) l.
(MaybeF :<: f, Typeable l) =>
Cxt h f a (Maybe l)
riNothingF
  insertF (Just x :: Cxt h e a l
x) = Cxt h e a l -> Cxt h e a (Maybe l)
forall (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l) =>
Cxt h f a l -> Cxt h f a (Maybe l)
iJust 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 :: (f (g a) -> f (h b)) -> g (f a) -> h (f b)
liftF f :: f (g a) -> f (h b)
f = f (h b) -> h (f b)
forall (f :: * -> *) (e :: * -> *) 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 (f :: * -> *) (e :: * -> *) 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 :: (g a -> h b) -> g (f a) -> h (f b)
mapF f :: g a -> h b
f = (f (g a) -> f (h b)) -> g (f a) -> h (f b)
forall (f :: * -> *) (h :: * -> *) (g :: * -> *) 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 (f :: * -> *) 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 $bJust' :: Cxt h f a l -> Cxt h f a (Maybe l)
$mJust' :: forall r (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h f a (Maybe l) -> (Cxt h f a l -> r) -> (Void# -> r) -> r
Just' x <- (project -> (Just (JustF x))) where
  Just' x :: Cxt h f a l
x = MaybeF (Cxt h f a) (Maybe l) -> Cxt h f a (Maybe l)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 l (e :: * -> *). Typeable l => e l -> MaybeF e (Maybe l)
JustF Cxt h f a l
x

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


pattern NilF' :: (ListF :<: f, Typeable l, HFunctor f) => Cxt h f a [l]
pattern $bNilF' :: Cxt h f a [l]
$mNilF' :: forall r (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l] -> (Void# -> r) -> (Void# -> r) -> r
NilF' <- (project -> Just NilF) where
  NilF' = ListF (Cxt h f a) [l] -> Cxt h f a [l]
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject ListF (Cxt h f a) [l]
forall l (e :: * -> *). Typeable l => ListF e [l]
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 $bConsF' :: Cxt h f a l -> Cxt h f a [l] -> Cxt h f a [l]
$mConsF' :: forall r (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l]
-> (Cxt h f a l -> Cxt h f a [l] -> r) -> (Void# -> r) -> r
ConsF' x xs <- (project -> (Just (ConsF x xs))) where
  ConsF' x :: Cxt h f a l
x xs :: Cxt h f a [l]
xs = ListF (Cxt h f a) [l] -> Cxt h f a [l]
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 l (e :: * -> *). Typeable l => e l -> e [l] -> ListF e [l]
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 $bSingletonF' :: Cxt h f a l -> Cxt h f a [l]
$mSingletonF' :: forall r (f :: (* -> *) -> * -> *) l h (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h f a [l] -> (Cxt h f a l -> r) -> (Void# -> r) -> r
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 $bPairF' :: Cxt h f a l -> Cxt h f a l' -> Cxt h f a (l, l')
$mPairF' :: forall r (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(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) -> (Void# -> r) -> r
PairF' x y <- (project -> (Just (PairF x y))) where
  PairF' x :: Cxt h f a l
x y :: Cxt h f a l'
y = PairF (Cxt h f a) (l, l') -> Cxt h f a (l, l')
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 :: * -> *).
(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 $bTripleF' :: Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> Cxt h f a (i, j, k)
$mTripleF' :: forall r (f :: (* -> *) -> * -> *) i j k h (a :: * -> *).
(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)
-> (Void# -> r)
-> r
TripleF' x y z <- (project -> Just (TripleF x y z)) where
  TripleF' x :: Cxt h f a i
x y :: Cxt h f a j
y z :: Cxt h f a k
z = TripleF (Cxt h f a) (i, j, k) -> Cxt h f a (i, j, k)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 :: * -> *).
(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 $bLeft' :: Cxt h f a l -> Cxt h f a (Either l l')
$mLeft' :: forall r (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a (Either l l') -> (Cxt h f a l -> r) -> (Void# -> r) -> r
Left'  x <- (project -> (Just (LeftF x))) where
  Left'  x :: Cxt h f a l
x = EitherF (Cxt h f a) (Either l l') -> Cxt h f a (Either l l')
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 :: * -> *).
(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 $bRight' :: Cxt h f a l' -> Cxt h f a (Either l l')
$mRight' :: forall r (f :: (* -> *) -> * -> *) l l' h (a :: * -> *).
(EitherF :<: f, Typeable l, Typeable l', HFunctor f) =>
Cxt h f a (Either l l') -> (Cxt h f a l' -> r) -> (Void# -> r) -> r
Right' x <- (project -> (Just (RightF x))) where
  Right' x :: Cxt h f a l'
x = EitherF (Cxt h f a) (Either l l') -> Cxt h f a (Either l l')
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(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 :: * -> *).
(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 :: (* -> *) -> * -> *) l h p (a :: * -> *).
(MaybeF :<: f, Typeable l, HFunctor f) =>
Cxt h (f :&: p) a (Maybe l)
-> (Cxt h (f :&: p) a l -> r) -> (Void# -> 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 :: (* -> *) -> * -> *) l h p (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h (f :&: p) a [l] -> (Void# -> r) -> (Void# -> 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 :: (* -> *) -> * -> *) l h p (a :: * -> *).
(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)
-> (Void# -> 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 :: (* -> *) -> * -> *) l h p (a :: * -> *).
(ListF :<: f, Typeable l, HFunctor f) =>
Cxt h (f :&: p) a [l]
-> (Cxt h (f :&: p) a l -> r) -> (Void# -> r) -> r
SingletonFA' x <- (ConsFA' x NilFA')