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

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           Hyper.Internal.Prelude

data Prune h =
    Pruned | Unpruned (h :# Prune)
    deriving (forall x. Prune h -> Rep (Prune h) x)
-> (forall x. Rep (Prune h) x -> Prune h) -> Generic (Prune h)
forall x. Rep (Prune h) x -> Prune h
forall x. Prune h -> Rep (Prune h) x
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

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 (n :: HyperType). HWitness Prune n -> p # n) -> Prune # p
hpure forall (n :: HyperType). HWitness Prune n -> p # n
f = ('AHyperType p :# Prune) -> Prune # p
forall (h :: AHyperType). (h :# Prune) -> Prune h
Unpruned (HWitness Prune Prune -> p # Prune
forall (n :: HyperType). HWitness Prune n -> p # n
f (HWitnessType Prune Prune -> HWitness Prune Prune
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType Prune Prune
W_Prune Prune
W_Prune_Prune))

instance HApply Prune where
    hzip :: (Prune # p) -> (Prune # q) -> Prune # (p :*: q)
hzip Prune # p
Pruned Prune # q
_ = Prune # (p :*: q)
forall (h :: AHyperType). Prune h
Pruned
    hzip Prune # p
_ Prune # q
Pruned = Prune # (p :*: q)
forall (h :: AHyperType). Prune h
Pruned
    hzip (Unpruned 'AHyperType p :# Prune
x) (Unpruned 'AHyperType q :# Prune
y) = p ('AHyperType Prune)
'AHyperType p :# Prune
x p ('AHyperType Prune)
-> q ('AHyperType Prune) -> (:*:) p q ('AHyperType Prune)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: q ('AHyperType Prune)
'AHyperType q :# Prune
y (:*:) p q ('AHyperType Prune)
-> ((:*:) p q ('AHyperType Prune) -> Prune # (p :*: q))
-> Prune # (p :*: q)
forall a b. a -> (a -> b) -> b
& (:*:) p q ('AHyperType Prune) -> Prune # (p :*: q)
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 :: (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) =
        Dict
  (HNodesConstraint t (Infer m),
   HNodesConstraint (InferOf t) (UnifyGen m))
-> ((HNodesConstraint t (Infer m),
     HNodesConstraint (InferOf t) (UnifyGen m)) =>
    m (HCompose Prune t # h, InferOf t # UVarOf m))
-> m (HCompose Prune t # h, InferOf t # UVarOf m)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy m
-> Proxy t
-> Dict
     (HNodesConstraint t (Infer m),
      HNodesConstraint (InferOf t) (UnifyGen m))
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 (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) (((HNodesConstraint t (Infer m),
   HNodesConstraint (InferOf t) (UnifyGen m)) =>
  m (HCompose Prune t # h, InferOf t # UVarOf m))
 -> m (HCompose Prune t # h, InferOf t # UVarOf m))
-> ((HNodesConstraint t (Infer m),
     HNodesConstraint (InferOf t) (UnifyGen m)) =>
    m (HCompose Prune t # h, InferOf t # UVarOf m))
-> m (HCompose Prune t # h, InferOf t # UVarOf m)
forall a b. (a -> b) -> a -> b
$
        (forall (n :: HyperType).
 HWitness (InferOf t) n -> ContainedH m (UVarOf m) # n)
-> InferOf t # ContainedH m (UVarOf m)
forall (h :: HyperType) (p :: HyperType).
HPointed h =>
(forall (n :: HyperType). HWitness h n -> p # n) -> h # p
hpure (Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m n => ContainedH m (UVarOf m) # n)
-> HWitness (InferOf t) n
-> ContainedH m (UVarOf m) # n
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> m (UVarOf m ('AHyperType n)) -> ContainedH m (UVarOf m) # n
forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
f (p h) -> ContainedH f p h
MkContainedH m (UVarOf m ('AHyperType n))
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
m (UVarOf m # t)
newUnbound)
        (InferOf t # ContainedH m (UVarOf m))
-> ((InferOf t # ContainedH m (UVarOf m))
    -> m (InferOf t # UVarOf m))
-> m (InferOf t # UVarOf m)
forall a b. a -> (a -> b) -> b
& (InferOf t # ContainedH m (UVarOf m)) -> m (InferOf t # UVarOf m)
forall (h :: HyperType) (f :: * -> *) (p :: HyperType).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence
        m (InferOf t # UVarOf m)
-> ((InferOf t # UVarOf m)
    -> (HCompose Prune t # h, InferOf t # UVarOf m))
-> m (HCompose Prune t # h, InferOf t # UVarOf m)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Tagged (Prune # HCompose t h) (Identity (Prune # HCompose t h))
-> Tagged (HCompose Prune t # h) (Identity (HCompose Prune t # h))
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 (Tagged (Prune # HCompose t h) (Identity (Prune # HCompose t h))
 -> Tagged (HCompose Prune t # h) (Identity (HCompose Prune t # h)))
-> (Prune # HCompose t h) -> HCompose Prune t # h
forall t b. AReview t b -> b -> t
# Prune # HCompose t h
forall (h :: AHyperType). Prune h
Pruned, )
    inferBody (HCompose (Unpruned (HCompose x))) =
        (forall (n :: HyperType).
 HWitness t n
 -> (HCompose (InferChild m h) Prune # n)
 -> InferChild m (HCompose h Prune) # n)
-> (t # HCompose (InferChild m h) Prune)
-> t # InferChild m (HCompose h Prune)
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 i)) ->
            m (InferredChild (UVarOf m) h ('AHyperType (HCompose Prune n)))
i m (InferredChild (UVarOf m) h ('AHyperType (HCompose Prune n)))
-> (InferredChild (UVarOf m) h ('AHyperType (HCompose Prune n))
    -> InferredChild (UVarOf m) (HCompose h Prune) ('AHyperType n))
-> m (InferredChild (UVarOf m) (HCompose h Prune) ('AHyperType n))
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) -> HCompose h Prune ('AHyperType n)
-> (InferOf (GetHyperType ('AHyperType n)) # UVarOf m)
-> InferredChild (UVarOf m) (HCompose h Prune) ('AHyperType n)
forall (v :: HyperType) (h :: HyperType) (t :: AHyperType).
h t -> (InferOf (GetHyperType t) # v) -> InferredChild v h t
InferredChild (Tagged
  (h ('AHyperType (HCompose Prune n)))
  (Identity (h ('AHyperType (HCompose Prune n))))
-> Tagged
     (HCompose h Prune ('AHyperType n))
     (Identity (HCompose h Prune ('AHyperType n)))
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 (Tagged
   (h ('AHyperType (HCompose Prune n)))
   (Identity (h ('AHyperType (HCompose Prune n))))
 -> Tagged
      (HCompose h Prune ('AHyperType n))
      (Identity (HCompose h Prune ('AHyperType n))))
-> h ('AHyperType (HCompose Prune n))
-> HCompose h Prune ('AHyperType n)
forall t b. AReview t b -> b -> t
# h ('AHyperType (HCompose Prune n))
r) InferOf (GetHyperType ('AHyperType n)) # UVarOf m
InferOf (GetHyperType ('AHyperType (HCompose Prune n))) # UVarOf m
t)
            m (InferredChild (UVarOf m) (HCompose h Prune) ('AHyperType n))
-> (m (InferredChild (UVarOf m) (HCompose h Prune) ('AHyperType n))
    -> InferChild m (HCompose h Prune) # n)
-> InferChild m (HCompose h Prune) # n
forall a b. a -> (a -> b) -> b
& m (InferredChild (UVarOf m) (HCompose h Prune) ('AHyperType n))
-> InferChild m (HCompose h Prune) # n
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))
t # HCompose (InferChild m h) Prune
x
        (t # InferChild m (HCompose h Prune))
-> ((t # InferChild m (HCompose h Prune))
    -> m (t # HCompose h Prune, InferOf t # UVarOf m))
-> m (t # HCompose h Prune, InferOf t # UVarOf m)
forall a b. a -> (a -> b) -> b
& (t # InferChild m (HCompose h Prune))
-> m (t # HCompose h Prune, InferOf t # UVarOf m)
forall (m :: * -> *) (t :: HyperType) (h :: HyperType).
Infer m t =>
(t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)
inferBody
        m (t # HCompose h Prune, InferOf t # UVarOf m)
-> ((t # HCompose h Prune, InferOf t # UVarOf m)
    -> (HCompose Prune t # h, InferOf t # UVarOf m))
-> m (HCompose Prune t # h, InferOf t # UVarOf m)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ((t # HCompose h Prune) -> Identity (HCompose Prune t # h))
-> (t # HCompose h Prune, InferOf t # UVarOf m)
-> Identity (HCompose Prune t # h, InferOf t # UVarOf m)
forall s t a b. Field1 s t a b => Lens s t a b
Lens._1 (((t # HCompose h Prune) -> Identity (HCompose Prune t # h))
 -> (t # HCompose h Prune, InferOf t # UVarOf m)
 -> Identity (HCompose Prune t # h, InferOf t # UVarOf m))
-> ((t # HCompose h Prune) -> HCompose Prune t # h)
-> (t # HCompose h Prune, InferOf t # UVarOf m)
-> (HCompose Prune t # h, InferOf t # UVarOf m)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Optic
  Tagged
  Identity
  (Prune # HCompose t h)
  (Prune # HCompose t h)
  (HCompose t h # Prune)
  (HCompose t h # Prune)
-> Optic
     Tagged
     Identity
     (HCompose Prune t # h)
     (HCompose Prune t # h)
     (t # HCompose h Prune)
     (t # HCompose h Prune)
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 Optic
  Tagged
  Identity
  (Prune # HCompose t h)
  (Prune # HCompose t h)
  (HCompose t h # Prune)
  (HCompose t h # Prune)
forall (h :: AHyperType) (h :: AHyperType).
Prism (Prune h) (Prune h) (h :# Prune) (h :# Prune)
_Unpruned Optic
  Tagged
  Identity
  (HCompose Prune t # h)
  (HCompose Prune t # h)
  (t # HCompose h Prune)
  (t # HCompose h Prune)
-> (t # HCompose h Prune) -> HCompose Prune t # h
forall t b. AReview t b -> b -> t
#)
    inferContext :: 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)
_ = Dict
  (HNodesConstraint t (Infer m),
   HNodesConstraint (InferOf t) (UnifyGen m))
-> ((HNodesConstraint t (Infer m),
     HNodesConstraint (InferOf t) (UnifyGen m)) =>
    Dict
      (HComposeConstraint0 (Infer m) t Prune,
       HNodesConstraint (InferOf t) (UnifyGen m)))
-> Dict
     (HComposeConstraint0 (Infer m) t Prune,
      HNodesConstraint (InferOf t) (UnifyGen m))
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (proxy0 m
-> Proxy t
-> Dict
     (HNodesConstraint t (Infer m),
      HNodesConstraint (InferOf t) (UnifyGen m))
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 (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) (HNodesConstraint t (Infer m),
 HNodesConstraint (InferOf t) (UnifyGen m)) =>
Dict
  (HComposeConstraint0 (Infer m) t Prune,
   HNodesConstraint (InferOf t) (UnifyGen m))
forall (a :: Constraint). a => Dict a
Dict

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)
_ = Proxy t -> (InferOf t # UVarOf m) -> (InferOf t # UVarOf m) -> m ()
forall (m :: * -> *) (t :: HyperType).
Blame m t =>
Proxy t -> (InferOf t # UVarOf m) -> (InferOf t # UVarOf m) -> m ()
inferOfUnify (Proxy t
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)
_ = Proxy t
-> (InferOf t # UVarOf m) -> (InferOf t # UVarOf m) -> m Bool
forall (m :: * -> *) (t :: HyperType).
Blame m t =>
Proxy t
-> (InferOf t # UVarOf m) -> (InferOf t # UVarOf m) -> m Bool
inferOfMatches (Proxy t
forall k (t :: k). Proxy t
Proxy @t)