{-# LANGUAGE DeriveFoldable        #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
module Free.Scoped where

import           Control.Monad      (ap)
import           Data.Bifoldable
import           Data.Bifunctor
import           Data.Bifunctor.TH
import           Data.Bitraversable
import           Data.Function      (on)
import qualified GHC.Generics       as GHC

data Inc var = Z | S var
  deriving (Inc var -> Inc var -> Bool
forall var. Eq var => Inc var -> Inc var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Inc var -> Inc var -> Bool
$c/= :: forall var. Eq var => Inc var -> Inc var -> Bool
== :: Inc var -> Inc var -> Bool
$c== :: forall var. Eq var => Inc var -> Inc var -> Bool
Eq, Int -> Inc var -> ShowS
forall var. Show var => Int -> Inc var -> ShowS
forall var. Show var => [Inc var] -> ShowS
forall var. Show var => Inc var -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Inc var] -> ShowS
$cshowList :: forall var. Show var => [Inc var] -> ShowS
show :: Inc var -> String
$cshow :: forall var. Show var => Inc var -> String
showsPrec :: Int -> Inc var -> ShowS
$cshowsPrec :: forall var. Show var => Int -> Inc var -> ShowS
Show, forall a b. a -> Inc b -> Inc a
forall a b. (a -> b) -> Inc a -> Inc b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Inc b -> Inc a
$c<$ :: forall a b. a -> Inc b -> Inc a
fmap :: forall a b. (a -> b) -> Inc a -> Inc b
$cfmap :: forall a b. (a -> b) -> Inc a -> Inc b
Functor, forall a. Eq a => a -> Inc a -> Bool
forall a. Num a => Inc a -> a
forall a. Ord a => Inc a -> a
forall m. Monoid m => Inc m -> m
forall a. Inc a -> Bool
forall a. Inc a -> Int
forall a. Inc a -> [a]
forall a. (a -> a -> a) -> Inc a -> a
forall m a. Monoid m => (a -> m) -> Inc a -> m
forall b a. (b -> a -> b) -> b -> Inc a -> b
forall a b. (a -> b -> b) -> b -> Inc a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Inc a -> a
$cproduct :: forall a. Num a => Inc a -> a
sum :: forall a. Num a => Inc a -> a
$csum :: forall a. Num a => Inc a -> a
minimum :: forall a. Ord a => Inc a -> a
$cminimum :: forall a. Ord a => Inc a -> a
maximum :: forall a. Ord a => Inc a -> a
$cmaximum :: forall a. Ord a => Inc a -> a
elem :: forall a. Eq a => a -> Inc a -> Bool
$celem :: forall a. Eq a => a -> Inc a -> Bool
length :: forall a. Inc a -> Int
$clength :: forall a. Inc a -> Int
null :: forall a. Inc a -> Bool
$cnull :: forall a. Inc a -> Bool
toList :: forall a. Inc a -> [a]
$ctoList :: forall a. Inc a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Inc a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Inc a -> a
foldr1 :: forall a. (a -> a -> a) -> Inc a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Inc a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Inc a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Inc a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Inc a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Inc a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Inc a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Inc a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Inc a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Inc a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Inc a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Inc a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Inc a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Inc a -> m
fold :: forall m. Monoid m => Inc m -> m
$cfold :: forall m. Monoid m => Inc m -> m
Foldable, Functor Inc
Foldable Inc
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Inc (m a) -> m (Inc a)
forall (f :: * -> *) a. Applicative f => Inc (f a) -> f (Inc a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Inc a -> m (Inc b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Inc a -> f (Inc b)
sequence :: forall (m :: * -> *) a. Monad m => Inc (m a) -> m (Inc a)
$csequence :: forall (m :: * -> *) a. Monad m => Inc (m a) -> m (Inc a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Inc a -> m (Inc b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Inc a -> m (Inc b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Inc (f a) -> f (Inc a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Inc (f a) -> f (Inc a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Inc a -> f (Inc b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Inc a -> f (Inc b)
Traversable)

type Scope term var = term (Inc var)

instantiate :: Monad f => f a -> f (Inc a) -> f a
instantiate :: forall (f :: * -> *) a. Monad f => f a -> f (Inc a) -> f a
instantiate f a
e f (Inc a)
f = f (Inc a)
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Inc a -> f a
g
  where
    g :: Inc a -> f a
g Inc a
Z     = f a
e
    g (S a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return a
x

abstract :: (Eq a, Functor f) => a -> f a -> f (Inc a)
abstract :: forall a (f :: * -> *). (Eq a, Functor f) => a -> f a -> f (Inc a)
abstract a
x f a
e = a -> Inc a
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
e
  where
    k :: a -> Inc a
k a
y | a
x forall a. Eq a => a -> a -> Bool
== a
y    = forall var. Inc var
Z
        | Bool
otherwise = forall var. var -> Inc var
S a
y

data FS t a
  = Pure a
  | Free (t (Scope (FS t) a) (FS t a))

deriving instance (Eq a, forall x y. (Eq x, Eq y) => Eq (t x y)) => Eq (FS t a)

instance Bifunctor t => Functor (FS t) where
  fmap :: forall a b. (a -> b) -> FS t a -> FS t b
fmap a -> b
f (Pure a
x) = forall (t :: * -> * -> *) a. a -> FS t a
Pure (a -> b
f a
x)
  fmap a -> b
f (Free t (Scope (FS t) a) (FS t a)
t) = forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free
    (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) t (Scope (FS t) a) (FS t a)
t)

instance Bifoldable t => Foldable (FS t) where
  foldMap :: forall m a. Monoid m => (a -> m) -> FS t a -> m
foldMap a -> m
f (Pure a
x) = a -> m
f a
x
  foldMap a -> m
f (Free t (Scope (FS t) a) (FS t a)
t) = forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f)) (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) t (Scope (FS t) a) (FS t a)
t

instance Bitraversable t => Traversable (FS t) where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FS t a -> f (FS t b)
traverse a -> f b
f (Pure a
x) = forall (t :: * -> * -> *) a. a -> FS t a
Pure forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x
  traverse a -> f b
f (Free t (Scope (FS t) a) (FS t a)
t) = forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f)) (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f) t (Scope (FS t) a) (FS t a)
t

instance Bifunctor t => Applicative (FS t) where
  pure :: forall a. a -> FS t a
pure = forall (t :: * -> * -> *) a. a -> FS t a
Pure
  <*> :: forall a b. FS t (a -> b) -> FS t a -> FS t b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Bifunctor t => Monad (FS t) where
  return :: forall a. a -> FS t a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Pure a
x >>= :: forall a b. FS t a -> (a -> FS t b) -> FS t b
>>= a -> FS t b
f = a -> FS t b
f a
x
  Free t (Scope (FS t) a) (FS t a)
t >>= a -> FS t b
f = forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free
    (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> FS t b
f)) (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> FS t b
f) t (Scope (FS t) a) (FS t a)
t)

data Sum f g scope term
  = InL (f scope term)
  | InR (g scope term)
  deriving (forall a b. a -> Sum f g scope b -> Sum f g scope a
forall a b. (a -> b) -> Sum f g scope a -> Sum f g scope b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (f :: * -> * -> *) (g :: * -> * -> *) scope a b.
(Functor (f scope), Functor (g scope)) =>
a -> Sum f g scope b -> Sum f g scope a
forall (f :: * -> * -> *) (g :: * -> * -> *) scope a b.
(Functor (f scope), Functor (g scope)) =>
(a -> b) -> Sum f g scope a -> Sum f g scope b
<$ :: forall a b. a -> Sum f g scope b -> Sum f g scope a
$c<$ :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a b.
(Functor (f scope), Functor (g scope)) =>
a -> Sum f g scope b -> Sum f g scope a
fmap :: forall a b. (a -> b) -> Sum f g scope a -> Sum f g scope b
$cfmap :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a b.
(Functor (f scope), Functor (g scope)) =>
(a -> b) -> Sum f g scope a -> Sum f g scope b
Functor, forall a. Sum f g scope a -> Bool
forall m a. Monoid m => (a -> m) -> Sum f g scope a -> m
forall a b. (a -> b -> b) -> b -> Sum f g scope a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope), Eq a) =>
a -> Sum f g scope a -> Bool
forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope), Num a) =>
Sum f g scope a -> a
forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope), Ord a) =>
Sum f g scope a -> a
forall (f :: * -> * -> *) (g :: * -> * -> *) scope m.
(Foldable (f scope), Foldable (g scope), Monoid m) =>
Sum f g scope m -> m
forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
Sum f g scope a -> Bool
forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
Sum f g scope a -> Int
forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
Sum f g scope a -> [a]
forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
(a -> a -> a) -> Sum f g scope a -> a
forall (f :: * -> * -> *) (g :: * -> * -> *) scope m a.
(Foldable (f scope), Foldable (g scope), Monoid m) =>
(a -> m) -> Sum f g scope a -> m
forall (f :: * -> * -> *) (g :: * -> * -> *) scope b a.
(Foldable (f scope), Foldable (g scope)) =>
(b -> a -> b) -> b -> Sum f g scope a -> b
forall (f :: * -> * -> *) (g :: * -> * -> *) scope a b.
(Foldable (f scope), Foldable (g scope)) =>
(a -> b -> b) -> b -> Sum f g scope a -> b
product :: forall a. Num a => Sum f g scope a -> a
$cproduct :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope), Num a) =>
Sum f g scope a -> a
sum :: forall a. Num a => Sum f g scope a -> a
$csum :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope), Num a) =>
Sum f g scope a -> a
minimum :: forall a. Ord a => Sum f g scope a -> a
$cminimum :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope), Ord a) =>
Sum f g scope a -> a
maximum :: forall a. Ord a => Sum f g scope a -> a
$cmaximum :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope), Ord a) =>
Sum f g scope a -> a
elem :: forall a. Eq a => a -> Sum f g scope a -> Bool
$celem :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope), Eq a) =>
a -> Sum f g scope a -> Bool
length :: forall a. Sum f g scope a -> Int
$clength :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
Sum f g scope a -> Int
null :: forall a. Sum f g scope a -> Bool
$cnull :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
Sum f g scope a -> Bool
toList :: forall a. Sum f g scope a -> [a]
$ctoList :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
Sum f g scope a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Sum f g scope a -> a
$cfoldl1 :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
(a -> a -> a) -> Sum f g scope a -> a
foldr1 :: forall a. (a -> a -> a) -> Sum f g scope a -> a
$cfoldr1 :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
(a -> a -> a) -> Sum f g scope a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Sum f g scope a -> b
$cfoldl' :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope b a.
(Foldable (f scope), Foldable (g scope)) =>
(b -> a -> b) -> b -> Sum f g scope a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Sum f g scope a -> b
$cfoldl :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope b a.
(Foldable (f scope), Foldable (g scope)) =>
(b -> a -> b) -> b -> Sum f g scope a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Sum f g scope a -> b
$cfoldr' :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a b.
(Foldable (f scope), Foldable (g scope)) =>
(a -> b -> b) -> b -> Sum f g scope a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Sum f g scope a -> b
$cfoldr :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a b.
(Foldable (f scope), Foldable (g scope)) =>
(a -> b -> b) -> b -> Sum f g scope a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Sum f g scope a -> m
$cfoldMap' :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope m a.
(Foldable (f scope), Foldable (g scope), Monoid m) =>
(a -> m) -> Sum f g scope a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Sum f g scope a -> m
$cfoldMap :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope m a.
(Foldable (f scope), Foldable (g scope), Monoid m) =>
(a -> m) -> Sum f g scope a -> m
fold :: forall m. Monoid m => Sum f g scope m -> m
$cfold :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope m.
(Foldable (f scope), Foldable (g scope), Monoid m) =>
Sum f g scope m -> m
Foldable, forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Sum f g scope a -> f (Sum f g scope b)
forall {f :: * -> * -> *} {g :: * -> * -> *} {scope}.
(Traversable (f scope), Traversable (g scope)) =>
Functor (Sum f g scope)
forall {f :: * -> * -> *} {g :: * -> * -> *} {scope}.
(Traversable (f scope), Traversable (g scope)) =>
Foldable (Sum f g scope)
forall (f :: * -> * -> *) (g :: * -> * -> *) scope (m :: * -> *) a.
(Traversable (f scope), Traversable (g scope), Monad m) =>
Sum f g scope (m a) -> m (Sum f g scope a)
forall (f :: * -> * -> *) (g :: * -> * -> *) scope (f :: * -> *) a.
(Traversable (f scope), Traversable (g scope), Applicative f) =>
Sum f g scope (f a) -> f (Sum f g scope a)
forall (f :: * -> * -> *) (g :: * -> * -> *) scope (m :: * -> *) a
       b.
