{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

module Hyper.Type.Prune
    ( Prune (..)
    , W_Prune (..)
    , _Pruned
    , _Unpruned
    ) where

import qualified Control.Lens as Lens
import Hyper
import Hyper.Class.Traversable
import Hyper.Class.Unify (UnifyGen)
import Hyper.Combinator.Compose (HComposeConstraint1)
import Hyper.Infer
import Hyper.Infer.Blame (Blame (..))
import Hyper.Unify.New (newUnbound)
import qualified Text.PrettyPrint as Pretty
import Text.PrettyPrint.HughesPJClass (Pretty (..))

import Hyper.Internal.Prelude

data Prune h
    = Pruned
    | Unpruned (h :# Prune)
    deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (h :: AHyperType) x. Rep (Prune h) x -> Prune h
forall (h :: AHyperType) x. Prune h -> Rep (Prune h) x
$cto :: forall (h :: AHyperType) x. Rep (Prune h) x -> Prune h
$cfrom :: forall (h :: AHyperType) x. Prune h -> Rep (Prune h) x
Generic)

instance Pretty (h :# Prune) => Pretty (Prune h) where
    pPrintPrec :: PrettyLevel -> Rational -> Prune h -> Doc
pPrintPrec PrettyLevel
_ Rational
_ Prune h
Pruned = String -> Doc
Pretty.text String
"<pruned>"
    pPrintPrec PrettyLevel
level Rational
prec (Unpruned h :# Prune
x) = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
level Rational
prec h :# Prune
x

makeCommonInstances [''Prune]
makePrisms ''Prune
makeHTraversableAndBases ''Prune
makeZipMatch ''Prune
makeHContext ''Prune

-- `HPointed` and `HApplicative` instances in the spirit of `Maybe`

instance HPointed Prune where
    hpure :: forall (p :: HyperType).
(forall (n :: HyperType). HWitness Prune n -> p # n) -> Prune # p
hpure forall (n :: HyperType). HWitness Prune n -> p # n
f = forall (h :: AHyperType). (h :# Prune) -> Prune h
Unpruned (forall (n :: HyperType). HWitness Prune n -> p # n
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness W_Prune Prune
W_Prune_Prune))

instance HApply Prune where
    hzip :: forall (p :: HyperType) (q :: HyperType).
(Prune # p) -> (Prune # q) -> Prune # (p :*: q)
hzip Prune ('AHyperType p)
Pruned Prune # q
_ = forall (h :: AHyperType). Prune h
Pruned
    hzip Prune ('AHyperType p)
_ Prune # q
Pruned = forall (h :: AHyperType). Prune h
Pruned
    hzip (Unpruned 'AHyperType p :# Prune
x) (Unpruned 'AHyperType q :# Prune
y) = 'AHyperType p :# Prune
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: 'AHyperType q :# Prune
y forall a b. a -> (a -> b) -> b
& forall (h :: AHyperType). (h :# Prune) -> Prune h
Unpruned

instance RNodes Prune
instance c Prune => Recursively c Prune
instance RTraversable Prune

type instance InferOf (HCompose Prune t) = InferOf t

instance
    ( Infer m t
    , HPointed (InferOf t)
    , HTraversable (InferOf t)
    , HNodesConstraint t (HComposeConstraint1 (Infer m) Prune)
    ) =>
    Infer m (HCompose Prune t)
    where
    inferBody :: forall (h :: HyperType).
(HCompose Prune t # InferChild m h)
-> m (HCompose Prune t # h, InferOf (HCompose Prune t) # UVarOf m)
inferBody (HCompose Prune
  ('AHyperType
     (HCompose t (GetHyperType ('AHyperType (InferChild m h)))))
Pruned) =
        forall (h :: HyperType) (p :: HyperType).
HPointed h =>
(forall (n :: HyperType). HWitness h n -> p # n) -> h # p
hpure (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
f (p h) -> ContainedH f p h
MkContainedH forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
m (UVarOf m # t)
newUnbound)
            forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: * -> *) (t :: HyperType) (proxy0 :: (* -> *) -> *)
       (proxy1 :: HyperType -> *).
Infer m t =>
proxy0 m
-> proxy1 t
-> Dict
     (HNodesConstraint t (Infer m),
      HNodesConstraint (InferOf t) (UnifyGen m))
inferContext (forall {k} (t :: k). Proxy t
Proxy @m) (forall {k} (t :: k). Proxy t
Proxy @t)
            forall a b. a -> (a -> b) -> b
& forall (h :: HyperType) (f :: * -> *) (p :: HyperType).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence
            forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall (a0 :: HyperType) (b0 :: HyperType) (h0 :: HyperType)
       (a1 :: HyperType) (b1 :: HyperType) (h1 :: HyperType).
Iso
  (HCompose a0 b0 # h0)
  (HCompose a1 b1 # h1)
  (a0 # HCompose b0 h0)
  (a1 # HCompose b1 h1)
_HCompose forall t b. AReview t b -> b -> t
# forall (h :: AHyperType). Prune h
Pruned,)
    inferBody (HCompose (Unpruned (HCompose t # HCompose (InferChild m h) (GetHyperType ('AHyperType Prune))
x))) =
        forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
            ( \HWitness t n
_ (HCompose (InferChild m (InferredChild (UVarOf m) h ('AHyperType (HCompose Prune n)))
i)) ->
                m (InferredChild (UVarOf m) h ('AHyperType (HCompose Prune n)))
i
                    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (\(InferredChild h ('AHyperType (HCompose Prune n))
r InferOf (GetHyperType ('AHyperType (HCompose Prune n))) # UVarOf m
t) -> forall (v :: HyperType) (h :: HyperType) (t :: AHyperType).
h t -> (InferOf (GetHyperType t) # v) -> InferredChild v h t
InferredChild (forall (a0 :: HyperType) (b0 :: HyperType) (h0 :: HyperType)
       (a1 :: HyperType) (b1 :: HyperType) (h1 :: HyperType).
Iso
  (HCompose a0 b0 # h0)
  (HCompose a1 b1 # h1)
  (a0 # HCompose b0 h0)
  (a1 # HCompose b1 h1)
_HCompose forall t b. AReview t b -> b -> t
# h ('AHyperType (HCompose Prune n))
r) InferOf (GetHyperType ('AHyperType (HCompose Prune n))) # UVarOf m
t)
                    forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
m (InferredChild (UVarOf m) h t) -> InferChild m h t
InferChild
            )
            t # HCompose (InferChild m h) (GetHyperType ('AHyperType Prune))
x
            forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) (t :: HyperType) (h :: HyperType).
Infer m t =>
(t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)
inferBody
            forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall s t a b. Field1 s t a b => Lens s t a b
Lens._1 forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (p :: * -> * -> *) (f :: * -> *) (a0 :: HyperType)
       (b0 :: HyperType) (c0 :: HyperType) (a1 :: HyperType)
       (b1 :: HyperType) (c1 :: HyperType) (a2 :: HyperType)
       (b2 :: HyperType) (c2 :: HyperType) (a3 :: HyperType)
       (b3 :: HyperType) (c3 :: HyperType).
(Profunctor p, Functor f) =>
Optic
  p
  f
  (a0 # HCompose b0 c0)
  (a1 # HCompose b1 c1)
  (HCompose a2 b2 # c2)
  (HCompose a3 b3 # c3)
-> Optic
     p
     f
     (HCompose a0 b0 # c0)
     (HCompose a1 b1 # c1)
     (a2 # HCompose b2 c2)
     (a3 # HCompose b3 c3)
hcomposed forall (h :: AHyperType) (h :: AHyperType).
Prism (Prune h) (Prune h) (h :# Prune) (h :# Prune)
_Unpruned forall t b. AReview t b -> b -> t
#)
    inferContext :: forall (proxy0 :: (* -> *) -> *) (proxy1 :: HyperType -> *).
proxy0 m
-> proxy1 (HCompose Prune t)
-> Dict
     (HNodesConstraint (HCompose Prune t) (Infer m),
      HNodesConstraint (InferOf (HCompose Prune t)) (UnifyGen m))
inferContext proxy0 m
m proxy1 (HCompose Prune t)
_ = forall (a :: Constraint). a => Dict a
Dict forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: * -> *) (t :: HyperType) (proxy0 :: (* -> *) -> *)
       (proxy1 :: HyperType -> *).
Infer m t =>
proxy0 m
-> proxy1 t
-> Dict
     (HNodesConstraint t (Infer m),
      HNodesConstraint (InferOf t) (UnifyGen m))
inferContext proxy0 m
m (forall {k} (t :: k). Proxy t
Proxy @t)

instance
    ( Blame m t
    , HNodesConstraint t (HComposeConstraint1 (Infer m) Prune)
    , HNodesConstraint t (HComposeConstraint1 (Blame m) Prune)
    , HNodesConstraint t (HComposeConstraint1 RNodes Prune)
    , HNodesConstraint t (HComposeConstraint1 (Recursively HFunctor) Prune)
    , HNodesConstraint t (HComposeConstraint1 (Recursively HFoldable) Prune)
    , HNodesConstraint t (HComposeConstraint1 RTraversable Prune)
    ) =>
    Blame m (HCompose Prune t)
    where
    inferOfUnify :: Proxy (HCompose Prune t)
-> (InferOf (HCompose Prune t) # UVarOf m)
-> (InferOf (HCompose Prune t) # UVarOf m)
-> m ()
inferOfUnify Proxy (HCompose Prune t)
_ = forall (m :: * -> *) (t :: HyperType).
Blame m t =>
Proxy t -> (InferOf t # UVarOf m) -> (InferOf t # UVarOf m) -> m ()
inferOfUnify (forall {k} (t :: k). Proxy t
Proxy @t)
    inferOfMatches :: Proxy (HCompose Prune t)
-> (InferOf (HCompose Prune t) # UVarOf m)
-> (InferOf (HCompose Prune t) # UVarOf m)
-> m Bool
inferOfMatches Proxy (HCompose Prune t)
_ = forall (m :: * -> *) (t :: HyperType).
Blame m t =>
Proxy t
-> (InferOf t # UVarOf m) -> (InferOf t # UVarOf m) -> m Bool
inferOfMatches (forall {k} (t :: k). Proxy t
Proxy @t)