content: {-# LANGUAGE TypeFamilyDependencies #-}
  
  {-# LANGUAGE DataKinds #-}
  
  {-# language LambdaCase, TemplateHaskell, BlockArguments, RankNTypes,
      MultiParamTypeClasses, FunctionalDependencies, TypeApplications,
      ScopedTypeVariables, UndecidableInstances, QuantifiedConstraints,
      TypeFamilies, CPP, PartialTypeSignatures, MagicHash, AllowAmbiguousTypes #-}
  {-# OPTIONS_GHC -Wno-partial-type-signatures #-}
  
  module Gen3 where
  
  import Prelude hiding (filter, zip, zipWith, take, drop)
  import qualified Prelude as P
  import Control.Monad
  import Language.Haskell.TH hiding (ListT, ListE, Type)
  import Control.Monad.State.Strict
  import Control.Monad.Reader
  import Control.Monad.Except
  import Control.Monad.Identity
  import Control.Monad.Trans
  import Control.Monad.Trans.Maybe
  import Data.Coerce
  import Control.Applicative
  import Data.Kind
  import Up
  
  import GHC.Exts
  
  #include "Sugar.h"
  
  newtype Gen a = Gen {unGen :: forall r. (a -> Up r) -> Up r}
  
  runGen :: Gen (Up a) -> Up a
  runGen (Gen f) = f id
  
  instance Functor Gen where
    fmap f ma = Gen \k -> unGen ma \a -> k (f a)
  
  instance Applicative Gen where
    pure a = Gen \k -> k a
    (<*>) gf ga = Gen \k -> unGen gf \f -> unGen ga \a -> k (f a)
  
  instance Monad Gen where
    return = pure
    (>>=) ga f = Gen \k -> unGen ga \a -> unGen (f a) k
  
  instance MonadFail Gen where
    fail = error
  
  class Monad m => MonadGen m where
    liftGen :: Gen a -> m a
  
  instance MonadGen Gen where
    liftGen = id
  
  instance MonadGen m => MonadGen (StateT s m) where
    liftGen = lift . liftGen
  
  instance MonadGen m => MonadGen (ReaderT r m) where
    liftGen = lift . liftGen
  
  instance MonadGen m => MonadGen (ExceptT e m) where
    liftGen = lift . liftGen
  
  instance MonadGen m => MonadGen (MaybeT m) where
    liftGen = lift . liftGen
  
  --------------------------------------------------------------------------------
  
  type Rep :: Type -> Type
  type family Rep a = r | r -> a
  
  class Repr a where
    up   :: Up (Rep a) -> a
    down :: a -> Up (Rep a)
  
  type instance Rep (Gen Bool) = Bool
  instance Repr (Gen Bool) where
    up x   = Gen \k -> [|| if $$x then $$(k True) else $$(k False) ||]
    down x = unGen x \x -> if x then [||True||] else [||False||]
  
  type instance Rep (Gen (Either a b)) = Either (Rep a) (Rep b)
  instance (Repr a, Repr b) => Repr (Gen (Either a b)) where
    up x = Gen \k ->
      [|| case $$x of Left x -> $$(k (Left (up [||x||]))); Right x -> $$(k (Right (up [||x||]))) ||]
    down x =
      unGen x \case Left x -> [|| Left $$(down x) ||]; Right x -> [|| Right $$(down x) ||]
  
  type instance Rep (Gen (Maybe a)) = Maybe (Rep a)
  instance (Repr a) => Repr (Gen (Maybe a)) where
    up x = Gen \k ->
      [|| case $$x of Nothing -> $$(k Nothing); Just x -> $$(k (Just (up [||x||]))) ||]
    down x =
      unGen x \case Nothing -> [|| Nothing ||]; Just x -> [|| Just $$(down x) ||]
  
  type instance Rep () = ()
  instance Repr () where
    up _ = ()
    down _ = [||()||]
  
  type instance Rep (Gen (a, b)) = (Rep a, Rep b)
  instance (Repr a, Repr b) => Repr (Gen (a, b)) where
    up x   = Gen \k -> [|| case $$x of (x, y) -> $$(k (up [||x||], up [||y||])) ||]
    down x = unGen x \(x, y) -> [|| ($$(down x), $$(down y)) ||]
  
  type Rep1 :: (Type -> Type) -> (Type -> Type)
  type family Rep1 f = r | r -> f
  
  class Repr1 f where
    up1   :: Repr a => Up (Rep1 f (Rep a)) -> f a
    down1 :: Repr a => f a -> Up (Rep1 f (Rep a))
  
  type instance Rep1 Gen = Identity
  instance Repr1 Gen where
    up1 x = Gen \k -> k (up [|| runIdentity $$x ||])
    down1 x = unGen x \a -> [|| Identity $$(down a) ||]
  
  
  
  -- Finite
  --------------------------------------------------------------------------------
  
  -- -- a finite product of Up-s
  -- data ProdUp a where
  --   HUp   :: ProdUp (Up a)
  --   HPair :: ProdUp a -> ProdUp b -> ProdUp (a, b)
  
  -- -- a finite product/sum of Up-s
  -- data ProdSumUp a where
  --   JUp     :: ProdSumUp (Up a)
  --   JEither :: ProdSumUp a -> ProdSumUp b -> ProdSumUp (Either a b)
  --   JMaybe  :: ProdSumUp a -> ProdSumUp (Maybe a)
  --   JPair   :: ProdSumUp a -> ProdSumUp b -> ProdSumUp (a, b)
  
  -- class IsProdSumUp a where
  --   prodSumUp :: ProdSumUp a
  -- instance IsProdSumUp (Up a) where
  --   prodSumUp = JUp
  -- instance (IsProdSumUp a, IsProdSumUp b) => IsProdSumUp (Either a b) where
  --   prodSumUp = JEither prodSumUp prodSumUp
  -- instance (IsProdSumUp a, IsProdSumUp b) => IsProdSumUp (a, b) where
  --   prodSumUp = JPair prodSumUp prodSumUp
  -- instance IsProdSumUp a => IsProdSumUp (Maybe a) where
  --   prodSumUp = JMaybe prodSumUp
  
  -- type family Arr a r where
  --   Arr (Up a)       (Up r) = Up (a -> r)
  --   Arr (a, b)       (Up r) = Arr a (Arr b (Up r))
  --   Arr (Either a b) (Up r) = (Arr a (Up r), Arr b (Up r))
  --   Arr (Maybe a)    (Up r) = (Arr (Up ()) (Up r), Arr a (Up r))
  --   Arr a            (b, c) = (Arr a b, Arr a c)
  
  -- arrIsProdUp :: forall a r. ProdSumUp a -> ProdUp r -> ProdUp (Arr a r)
  -- arrIsProdUp JUp           r@HUp = HUp
  -- arrIsProdUp (JPair a b)   r@HUp = arrIsProdUp a (arrIsProdUp b r)
  -- arrIsProdUp (JEither a b) r@HUp = HPair (arrIsProdUp a r) (arrIsProdUp b r)
  -- arrIsProdUp (JMaybe a)    r@HUp = HPair (arrIsProdUp JUp r) (arrIsProdUp a r)
  -- arrIsProdUp a     r@(HPair b c) = HPair (arrIsProdUp a b) (arrIsProdUp a c)
  
  -- handle :: forall a r. ProdSumUp a -> ProdUp r -> (a -> r) -> Arr a r
  -- handle JUp           r@HUp f = [|| \a -> $$(f [||a||]) ||]
  -- handle (JPair a b)   r@HUp f = handle a (arrIsProdUp b r) \x -> handle b r \y -> f (x, y)
  -- handle (JEither a b) r@HUp f = (handle a r (f . Left), handle b r (f . Right))
  -- handle (JMaybe a)    r@HUp f = (handle JUp r (const (f Nothing)), handle a r (f . Just))
  -- handle a     r@(HPair b c) f = (handle a b (fst . f), handle a c (snd . f))
  
  -- unhandle :: forall a r. ProdSumUp a -> ProdUp r -> Arr a r -> (a -> r)
  -- unhandle JUp           r@HUp f = \x -> [|| $$f $$x ||]
  -- unhandle (JPair a b)   r@HUp f = \(x, y) -> unhandle b r (unhandle a (arrIsProdUp b r) f x) y
  -- unhandle (JEither a b) r@HUp f = either (unhandle a r (fst f)) (unhandle b r (snd f))
  -- unhandle (JMaybe a)    r@HUp f = maybe (unhandle JUp r (fst f) tt) (unhandle a r (snd f))
  -- unhandle a     r@(HPair b c) f = \x -> (unhandle a b (fst f) x, unhandle a c (snd f) x)
  
  
  -- letG :: forall a m. (IsProdSumUp a, MonadGen m) => a -> m a
  -- letG a = liftGen (go prodSumUp a) where
  --   go :: forall a. ProdSumUp a -> a -> Gen a
  --   go JUp           x = Gen $ \k -> [|| let y = $$x in seq y $$(k Q(y)) ||]
  --   go (JEither a b) x = either ((Left <$>). go a) ((Right <$>). go b) x
  --   go (JMaybe a)    x = maybe (pure Nothing) ((Just <$>) . go a) x
  --   go (JPair a b)   x = (,) <$> go a (fst x) <*> go b (snd x)
  
  -- -- letG :: MonadGen m => Up a -> m (Up a)
  -- -- letG a = liftGen $ Gen $ \k -> [|| let x = $$a in seq x $$(k Q(x)) ||]
  
  
  -- --------------------------------------------------------------------------------
  
  -- class Split a b | a -> b, b -> a where
  --   split :: Up a -> Gen b
  
  -- caseG :: MonadGen m => Split a b => Up a -> (b -> m c) -> m c
  -- caseG a f = liftGen (split a) >>= f
  
  -- instance Split Bool Bool where
  --   split x = Gen \k -> [|| case $$x of
  --     True -> $$(k True)
  --     _    -> $$(k False) ||]
  
  -- instance Split [a] (Maybe (Up a, Up [a])) where
  --   split x = Gen \k -> [|| case $$x of
  --     []   -> $$(k Nothing)
  --     a:as -> $$(k (Just (Q(a), Q(as)))) ||]
  
  -- instance Split (a, b) (Up a, Up b) where
  --   split x = Gen \k -> [|| case $$x of
  --     (a, b) -> $$(k (Q(a), Q(b))) ||]
  
  -- instance Split (Either a b) (Either (Up a) (Up b)) where
  --   split x = Gen \k -> [|| case $$x of
  --     Left a  -> $$(k (Left Q(a)))
  --     Right b -> $$(k (Right Q(b))) ||]
  
  -- --------------------------------------------------------------------------------
  
  -- class MonadGen n => Improve m n | m -> n, n -> m where
  --   up   :: Up (m a) -> n (Up a)
  --   down :: n (Up a) -> Up (m a)
  
  -- instance Improve Identity Gen where
  --   up x = Gen \k -> k Q(runIdentity $$x)
  --   down x = unGen x \a -> Q(Identity $$a)
  
  -- instance Improve m n => Improve (StateT s m) (StateT (Up s) n) where
  
  --   up x = StateT \s ->
  --     do as <- up [|| runStateT $$x $$s ||]
  --        caseG as pure
  
  --   down x = [|| StateT \s -> $$(down
  --     do (a, s) <- runStateT x Q(s)
  --        pure Q(($$a, $$s))
  --        )||]
  
  -- instance Improve m n => Improve (ExceptT e m) (ExceptT (Up e) n) where
  --   up x = ExceptT do
  --     ea <- up Q(runExceptT $$x)
  --     caseG ea pure
  
  --   down (ExceptT x) =
  --     [|| ExceptT $$(down (x >>= \case
  --           Left e  -> pure Q(Left $$e)
  --           Right a -> pure Q(Right $$a)
  --                         )) ||]
  
  -- instance Improve m n => Improve (ReaderT r m) (ReaderT (Up r) n) where
  --   up   x = ReaderT \r -> up Q(runReaderT $$x $$r)
  --   down x = [|| ReaderT \r -> $$(down (runReaderT x Q(r))) ||]
  
  -- --------------------------------------------------------------------------------
  
  -- -- putG :: (MonadGen m, MonadState (Up s) m) => Up s -> m (Up ())
  -- -- putG s = do
  -- --   s <- letG s
  -- --   put s
  -- --   pure Q(())
  
  -- -- modifyG :: (MonadGen m, MonadState (Up s) m) => (Up s -> Up s) -> m (Up ())
  -- -- modifyG f = do
  -- --   s <- get
  -- --   putG (f s)
  
  -- -- localG :: (MonadGen m, MonadReader (Up r) m) => (Up r -> Up r) -> m a -> m a
  -- -- localG f ma = do
  -- --   r  <- ask
  -- --   r' <- letGLazy (f r)
  -- --   local (const r') ma
  
  -- -- -- Push
  -- -- --------------------------------------------------------------------------------
  
  -- -- newtype Push a = Push {unPush :: forall r. (a -> Up r -> Up r) -> Up r -> Up r}
  -- --   deriving Functor
  
  -- -- instance Semigroup (Push  a) where
  -- --   Push xs <> Push ys = Push \c n -> xs c (ys c n)
  
  -- -- instance Monoid (Push a) where
  -- --   mempty = Push \c n -> n
  
  -- -- instance Applicative Push where
  -- --   pure a = Push \c n -> c a n
  -- --   Push fs <*> Push as = Push \c -> fs \f -> as \a -> c (f a)
  
  -- -- instance Monad Push where
  -- --   return = pure
  -- --   Push as >>= f = Push \c -> as \a -> unPush (f a) c
  
  -- -- instance MonadGen Push where
  -- --   liftGen ga = Push \c n -> unGen ga \a -> c a n
  
  -- -- class ToPush a b | a -> b where
  -- --   push :: a -> Push b
  
  -- -- instance ToPush (Up [a]) (Up a) where
  -- --   push as = Push \c n -> Q(let go [] = $$n; go (a:as) = $$(c Q(a) Q(go as)) in go $$as)
  
  -- -- class ToList a b | a -> b where
  -- --   list :: a -> Up [b]
  
  -- -- instance ToList (Push (Up a)) a where
  -- --   list as = unPush as (\a as -> Q($$a : $$as)) Q([])
  
  -- -- class Filter f where
  -- --   filter :: (a -> Up Bool) -> f a -> f a
  
  -- -- instance Filter Push where
  -- --   filter f as = do
  -- --     a <- as
  -- --     caseG (f a) \case
  -- --       True -> pure a
  -- --       _    -> mempty
  
  -- -- class Drop f where
  -- --   drop :: Up Int -> f a -> f a
  
  -- -- instance Drop Push where
  -- --   drop n (Push as) = Push \c nil -> [||
  -- --     $$(as (\a hyp -> [||\i -> case i <=# 0# of
  -- --               1# -> $$(c a [|| $$hyp 0# ||])
  -- --               _  -> $$hyp (i -# 1#) ||])
  -- --           [|| \_ -> $$nil ||]) (case $$n of I# i -> i)  ||]
  
  -- -- class Take f where
  -- --   take :: Up Int -> f a -> f a
  
  -- -- instance Take Push where
  -- --   take n (Push as) = Push \c nil -> [||
  -- --     $$(as (\a hyp -> [||\i -> case i <=# 0# of
  -- --               1# -> $$nil
  -- --               _  -> $$(c a [|| $$hyp (i -# 1#) ||]) ||])
  -- --           [|| \_ -> $$nil ||]) (case $$n of I# i -> i)
  -- --     ||]
  
  -- -- instance Improve [] Push where
  -- --   up   = push
  -- --   down = list
  
  -- -- traversePush :: Improve m n => (Up a -> n (Up b)) -> Push (Up a) -> Up (m [b])
  -- -- traversePush f as =
  -- --   unPush as (\a bs -> down do {bs <- up bs; b <- f a; pure [|| $$b : $$bs ||]}) (down $ pure [||[]||])
  
  -- -- --------------------------------------------------------------------------------
  
  -- -- data Pull a = forall s. Pull (Up s) (Up s -> MaybeT Gen (Up s, a))
  
  -- -- data Pair a b = Pair !a !b
  
  -- -- instance Split (Pair a b) (Pair (Up a) (Up b)) where
  -- --   split ab = Gen \k -> [|| case $$ab of Pair a b -> $$(k (Pair Q(a) Q(b))) ||]
  
  -- -- instance Functor Pull where
  -- --   fmap f (Pull s step) = Pull s (fmap (fmap (fmap f)) step)
  
  -- -- instance Applicative Pull where
  -- --   pure a = Pull Up.tt \s -> pure (s, a)
  -- --   Pull s step <*> Pull s' step' =
  -- --     Pull [||Pair $$s $$s'||] \ss' ->
  -- --       caseG ss' \(Pair s s') -> do
  -- --         (s, f)  <- step s
  -- --         (s', a) <- step' s'
  -- --         pure ([|| Pair $$s $$s' ||], f a)
  
  -- -- range :: Up Int -> Up Int -> Pull (Up Int)
  -- -- range x y = Pull [|| Pair $$x $$y ||] \xy ->
  -- --   caseG xy \(Pair x y) ->
  -- --   caseG (x Up.>= y) \case
  -- --     True -> empty
  -- --     _    -> pure ([|| Pair ($$x + 1) $$y ||], x)
  
  -- -- instance ToPush (Pull a) a where
  -- --   push (Pull s step) = Push \c n ->
  -- --     [|| let go s = seq s $$(unGen (runMaybeT (step [||s||])) \case
  -- --                            Nothing     -> n
  -- --                            Just (s, a) -> c a [||go $$s||]) in
  -- --         go $$s ||]
  
  -- -- tee :: Functor f => f a -> f (a, a)
  -- -- tee = fmap (\a -> (a, a))
  
  -- -- --------------------------------------------------------------------------------
  