(Traversable (f scope), Traversable (g scope), Monad m) =>
(a -> m b) -> Sum f g scope a -> m (Sum f g scope b)
forall (f :: * -> * -> *) (g :: * -> * -> *) scope (f :: * -> *) a
       b.
(Traversable (f scope), Traversable (g scope), Applicative f) =>
(a -> f b) -> Sum f g scope a -> f (Sum f g scope b)
sequence :: forall (m :: * -> *) a.
Monad m =>
Sum f g scope (m a) -> m (Sum f g scope a)
$csequence :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope (m :: * -> *) a.
(Traversable (f scope), Traversable (g scope), Monad m) =>
Sum f g scope (m a) -> m (Sum f g scope a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Sum f g scope a -> m (Sum f g scope b)
$cmapM :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope (m :: * -> *) a
       b.
(Traversable (f scope), Traversable (g scope), Monad m) =>
(a -> m b) -> Sum f g scope a -> m (Sum f g scope b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Sum f g scope (f a) -> f (Sum f g scope a)
$csequenceA :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope (f :: * -> *) a.
(Traversable (f scope), Traversable (g scope), Applicative f) =>
Sum f g scope (f a) -> f (Sum f g scope a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Sum f g scope a -> f (Sum f g scope b)
$ctraverse :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope (f :: * -> *) a
       b.
(Traversable (f scope), Traversable (g scope), Applicative f) =>
(a -> f b) -> Sum f g scope a -> f (Sum f g scope b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (f :: * -> * -> *) (g :: * -> * -> *) scope term x.
Rep (Sum f g scope term) x -> Sum f g scope term
forall (f :: * -> * -> *) (g :: * -> * -> *) scope term x.
Sum f g scope term -> Rep (Sum f g scope term) x
$cto :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope term x.
Rep (Sum f g scope term) x -> Sum f g scope term
$cfrom :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope term x.
Sum f g scope term -> Rep (Sum f g scope term) x
GHC.Generic)
deriveBifunctor ''Sum
deriveBifoldable ''Sum
deriveBitraversable ''Sum

type (:+:) = Sum

data Empty scope term
  deriving (forall a b. (a -> b) -> Empty scope a -> Empty scope b
forall scope a b. a -> Empty scope b -> Empty scope a
forall scope a b. (a -> b) -> Empty scope a -> Empty scope b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Empty scope b -> Empty scope a
$c<$ :: forall scope a b. a -> Empty scope b -> Empty scope a
fmap :: forall a b. (a -> b) -> Empty scope a -> Empty scope b
$cfmap :: forall scope a b. (a -> b) -> Empty scope a -> Empty scope b
Functor, forall scope a. Eq a => a -> Empty scope a -> Bool
forall scope a. Num a => Empty scope a -> a
forall scope a. Ord a => Empty scope a -> a
forall m a. Monoid m => (a -> m) -> Empty scope a -> m
forall scope m. Monoid m => Empty scope m -> m
forall scope a. Empty scope a -> Bool
forall scope a. Empty scope a -> Int
forall scope a. Empty scope a -> [a]
forall scope a. (a -> a -> a) -> Empty scope a -> a
forall scope m a. Monoid m => (a -> m) -> Empty scope a -> m
forall scope b a. (b -> a -> b) -> b -> Empty scope a -> b
forall scope a b. (a -> b -> b) -> b -> Empty scope a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Empty scope a -> a
$cproduct :: forall scope a. Num a => Empty scope a -> a
sum :: forall a. Num a => Empty scope a -> a
$csum :: forall scope a. Num a => Empty scope a -> a
minimum :: forall a. Ord a => Empty scope a -> a
$cminimum :: forall scope a. Ord a => Empty scope a -> a
maximum :: forall a. Ord a => Empty scope a -> a
$cmaximum :: forall scope a. Ord a => Empty scope a -> a
elem :: forall a. Eq a => a -> Empty scope a -> Bool
$celem :: forall scope a. Eq a => a -> Empty scope a -> Bool
length :: forall a. Empty scope a -> Int
$clength :: forall scope a. Empty scope a -> Int
null :: forall a. Empty scope a -> Bool
$cnull :: forall scope a. Empty scope a -> Bool
toList :: forall a. Empty scope a -> [a]
$ctoList :: forall scope a. Empty scope a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Empty scope a -> a
$cfoldl1 :: forall scope a. (a -> a -> a) -> Empty scope a -> a
foldr1 :: forall a. (a -> a -> a) -> Empty scope a -> a
$cfoldr1 :: forall scope a. (a -> a -> a) -> Empty scope a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Empty scope a -> b
$cfoldl' :: forall scope b a. (b -> a -> b) -> b -> Empty scope a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Empty scope a -> b
$cfoldl :: forall scope b a. (b -> a -> b) -> b -> Empty scope a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Empty scope a -> b
$cfoldr' :: forall scope a b. (a -> b -> b) -> b -> Empty scope a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Empty scope a -> b
$cfoldr :: forall scope a b. (a -> b -> b) -> b -> Empty scope a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Empty scope a -> m
$cfoldMap' :: forall scope m a. Monoid m => (a -> m) -> Empty scope a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Empty scope a -> m
$cfoldMap :: forall scope m a. Monoid m => (a -> m) -> Empty scope a -> m
fold :: forall m. Monoid m => Empty scope m -> m
$cfold :: forall scope m. Monoid m => Empty scope m -> m
Foldable, forall scope. Functor (Empty scope)
forall scope. Foldable (Empty scope)
forall scope (m :: * -> *) a.
Monad m =>
Empty scope (m a) -> m (Empty scope a)
forall scope (f :: * -> *) a.
Applicative f =>
Empty scope (f a) -> f (Empty scope a)
forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Empty scope a -> m (Empty scope b)
forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Empty scope a -> f (Empty scope b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Empty scope a -> f (Empty scope b)
sequence :: forall (m :: * -> *) a.
Monad m =>
Empty scope (m a) -> m (Empty scope a)
$csequence :: forall scope (m :: * -> *) a.
Monad m =>
Empty scope (m a) -> m (Empty scope a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Empty scope a -> m (Empty scope b)
$cmapM :: forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Empty scope a -> m (Empty scope b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Empty scope (f a) -> f (Empty scope a)
$csequenceA :: forall scope (f :: * -> *) a.
Applicative f =>
Empty scope (f a) -> f (Empty scope a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Empty scope a -> f (Empty scope b)
$ctraverse :: forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Empty scope a -> f (Empty scope b)
Traversable)
deriveBifunctor ''Empty
deriveBifoldable ''Empty
deriveBitraversable ''Empty

data AnnF ann term scope typedTerm = AnnF
  { forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
AnnF ann term scope typedTerm -> ann typedTerm
annF  :: ann typedTerm
  , forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
AnnF ann term scope typedTerm -> term scope typedTerm
termF :: term scope typedTerm
  } deriving (Int -> AnnF ann term scope typedTerm -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
(Show (ann typedTerm), Show (term scope typedTerm)) =>
Int -> AnnF ann term scope typedTerm -> ShowS
forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
(Show (ann typedTerm), Show (term scope typedTerm)) =>
[AnnF ann term scope typedTerm] -> ShowS
forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
(Show (ann typedTerm), Show (term scope typedTerm)) =>
AnnF ann term scope typedTerm -> String
showList :: [AnnF ann term scope typedTerm] -> ShowS
$cshowList :: forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
(Show (ann typedTerm), Show (term scope typedTerm)) =>
[AnnF ann term scope typedTerm] -> ShowS
show :: AnnF ann term scope typedTerm -> String
$cshow :: forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
(Show (ann typedTerm), Show (term scope typedTerm)) =>
AnnF ann term scope typedTerm -> String
showsPrec :: Int -> AnnF ann term scope typedTerm -> ShowS
$cshowsPrec :: forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
(Show (ann typedTerm), Show (term scope typedTerm)) =>
Int -> AnnF ann term scope typedTerm -> ShowS
Show, forall a b. a -> AnnF ann term scope b -> AnnF ann term scope a
forall a b.
(a -> b) -> AnnF ann term scope a -> AnnF ann term scope b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (ann :: * -> *) (term :: * -> * -> *) scope a b.
(Functor ann, Functor (term scope)) =>
a -> AnnF ann term scope b -> AnnF ann term scope a
forall (ann :: * -> *) (term :: * -> * -> *) scope a b.
(Functor ann, Functor (term scope)) =>
(a -> b) -> AnnF ann term scope a -> AnnF ann term scope b
<$ :: forall a b. a -> AnnF ann term scope b -> AnnF ann term scope a
$c<$ :: forall (ann :: * -> *) (term :: * -> * -> *) scope a b.
(Functor ann, Functor (term scope)) =>
a -> AnnF ann term scope b -> AnnF ann term scope a
fmap :: forall a b.
(a -> b) -> AnnF ann term scope a -> AnnF ann term scope b
$cfmap :: forall (ann :: * -> *) (term :: * -> * -> *) scope a b.
(Functor ann, Functor (term scope)) =>
(a -> b) -> AnnF ann term scope a -> AnnF ann term scope b
Functor)

-- | Important: does not compare the `annF` component!
instance Eq (term scope typedTerm) => Eq (AnnF ann term scope typedTerm) where
  == :: AnnF ann term scope typedTerm
-> AnnF ann term scope typedTerm -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
AnnF ann term scope typedTerm -> term scope typedTerm
termF

instance (Functor ann, Bifunctor term) => Bifunctor (AnnF ann term) where
  bimap :: forall a b c d.
(a -> b) -> (c -> d) -> AnnF ann term a c -> AnnF ann term b d
bimap a -> b
f c -> d
g (AnnF ann c
t term a c
x) = forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> d
g ann c
t) (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f c -> d
g term a c
x)

-- | Important: does not fold over the 'annF' component!
instance Bifoldable term => Bifoldable (AnnF ann term) where
  bifoldMap :: forall m a b.
Monoid m =>
(a -> m) -> (b -> m) -> AnnF ann term a b -> m
bifoldMap a -> m
f b -> m
g (AnnF ann b
_ty term a b
x) = {- g ty <> -} forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap a -> m
f b -> m
g term a b
x

instance (Traversable ann, Bitraversable term) => Bitraversable (AnnF ann term) where
  bitraverse :: forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c)
-> (b -> f d) -> AnnF ann term a b -> f (AnnF ann term c d)
bitraverse a -> f c
f b -> f d
g (AnnF ann b
t term a b
x) = forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse b -> f d
g ann b
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse a -> f c
f b -> f d
g term a b
x

transFS
  :: (Bifunctor term)
  => (forall s t. term s t -> term' s t)
  -> FS term a -> FS term' a
transFS :: forall (term :: * -> * -> *) (term' :: * -> * -> *) a.
Bifunctor term =>
(forall s t. term s t -> term' s t) -> FS term a -> FS term' a
transFS forall s t. term s t -> term' s t
phi = \case
  Pure a
x -> forall (t :: * -> * -> *) a. a -> FS t a
Pure a
x
  Free term (Scope (FS term) a) (FS term a)
t -> forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free (forall s t. term s t -> term' s t
phi (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall (term :: * -> * -> *) (term' :: * -> * -> *) a.
Bifunctor term =>
(forall s t. term s t -> term' s t) -> FS term a -> FS term' a
transFS forall s t. term s t -> term' s t
phi) (forall (term :: * -> * -> *) (term' :: * -> * -> *) a.
Bifunctor term =>
(forall s t. term s t -> term' s t) -> FS term a -> FS term' a
transFS forall s t. term s t -> term' s t
phi) term (Scope (FS term) a) (FS term a)
t))

untyped :: (Functor ann, Bifunctor term) => FS (AnnF ann term) a -> FS term a
untyped :: forall (ann :: * -> *) (term :: * -> * -> *) a.
(Functor ann, Bifunctor term) =>
FS (AnnF ann term) a -> FS term a
untyped = forall (term :: * -> * -> *) (term' :: * -> * -> *) a.
Bifunctor term =>
(forall s t. term s t -> term' s t) -> FS term a -> FS term' a
transFS forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
AnnF ann term scope typedTerm -> term scope typedTerm
termF

pattern ExtE :: ext (Scope (FS (t :+: ext)) a) (FS (t :+: ext) a) -> FS (t :+: ext) a
pattern $bExtE :: forall (ext :: * -> * -> *) (t :: * -> * -> *) a.
ext (Scope (FS (t :+: ext)) a) (FS (t :+: ext) a)
-> FS (t :+: ext) a
$mExtE :: forall {r} {ext :: * -> * -> *} {t :: * -> * -> *} {a}.
FS (t :+: ext) a
-> (ext (Scope (FS (t :+: ext)) a) (FS (t :+: ext) a) -> r)
-> ((# #) -> r)
-> r
ExtE t = Free (InR t)

substitute :: Bifunctor t => FS t a -> Scope (FS t) a -> FS t a
substitute :: forall (t :: * -> * -> *) a.
Bifunctor t =>
FS t a -> Scope (FS t) a -> FS t a
substitute FS t a
t = (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Inc a -> FS t a
f)
  where
    f :: Inc a -> FS t a
f Inc a
Z     = FS t a
t
    f (S a
y) = forall (t :: * -> * -> *) a. a -> FS t a
Pure a
y