-- | Combinators for processing/constructing trees recursively

{-# LANGUAGE FlexibleContexts #-}

module Hyper.Recurse
    ( module Hyper.Class.Recursive
    , fold, unfold
    , wrap, wrapM, unwrap, unwrapM
    , foldMapRecursive
    , HRecWitness(..)
    , (#>>), (#**#), (##>>)
    ) where

import Hyper.Class.Foldable
import Hyper.Class.Functor (HFunctor(..))
import Hyper.Class.Nodes (HWitness, (#>), (#*#))
import Hyper.Class.Recursive
import Hyper.Class.Traversable
import Hyper.Type
import Hyper.Type.Pure (Pure(..), _Pure)

import Hyper.Internal.Prelude

-- | @HRecWitness h n@ is a witness that @n@ is a recursive node of @h@
data HRecWitness h n where
    HRecSelf :: HRecWitness h h
    HRecSub :: HWitness h c -> HRecWitness c n -> HRecWitness h n

-- | Monadically convert a 'Pure' to a different 'HyperType' from the bottom up
{-# INLINE wrapM #-}
wrapM ::
    forall m h w.
    (Monad m, RTraversable h) =>
    (forall n. HRecWitness h n -> n # w -> m (w # n)) ->
    Pure # h ->
    m (w # h)
wrapM :: (forall (n :: HyperType). HRecWitness h n -> (n # w) -> m (w # n))
-> (Pure # h) -> m (w # h)
wrapM forall (n :: HyperType). HRecWitness h n -> (n # w) -> m (w # n)
f Pure # h
x =
    Dict (HNodesConstraint h RTraversable)
-> (HNodesConstraint h RTraversable => m (w # h)) -> m (w # h)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (RTraversable h) -> Dict (HNodesConstraint h RTraversable)
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (RTraversable h)
forall k (t :: k). Proxy t
Proxy @(RTraversable h))) ((HNodesConstraint h RTraversable => m (w # h)) -> m (w # h))
-> (HNodesConstraint h RTraversable => m (w # h)) -> m (w # h)
forall a b. (a -> b) -> a -> b
$
    Pure # h
x (Pure # h) -> Getting (h # Pure) (Pure # h) (h # Pure) -> h # Pure
forall s a. s -> Getting a s a -> a
^. Getting (h # Pure) (Pure # h) (h # Pure)
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure
    (h # Pure) -> ((h # Pure) -> m (h # w)) -> m (h # w)
forall a b. a -> (a -> b) -> b
& (forall (n :: HyperType). HWitness h n -> (Pure # n) -> m (w # n))
-> (h # Pure) -> m (h # w)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy RTraversable
forall k (t :: k). Proxy t
Proxy @RTraversable Proxy RTraversable
-> (RTraversable n => HWitness h n -> (Pure # n) -> m (w # n))
-> HWitness h n
-> (Pure # n)
-> m (w # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*# \HWitness h n
w -> (forall (n :: HyperType). HRecWitness n n -> (n # w) -> m (w # n))
-> (Pure # n) -> m (w # n)
forall (m :: * -> *) (h :: HyperType) (w :: HyperType).
(Monad m, RTraversable h) =>
(forall (n :: HyperType). HRecWitness h n -> (n # w) -> m (w # n))
-> (Pure # h) -> m (w # h)
wrapM (HRecWitness h n -> (n # w) -> m (w # n)
forall (n :: HyperType). HRecWitness h n -> (n # w) -> m (w # n)
f (HRecWitness h n -> (n # w) -> m (w # n))
-> (HRecWitness n n -> HRecWitness h n)
-> HRecWitness n n
-> (n # w)
-> m (w # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HWitness h n -> HRecWitness n n -> HRecWitness h n
forall (h :: HyperType) (c :: HyperType) (n :: HyperType).
HWitness h c -> HRecWitness c n -> HRecWitness h n
HRecSub HWitness h n
w))
    m (h # w) -> ((h # w) -> m (w # h)) -> m (w # h)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= HRecWitness h h -> (h # w) -> m (w # h)
forall (n :: HyperType). HRecWitness h n -> (n # w) -> m (w # n)
f HRecWitness h h
forall (h :: HyperType). HRecWitness h h
HRecSelf

-- | Monadically unwrap a tree from the top down, replacing its 'HyperType' with 'Pure'
{-# INLINE unwrapM #-}
unwrapM ::
    forall m h w.
    (Monad m, RTraversable h) =>
    (forall n. HRecWitness h n -> w # n -> m (n # w)) ->
    w # h ->
    m (Pure # h)
unwrapM :: (forall (n :: HyperType). HRecWitness h n -> (w # n) -> m (n # w))
-> (w # h) -> m (Pure # h)
unwrapM forall (n :: HyperType). HRecWitness h n -> (w # n) -> m (n # w)
f w # h
x =
    Dict (HNodesConstraint h RTraversable)
-> (HNodesConstraint h RTraversable => m (Pure # h))
-> m (Pure # h)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (RTraversable h) -> Dict (HNodesConstraint h RTraversable)
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (RTraversable h)
forall k (t :: k). Proxy t
Proxy @(RTraversable h))) ((HNodesConstraint h RTraversable => m (Pure # h)) -> m (Pure # h))
-> (HNodesConstraint h RTraversable => m (Pure # h))
-> m (Pure # h)
forall a b. (a -> b) -> a -> b
$
    HRecWitness h h -> (w # h) -> m (h # w)
forall (n :: HyperType). HRecWitness h n -> (w # n) -> m (n # w)
f HRecWitness h h
forall (h :: HyperType). HRecWitness h h
HRecSelf w # h
x
    m (h # w) -> ((h # w) -> m (h # Pure)) -> m (h # Pure)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (n :: HyperType). HWitness h n -> (w # n) -> m (Pure # n))
-> (h # w) -> m (h # Pure)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy RTraversable
forall k (t :: k). Proxy t
Proxy @RTraversable Proxy RTraversable
-> (RTraversable n => HWitness h n -> (w # n) -> m (Pure # n))
-> HWitness h n
-> (w # n)
-> m (Pure # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*# \HWitness h n
w -> (forall (n :: HyperType). HRecWitness n n -> (w # n) -> m (n # w))
-> (w # n) -> m (Pure # n)
forall (m :: * -> *) (h :: HyperType) (w :: HyperType).
(Monad m, RTraversable h) =>
(forall (n :: HyperType). HRecWitness h n -> (w # n) -> m (n # w))
-> (w # h) -> m (Pure # h)
unwrapM (HRecWitness h n -> (w # n) -> m (n # w)
forall (n :: HyperType). HRecWitness h n -> (w # n) -> m (n # w)
f (HRecWitness h n -> (w # n) -> m (n # w))
-> (HRecWitness n n -> HRecWitness h n)
-> HRecWitness n n
-> (w # n)
-> m (n # w)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HWitness h n -> HRecWitness n n -> HRecWitness h n
forall (h :: HyperType) (c :: HyperType) (n :: HyperType).
HWitness h c -> HRecWitness c n -> HRecWitness h n
HRecSub HWitness h n
w))
    m (h # Pure) -> ((h # Pure) -> Pure # h) -> m (Pure # h)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Tagged (h # Pure) (Identity (h # Pure))
-> Tagged (Pure # h) (Identity (Pure # h))
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure (Tagged (h # Pure) (Identity (h # Pure))
 -> Tagged (Pure # h) (Identity (Pure # h)))
-> (h # Pure) -> Pure # h
forall t b. AReview t b -> b -> t
#)

-- | Wrap a 'Pure' to a different 'HyperType' from the bottom up
{-# INLINE wrap #-}
wrap ::
    forall h w.
    Recursively HFunctor h =>
    (forall n. HRecWitness h n -> n # w -> w # n) ->
    Pure # h ->
    w # h
wrap :: (forall (n :: HyperType). HRecWitness h n -> (n # w) -> w # n)
-> (Pure # h) -> w # h
wrap forall (n :: HyperType). HRecWitness h n -> (n # w) -> w # n
f Pure # h
x =
    Dict (HFunctor h, HNodesConstraint h (Recursively HFunctor))
-> ((HFunctor h, HNodesConstraint h (Recursively HFunctor)) =>
    w # h)
-> w # h
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFunctor h)
-> Dict (HFunctor h, HNodesConstraint h (Recursively HFunctor))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFunctor h)
forall k (t :: k). Proxy t
Proxy @(HFunctor h))) (((HFunctor h, HNodesConstraint h (Recursively HFunctor)) => w # h)
 -> w # h)
-> ((HFunctor h, HNodesConstraint h (Recursively HFunctor)) =>
    w # h)
-> w # h
forall a b. (a -> b) -> a -> b
$
    Pure # h
x (Pure # h) -> Getting (h # Pure) (Pure # h) (h # Pure) -> h # Pure
forall s a. s -> Getting a s a -> a
^. Getting (h # Pure) (Pure # h) (h # Pure)
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure
    (h # Pure) -> ((h # Pure) -> h # w) -> h # w
forall a b. a -> (a -> b) -> b
& (forall (n :: HyperType). HWitness h n -> (Pure # n) -> w # n)
-> (h # Pure) -> h # w
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (Proxy (Recursively HFunctor)
forall k (t :: k). Proxy t
Proxy @(Recursively HFunctor) Proxy (Recursively HFunctor)
-> (Recursively HFunctor n => HWitness h n -> (Pure # n) -> w # n)
-> HWitness h n
-> (Pure # n)
-> w # n
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*# \HWitness h n
w -> (forall (n :: HyperType). HRecWitness n n -> (n # w) -> w # n)
-> (Pure # n) -> w # n
forall (h :: HyperType) (w :: HyperType).
Recursively HFunctor h =>
(forall (n :: HyperType). HRecWitness h n -> (n # w) -> w # n)
-> (Pure # h) -> w # h
wrap (HRecWitness h n -> (n # w) -> w # n
forall (n :: HyperType). HRecWitness h n -> (n # w) -> w # n
f (HRecWitness h n -> (n # w) -> w # n)
-> (HRecWitness n n -> HRecWitness h n)
-> HRecWitness n n
-> (n # w)
-> w # n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HWitness h n -> HRecWitness n n -> HRecWitness h n
forall (h :: HyperType) (c :: HyperType) (n :: HyperType).
HWitness h c -> HRecWitness c n -> HRecWitness h n
HRecSub HWitness h n
w))
    (h # w) -> ((h # w) -> w # h) -> w # h
forall a b. a -> (a -> b) -> b
& HRecWitness h h -> (h # w) -> w # h
forall (n :: HyperType). HRecWitness h n -> (n # w) -> w # n
f HRecWitness h h
forall (h :: HyperType). HRecWitness h h
HRecSelf

-- | Unwrap a tree from the top down, replacing its 'HyperType' with 'Pure'
{-# INLINE unwrap #-}
unwrap ::
    forall h w.
    Recursively HFunctor h =>
    (forall n. HRecWitness h n -> w # n -> n # w) ->
    w # h ->
    Pure # h
unwrap :: (forall (n :: HyperType). HRecWitness h n -> (w # n) -> n # w)
-> (w # h) -> Pure # h
unwrap forall (n :: HyperType). HRecWitness h n -> (w # n) -> n # w
f w # h
x =
    Dict (HFunctor h, HNodesConstraint h (Recursively HFunctor))
-> ((HFunctor h, HNodesConstraint h (Recursively HFunctor)) =>
    Pure # h)
-> Pure # h
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFunctor h)
-> Dict (HFunctor h, HNodesConstraint h (Recursively HFunctor))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFunctor h)
forall k (t :: k). Proxy t
Proxy @(HFunctor h))) (((HFunctor h, HNodesConstraint h (Recursively HFunctor)) =>
  Pure # h)
 -> Pure # h)
-> ((HFunctor h, HNodesConstraint h (Recursively HFunctor)) =>
    Pure # h)
-> Pure # h
forall a b. (a -> b) -> a -> b
$
    Tagged (h # Pure) (Identity (h # Pure))
-> Tagged (Pure # h) (Identity (Pure # h))
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure (Tagged (h # Pure) (Identity (h # Pure))
 -> Tagged (Pure # h) (Identity (Pure # h)))
-> (h # Pure) -> Pure # h
forall t b. AReview t b -> b -> t
#
    (forall (n :: HyperType). HWitness h n -> (w # n) -> Pure # n)
-> (h # w) -> h # Pure
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (Proxy (Recursively HFunctor)
forall k (t :: k). Proxy t
Proxy @(Recursively HFunctor) Proxy (Recursively HFunctor)
-> (Recursively HFunctor n => HWitness h n -> (w # n) -> Pure # n)
-> HWitness h n
-> (w # n)
-> Pure # n
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*# \HWitness h n
w -> (forall (n :: HyperType). HRecWitness n n -> (w # n) -> n # w)
-> (w # n) -> Pure # n
forall (h :: HyperType) (w :: HyperType).
Recursively HFunctor h =>
(forall (n :: HyperType). HRecWitness h n -> (w # n) -> n # w)
-> (w # h) -> Pure # h
unwrap (HRecWitness h n -> (w # n) -> n # w
forall (n :: HyperType). HRecWitness h n -> (w # n) -> n # w
f (HRecWitness h n -> (w # n) -> n # w)
-> (HRecWitness n n -> HRecWitness h n)
-> HRecWitness n n
-> (w # n)
-> n # w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HWitness h n -> HRecWitness n n -> HRecWitness h n
forall (h :: HyperType) (c :: HyperType) (n :: HyperType).
HWitness h c -> HRecWitness c n -> HRecWitness h n
HRecSub HWitness h n
w))
    (HRecWitness h h -> (w # h) -> h # w
forall (n :: HyperType). HRecWitness h n -> (w # n) -> n # w
f HRecWitness h h
forall (h :: HyperType). HRecWitness h h
HRecSelf w # h
x)

-- | Recursively fold up a tree to produce a result (aka catamorphism)
{-# INLINE fold #-}
fold ::
    Recursively HFunctor h =>
    (forall n. HRecWitness h n -> n # Const a -> a) ->
    Pure # h ->
    a
fold :: (forall (n :: HyperType). HRecWitness h n -> (n # Const a) -> a)
-> (Pure # h) -> a
fold forall (n :: HyperType). HRecWitness h n -> (n # Const a) -> a
f = Const a ('AHyperType h) -> a
forall a k (b :: k). Const a b -> a
getConst (Const a ('AHyperType h) -> a)
-> ((Pure # h) -> Const a ('AHyperType h)) -> (Pure # h) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (n :: HyperType).
 HRecWitness h n -> (n # Const a) -> Const a # n)
-> (Pure # h) -> Const a ('AHyperType h)
forall (h :: HyperType) (w :: HyperType).
Recursively HFunctor h =>
(forall (n :: HyperType). HRecWitness h n -> (n # w) -> w # n)
-> (Pure # h) -> w # h
wrap ((a -> Const a ('AHyperType n))
-> ((n # Const a) -> a) -> (n # Const a) -> Const a ('AHyperType n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Const a ('AHyperType n)
forall k a (b :: k). a -> Const a b
Const (((n # Const a) -> a) -> (n # Const a) -> Const a ('AHyperType n))
-> (HRecWitness h n -> (n # Const a) -> a)
-> HRecWitness h n
-> (n # Const a)
-> Const a ('AHyperType n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HRecWitness h n -> (n # Const a) -> a
forall (n :: HyperType). HRecWitness h n -> (n # Const a) -> a
f)

-- | Build/load a tree from a seed value (aka anamorphism)
{-# INLINE unfold #-}
unfold ::
    Recursively HFunctor h =>
    (forall n. HRecWitness h n -> a -> n # Const a) ->
    a ->
    Pure # h
unfold :: (forall (n :: HyperType). HRecWitness h n -> a -> n # Const a)
-> a -> Pure # h
unfold forall (n :: HyperType). HRecWitness h n -> a -> n # Const a
f = (forall (n :: HyperType).
 HRecWitness h n -> (Const a # n) -> n # Const a)
-> (Const a # h) -> Pure # h
forall (h :: HyperType) (w :: HyperType).
Recursively HFunctor h =>
(forall (n :: HyperType). HRecWitness h n -> (w # n) -> n # w)
-> (w # h) -> Pure # h
unwrap (((a -> n # Const a) -> Const a ('AHyperType n) -> n # Const a)
-> (HRecWitness h n -> a -> n # Const a)
-> HRecWitness h n
-> Const a ('AHyperType n)
-> n # Const a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> n # Const a)
-> (Const a ('AHyperType n) -> a)
-> Const a ('AHyperType n)
-> n # Const a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const a ('AHyperType n) -> a
forall a k (b :: k). Const a b -> a
getConst) HRecWitness h n -> a -> n # Const a
forall (n :: HyperType). HRecWitness h n -> a -> n # Const a
f) ((Const a # h) -> Pure # h) -> (a -> Const a # h) -> a -> Pure # h
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Const a # h
forall k a (b :: k). a -> Const a b
Const

-- | Fold over all of the recursive child nodes of a tree in pre-order
{-# INLINE foldMapRecursive #-}
foldMapRecursive ::
    forall h p a.
    (Recursively HFoldable h, Recursively HFoldable p, Monoid a) =>
    (forall n q. HRecWitness h n -> n # q -> a) ->
    h # p ->
    a
foldMapRecursive :: (forall (n :: HyperType) (q :: HyperType).
 HRecWitness h n -> (n # q) -> a)
-> (h # p) -> a
foldMapRecursive forall (n :: HyperType) (q :: HyperType).
HRecWitness h n -> (n # q) -> a
f h # p
x =
    Dict (HFoldable h, HNodesConstraint h (Recursively HFoldable))
-> ((HFoldable h, HNodesConstraint h (Recursively HFoldable)) => a)
-> a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFoldable h)
-> Dict (HFoldable h, HNodesConstraint h (Recursively HFoldable))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFoldable h)
forall k (t :: k). Proxy t
Proxy @(HFoldable h))) (((HFoldable h, HNodesConstraint h (Recursively HFoldable)) => a)
 -> a)
-> ((HFoldable h, HNodesConstraint h (Recursively HFoldable)) => a)
-> a
forall a b. (a -> b) -> a -> b
$
    Dict (HFoldable p, HNodesConstraint p (Recursively HFoldable))
-> ((HFoldable p, HNodesConstraint p (Recursively HFoldable)) => a)
-> a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFoldable p)
-> Dict (HFoldable p, HNodesConstraint p (Recursively HFoldable))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFoldable p)
forall k (t :: k). Proxy t
Proxy @(HFoldable p))) (((HFoldable p, HNodesConstraint p (Recursively HFoldable)) => a)
 -> a)
-> ((HFoldable p, HNodesConstraint p (Recursively HFoldable)) => a)
-> a
forall a b. (a -> b) -> a -> b
$
    HRecWitness h h -> (h # p) -> a
forall (n :: HyperType) (q :: HyperType).
HRecWitness h n -> (n # q) -> a
f HRecWitness h h
forall (h :: HyperType). HRecWitness h h
HRecSelf h # p
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<>
    (forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap
    ( Proxy (Recursively HFoldable)
forall k (t :: k). Proxy t
Proxy @(Recursively HFoldable) Proxy (Recursively HFoldable)
-> (Recursively HFoldable n => HWitness h n -> (p # n) -> a)
-> HWitness h n
-> (p # n)
-> a
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*#
        \HWitness h n
w -> (forall (n :: HyperType). HWitness p n -> (n # n) -> a)
-> (p # n) -> a
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (Proxy (Recursively HFoldable)
forall k (t :: k). Proxy t
Proxy @(Recursively HFoldable) Proxy (Recursively HFoldable)
-> (Recursively HFoldable n => (n # n) -> a)
-> HWitness p n
-> (n # n)
-> a
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (forall (n :: HyperType) (q :: HyperType).
 HRecWitness n n -> (n # q) -> a)
-> (n # n) -> a
forall (h :: HyperType) (p :: HyperType) a.
(Recursively HFoldable h, Recursively HFoldable p, Monoid a) =>
(forall (n :: HyperType) (q :: HyperType).
 HRecWitness h n -> (n # q) -> a)
-> (h # p) -> a
foldMapRecursive (HRecWitness h n -> (n # q) -> a
forall (n :: HyperType) (q :: HyperType).
HRecWitness h n -> (n # q) -> a
f (HRecWitness h n -> (n # q) -> a)
-> (HRecWitness n n -> HRecWitness h n)
-> HRecWitness n n
-> (n # q)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HWitness h n -> HRecWitness n n -> HRecWitness h n
forall (h :: HyperType) (c :: HyperType) (n :: HyperType).
HWitness h c -> HRecWitness c n -> HRecWitness h n
HRecSub HWitness h n
w))
    ) h # p
x

infixr 0 #>>
infixr 0 ##>>
infixr 0 #**#

-- | @Proxy @c #> r@ replaces a recursive witness parameter of @r@ with a constraint on the witnessed node
{-# INLINE (#>>) #-}
(#>>) ::
    forall c h n r.
    (Recursive c, c h, RNodes h) =>
    Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> :: Proxy c -> (c n => r) -> HRecWitness h n -> r
(#>>) Proxy c
_ c n => r
r HRecWitness h n
HRecSelf = r
c n => r
r
(#>>) Proxy c
p c n => r
r (HRecSub HWitness h c
w0 HRecWitness c n
w1) =
    Dict (HNodesConstraint h RNodes)
-> (HNodesConstraint h RNodes => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (RNodes h) -> Dict (HNodesConstraint h RNodes)
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (RNodes h)
forall k (t :: k). Proxy t
Proxy @(RNodes h))) ((HNodesConstraint h RNodes => r) -> r)
-> (HNodesConstraint h RNodes => r) -> r
forall a b. (a -> b) -> a -> b
$
    Dict (HNodesConstraint h c) -> (HNodesConstraint h c => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (c h) -> Dict (HNodesConstraint h c)
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (c h)
forall k (t :: k). Proxy t
Proxy @(c h))) ((HNodesConstraint h c => r) -> r)
-> (HNodesConstraint h c => r) -> r
forall a b. (a -> b) -> a -> b
$
    (Proxy RNodes
forall k (t :: k). Proxy t
Proxy @RNodes Proxy RNodes
-> (RNodes c => HWitness h c -> r) -> HWitness h c -> r
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*# Proxy c
p Proxy c -> (c c => r) -> HWitness h c -> r
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (Proxy c
p Proxy c -> (c n => r) -> HRecWitness c n -> r
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (n :: HyperType) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> c n => r
r) HRecWitness c n
w1) HWitness h c
w0

-- | @Proxy @c #> r@ replaces a recursive witness parameter of @r@ with a @Recursively c@ constraint on the witnessed node
{-# INLINE (##>>) #-}
(##>>) ::
    forall c h n r.
    Recursively c h =>
    Proxy c -> (c n => r) -> HRecWitness h n -> r
##>> :: Proxy c -> (c n => r) -> HRecWitness h n -> r
(##>>) Proxy c
p c n => r
r =
    Dict (c h, HNodesConstraint h (Recursively c))
-> ((c h, HNodesConstraint h (Recursively c)) =>
    HRecWitness h n -> r)
-> HRecWitness h n
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (c h)
forall k (t :: k). Proxy t
Proxy @(c h))) (((c h, HNodesConstraint h (Recursively c)) =>
  HRecWitness h n -> r)
 -> HRecWitness h n -> r)
-> ((c h, HNodesConstraint h (Recursively c)) =>
    HRecWitness h n -> r)
-> HRecWitness h n
-> r
forall a b. (a -> b) -> a -> b
$
    \case
    HRecWitness h n
HRecSelf -> r
c n => r
r
    HRecSub HWitness h c
w0 HRecWitness c n
w1 -> (Proxy (Recursively c)
forall k (t :: k). Proxy t
Proxy @(Recursively c) Proxy (Recursively c)
-> (Recursively c c => r) -> HWitness h c -> r
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (Proxy c
p Proxy c -> (c n => r) -> HRecWitness c n -> r
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (n :: HyperType) r.
Recursively c h =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
##>> c n => r
r) HRecWitness c n
w1) HWitness h c
w0

-- | A variant of '#>>' which does not consume the witness parameter.
--
-- @Proxy @c0 #**# Proxy @c1 #>> r@ brings into context both the @c0 n@ and @c1 n@ constraints.
{-# INLINE (#**#) #-}
(#**#) ::
    (Recursive c, c h, RNodes h) =>
    Proxy c -> (c n => HRecWitness h n -> r) -> HRecWitness h n -> r
#**# :: Proxy c -> (c n => HRecWitness h n -> r) -> HRecWitness h n -> r
(#**#) Proxy c
p c n => HRecWitness h n -> r
r HRecWitness h n
w = (Proxy c
p Proxy c
-> (c n => HRecWitness h n -> r)
-> HRecWitness h n
-> HRecWitness h n
-> r
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (n :: HyperType) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> c n => HRecWitness h n -> r
r) HRecWitness h n
w HRecWitness h n
w