{-# 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
(Inc var -> Inc var -> Bool)
-> (Inc var -> Inc var -> Bool) -> Eq (Inc var)
forall var. Eq var => Inc var -> Inc var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Inc var -> Inc var -> Bool
Eq, Int -> Inc var -> ShowS
[Inc var] -> ShowS
Inc var -> String
(Int -> Inc var -> ShowS)
-> (Inc var -> String) -> ([Inc var] -> ShowS) -> Show (Inc var)
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
$cshowsPrec :: forall var. Show var => Int -> Inc var -> ShowS
showsPrec :: Int -> Inc var -> ShowS
$cshow :: forall var. Show var => Inc var -> String
show :: Inc var -> String
$cshowList :: forall var. Show var => [Inc var] -> ShowS
showList :: [Inc var] -> ShowS
Show, (forall a b. (a -> b) -> Inc a -> Inc b)
-> (forall a b. a -> Inc b -> Inc a) -> Functor Inc
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
$cfmap :: forall a b. (a -> b) -> Inc a -> Inc b
fmap :: forall a b. (a -> b) -> Inc a -> Inc b
$c<$ :: forall a b. a -> Inc b -> Inc a
<$ :: forall a b. a -> Inc b -> Inc a
Functor, (forall m. Monoid m => Inc m -> m)
-> (forall m a. Monoid m => (a -> m) -> Inc a -> m)
-> (forall m a. Monoid m => (a -> m) -> Inc a -> m)
-> (forall a b. (a -> b -> b) -> b -> Inc a -> b)
-> (forall a b. (a -> b -> b) -> b -> Inc a -> b)
-> (forall b a. (b -> a -> b) -> b -> Inc a -> b)
-> (forall b a. (b -> a -> b) -> b -> Inc a -> b)
-> (forall a. (a -> a -> a) -> Inc a -> a)
-> (forall a. (a -> a -> a) -> Inc a -> a)
-> (forall a. Inc a -> [a])
-> (forall a. Inc a -> Bool)
-> (forall a. Inc a -> Int)
-> (forall a. Eq a => a -> Inc a -> Bool)
-> (forall a. Ord a => Inc a -> a)
-> (forall a. Ord a => Inc a -> a)
-> (forall a. Num a => Inc a -> a)
-> (forall a. Num a => Inc a -> a)
-> Foldable Inc
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
$cfold :: forall m. Monoid m => Inc m -> m
fold :: forall m. Monoid m => Inc m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Inc a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Inc a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Inc a -> a
foldr1 :: forall a. (a -> a -> a) -> Inc a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Inc a -> a
foldl1 :: forall a. (a -> a -> a) -> Inc a -> a
$ctoList :: forall a. Inc a -> [a]
toList :: forall a. Inc a -> [a]
$cnull :: forall a. Inc a -> Bool
null :: forall a. Inc a -> Bool
$clength :: forall a. Inc a -> Int
length :: forall a. Inc a -> Int
$celem :: forall a. Eq a => a -> Inc a -> Bool
elem :: forall a. Eq a => a -> Inc a -> Bool
$cmaximum :: forall a. Ord a => Inc a -> a
maximum :: forall a. Ord a => Inc a -> a
$cminimum :: forall a. Ord a => Inc a -> a
minimum :: forall a. Ord a => Inc a -> a
$csum :: forall a. Num a => Inc a -> a
sum :: forall a. Num a => Inc a -> a
$cproduct :: forall a. Num a => Inc a -> a
product :: forall a. Num a => Inc a -> a
Foldable, Functor Inc
Foldable Inc
(Functor Inc, Foldable Inc) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Inc a -> f (Inc b))
-> (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 (m :: * -> *) a. Monad m => Inc (m a) -> m (Inc a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Inc a -> f (Inc b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Inc a -> f (Inc b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Inc (f a) -> f (Inc a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Inc (f a) -> f (Inc a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Inc a -> m (Inc b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Inc a -> m (Inc b)
$csequence :: forall (m :: * -> *) a. Monad m => Inc (m a) -> m (Inc a)
sequence :: forall (m :: * -> *) a. Monad m => Inc (m a) -> m (Inc a)
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 f (Inc a) -> (Inc a -> f a) -> f a
forall a b. f a -> (a -> f b) -> f b
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) = a -> f a
forall a. a -> f a
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 (a -> Inc a) -> f a -> f (Inc a)
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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y    = Inc a
forall var. Inc var
Z
        | Bool
otherwise = a -> Inc a
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) = b -> FS t b
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) = t (Scope (FS t) b) (FS t b) -> FS t b
forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free
    ((Scope (FS t) a -> Scope (FS t) b)
-> (FS t a -> FS t b)
-> t (Scope (FS t) a) (FS t a)
-> t (Scope (FS t) b) (FS t b)
forall a b c d. (a -> b) -> (c -> d) -> t a c -> t b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((Inc a -> Inc b) -> Scope (FS t) a -> Scope (FS t) b
forall a b. (a -> b) -> FS t a -> FS t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> Inc a -> Inc b
forall a b. (a -> b) -> Inc a -> Inc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) ((a -> b) -> FS t a -> FS t b
forall a b. (a -> b) -> FS t a -> FS t b
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) = (Scope (FS t) a -> m)
-> (FS t a -> m) -> t (Scope (FS t) a) (FS t a) -> m
forall m a b. Monoid m => (a -> m) -> (b -> m) -> t a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap ((Inc a -> m) -> Scope (FS t) a -> m
forall m a. Monoid m => (a -> m) -> FS t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> Inc a -> m
forall m a. Monoid m => (a -> m) -> Inc a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f)) ((a -> m) -> FS t a -> m
forall m a. Monoid m => (a -> m) -> FS t a -> m
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) = b -> FS t b
forall (t :: * -> * -> *) a. a -> FS t a
Pure (b -> FS t b) -> f b -> f (FS t b)
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) = t (Scope (FS t) b) (FS t b) -> FS t b
forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free (t (Scope (FS t) b) (FS t b) -> FS t b)
-> f (t (Scope (FS t) b) (FS t b)) -> f (FS t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    (Scope (FS t) a -> f (Scope (FS t) b))
-> (FS t a -> f (FS t b))
-> t (Scope (FS t) a) (FS t a)
-> f (t (Scope (FS t) b) (FS t b))
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
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 ((Inc a -> f (Inc b)) -> Scope (FS t) a -> f (Scope (FS t) b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FS t a -> f (FS t b)
traverse ((a -> f b) -> Inc a -> f (Inc b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Inc a -> f (Inc b)
traverse a -> f b
f)) ((a -> f b) -> FS t a -> f (FS t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FS t a -> f (FS 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 = a -> FS t a
forall (t :: * -> * -> *) a. a -> FS t a
Pure
  <*> :: forall a b. FS t (a -> b) -> FS t a -> FS t 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 = a -> FS t a
forall a. a -> FS t a
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 = t (Scope (FS t) b) (FS t b) -> FS t b
forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free
    ((Scope (FS t) a -> Scope (FS t) b)
-> (FS t a -> FS t b)
-> t (Scope (FS t) a) (FS t a)
-> t (Scope (FS t) b) (FS t b)
forall a b c d. (a -> b) -> (c -> d) -> t a c -> t b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((Scope (FS t) a -> (Inc a -> Scope (FS t) b) -> Scope (FS t) b
forall a b. FS t a -> (a -> FS t b) -> FS t b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a -> FS t b) -> Inc a -> Scope (FS t) b
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Inc a -> f (Inc b)
traverse a -> FS t b
f)) (FS t a -> (a -> FS t b) -> FS t b
forall a b. FS t a -> (a -> FS t b) -> FS t b
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 -> 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)
-> Functor (Sum f g scope)
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
$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
fmap :: forall a b. (a -> b) -> Sum f g scope a -> Sum f g scope b
$c<$ :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a b.
(Functor (f scope), Functor (g scope)) =>
a -> Sum f g scope b -> Sum f g scope a
<$ :: forall a b. a -> Sum f g scope b -> Sum f g scope a
Functor, (forall m. Monoid m => Sum f g scope m -> m)
-> (forall m a. Monoid m => (a -> m) -> Sum f g scope a -> m)
-> (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 a b. (a -> b -> b) -> b -> Sum f g scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> Sum f g scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> Sum f g scope a -> b)
-> (forall a. (a -> a -> a) -> Sum f g scope a -> a)
-> (forall a. (a -> a -> a) -> Sum f g scope a -> a)
-> (forall a. Sum f g scope a -> [a])
-> (forall a. Sum f g scope a -> Bool)
-> (forall a. Sum f g scope a -> Int)
-> (forall a. Eq a => a -> Sum f g scope a -> Bool)
-> (forall a. Ord a => Sum f g scope a -> a)
-> (forall a. Ord a => Sum f g scope a -> a)
-> (forall a. Num a => Sum f g scope a -> a)
-> (forall a. Num a => Sum f g scope a -> a)
-> Foldable (Sum f g scope)
forall a. Eq a => a -> Sum f g scope a -> Bool
forall a. Num a => Sum f g scope a -> a
forall a. Ord a => Sum f g scope a -> a
forall m. Monoid m => Sum f g scope m -> m
forall a. Sum f g scope a -> Bool
forall a. Sum f g scope a -> Int
forall a. Sum f g scope a -> [a]
forall a. (a -> a -> a) -> Sum f g scope a -> a
forall m a. Monoid m => (a -> m) -> Sum f g scope a -> m
forall b a. (b -> a -> b) -> b -> Sum f g scope a -> b
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
$cfold :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope m.
(Foldable (f scope), Foldable (g scope), Monoid m) =>
Sum f g scope m -> m
fold :: forall m. Monoid m => Sum f g scope m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Sum f g scope a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Sum f g scope a -> b
$cfoldr1 :: 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
$cfoldl1 :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
(a -> a -> a) -> Sum f g scope a -> a
foldl1 :: forall a. (a -> a -> 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]
toList :: forall a. Sum f g scope a -> [a]
$cnull :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
Sum f g scope a -> Bool
null :: forall a. Sum f g scope a -> Bool
$clength :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope)) =>
Sum f g scope a -> Int
length :: forall a. Sum f g scope a -> Int
$celem :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope), Eq a) =>
a -> Sum f g scope a -> Bool
elem :: forall a. Eq a => a -> Sum f g scope a -> Bool
$cmaximum :: 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
$cminimum :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope a.
(Foldable (f scope), Foldable (g scope), Ord a) =>
Sum f g scope a -> a
minimum :: forall a. Ord 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
sum :: 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
product :: forall a. Num a => Sum f g scope a -> a
Foldable, Functor (Sum f g scope)
Foldable (Sum f g scope)
(Functor (Sum f g scope), Foldable (Sum f g scope)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Sum f g scope a -> f (Sum f g scope b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Sum f g scope (f a) -> f (Sum f g scope a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Sum f g scope a -> m (Sum f g scope b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Sum f g scope (m a) -> m (Sum f g scope a))
-> Traversable (Sum f g scope)
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 =>
Sum f g scope (m a) -> m (Sum f g scope a)
forall (f :: * -> *) a.
Applicative f =>
Sum f g scope (f a) -> f (Sum f g scope a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Sum f g scope a -> m (Sum f g scope b)
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)
$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)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Sum f g scope a -> f (Sum f g scope b)
$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)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Sum f g scope (f a) -> f (Sum f g scope a)
$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)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Sum f g scope a -> m (Sum f g scope b)
$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)
sequence :: forall (m :: * -> *) a.
Monad m =>
Sum f g scope (m a) -> m (Sum f g scope a)
Traversable, (forall x. Sum f g scope term -> Rep (Sum f g scope term) x)
-> (forall x. Rep (Sum f g scope term) x -> Sum f g scope term)
-> Generic (Sum f g scope term)
forall x. Rep (Sum f g scope term) x -> Sum f g scope term
forall x. Sum f g scope term -> Rep (Sum f g scope term) x
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
$cfrom :: forall (f :: * -> * -> *) (g :: * -> * -> *) scope term x.
Sum f g scope term -> Rep (Sum f g scope term) x
from :: forall 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
to :: forall x. Rep (Sum f g scope term) x -> Sum f g scope term
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 a b. a -> Empty scope b -> Empty scope a)
-> Functor (Empty scope)
forall a b. a -> Empty scope b -> Empty scope a
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
$cfmap :: forall scope a b. (a -> b) -> Empty scope a -> Empty scope b
fmap :: forall a b. (a -> b) -> Empty scope a -> Empty scope b
$c<$ :: forall scope a b. a -> Empty scope b -> Empty scope a
<$ :: forall a b. a -> Empty scope b -> Empty scope a
Functor, (forall m. Monoid m => Empty scope m -> m)
-> (forall m a. Monoid m => (a -> m) -> Empty scope a -> m)
-> (forall m a. Monoid m => (a -> m) -> Empty scope a -> m)
-> (forall a b. (a -> b -> b) -> b -> Empty scope a -> b)
-> (forall a b. (a -> b -> b) -> b -> Empty scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> Empty scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> Empty scope a -> b)
-> (forall a. (a -> a -> a) -> Empty scope a -> a)
-> (forall a. (a -> a -> a) -> Empty scope a -> a)
-> (forall a. Empty scope a -> [a])
-> (forall a. Empty scope a -> Bool)
-> (forall a. Empty scope a -> Int)
-> (forall a. Eq a => a -> Empty scope a -> Bool)
-> (forall a. Ord a => Empty scope a -> a)
-> (forall a. Ord a => Empty scope a -> a)
-> (forall a. Num a => Empty scope a -> a)
-> (forall a. Num a => Empty scope a -> a)
-> Foldable (Empty scope)
forall a. Eq a => a -> Empty scope a -> Bool
forall a. Num a => Empty scope a -> a
forall a. Ord a => Empty scope a -> a
forall m. Monoid m => Empty scope m -> m
forall a. Empty scope a -> Bool
forall a. Empty scope a -> Int
forall a. Empty scope a -> [a]
forall a. (a -> a -> a) -> Empty scope a -> a
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 scope m. Monoid m => Empty scope m -> m
forall m a. Monoid m => (a -> m) -> Empty scope a -> m
forall scope a. Empty scope a -> Bool
forall scope a. Empty scope a -> Int
forall scope a. Empty scope a -> [a]
forall b a. (b -> a -> b) -> b -> Empty scope a -> b
forall a b. (a -> b -> b) -> b -> Empty scope a -> b
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
$cfold :: forall scope m. Monoid m => Empty scope m -> m
fold :: forall m. Monoid m => Empty scope m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Empty scope a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Empty scope a -> b
$cfoldr1 :: forall scope a. (a -> a -> a) -> Empty scope a -> a
foldr1 :: forall a. (a -> a -> a) -> Empty scope a -> a
$cfoldl1 :: forall scope a. (a -> a -> a) -> Empty scope a -> a
foldl1 :: forall a. (a -> a -> a) -> Empty scope a -> a
$ctoList :: forall scope a. Empty scope a -> [a]
toList :: forall a. Empty scope a -> [a]
$cnull :: forall scope a. Empty scope a -> Bool
null :: forall a. Empty scope a -> Bool
$clength :: forall scope a. Empty scope a -> Int
length :: forall a. Empty scope a -> Int
$celem :: forall scope a. Eq a => a -> Empty scope a -> Bool
elem :: forall a. Eq a => a -> Empty scope a -> Bool
$cmaximum :: forall scope a. Ord a => Empty scope a -> a
maximum :: forall a. Ord a => Empty scope a -> a
$cminimum :: forall scope a. Ord a => Empty scope a -> a
minimum :: forall a. Ord a => Empty scope a -> a
$csum :: forall scope a. Num a => Empty scope a -> a
sum :: forall a. Num a => Empty scope a -> a
$cproduct :: forall scope a. Num a => Empty scope a -> a
product :: forall a. Num a => Empty scope a -> a
Foldable, Functor (Empty scope)
Foldable (Empty scope)
(Functor (Empty scope), Foldable (Empty scope)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Empty scope a -> f (Empty scope b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Empty scope (f a) -> f (Empty scope a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Empty scope a -> m (Empty scope b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Empty scope (m a) -> m (Empty scope a))
-> Traversable (Empty scope)
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 (m :: * -> *) a.
Monad m =>
Empty scope (m a) -> m (Empty scope a)
forall (f :: * -> *) a.
Applicative f =>
Empty scope (f a) -> f (Empty scope a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Empty scope a -> m (Empty scope b)
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)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Empty scope a -> f (Empty scope b)
$csequenceA :: forall scope (f :: * -> *) a.
Applicative f =>
Empty scope (f a) -> f (Empty scope a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Empty scope (f a) -> f (Empty scope a)
$cmapM :: forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Empty scope a -> m (Empty scope b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Empty scope a -> m (Empty scope b)
$csequence :: forall scope (m :: * -> *) a.
Monad m =>
Empty scope (m a) -> m (Empty scope a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Empty scope (m a) -> m (Empty scope a)
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
[AnnF ann term scope typedTerm] -> ShowS
AnnF ann term scope typedTerm -> String
(Int -> AnnF ann term scope typedTerm -> ShowS)
-> (AnnF ann term scope typedTerm -> String)
-> ([AnnF ann term scope typedTerm] -> ShowS)
-> Show (AnnF ann term scope typedTerm)
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
$cshowsPrec :: forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
(Show (ann typedTerm), Show (term scope typedTerm)) =>
Int -> AnnF ann term scope typedTerm -> ShowS
showsPrec :: Int -> AnnF ann term scope typedTerm -> ShowS
$cshow :: forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
(Show (ann typedTerm), Show (term scope typedTerm)) =>
AnnF ann term scope typedTerm -> String
show :: AnnF ann term scope typedTerm -> String
$cshowList :: forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
(Show (ann typedTerm), Show (term scope typedTerm)) =>
[AnnF ann term scope typedTerm] -> ShowS
showList :: [AnnF ann term scope typedTerm] -> ShowS
Show, (forall a b.
 (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)
-> Functor (AnnF ann term scope)
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
$cfmap :: forall (ann :: * -> *) (term :: * -> * -> *) scope a b.
(Functor ann, Functor (term scope)) =>
(a -> b) -> AnnF ann term scope a -> AnnF ann term scope b
fmap :: forall a b.
(a -> b) -> AnnF ann term scope a -> AnnF ann term scope b
$c<$ :: forall (ann :: * -> *) (term :: * -> * -> *) scope a b.
(Functor ann, Functor (term scope)) =>
a -> AnnF ann term scope b -> AnnF ann term scope a
<$ :: forall a b. a -> AnnF ann term scope b -> AnnF ann term scope a
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
(==) = term scope typedTerm -> term scope typedTerm -> Bool
forall a. Eq a => a -> a -> Bool
(==) (term scope typedTerm -> term scope typedTerm -> Bool)
-> (AnnF ann term scope typedTerm -> term scope typedTerm)
-> AnnF ann term scope typedTerm
-> AnnF ann term scope typedTerm
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` AnnF ann term scope typedTerm -> term scope typedTerm
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) = ann d -> term b d -> AnnF ann term b d
forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF ((c -> d) -> ann c -> ann d
forall a b. (a -> b) -> ann a -> ann b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> d
g ann c
t) ((a -> b) -> (c -> d) -> term a c -> term b d
forall a b c d. (a -> b) -> (c -> d) -> term a c -> term b d
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 <> -} (a -> m) -> (b -> m) -> term a b -> m
forall m a b. Monoid m => (a -> m) -> (b -> m) -> term a b -> m
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) = ann d -> term c d -> AnnF ann term c d
forall (ann :: * -> *) (term :: * -> * -> *) scope typedTerm.
ann typedTerm
-> term scope typedTerm -> AnnF ann term scope typedTerm
AnnF (ann d -> term c d -> AnnF ann term c d)
-> f (ann d) -> f (term c d -> AnnF ann term c d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (b -> f d) -> ann b -> f (ann d)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ann a -> f (ann b)
traverse b -> f d
g ann b
t f (term c d -> AnnF ann term c d)
-> f (term c d) -> f (AnnF ann term c d)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f c) -> (b -> f d) -> term a b -> f (term c d)
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> term a b -> f (term c d)
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 -> a -> FS term' a
forall (t :: * -> * -> *) a. a -> FS t a
Pure a
x
  Free term (Scope (FS term) a) (FS term a)
t -> term' (Scope (FS term') a) (FS term' a) -> FS term' a
forall (t :: * -> * -> *) a. t (Scope (FS t) a) (FS t a) -> FS t a
Free (term (Scope (FS term') a) (FS term' a)
-> term' (Scope (FS term') a) (FS term' a)
forall s t. term s t -> term' s t
phi ((Scope (FS term) a -> Scope (FS term') a)
-> (FS term a -> FS term' a)
-> term (Scope (FS term) a) (FS term a)
-> term (Scope (FS term') a) (FS term' a)
forall a b c d. (a -> b) -> (c -> d) -> term a c -> term b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((forall s t. term s t -> term' s t)
-> Scope (FS term) a -> Scope (FS term') a
forall (term :: * -> * -> *) (term' :: * -> * -> *) a.
Bifunctor term =>
(forall s t. term s t -> term' s t) -> FS term a -> FS term' a
transFS term s t -> term' s t
forall s t. term s t -> term' s t
phi) ((forall s t. term s t -> term' s t) -> FS term a -> FS term' a
forall (term :: * -> * -> *) (term' :: * -> * -> *) a.
Bifunctor term =>
(forall s t. term s t -> term' s t) -> FS term a -> FS term' a
transFS term s t -> term' s t
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 s t. AnnF ann term s t -> term s t)
-> FS (AnnF ann term) a -> FS term a
forall (term :: * -> * -> *) (term' :: * -> * -> *) a.
Bifunctor term =>
(forall s t. term s t -> term' s t) -> FS term a -> FS term' a
transFS AnnF ann term s t -> term s t
forall s t. AnnF ann term s t -> term s t
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 $mExtE :: forall {r} {ext :: * -> * -> *} {t :: * -> * -> *} {a}.
FS (t :+: ext) a
-> (ext (Scope (FS (t :+: ext)) a) (FS (t :+: ext) a) -> r)
-> ((# #) -> r)
-> r
$bExtE :: forall (ext :: * -> * -> *) (t :: * -> * -> *) a.
ext (Scope (FS (t :+: ext)) a) (FS (t :+: ext) a)
-> FS (t :+: ext) a
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 = (FS t (Inc a) -> (Inc a -> FS t a) -> FS t a
forall a b. FS t a -> (a -> FS t b) -> FS t b
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) = a -> FS t a
forall (t :: * -> * -> *) a. a -> FS t a
Pure a
y