{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE TypeOperators             #-}

module Language.Expression.Scope where

import           Control.Lens

import           Language.Expression

--------------------------------------------------------------------------------
--  Classes
--------------------------------------------------------------------------------

class HBound k where
  (^>>>=) :: (HMonad h) => k h t a -> (forall b. t b -> h t' b) -> k h t' a

--------------------------------------------------------------------------------
--  Bound or free variables
--------------------------------------------------------------------------------

data BV g f a where
  -- | Bound variable
  B :: g a -> BV g f a
  -- | Free variable
  F :: f a -> BV g f a

instance HFunctor (BV g) where
  hmap :: (forall (b :: u). t b -> t' b) -> BV g t a -> BV g t' a
hmap = (forall (b :: u). t b -> t' b) -> BV g t a -> BV g t' a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (t' :: k -> *)
       (a :: k).
(HPointed h, HBind h) =>
(forall (b :: k). t b -> t' b) -> h t a -> h t' a
hliftM

instance HPointed (BV g) where
  hpure :: t a -> BV g t a
hpure = t a -> BV g t a
forall k (f :: k -> *) (a :: k) (g :: k -> *). f a -> BV g f a
F

instance HBind (BV g) where
  B g a
x ^>>= :: BV g t a -> (forall (b :: k). t b -> BV g t' b) -> BV g t' a
^>>= forall (b :: k). t b -> BV g t' b
_ = g a -> BV g t' a
forall k (g :: k -> *) (a :: k) (f :: k -> *). g a -> BV g f a
B g a
x
  F t a
x ^>>= forall (b :: k). t b -> BV g t' b
f = t a -> BV g t' a
forall (b :: k). t b -> BV g t' b
f t a
x

instance HMonad (BV g)

-- instance (HFoldableAt k g) => HFoldableAt k (BV g) where
--   hfoldMap = hbifoldMap . hfoldMap

instance HTraversable (BV g) where
  htraverse :: (forall (b :: u). t b -> f (t' b)) -> BV g t a -> f (BV g t' a)
htraverse = (g a -> f (g a)) -> (t a -> f (t' a)) -> BV g t a -> f (BV g t' a)
forall k k (t :: * -> *) (g :: k -> *) (a :: k) (g' :: k -> *)
       (b :: k) (f :: k -> *) (f' :: k -> *).
Functor t =>
(g a -> t (g' b))
-> (f a -> t (f' b)) -> BV g f a -> t (BV g' f' b)
hbitraverseBV g a -> f (g a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

foldBV :: (w a -> r) -> (v a -> r) -> BV w v a -> r
foldBV :: (w a -> r) -> (v a -> r) -> BV w v a -> r
foldBV w a -> r
f v a -> r
g = \case
  B w a
x -> w a -> r
f w a
x
  F v a
y -> v a -> r
g v a
y

instance HBifunctor BV where
  hbimap :: (forall (b :: k). s b -> s' b)
-> (forall (b :: k). t b -> t' b) -> BV s t a -> BV s' t' a
hbimap = (forall (b :: k). s b -> s' b)
-> (forall (b :: k). t b -> t' b) -> BV s t a -> BV s' t' a
forall k k (g :: k -> *) (a :: k) (g' :: k -> *) (b :: k)
       (f :: k -> *) (f' :: k -> *).
(g a -> g' b) -> (f a -> f' b) -> BV g f a -> BV g' f' b
hbimapBV

instance HBitraversable BV where
  hbitraverse :: (forall (b :: k). s b -> f (s' b))
-> (forall (b :: k). t b -> f (t' b)) -> BV s t a -> f (BV s' t' a)
hbitraverse = (forall (b :: k). s b -> f (s' b))
-> (forall (b :: k). t b -> f (t' b)) -> BV s t a -> f (BV s' t' a)
forall k k (t :: * -> *) (g :: k -> *) (a :: k) (g' :: k -> *)
       (b :: k) (f :: k -> *) (f' :: k -> *).
Functor t =>
(g a -> t (g' b))
-> (f a -> t (f' b)) -> BV g f a -> t (BV g' f' b)
hbitraverseBV

hbitraverseBV :: (Functor t) => (g a -> t (g' b)) -> (f a -> t (f' b)) -> BV g f a -> t (BV g' f' b)
hbitraverseBV :: (g a -> t (g' b))
-> (f a -> t (f' b)) -> BV g f a -> t (BV g' f' b)
hbitraverseBV g a -> t (g' b)
f f a -> t (f' b)
g = (g a -> t (BV g' f' b))
-> (f a -> t (BV g' f' b)) -> BV g f a -> t (BV g' f' b)
forall k (w :: k -> *) (a :: k) r (v :: k -> *).
(w a -> r) -> (v a -> r) -> BV w v a -> r
foldBV ((g' b -> BV g' f' b) -> t (g' b) -> t (BV g' f' b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g' b -> BV g' f' b
forall k (g :: k -> *) (a :: k) (f :: k -> *). g a -> BV g f a
B (t (g' b) -> t (BV g' f' b))
-> (g a -> t (g' b)) -> g a -> t (BV g' f' b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> t (g' b)
f) ((f' b -> BV g' f' b) -> t (f' b) -> t (BV g' f' b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f' b -> BV g' f' b
forall k (f :: k -> *) (a :: k) (g :: k -> *). f a -> BV g f a
F (t (f' b) -> t (BV g' f' b))
-> (f a -> t (f' b)) -> f a -> t (BV g' f' b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> t (f' b)
g)

hbimapBV :: (g a -> g' b) -> (f a -> f' b) -> BV g f a -> BV g' f' b
hbimapBV :: (g a -> g' b) -> (f a -> f' b) -> BV g f a -> BV g' f' b
hbimapBV g a -> g' b
f f a -> f' b
g = (g a -> BV g' f' b)
-> (f a -> BV g' f' b) -> BV g f a -> BV g' f' b
forall k (w :: k -> *) (a :: k) r (v :: k -> *).
(w a -> r) -> (v a -> r) -> BV w v a -> r
foldBV (g' b -> BV g' f' b
forall k (g :: k -> *) (a :: k) (f :: k -> *). g a -> BV g f a
B (g' b -> BV g' f' b) -> (g a -> g' b) -> g a -> BV g' f' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> g' b
f) (f' b -> BV g' f' b
forall k (f :: k -> *) (a :: k) (g :: k -> *). f a -> BV g f a
F (f' b -> BV g' f' b) -> (f a -> f' b) -> f a -> BV g' f' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> f' b
g)

instance HBifoldableAt k BV where
  hbifoldMap :: (forall (b :: k). f b -> k b)
-> (forall (b :: k). g b -> k b) -> BV f g a -> k a
hbifoldMap = (forall (b :: k). f b -> k b)
-> (forall (b :: k). g b -> k b) -> BV f g a -> k a
forall k (w :: k -> *) (a :: k) r (v :: k -> *).
(w a -> r) -> (v a -> r) -> BV w v a -> r
foldBV

--------------------------------------------------------------------------------
--  Scopes
--------------------------------------------------------------------------------

newtype Scope g h f a = Scope { Scope g h f a -> h (BV g (h f)) a
unscope :: h (BV g (h f)) a }

_Scope :: Iso (Scope g h f a) (Scope g' h' f' a') (h (BV g (h f)) a) (h' (BV g' (h' f')) a')
_Scope :: p (h (BV g (h f)) a) (f (h' (BV g' (h' f')) a'))
-> p (Scope g h f a) (f (Scope g' h' f' a'))
_Scope = (Scope g h f a -> h (BV g (h f)) a)
-> (h' (BV g' (h' f')) a' -> Scope g' h' f' a')
-> Iso
     (Scope g h f a)
     (Scope g' h' f' a')
     (h (BV g (h f)) a)
     (h' (BV g' (h' f')) a')
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso Scope g h f a -> h (BV g (h f)) a
forall k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
Scope g h f a -> h (BV g (h f)) a
unscope h' (BV g' (h' f')) a' -> Scope g' h' f' a'
forall k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
h (BV g (h f)) a -> Scope g h f a
Scope

instance HFunctor h => HFunctor (Scope g h) where
  hmap :: (forall (b :: u). t b -> t' b) -> Scope g h t a -> Scope g h t' a
hmap forall (b :: u). t b -> t' b
f = AnIso
  (Scoped h t' g a) (Scoped h t g a) (Scope g h t' a) (Scope g h t a)
-> Iso
     (Scope g h t a) (Scope g h t' a) (Scoped h t g a) (Scoped h t' g a)
forall s t a b. AnIso s t a b -> Iso b a t s
from AnIso
  (Scoped h t' g a) (Scoped h t g a) (Scope g h t' a) (Scope g h t a)
forall k k (h :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (a :: k) (h' :: (k -> *) -> k -> *) (f' :: k -> *) (g' :: k -> *)
       (a' :: k).
Iso
  (Scoped h f g a)
  (Scoped h' f' g' a')
  (Scope g h f a)
  (Scope g' h' f' a')
_Scoped ((Scoped h t g a -> Identity (Scoped h t' g a))
 -> Scope g h t a -> Identity (Scope g h t' a))
-> (Scoped h t g a -> Scoped h t' g a)
-> Scope g h t a
-> Scope g h t' a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (b :: u). t b -> t' b) -> Scoped h t g a -> Scoped h t' g a
forall k (h :: (k -> *) -> (k -> *) -> k -> *) (s :: k -> *)
       (s' :: k -> *) (t :: k -> *) (a :: k).
HBifunctor h =>
(forall (b :: k). s b -> s' b) -> h s t a -> h s' t a
hfirst forall (b :: u). t b -> t' b
f

instance HPointed h => HPointed (Scope g h) where
  hpure :: t a -> Scope g h t a
hpure = h (BV g (h t)) a -> Scope g h t a
forall k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
h (BV g (h f)) a -> Scope g h f a
Scope (h (BV g (h t)) a -> Scope g h t a)
-> (t a -> h (BV g (h t)) a) -> t a -> Scope g h t a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV g (h t) a -> h (BV g (h t)) a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure (BV g (h t) a -> h (BV g (h t)) a)
-> (t a -> BV g (h t) a) -> t a -> h (BV g (h t)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h t a -> BV g (h t) a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure (h t a -> BV g (h t) a) -> (t a -> h t a) -> t a -> BV g (h t) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> h t a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure

instance HTraversable h => HTraversable (Scope g h) where
  htraverse :: (forall (b :: u). t b -> f (t' b))
-> Scope g h t a -> f (Scope g h t' a)
htraverse forall (b :: u). t b -> f (t' b)
f = (h (BV g (h t)) a -> f (h (BV g (h t')) a))
-> Scope g h t a -> f (Scope g h t' a)
forall k k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k) (g' :: k -> *) (h' :: (k -> *) -> k -> *) (f' :: k -> *)
       (a' :: k).
Iso
  (Scope g h f a)
  (Scope g' h' f' a')
  (h (BV g (h f)) a)
  (h' (BV g' (h' f')) a')
_Scope ((h (BV g (h t)) a -> f (h (BV g (h t')) a))
 -> Scope g h t a -> f (Scope g h t' a))
-> (h (BV g (h t)) a -> f (h (BV g (h t')) a))
-> Scope g h t a
-> f (Scope g h t' a)
forall k (f :: k -> *) s (t :: k) a (b :: k).
LensLike f s t a b -> LensLike f s t a b
%%~ (forall (b :: u). BV g (h t) b -> f (BV g (h t') b))
-> h (BV g (h t)) a -> f (h (BV g (h t')) a)
forall u (h :: (u -> *) -> u -> *) (f :: * -> *) (t :: u -> *)
       (t' :: u -> *) (a :: u).
(HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (t' b)) -> h t a -> f (h t' a)
htraverse ((forall (b :: u). h t b -> f (h t' b))
-> BV g (h t) b -> f (BV g (h t') b)
forall u (h :: (u -> *) -> u -> *) (f :: * -> *) (t :: u -> *)
       (t' :: u -> *) (a :: u).
(HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (t' b)) -> h t a -> f (h t' a)
htraverse ((forall (b :: u). t b -> f (t' b)) -> h t b -> f (h t' b)
forall u (h :: (u -> *) -> u -> *) (f :: * -> *) (t :: u -> *)
       (t' :: u -> *) (a :: u).
(HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (t' b)) -> h t a -> f (h t' a)
htraverse forall (b :: u). t b -> f (t' b)
f))


instance HDuofunctor (Scope g) where
  hduomap :: (forall (g :: u -> *) (g' :: u -> *) (b :: u).
 (forall (c :: u). g c -> g' c) -> s g b -> s' g' b)
-> (forall (b :: u). t b -> t' b)
-> Scope g s t a
-> Scope g s' t' a
hduomap forall (g :: u -> *) (g' :: u -> *) (b :: u).
(forall (c :: u). g c -> g' c) -> s g b -> s' g' b
g forall (b :: u). t b -> t' b
f = (s (BV g (s t)) a -> Identity (s' (BV g (s' t')) a))
-> Scope g s t a -> Identity (Scope g s' t' a)
forall k k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k) (g' :: k -> *) (h' :: (k -> *) -> k -> *) (f' :: k -> *)
       (a' :: k).
Iso
  (Scope g h f a)
  (Scope g' h' f' a')
  (h (BV g (h f)) a)
  (h' (BV g' (h' f')) a')
_Scope ((s (BV g (s t)) a -> Identity (s' (BV g (s' t')) a))
 -> Scope g s t a -> Identity (Scope g s' t' a))
-> (s (BV g (s t)) a -> s' (BV g (s' t')) a)
-> Scope g s t a
-> Scope g s' t' a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (c :: u). BV g (s t) c -> BV g (s' t') c)
-> s (BV g (s t)) a -> s' (BV g (s' t')) a
forall (g :: u -> *) (g' :: u -> *) (b :: u).
(forall (c :: u). g c -> g' c) -> s g b -> s' g' b
g ((forall (b :: u). s t b -> s' t' b)
-> BV g (s t) c -> BV g (s' t') c
forall u (h :: (u -> *) -> u -> *) (t :: u -> *) (t' :: u -> *)
       (a :: u).
HFunctor h =>
(forall (b :: u). t b -> t' b) -> h t a -> h t' a
hmap ((forall (b :: u). t b -> t' b) -> s t b -> s' t' b
forall (g :: u -> *) (g' :: u -> *) (b :: u).
(forall (c :: u). g c -> g' c) -> s g b -> s' g' b
g forall (b :: u). t b -> t' b
f))

instance HDuotraversable (Scope g) where
  hduotraverse :: (forall (g :: u -> *) (g' :: u -> *) (b :: u).
 (forall (c :: u). g c -> f (g' c)) -> s g b -> f (s' g' b))
-> (forall (b :: u). t b -> f (t' b))
-> Scope g s t a
-> f (Scope g s' t' a)
hduotraverse forall (g :: u -> *) (g' :: u -> *) (b :: u).
(forall (c :: u). g c -> f (g' c)) -> s g b -> f (s' g' b)
g forall (b :: u). t b -> f (t' b)
f = (s (BV g (s t)) a -> f (s' (BV g (s' t')) a))
-> Scope g s t a -> f (Scope g s' t' a)
forall k k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k) (g' :: k -> *) (h' :: (k -> *) -> k -> *) (f' :: k -> *)
       (a' :: k).
Iso
  (Scope g h f a)
  (Scope g' h' f' a')
  (h (BV g (h f)) a)
  (h' (BV g' (h' f')) a')
_Scope ((s (BV g (s t)) a -> f (s' (BV g (s' t')) a))
 -> Scope g s t a -> f (Scope g s' t' a))
-> (s (BV g (s t)) a -> f (s' (BV g (s' t')) a))
-> Scope g s t a
-> f (Scope g s' t' a)
forall k (f :: k -> *) s (t :: k) a (b :: k).
LensLike f s t a b -> LensLike f s t a b
%%~ (forall (c :: u). BV g (s t) c -> f (BV g (s' t') c))
-> s (BV g (s t)) a -> f (s' (BV g (s' t')) a)
forall (g :: u -> *) (g' :: u -> *) (b :: u).
(forall (c :: u). g c -> f (g' c)) -> s g b -> f (s' g' b)
g ((forall (b :: u). s t b -> f (s' t' b))
-> BV g (s t) c -> f (BV g (s' t') c)
forall u (h :: (u -> *) -> u -> *) (f :: * -> *) (t :: u -> *)
       (t' :: u -> *) (a :: u).
(HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (t' b)) -> h t a -> f (h t' a)
htraverse ((forall (b :: u). t b -> f (t' b)) -> s t b -> f (s' t' b)
forall (g :: u -> *) (g' :: u -> *) (b :: u).
(forall (c :: u). g c -> f (g' c)) -> s g b -> f (s' g' b)
g forall (b :: u). t b -> f (t' b)
f))


instance HBound (Scope g) where
  Scope h (BV g (h t)) a
x ^>>>= :: Scope g h t a -> (forall (b :: k). t b -> h t' b) -> Scope g h t' a
^>>>= forall (b :: k). t b -> h t' b
f = h (BV g (h t')) a -> Scope g h t' a
forall k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
h (BV g (h f)) a -> Scope g h f a
Scope (h (BV g (h t)) a
x h (BV g (h t)) a
-> (forall (b :: k). BV g (h t) b -> h (BV g (h t')) b)
-> h (BV g (h t')) a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k)
       (t' :: k -> *).
HBind h =>
h t a -> (forall (b :: k). t b -> h t' b) -> h t' a
^>>= (g b -> h (BV g (h t')) b)
-> (h t b -> h (BV g (h t')) b)
-> BV g (h t) b
-> h (BV g (h t')) b
forall k (w :: k -> *) (a :: k) r (v :: k -> *).
(w a -> r) -> (v a -> r) -> BV w v a -> r
foldBV (BV g (h t') b -> h (BV g (h t')) b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure (BV g (h t') b -> h (BV g (h t')) b)
-> (g b -> BV g (h t') b) -> g b -> h (BV g (h t')) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g b -> BV g (h t') b
forall k (g :: k -> *) (a :: k) (f :: k -> *). g a -> BV g f a
B) ((forall (b :: k). t b -> BV g (h t') b)
-> h t b -> h (BV g (h t')) b
forall u (h :: (u -> *) -> u -> *) (t :: u -> *) (t' :: u -> *)
       (a :: u).
HFunctor h =>
(forall (b :: u). t b -> t' b) -> h t a -> h t' a
hmap (h t' b -> BV g (h t') b
forall k (f :: k -> *) (a :: k) (g :: k -> *). f a -> BV g f a
F (h t' b -> BV g (h t') b)
-> (t b -> h t' b) -> t b -> BV g (h t') b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t b -> h t' b
forall (b :: k). t b -> h t' b
f)))


hbitraverseScope
  :: (Applicative t, HTraversable h)
  => (forall b. g b -> t (g' b))
  -> (forall b. f b -> t (f' b))
  -> Scope g h f a
  -> t (Scope g' h f' a)
hbitraverseScope :: (forall (b :: k). g b -> t (g' b))
-> (forall (b :: k). f b -> t (f' b))
-> Scope g h f a
-> t (Scope g' h f' a)
hbitraverseScope forall (b :: k). g b -> t (g' b)
g forall (b :: k). f b -> t (f' b)
f = AnIso
  (Scoped h f' g' a)
  (Scoped h f g a)
  (Scope g' h f' a)
  (Scope g h f a)
-> Iso
     (Scope g h f a)
     (Scope g' h f' a)
     (Scoped h f g a)
     (Scoped h f' g' a)
forall s t a b. AnIso s t a b -> Iso b a t s
from AnIso
  (Scoped h f' g' a)
  (Scoped h f g a)
  (Scope g' h f' a)
  (Scope g h f a)
forall k k (h :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (a :: k) (h' :: (k -> *) -> k -> *) (f' :: k -> *) (g' :: k -> *)
       (a' :: k).
Iso
  (Scoped h f g a)
  (Scoped h' f' g' a')
  (Scope g h f a)
  (Scope g' h' f' a')
_Scoped ((Scoped h f g a -> t (Scoped h f' g' a))
 -> Scope g h f a -> t (Scope g' h f' a))
-> (Scoped h f g a -> t (Scoped h f' g' a))
-> Scope g h f a
-> t (Scope g' h f' a)
forall k (f :: k -> *) s (t :: k) a (b :: k).
LensLike f s t a b -> LensLike f s t a b
%%~ (forall (b :: k). f b -> t (f' b))
-> (forall (b :: k). g b -> t (g' b))
-> Scoped h f g a
-> t (Scoped h f' g' a)
forall k (h :: (k -> *) -> (k -> *) -> k -> *) (f :: * -> *)
       (s :: k -> *) (s' :: k -> *) (t :: k -> *) (t' :: k -> *) (a :: k).
(HBitraversable h, Applicative f) =>
(forall (b :: k). s b -> f (s' b))
-> (forall (b :: k). t b -> f (t' b)) -> h s t a -> f (h s' t' a)
hbitraverse forall (b :: k). f b -> t (f' b)
f forall (b :: k). g b -> t (g' b)
g


freeVar :: (HPointed h) => f a -> Scope g h f a
freeVar :: f a -> Scope g h f a
freeVar = h (BV g (h f)) a -> Scope g h f a
forall k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
h (BV g (h f)) a -> Scope g h f a
Scope (h (BV g (h f)) a -> Scope g h f a)
-> (f a -> h (BV g (h f)) a) -> f a -> Scope g h f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV g (h f) a -> h (BV g (h f)) a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure (BV g (h f) a -> h (BV g (h f)) a)
-> (f a -> BV g (h f) a) -> f a -> h (BV g (h f)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h f a -> BV g (h f) a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure (h f a -> BV g (h f) a) -> (f a -> h f a) -> f a -> BV g (h f) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> h f a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure


boundVar :: (HPointed h) => g a -> Scope g h f a
boundVar :: g a -> Scope g h f a
boundVar = h (BV g (h f)) a -> Scope g h f a
forall k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
h (BV g (h f)) a -> Scope g h f a
Scope (h (BV g (h f)) a -> Scope g h f a)
-> (g a -> h (BV g (h f)) a) -> g a -> Scope g h f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV g (h f) a -> h (BV g (h f)) a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure (BV g (h f) a -> h (BV g (h f)) a)
-> (g a -> BV g (h f) a) -> g a -> h (BV g (h f)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> BV g (h f) a
forall k (g :: k -> *) (a :: k) (f :: k -> *). g a -> BV g f a
B


liftScope :: (HFunctor h, HPointed h) => h f a -> Scope g h f a
liftScope :: h f a -> Scope g h f a
liftScope = h (BV g (h f)) a -> Scope g h f a
forall k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
h (BV g (h f)) a -> Scope g h f a
Scope (h (BV g (h f)) a -> Scope g h f a)
-> (h f a -> h (BV g (h f)) a) -> h f a -> Scope g h f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (b :: k). f b -> BV g (h f) b) -> h f a -> h (BV g (h f)) a
forall u (h :: (u -> *) -> u -> *) (t :: u -> *) (t' :: u -> *)
       (a :: u).
HFunctor h =>
(forall (b :: u). t b -> t' b) -> h t a -> h t' a
hmap (h f b -> BV g (h f) b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure (h f b -> BV g (h f) b) -> (f b -> h f b) -> f b -> BV g (h f) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f b -> h f b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure)


abstractTraverse :: (HMonad h, HTraversable h, Applicative t) => (forall b. f b -> t (Maybe (g b))) -> h f a -> t (Scope g h f a)
abstractTraverse :: (forall (b :: k). f b -> t (Maybe (g b)))
-> h f a -> t (Scope g h f a)
abstractTraverse forall (b :: k). f b -> t (Maybe (g b))
f = (h (BV g (h f)) a -> Scope g h f a)
-> t (h (BV g (h f)) a) -> t (Scope g h f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap h (BV g (h f)) a -> Scope g h f a
forall k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
h (BV g (h f)) a -> Scope g h f a
Scope (t (h (BV g (h f)) a) -> t (Scope g h f a))
-> (h f a -> t (h (BV g (h f)) a)) -> h f a -> t (Scope g h f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (b :: k). f b -> t (BV g (h f) b))
-> h f a -> t (h (BV g (h f)) a)
forall u (h :: (u -> *) -> u -> *) (f :: * -> *) (t :: u -> *)
       (t' :: u -> *) (a :: u).
(HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (t' b)) -> h t a -> f (h t' a)
htraverse (\f b
y -> BV g (h f) b
-> (g b -> BV g (h f) b) -> Maybe (g b) -> BV g (h f) b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((h f b -> BV g (h f) b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure (h f b -> BV g (h f) b) -> (f b -> h f b) -> f b -> BV g (h f) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f b -> h f b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure) f b
y) g b -> BV g (h f) b
forall k (g :: k -> *) (a :: k) (f :: k -> *). g a -> BV g f a
B (Maybe (g b) -> BV g (h f) b)
-> t (Maybe (g b)) -> t (BV g (h f) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f b -> t (Maybe (g b))
forall (b :: k). f b -> t (Maybe (g b))
f f b
y)


abstract :: (HMonad h) => (forall b. f b -> Maybe (g b)) -> h f a -> Scope g h f a
abstract :: (forall (b :: k). f b -> Maybe (g b)) -> h f a -> Scope g h f a
abstract forall (b :: k). f b -> Maybe (g b)
f = h (BV g (h f)) a -> Scope g h f a
forall k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
h (BV g (h f)) a -> Scope g h f a
Scope (h (BV g (h f)) a -> Scope g h f a)
-> (h f a -> h (BV g (h f)) a) -> h f a -> Scope g h f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (b :: k). f b -> BV g (h f) b) -> h f a -> h (BV g (h f)) a
forall u (h :: (u -> *) -> u -> *) (t :: u -> *) (t' :: u -> *)
       (a :: u).
HFunctor h =>
(forall (b :: u). t b -> t' b) -> h t a -> h t' a
hmap (\f b
y -> BV g (h f) b
-> (g b -> BV g (h f) b) -> Maybe (g b) -> BV g (h f) b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((h f b -> BV g (h f) b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure (h f b -> BV g (h f) b) -> (f b -> h f b) -> f b -> BV g (h f) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f b -> h f b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure) f b
y) g b -> BV g (h f) b
forall k (g :: k -> *) (a :: k) (f :: k -> *). g a -> BV g f a
B (Maybe (g b) -> BV g (h f) b) -> Maybe (g b) -> BV g (h f) b
forall a b. (a -> b) -> a -> b
$ f b -> Maybe (g b)
forall (b :: k). f b -> Maybe (g b)
f f b
y)


-- instantiate :: (Substitutive op, Applicative f) => (forall b. w b -> f (op v b)) -> Scope g h f a -> f (op v a)
-- instantiate f (Scope x) = bindVars (foldBV f pure) x

-- | Sometimes it's convenient to move around the type arguments to 'Scope'.
newtype Scoped h f g a = Scoped { Scoped h f g a -> Scope g h f a
unscoped :: Scope g h f a }

_Scoped :: Iso (Scoped h f g a) (Scoped h' f' g' a') (Scope g h f a) (Scope g' h' f' a')
_Scoped :: p (Scope g h f a) (f (Scope g' h' f' a'))
-> p (Scoped h f g a) (f (Scoped h' f' g' a'))
_Scoped = (Scoped h f g a -> Scope g h f a)
-> (Scope g' h' f' a' -> Scoped h' f' g' a')
-> Iso
     (Scoped h f g a)
     (Scoped h' f' g' a')
     (Scope g h f a)
     (Scope g' h' f' a')
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso Scoped h f g a -> Scope g h f a
forall k (h :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (a :: k).
Scoped h f g a -> Scope g h f a
unscoped Scope g' h' f' a' -> Scoped h' f' g' a'
forall k (h :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (a :: k).
Scope g h f a -> Scoped h f g a
Scoped

instance HFunctor h => HFunctor (Scoped h f) where
  hmap :: (forall (b :: u). t b -> t' b) -> Scoped h f t a -> Scoped h f t' a
hmap = (forall (b :: u). t b -> t' b) -> Scoped h f t a -> Scoped h f t' a
forall k (h :: (k -> *) -> (k -> *) -> k -> *) (t :: k -> *)
       (t' :: k -> *) (s :: k -> *) (a :: k).
HBifunctor h =>
(forall (b :: k). t b -> t' b) -> h s t a -> h s t' a
hsecond

instance HFunctor h => HBifunctor (Scoped h) where
  hbimap :: (forall (b :: k). s b -> s' b)
-> (forall (b :: k). t b -> t' b)
-> Scoped h s t a
-> Scoped h s' t' a
hbimap forall (b :: k). s b -> s' b
f forall (b :: k). t b -> t' b
g = (Scope t h s a -> Identity (Scope t' h s' a))
-> Scoped h s t a -> Identity (Scoped h s' t' a)
forall k k (h :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (a :: k) (h' :: (k -> *) -> k -> *) (f' :: k -> *) (g' :: k -> *)
       (a' :: k).
Iso
  (Scoped h f g a)
  (Scoped h' f' g' a')
  (Scope g h f a)
  (Scope g' h' f' a')
_Scoped ((Scope t h s a -> Identity (Scope t' h s' a))
 -> Scoped h s t a -> Identity (Scoped h s' t' a))
-> ((h (BV t (h s)) a -> Identity (h (BV t' (h s')) a))
    -> Scope t h s a -> Identity (Scope t' h s' a))
-> (h (BV t (h s)) a -> Identity (h (BV t' (h s')) a))
-> Scoped h s t a
-> Identity (Scoped h s' t' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (h (BV t (h s)) a -> Identity (h (BV t' (h s')) a))
-> Scope t h s a -> Identity (Scope t' h s' a)
forall k k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k) (g' :: k -> *) (h' :: (k -> *) -> k -> *) (f' :: k -> *)
       (a' :: k).
Iso
  (Scope g h f a)
  (Scope g' h' f' a')
  (h (BV g (h f)) a)
  (h' (BV g' (h' f')) a')
_Scope ((h (BV t (h s)) a -> Identity (h (BV t' (h s')) a))
 -> Scoped h s t a -> Identity (Scoped h s' t' a))
-> (h (BV t (h s)) a -> h (BV t' (h s')) a)
-> Scoped h s t a
-> Scoped h s' t' a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (b :: k). BV t (h s) b -> BV t' (h s') b)
-> h (BV t (h s)) a -> h (BV t' (h s')) a
forall u (h :: (u -> *) -> u -> *) (t :: u -> *) (t' :: u -> *)
       (a :: u).
HFunctor h =>
(forall (b :: u). t b -> t' b) -> h t a -> h t' a
hmap ((forall (b :: k). t b -> t' b)
-> (forall (b :: k). h s b -> h s' b)
-> BV t (h s) b
-> BV t' (h s') b
forall k (h :: (k -> *) -> (k -> *) -> k -> *) (s :: k -> *)
       (s' :: k -> *) (t :: k -> *) (t' :: k -> *) (a :: k).
HBifunctor h =>
(forall (b :: k). s b -> s' b)
-> (forall (b :: k). t b -> t' b) -> h s t a -> h s' t' a
hbimap forall (b :: k). t b -> t' b
g ((forall (b :: k). s b -> s' b) -> h s b -> h s' b
forall u (h :: (u -> *) -> u -> *) (t :: u -> *) (t' :: u -> *)
       (a :: u).
HFunctor h =>
(forall (b :: u). t b -> t' b) -> h t a -> h t' a
hmap forall (b :: k). s b -> s' b
f))

instance HTraversable h => HBitraversable (Scoped h) where
  hbitraverse :: (forall (b :: k). s b -> f (s' b))
-> (forall (b :: k). t b -> f (t' b))
-> Scoped h s t a
-> f (Scoped h s' t' a)
hbitraverse forall (b :: k). s b -> f (s' b)
f forall (b :: k). t b -> f (t' b)
g = (Scope t h s a -> f (Scope t' h s' a))
-> Scoped h s t a -> f (Scoped h s' t' a)
forall k k (h :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (a :: k) (h' :: (k -> *) -> k -> *) (f' :: k -> *) (g' :: k -> *)
       (a' :: k).
Iso
  (Scoped h f g a)
  (Scoped h' f' g' a')
  (Scope g h f a)
  (Scope g' h' f' a')
_Scoped ((Scope t h s a -> f (Scope t' h s' a))
 -> Scoped h s t a -> f (Scoped h s' t' a))
-> ((h (BV t (h s)) a -> f (h (BV t' (h s')) a))
    -> Scope t h s a -> f (Scope t' h s' a))
-> (h (BV t (h s)) a -> f (h (BV t' (h s')) a))
-> Scoped h s t a
-> f (Scoped h s' t' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (h (BV t (h s)) a -> f (h (BV t' (h s')) a))
-> Scope t h s a -> f (Scope t' h s' a)
forall k k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k) (g' :: k -> *) (h' :: (k -> *) -> k -> *) (f' :: k -> *)
       (a' :: k).
Iso
  (Scope g h f a)
  (Scope g' h' f' a')
  (h (BV g (h f)) a)
  (h' (BV g' (h' f')) a')
_Scope ((h (BV t (h s)) a -> f (h (BV t' (h s')) a))
 -> Scoped h s t a -> f (Scoped h s' t' a))
-> (h (BV t (h s)) a -> f (h (BV t' (h s')) a))
-> Scoped h s t a
-> f (Scoped h s' t' a)
forall k (f :: k -> *) s (t :: k) a (b :: k).
LensLike f s t a b -> LensLike f s t a b
%%~ (forall (b :: k). BV t (h s) b -> f (BV t' (h s') b))
-> h (BV t (h s)) a -> f (h (BV t' (h s')) a)
forall u (h :: (u -> *) -> u -> *) (f :: * -> *) (t :: u -> *)
       (t' :: u -> *) (a :: u).
(HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (t' b)) -> h t a -> f (h t' a)
htraverse ((forall (b :: k). t b -> f (t' b))
-> (forall (b :: k). h s b -> f (h s' b))
-> BV t (h s) b
-> f (BV t' (h s') b)
forall k (h :: (k -> *) -> (k -> *) -> k -> *) (f :: * -> *)
       (s :: k -> *) (s' :: k -> *) (t :: k -> *) (t' :: k -> *) (a :: k).
(HBitraversable h, Applicative f) =>
(forall (b :: k). s b -> f (s' b))
-> (forall (b :: k). t b -> f (t' b)) -> h s t a -> f (h s' t' a)
hbitraverse forall (b :: k). t b -> f (t' b)
g ((forall (b :: k). s b -> f (s' b)) -> h s b -> f (h s' b)
forall u (h :: (u -> *) -> u -> *) (f :: * -> *) (t :: u -> *)
       (t' :: u -> *) (a :: u).
(HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (t' b)) -> h t a -> f (h t' a)
htraverse forall (b :: k). s b -> f (s' b)
f))

instance HTraversable h => HTraversable (Scoped h f) where
  htraverse :: (forall (b :: u). t b -> f (t' b))
-> Scoped h f t a -> f (Scoped h f t' a)
htraverse = (forall (b :: u). f b -> f (f b))
-> (forall (b :: u). t b -> f (t' b))
-> Scoped h f t a
-> f (Scoped h f t' a)
forall k (h :: (k -> *) -> (k -> *) -> k -> *) (f :: * -> *)
       (s :: k -> *) (s' :: k -> *) (t :: k -> *) (t' :: k -> *) (a :: k).
(HBitraversable h, Applicative f) =>
(forall (b :: k). s b -> f (s' b))
-> (forall (b :: k). t b -> f (t' b)) -> h s t a -> f (h s' t' a)
hbitraverse forall (b :: u). f b -> f (f b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

--------------------------------------------------------------------------------
--  Scoped Free Monads
--------------------------------------------------------------------------------

data SFree h f a
  = SPure (f a)
  | SWrap (h (Scoped (SFree h) f) (SFree h f) a)

instance HDuofunctor h => HFunctor (SFree h) where
  hmap :: (forall (b :: u). t b -> t' b) -> SFree h t a -> SFree h t' a
hmap = (forall (b :: u). t b -> t' b) -> SFree h t a -> SFree h t' a
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (t' :: k -> *)
       (a :: k).
(HPointed h, HBind h) =>
(forall (b :: k). t b -> t' b) -> h t a -> h t' a
hliftM

instance HPointed (SFree h) where
  hpure :: t a -> SFree h t a
hpure = t a -> SFree h t a
forall k (h :: ((k -> *) -> k -> *) -> (k -> *) -> k -> *)
       (t :: k -> *) (a :: k).
t a -> SFree h t a
SPure

instance HDuofunctor h => HBind (SFree h) where
  SPure t a
x ^>>= :: SFree h t a
-> (forall (b :: k). t b -> SFree h t' b) -> SFree h t' a
^>>= forall (b :: k). t b -> SFree h t' b
f = t a -> SFree h t' a
forall (b :: k). t b -> SFree h t' b
f t a
x
  SWrap h (Scoped (SFree h) t) (SFree h t) a
x ^>>= forall (b :: k). t b -> SFree h t' b
f = h (Scoped (SFree h) t') (SFree h t') a -> SFree h t' a
forall k (h :: ((k -> *) -> k -> *) -> (k -> *) -> k -> *)
       (f :: k -> *) (a :: k).
h (Scoped (SFree h) f) (SFree h f) a -> SFree h f a
SWrap ((forall (g :: k -> *) (g' :: k -> *) (b :: k).
 (forall (c :: k). g c -> g' c)
 -> Scoped (SFree h) t g b -> Scoped (SFree h) t' g' b)
-> (forall (b :: k). SFree h t b -> SFree h t' b)
-> h (Scoped (SFree h) t) (SFree h t) a
-> h (Scoped (SFree h) t') (SFree h t') a
forall u (h :: ((u -> *) -> u -> *) -> (u -> *) -> u -> *)
       (s :: (u -> *) -> u -> *) (s' :: (u -> *) -> u -> *) (t :: u -> *)
       (t' :: u -> *) (a :: u).
HDuofunctor h =>
(forall (g :: u -> *) (g' :: u -> *) (b :: u).
 (forall (c :: u). g c -> g' c) -> s g b -> s' g' b)
-> (forall (b :: u). t b -> t' b) -> h s t a -> h s' t' a
hduomap (\forall (c :: k). g c -> g' c
g -> (\(Scoped Scope g' (SFree h) t b
y) -> Scope g' (SFree h) t' b -> Scoped (SFree h) t' g' b
forall k (h :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (a :: k).
Scope g h f a -> Scoped h f g a
Scoped (Scope g' (SFree h) t b
y Scope g' (SFree h) t b
-> (forall (b :: k). t b -> SFree h t' b)
-> Scope g' (SFree h) t' b
forall k k (k :: ((k -> *) -> k -> *) -> (k -> *) -> k -> *)
       (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k) (t' :: k -> *).
(HBound k, HMonad h) =>
k h t a -> (forall (b :: k). t b -> h t' b) -> k h t' a
^>>>= forall (b :: k). t b -> SFree h t' b
f)) (Scoped (SFree h) t g' b -> Scoped (SFree h) t' g' b)
-> (Scoped (SFree h) t g b -> Scoped (SFree h) t g' b)
-> Scoped (SFree h) t g b
-> Scoped (SFree h) t' g' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (c :: k). g c -> g' c)
-> Scoped (SFree h) t g b -> Scoped (SFree h) t g' b
forall u (h :: (u -> *) -> u -> *) (t :: u -> *) (t' :: u -> *)
       (a :: u).
HFunctor h =>
(forall (b :: u). t b -> t' b) -> h t a -> h t' a
hmap forall (c :: k). g c -> g' c
g) (SFree h t b
-> (forall (b :: k). t b -> SFree h t' b) -> SFree h t' b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k)
       (t' :: k -> *).
HBind h =>
h t a -> (forall (b :: k). t b -> h t' b) -> h t' a
^>>= forall (b :: k). t b -> SFree h t' b
f) h (Scoped (SFree h) t) (SFree h t) a
x)

instance HDuofunctor h => HMonad (SFree h)

instance (HDuotraversable h) => HTraversable (SFree h) where
  htraverse :: (forall (b :: u). t b -> f (t' b))
-> SFree h t a -> f (SFree h t' a)
htraverse forall (b :: u). t b -> f (t' b)
f = \case
    SPure t a
x -> t' a -> SFree h t' a
forall k (h :: ((k -> *) -> k -> *) -> (k -> *) -> k -> *)
       (t :: k -> *) (a :: k).
t a -> SFree h t a
SPure (t' a -> SFree h t' a) -> f (t' a) -> f (SFree h t' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t a -> f (t' a)
forall (b :: u). t b -> f (t' b)
f t a
x
    SWrap h (Scoped (SFree h) t) (SFree h t) a
x -> h (Scoped (SFree h) t') (SFree h t') a -> SFree h t' a
forall k (h :: ((k -> *) -> k -> *) -> (k -> *) -> k -> *)
       (f :: k -> *) (a :: k).
h (Scoped (SFree h) f) (SFree h f) a -> SFree h f a
SWrap (h (Scoped (SFree h) t') (SFree h t') a -> SFree h t' a)
-> f (h (Scoped (SFree h) t') (SFree h t') a) -> f (SFree h t' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (g :: u -> *) (g' :: u -> *) (b :: u).
 (forall (c :: u). g c -> f (g' c))
 -> Scoped (SFree h) t g b -> f (Scoped (SFree h) t' g' b))
-> (forall (b :: u). SFree h t b -> f (SFree h t' b))
-> h (Scoped (SFree h) t) (SFree h t) a
-> f (h (Scoped (SFree h) t') (SFree h t') a)
forall u (h :: ((u -> *) -> u -> *) -> (u -> *) -> u -> *)
       (f :: * -> *) (s :: (u -> *) -> u -> *) (s' :: (u -> *) -> u -> *)
       (t :: u -> *) (t' :: u -> *) (a :: u).
(HDuotraversable h, Applicative f) =>
(forall (g :: u -> *) (g' :: u -> *) (b :: u).
 (forall (c :: u). g c -> f (g' c)) -> s g b -> f (s' g' b))
-> (forall (b :: u). t b -> f (t' b)) -> h s t a -> f (h s' t' a)
hduotraverse ((forall (b :: u). t b -> f (t' b))
-> (forall (c :: u). g c -> f (g' c))
-> Scoped (SFree h) t g b
-> f (Scoped (SFree h) t' g' b)
forall k (h :: (k -> *) -> (k -> *) -> k -> *) (f :: * -> *)
       (s :: k -> *) (s' :: k -> *) (t :: k -> *) (t' :: k -> *) (a :: k).
(HBitraversable h, Applicative f) =>
(forall (b :: k). s b -> f (s' b))
-> (forall (b :: k). t b -> f (t' b)) -> h s t a -> f (h s' t' a)
hbitraverse forall (b :: u). t b -> f (t' b)
f) ((forall (b :: u). t b -> f (t' b))
-> SFree h t b -> f (SFree h t' b)
forall u (h :: (u -> *) -> u -> *) (f :: * -> *) (t :: u -> *)
       (t' :: u -> *) (a :: u).
(HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (t' b)) -> h t a -> f (h t' a)
htraverse forall (b :: u). t b -> f (t' b)
f) h (Scoped (SFree h) t) (SFree h t) a
x


instance HDuofoldableAt k (Scope k) where
  hduofoldMap :: (forall (g :: k -> *) (b :: k).
 (forall (c :: k). g c -> k c) -> s g b -> k b)
-> (forall (b :: k). t b -> k b) -> Scope k s t a -> k a
hduofoldMap forall (g :: k -> *) (b :: k).
(forall (c :: k). g c -> k c) -> s g b -> k b
f forall (b :: k). t b -> k b
g = (forall (c :: k). BV k (s t) c -> k c) -> s (BV k (s t)) a -> k a
forall (g :: k -> *) (b :: k).
(forall (c :: k). g c -> k c) -> s g b -> k b
f ((forall (b :: k). k b -> k b)
-> (forall (b :: k). s t b -> k b) -> BV k (s t) c -> k c
forall k (k :: k -> *) (h :: (k -> *) -> (k -> *) -> k -> *)
       (f :: k -> *) (g :: k -> *) (a :: k).
HBifoldableAt k h =>
(forall (b :: k). f b -> k b)
-> (forall (b :: k). g b -> k b) -> h f g a -> k a
hbifoldMap forall (b :: k). k b -> k b
forall a. a -> a
id ((forall (b :: k). t b -> k b) -> s t b -> k b
forall (g :: k -> *) (b :: k).
(forall (c :: k). g c -> k c) -> s g b -> k b
f forall (b :: k). t b -> k b
g)) (s (BV k (s t)) a -> k a)
-> (Scope k s t a -> s (BV k (s t)) a) -> Scope k s t a -> k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (s (BV k (s t)) a) (Scope k s t a) (s (BV k (s t)) a)
-> Scope k s t a -> s (BV k (s t)) a
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (s (BV k (s t)) a) (Scope k s t a) (s (BV k (s t)) a)
forall k k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k) (g' :: k -> *) (h' :: (k -> *) -> k -> *) (f' :: k -> *)
       (a' :: k).
Iso
  (Scope g h f a)
  (Scope g' h' f' a')
  (h (BV g (h f)) a)
  (h' (BV g' (h' f')) a')
_Scope

instance (HFunctor h, HFoldableAt k h) => HBifoldableAt k (Scoped h) where
  hbifoldMap :: (forall (b :: k). f b -> k b)
-> (forall (b :: k). g b -> k b) -> Scoped h f g a -> k a
hbifoldMap forall (b :: k). f b -> k b
f forall (b :: k). g b -> k b
g = (forall (b :: k). BV g (h f) b -> k b) -> h (BV g (h f)) a -> k a
forall k (k :: k -> *) (h :: (k -> *) -> k -> *) (t :: k -> *)
       (a :: k).
HFoldableAt k h =>
(forall (b :: k). t b -> k b) -> h t a -> k a
hfoldMap ((forall (b :: k). g b -> k b)
-> (forall (b :: k). h f b -> k b) -> BV g (h f) b -> k b
forall k (k :: k -> *) (h :: (k -> *) -> (k -> *) -> k -> *)
       (f :: k -> *) (g :: k -> *) (a :: k).
HBifoldableAt k h =>
(forall (b :: k). f b -> k b)
-> (forall (b :: k). g b -> k b) -> h f g a -> k a
hbifoldMap forall (b :: k). g b -> k b
g ((forall (b :: k). f b -> k b) -> h f b -> k b
forall k (k :: k -> *) (h :: (k -> *) -> k -> *) (t :: k -> *)
       (a :: k).
HFoldableAt k h =>
(forall (b :: k). t b -> k b) -> h t a -> k a
hfoldMap forall (b :: k). f b -> k b
f)) (h (BV g (h f)) a -> k a)
-> (Scoped h f g a -> h (BV g (h f)) a) -> Scoped h f g a -> k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (h (BV g (h f)) a) (Scoped h f g a) (h (BV g (h f)) a)
-> Scoped h f g a -> h (BV g (h f)) a
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((Scope g h f a -> Const (h (BV g (h f)) a) (Scope g h f a))
-> Scoped h f g a -> Const (h (BV g (h f)) a) (Scoped h f g a)
forall k k (h :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (a :: k) (h' :: (k -> *) -> k -> *) (f' :: k -> *) (g' :: k -> *)
       (a' :: k).
Iso
  (Scoped h f g a)
  (Scoped h' f' g' a')
  (Scope g h f a)
  (Scope g' h' f' a')
_Scoped ((Scope g h f a -> Const (h (BV g (h f)) a) (Scope g h f a))
 -> Scoped h f g a -> Const (h (BV g (h f)) a) (Scoped h f g a))
-> ((h (BV g (h f)) a
     -> Const (h (BV g (h f)) a) (h (BV g (h f)) a))
    -> Scope g h f a -> Const (h (BV g (h f)) a) (Scope g h f a))
-> Getting (h (BV g (h f)) a) (Scoped h f g a) (h (BV g (h f)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (h (BV g (h f)) a -> Const (h (BV g (h f)) a) (h (BV g (h f)) a))
-> Scope g h f a -> Const (h (BV g (h f)) a) (Scope g h f a)
forall k k (g :: k -> *) (h :: (k -> *) -> k -> *) (f :: k -> *)
       (a :: k) (g' :: k -> *) (h' :: (k -> *) -> k -> *) (f' :: k -> *)
       (a' :: k).
Iso
  (Scope g h f a)
  (Scope g' h' f' a')
  (h (BV g (h f)) a)
  (h' (BV g' (h' f')) a')
_Scope)

instance (HDuotraversable h, HDuofoldableAt k h) => HFoldableAt k (SFree h) where
  hfoldMap :: (forall (b :: k). t b -> k b) -> SFree h t a -> k a
hfoldMap forall (b :: k). t b -> k b
f = \case
    SPure t a
x -> t a -> k a
forall (b :: k). t b -> k b
f t a
x
    SWrap h (Scoped (SFree h) t) (SFree h t) a
x ->
      (forall (g :: k -> *) (b :: k).
 (forall (c :: k). g c -> k c) -> Scoped (SFree h) t g b -> k b)
-> (forall (b :: k). SFree h t b -> k b)
-> h (Scoped (SFree h) t) (SFree h t) a
-> k a
forall k (k :: k -> *)
       (h :: ((k -> *) -> k -> *) -> (k -> *) -> k -> *)
       (s :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
(HDuofoldableAt k h, HTraversable s) =>
(forall (g :: k -> *) (b :: k).
 (forall (c :: k). g c -> k c) -> s g b -> k b)
-> (forall (b :: k). t b -> k b) -> h s t a -> k a
hduofoldMap
      (\forall (c :: k). g c -> k c
g -> (forall (t :: k -> *) (a :: k).
 (forall (b :: k). t b -> k b) -> SFree h t a -> k a)
-> (forall (b :: k). t b -> k b) -> Scope k (SFree h) t b -> k b
forall k (k :: k -> *)
       (h :: ((k -> *) -> k -> *) -> (k -> *) -> k -> *)
       (s :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
(HDuofoldableAt k h, HTraversable s) =>
(forall (g :: k -> *) (b :: k).
 (forall (c :: k). g c -> k c) -> s g b -> k b)
-> (forall (b :: k). t b -> k b) -> h s t a -> k a
hduofoldMap forall k (k :: k -> *) (h :: (k -> *) -> k -> *) (t :: k -> *)
       (a :: k).
HFoldableAt k h =>
(forall (b :: k). t b -> k b) -> h t a -> k a
forall (t :: k -> *) (a :: k).
(forall (b :: k). t b -> k b) -> SFree h t a -> k a
hfoldMap forall (b :: k). t b -> k b
f (Scope k (SFree h) t b -> k b)
-> (Scoped (SFree h) t g b -> Scope k (SFree h) t b)
-> Scoped (SFree h) t g b
-> k b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (Scope k (SFree h) t b)
  (Scoped (SFree h) t k b)
  (Scope k (SFree h) t b)
-> Scoped (SFree h) t k b -> Scope k (SFree h) t b
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Scope k (SFree h) t b)
  (Scoped (SFree h) t k b)
  (Scope k (SFree h) t b)
forall k k (h :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (a :: k) (h' :: (k -> *) -> k -> *) (f' :: k -> *) (g' :: k -> *)
       (a' :: k).
Iso
  (Scoped h f g a)
  (Scoped h' f' g' a')
  (Scope g h f a)
  (Scope g' h' f' a')
_Scoped (Scoped (SFree h) t k b -> Scope k (SFree h) t b)
-> (Scoped (SFree h) t g b -> Scoped (SFree h) t k b)
-> Scoped (SFree h) t g b
-> Scope k (SFree h) t b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (c :: k). g c -> k c)
-> Scoped (SFree h) t g b -> Scoped (SFree h) t k b
forall k (h :: (k -> *) -> (k -> *) -> k -> *) (t :: k -> *)
       (t' :: k -> *) (s :: k -> *) (a :: k).
HBifunctor h =>
(forall (b :: k). t b -> t' b) -> h s t a -> h s t' a
hsecond forall (c :: k). g c -> k c
g)
      ((forall (b :: k). t b -> k b) -> SFree h t b -> k b
forall k (k :: k -> *) (h :: (k -> *) -> k -> *) (t :: k -> *)
       (a :: k).
HFoldableAt k h =>
(forall (b :: k). t b -> k b) -> h t a -> k a
hfoldMap forall (b :: k). t b -> k b
f)
      h (Scoped (SFree h) t) (SFree h t) a
x