{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DerivingStrategies #-}
{-# language DeriveAnyClass #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# language CPP #-}
{-# options_ghc -Wno-unused-top-binds #-}
module Bound.Simple (Bound(..)
, Scope, toScope, fromScope
, Var
, abstract, abstract1
, instantiate, instantiate1
, bindings
, hoistScope
, closed
, substitute
, substituteVar
, isClosed
, Generically(..)
) where
import Control.Monad (ap, liftM)
import Control.Monad.Trans.Class (MonadTrans(..))
import Data.Functor.Classes (Show2(..), Show1(..), showsUnaryWith, showsPrec1, liftShowsPrec2, Eq2(..), Eq1(..), eq1, liftEq, liftEq2)
import GHC.Generics (Generic1)
import Data.Functor.Classes.Generic (Generically(..))
infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
deriving (Int -> Exp a -> ShowS
[Exp a] -> ShowS
Exp a -> String
(Int -> Exp a -> ShowS)
-> (Exp a -> String) -> ([Exp a] -> ShowS) -> Show (Exp a)
forall a. Show a => Int -> Exp a -> ShowS
forall a. Show a => [Exp a] -> ShowS
forall a. Show a => Exp a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Exp a] -> ShowS
$cshowList :: forall a. Show a => [Exp a] -> ShowS
show :: Exp a -> String
$cshow :: forall a. Show a => Exp a -> String
showsPrec :: Int -> Exp a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Exp a -> ShowS
Show, Exp a -> Exp a -> Bool
(Exp a -> Exp a -> Bool) -> (Exp a -> Exp a -> Bool) -> Eq (Exp a)
forall a. Eq a => Exp a -> Exp a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Exp a -> Exp a -> Bool
$c/= :: forall a. Eq a => Exp a -> Exp a -> Bool
== :: Exp a -> Exp a -> Bool
$c== :: forall a. Eq a => Exp a -> Exp a -> Bool
Eq, a -> Exp b -> Exp a
(a -> b) -> Exp a -> Exp b
(forall a b. (a -> b) -> Exp a -> Exp b)
-> (forall a b. a -> Exp b -> Exp a) -> Functor Exp
forall a b. a -> Exp b -> Exp a
forall a b. (a -> b) -> Exp a -> Exp b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Exp b -> Exp a
$c<$ :: forall a b. a -> Exp b -> Exp a
fmap :: (a -> b) -> Exp a -> Exp b
$cfmap :: forall a b. (a -> b) -> Exp a -> Exp b
Functor,Exp a -> Bool
(a -> m) -> Exp a -> m
(a -> b -> b) -> b -> Exp a -> b
(forall m. Monoid m => Exp m -> m)
-> (forall m a. Monoid m => (a -> m) -> Exp a -> m)
-> (forall m a. Monoid m => (a -> m) -> Exp a -> m)
-> (forall a b. (a -> b -> b) -> b -> Exp a -> b)
-> (forall a b. (a -> b -> b) -> b -> Exp a -> b)
-> (forall b a. (b -> a -> b) -> b -> Exp a -> b)
-> (forall b a. (b -> a -> b) -> b -> Exp a -> b)
-> (forall a. (a -> a -> a) -> Exp a -> a)
-> (forall a. (a -> a -> a) -> Exp a -> a)
-> (forall a. Exp a -> [a])
-> (forall a. Exp a -> Bool)
-> (forall a. Exp a -> Int)
-> (forall a. Eq a => a -> Exp a -> Bool)
-> (forall a. Ord a => Exp a -> a)
-> (forall a. Ord a => Exp a -> a)
-> (forall a. Num a => Exp a -> a)
-> (forall a. Num a => Exp a -> a)
-> Foldable Exp
forall a. Eq a => a -> Exp a -> Bool
forall a. Num a => Exp a -> a
forall a. Ord a => Exp a -> a
forall m. Monoid m => Exp m -> m
forall a. Exp a -> Bool
forall a. Exp a -> Int
forall a. Exp a -> [a]
forall a. (a -> a -> a) -> Exp a -> a
forall m a. Monoid m => (a -> m) -> Exp a -> m
forall b a. (b -> a -> b) -> b -> Exp a -> b
forall a b. (a -> b -> b) -> b -> Exp 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 :: Exp a -> a
$cproduct :: forall a. Num a => Exp a -> a
sum :: Exp a -> a
$csum :: forall a. Num a => Exp a -> a
minimum :: Exp a -> a
$cminimum :: forall a. Ord a => Exp a -> a
maximum :: Exp a -> a
$cmaximum :: forall a. Ord a => Exp a -> a
elem :: a -> Exp a -> Bool
$celem :: forall a. Eq a => a -> Exp a -> Bool
length :: Exp a -> Int
$clength :: forall a. Exp a -> Int
null :: Exp a -> Bool
$cnull :: forall a. Exp a -> Bool
toList :: Exp a -> [a]
$ctoList :: forall a. Exp a -> [a]
foldl1 :: (a -> a -> a) -> Exp a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Exp a -> a
foldr1 :: (a -> a -> a) -> Exp a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Exp a -> a
foldl' :: (b -> a -> b) -> b -> Exp a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Exp a -> b
foldl :: (b -> a -> b) -> b -> Exp a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Exp a -> b
foldr' :: (a -> b -> b) -> b -> Exp a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Exp a -> b
foldr :: (a -> b -> b) -> b -> Exp a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Exp a -> b
foldMap' :: (a -> m) -> Exp a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Exp a -> m
foldMap :: (a -> m) -> Exp a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Exp a -> m
fold :: Exp m -> m
$cfold :: forall m. Monoid m => Exp m -> m
Foldable,Functor Exp
Foldable Exp
Functor Exp
-> Foldable Exp
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Exp a -> f (Exp b))
-> (forall (f :: * -> *) a.
Applicative f =>
Exp (f a) -> f (Exp a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Exp a -> m (Exp b))
-> (forall (m :: * -> *) a. Monad m => Exp (m a) -> m (Exp a))
-> Traversable Exp
(a -> f b) -> Exp a -> f (Exp 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 => Exp (m a) -> m (Exp a)
forall (f :: * -> *) a. Applicative f => Exp (f a) -> f (Exp a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Exp a -> m (Exp b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Exp a -> f (Exp b)
sequence :: Exp (m a) -> m (Exp a)
$csequence :: forall (m :: * -> *) a. Monad m => Exp (m a) -> m (Exp a)
mapM :: (a -> m b) -> Exp a -> m (Exp b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Exp a -> m (Exp b)
sequenceA :: Exp (f a) -> f (Exp a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Exp (f a) -> f (Exp a)
traverse :: (a -> f b) -> Exp a -> f (Exp b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Exp a -> f (Exp b)
$cp2Traversable :: Foldable Exp
$cp1Traversable :: Functor Exp
Traversable, (forall a. Exp a -> Rep1 Exp a)
-> (forall a. Rep1 Exp a -> Exp a) -> Generic1 Exp
forall a. Rep1 Exp a -> Exp a
forall a. Exp a -> Rep1 Exp a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall a. Rep1 Exp a -> Exp a
$cfrom1 :: forall a. Exp a -> Rep1 Exp a
Generic1)
deriving ((Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Exp a -> ShowS
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Exp a] -> ShowS
(forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Exp a -> ShowS)
-> (forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Exp a] -> ShowS)
-> Show1 Exp
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Exp a -> ShowS
forall a. (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Exp a] -> ShowS
forall (f :: * -> *).
(forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS)
-> (forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS)
-> Show1 f
liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Exp a] -> ShowS
$cliftShowList :: forall a. (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Exp a] -> ShowS
liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Exp a -> ShowS
$cliftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Exp a -> ShowS
Show1, (a -> b -> Bool) -> Exp a -> Exp b -> Bool
(forall a b. (a -> b -> Bool) -> Exp a -> Exp b -> Bool) -> Eq1 Exp
forall a b. (a -> b -> Bool) -> Exp a -> Exp b -> Bool
forall (f :: * -> *).
(forall a b. (a -> b -> Bool) -> f a -> f b -> Bool) -> Eq1 f
liftEq :: (a -> b -> Bool) -> Exp a -> Exp b -> Bool
$cliftEq :: forall a b. (a -> b -> Bool) -> Exp a -> Exp b -> Bool
Eq1) via Generically Exp
data Var b a = B b
| F a
deriving (Var b a -> Var b a -> Bool
(Var b a -> Var b a -> Bool)
-> (Var b a -> Var b a -> Bool) -> Eq (Var b a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall b a. (Eq b, Eq a) => Var b a -> Var b a -> Bool
/= :: Var b a -> Var b a -> Bool
$c/= :: forall b a. (Eq b, Eq a) => Var b a -> Var b a -> Bool
== :: Var b a -> Var b a -> Bool
$c== :: forall b a. (Eq b, Eq a) => Var b a -> Var b a -> Bool
Eq, Int -> Var b a -> ShowS
[Var b a] -> ShowS
Var b a -> String
(Int -> Var b a -> ShowS)
-> (Var b a -> String) -> ([Var b a] -> ShowS) -> Show (Var b a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall b a. (Show b, Show a) => Int -> Var b a -> ShowS
forall b a. (Show b, Show a) => [Var b a] -> ShowS
forall b a. (Show b, Show a) => Var b a -> String
showList :: [Var b a] -> ShowS
$cshowList :: forall b a. (Show b, Show a) => [Var b a] -> ShowS
show :: Var b a -> String
$cshow :: forall b a. (Show b, Show a) => Var b a -> String
showsPrec :: Int -> Var b a -> ShowS
$cshowsPrec :: forall b a. (Show b, Show a) => Int -> Var b a -> ShowS
Show, a -> Var b b -> Var b a
(a -> b) -> Var b a -> Var b b
(forall a b. (a -> b) -> Var b a -> Var b b)
-> (forall a b. a -> Var b b -> Var b a) -> Functor (Var b)
forall a b. a -> Var b b -> Var b a
forall a b. (a -> b) -> Var b a -> Var b b
forall b a b. a -> Var b b -> Var b a
forall b a b. (a -> b) -> Var b a -> Var b b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Var b b -> Var b a
$c<$ :: forall b a b. a -> Var b b -> Var b a
fmap :: (a -> b) -> Var b a -> Var b b
$cfmap :: forall b a b. (a -> b) -> Var b a -> Var b b
Functor, Var b a -> Bool
(a -> m) -> Var b a -> m
(a -> b -> b) -> b -> Var b a -> b
(forall m. Monoid m => Var b m -> m)
-> (forall m a. Monoid m => (a -> m) -> Var b a -> m)
-> (forall m a. Monoid m => (a -> m) -> Var b a -> m)
-> (forall a b. (a -> b -> b) -> b -> Var b a -> b)
-> (forall a b. (a -> b -> b) -> b -> Var b a -> b)
-> (forall b a. (b -> a -> b) -> b -> Var b a -> b)
-> (forall b a. (b -> a -> b) -> b -> Var b a -> b)
-> (forall a. (a -> a -> a) -> Var b a -> a)
-> (forall a. (a -> a -> a) -> Var b a -> a)
-> (forall a. Var b a -> [a])
-> (forall a. Var b a -> Bool)
-> (forall a. Var b a -> Int)
-> (forall a. Eq a => a -> Var b a -> Bool)
-> (forall a. Ord a => Var b a -> a)
-> (forall a. Ord a => Var b a -> a)
-> (forall a. Num a => Var b a -> a)
-> (forall a. Num a => Var b a -> a)
-> Foldable (Var b)
forall a. Eq a => a -> Var b a -> Bool
forall a. Num a => Var b a -> a
forall a. Ord a => Var b a -> a
forall m. Monoid m => Var b m -> m
forall a. Var b a -> Bool
forall a. Var b a -> Int
forall a. Var b a -> [a]
forall a. (a -> a -> a) -> Var b a -> a
forall b a. Eq a => a -> Var b a -> Bool
forall b a. Num a => Var b a -> a
forall b a. Ord a => Var b a -> a
forall m a. Monoid m => (a -> m) -> Var b a -> m
forall b m. Monoid m => Var b m -> m
forall b a. Var b a -> Bool
forall b a. Var b a -> Int
forall b a. Var b a -> [a]
forall b a. (b -> a -> b) -> b -> Var b a -> b
forall a b. (a -> b -> b) -> b -> Var b a -> b
forall b a. (a -> a -> a) -> Var b a -> a
forall b m a. Monoid m => (a -> m) -> Var b a -> m
forall b b a. (b -> a -> b) -> b -> Var b a -> b
forall b a b. (a -> b -> b) -> b -> Var b 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 :: Var b a -> a
$cproduct :: forall b a. Num a => Var b a -> a
sum :: Var b a -> a
$csum :: forall b a. Num a => Var b a -> a
minimum :: Var b a -> a
$cminimum :: forall b a. Ord a => Var b a -> a
maximum :: Var b a -> a
$cmaximum :: forall b a. Ord a => Var b a -> a
elem :: a -> Var b a -> Bool
$celem :: forall b a. Eq a => a -> Var b a -> Bool
length :: Var b a -> Int
$clength :: forall b a. Var b a -> Int
null :: Var b a -> Bool
$cnull :: forall b a. Var b a -> Bool
toList :: Var b a -> [a]
$ctoList :: forall b a. Var b a -> [a]
foldl1 :: (a -> a -> a) -> Var b a -> a
$cfoldl1 :: forall b a. (a -> a -> a) -> Var b a -> a
foldr1 :: (a -> a -> a) -> Var b a -> a
$cfoldr1 :: forall b a. (a -> a -> a) -> Var b a -> a
foldl' :: (b -> a -> b) -> b -> Var b a -> b
$cfoldl' :: forall b b a. (b -> a -> b) -> b -> Var b a -> b
foldl :: (b -> a -> b) -> b -> Var b a -> b
$cfoldl :: forall b b a. (b -> a -> b) -> b -> Var b a -> b
foldr' :: (a -> b -> b) -> b -> Var b a -> b
$cfoldr' :: forall b a b. (a -> b -> b) -> b -> Var b a -> b
foldr :: (a -> b -> b) -> b -> Var b a -> b
$cfoldr :: forall b a b. (a -> b -> b) -> b -> Var b a -> b
foldMap' :: (a -> m) -> Var b a -> m
$cfoldMap' :: forall b m a. Monoid m => (a -> m) -> Var b a -> m
foldMap :: (a -> m) -> Var b a -> m
$cfoldMap :: forall b m a. Monoid m => (a -> m) -> Var b a -> m
fold :: Var b m -> m
$cfold :: forall b m. Monoid m => Var b m -> m
Foldable, Functor (Var b)
Foldable (Var b)
Functor (Var b)
-> Foldable (Var b)
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Var b a -> f (Var b b))
-> (forall (f :: * -> *) a.
Applicative f =>
Var b (f a) -> f (Var b a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Var b a -> m (Var b b))
-> (forall (m :: * -> *) a. Monad m => Var b (m a) -> m (Var b a))
-> Traversable (Var b)
(a -> f b) -> Var b a -> f (Var b b)
forall b. Functor (Var b)
forall b. Foldable (Var b)
forall b (m :: * -> *) a. Monad m => Var b (m a) -> m (Var b a)
forall b (f :: * -> *) a.
Applicative f =>
Var b (f a) -> f (Var b a)
forall b (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Var b a -> m (Var b b)
forall b (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Var b a -> f (Var b 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 => Var b (m a) -> m (Var b a)
forall (f :: * -> *) a. Applicative f => Var b (f a) -> f (Var b a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Var b a -> m (Var b b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Var b a -> f (Var b b)
sequence :: Var b (m a) -> m (Var b a)
$csequence :: forall b (m :: * -> *) a. Monad m => Var b (m a) -> m (Var b a)
mapM :: (a -> m b) -> Var b a -> m (Var b b)
$cmapM :: forall b (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Var b a -> m (Var b b)
sequenceA :: Var b (f a) -> f (Var b a)
$csequenceA :: forall b (f :: * -> *) a.
Applicative f =>
Var b (f a) -> f (Var b a)
traverse :: (a -> f b) -> Var b a -> f (Var b b)
$ctraverse :: forall b (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Var b a -> f (Var b b)
$cp2Traversable :: forall b. Foldable (Var b)
$cp1Traversable :: forall b. Functor (Var b)
Traversable)
instance Eq2 Var where
liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Var a c -> Var b d -> Bool
liftEq2 a -> b -> Bool
f c -> d -> Bool
_ (B a
a) (B b
c) = a -> b -> Bool
f a
a b
c
liftEq2 a -> b -> Bool
_ c -> d -> Bool
g (F c
b) (F d
d) = c -> d -> Bool
g c
b d
d
liftEq2 a -> b -> Bool
_ c -> d -> Bool
_ Var a c
_ Var b d
_ = Bool
False
instance Eq b => Eq1 (Var b) where liftEq :: (a -> b -> Bool) -> Var b a -> Var b b -> Bool
liftEq = (b -> b -> Bool) -> (a -> b -> Bool) -> Var b a -> Var b b -> Bool
forall (f :: * -> * -> *) a b c d.
Eq2 f =>
(a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
liftEq2 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
(==)
instance Show2 Var where
liftShowsPrec2 :: (Int -> a -> ShowS)
-> ([a] -> ShowS)
-> (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> Int
-> Var a b
-> ShowS
liftShowsPrec2 Int -> a -> ShowS
f [a] -> ShowS
_ Int -> b -> ShowS
_ [b] -> ShowS
_ Int
d (B a
a) = (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> a -> ShowS
f String
"B" Int
d a
a
liftShowsPrec2 Int -> a -> ShowS
_ [a] -> ShowS
_ Int -> b -> ShowS
h [b] -> ShowS
_ Int
d (F b
a) = (Int -> b -> ShowS) -> String -> Int -> b -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> b -> ShowS
h String
"F" Int
d b
a
instance Show b => Show1 (Var b) where
liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Var b a -> ShowS
liftShowsPrec = (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> (Int -> a -> ShowS)
-> ([a] -> ShowS)
-> Int
-> Var b a
-> ShowS
forall (f :: * -> * -> *) a b.
Show2 f =>
(Int -> a -> ShowS)
-> ([a] -> ShowS)
-> (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> Int
-> f a b
-> ShowS
liftShowsPrec2 Int -> b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec [b] -> ShowS
forall a. Show a => [a] -> ShowS
showList
newtype Scope b f a = Scope { Scope b f a -> f (Var b a)
unscope :: f (Var b a) }
deriving ((forall a. Scope b f a -> Rep1 (Scope b f) a)
-> (forall a. Rep1 (Scope b f) a -> Scope b f a)
-> Generic1 (Scope b f)
forall a. Rep1 (Scope b f) a -> Scope b f a
forall a. Scope b f a -> Rep1 (Scope b f) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall b (f :: * -> *) a.
Functor f =>
Rep1 (Scope b f) a -> Scope b f a
forall b (f :: * -> *) a.
Functor f =>
Scope b f a -> Rep1 (Scope b f) a
$cto1 :: forall b (f :: * -> *) a.
Functor f =>
Rep1 (Scope b f) a -> Scope b f a
$cfrom1 :: forall b (f :: * -> *) a.
Functor f =>
Scope b f a -> Rep1 (Scope b f) a
Generic1)
deriving ((Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS
(forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS)
-> (forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS)
-> Show1 (Scope b f)
forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS
forall b (f :: * -> *) a.
(Functor f, Show1 f, Show b) =>
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS
forall b (f :: * -> *) a.
(Functor f, Show1 f, Show b) =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS
forall (f :: * -> *).
(forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS)
-> (forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS)
-> Show1 f
liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS
$cliftShowList :: forall b (f :: * -> *) a.
(Functor f, Show1 f, Show b) =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS
liftShowsPrec :: (Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS
$cliftShowsPrec :: forall b (f :: * -> *) a.
(Functor f, Show1 f, Show b) =>
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS
Show1, (a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
(forall a b.
(a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool)
-> Eq1 (Scope b f)
forall a b. (a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
forall b (f :: * -> *) a b.
(Functor f, Eq1 f, Eq b) =>
(a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
forall (f :: * -> *).
(forall a b. (a -> b -> Bool) -> f a -> f b -> Bool) -> Eq1 f
liftEq :: (a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
$cliftEq :: forall b (f :: * -> *) a b.
(Functor f, Eq1 f, Eq b) =>
(a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
Eq1) via (Generically (Scope b f))
instance (Eq e, Functor m, Eq1 m, Eq a) => Eq (Scope e m a) where == :: Scope e m a -> Scope e m a -> Bool
(==) = Scope e m a -> Scope e m a -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1
instance (Show e, Functor m, Show1 m, Show a) => Show (Scope e m a) where showsPrec :: Int -> Scope e m a -> ShowS
showsPrec = Int -> Scope e m a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1
fromScope :: Scope b f a -> f (Var b a)
fromScope :: Scope b f a -> f (Var b a)
fromScope = Scope b f a -> f (Var b a)
forall b (f :: * -> *) a. Scope b f a -> f (Var b a)
unscope
{-# INLINE fromScope #-}
toScope :: f (Var b a) -> Scope b f a
toScope :: f (Var b a) -> Scope b f a
toScope = f (Var b a) -> Scope b f a
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope
{-# INLINE toScope #-}
class Bound t where
(>>>=) :: Monad f => t f a -> (a -> f c) -> t f c
#if defined(__GLASGOW_HASKELL__)
default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) =>
t f a -> (a -> f c) -> t f c
t f a
m >>>= a -> f c
f = t f a
m t f a -> (a -> t f c) -> t f c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= f c -> t f c
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (f c -> t f c) -> (a -> f c) -> a -> t f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f c
f
{-# INLINE (>>>=) #-}
#endif
instance Bound (Scope b) where
Scope f (Var b a)
m >>>= :: Scope b f a -> (a -> f c) -> Scope b f c
>>>= a -> f c
f = f (Var b c) -> Scope b f c
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope (f (Var b c) -> Scope b f c) -> f (Var b c) -> Scope b f c
forall a b. (a -> b) -> a -> b
$ f (Var b a)
m f (Var b a) -> (Var b a -> f (Var b c)) -> f (Var b c)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var b a
v -> case Var b a
v of
B b
b -> Var b c -> f (Var b c)
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Var b c
forall b a. b -> Var b a
B b
b)
F a
a -> (c -> Var b c) -> f c -> f (Var b c)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM c -> Var b c
forall b a. a -> Var b a
F (a -> f c
f a
a)
{-# INLINE (>>>=) #-}
instance Functor f => Functor (Scope b f) where
fmap :: (a -> b) -> Scope b f a -> Scope b f b
fmap a -> b
f (Scope f (Var b a)
a) = f (Var b b) -> Scope b f b
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope ((Var b a -> Var b b) -> f (Var b a) -> f (Var b b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> Var b a -> Var b b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) f (Var b a)
a)
{-# INLINE fmap #-}
instance Foldable f => Foldable (Scope b f) where
foldMap :: (a -> m) -> Scope b f a -> m
foldMap a -> m
f (Scope f (Var b a)
a) = (Var b a -> m) -> f (Var b a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> Var b a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) f (Var b a)
a
{-# INLINE foldMap #-}
instance Traversable f => Traversable (Scope b f) where
traverse :: (a -> f b) -> Scope b f a -> f (Scope b f b)
traverse a -> f b
f (Scope f (Var b a)
a) = f (Var b b) -> Scope b f b
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope (f (Var b b) -> Scope b f b) -> f (f (Var b b)) -> f (Scope b f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var b a -> f (Var b b)) -> f (Var b a) -> f (f (Var b b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> f b) -> Var b a -> f (Var b b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f) f (Var b a)
a
{-# INLINE traverse #-}
#if !MIN_VERSION_base(4,8,0)
instance (Functor f, Monad f) => Applicative (Scope b f) where
#else
instance Monad f => Applicative (Scope b f) where
#endif
pure :: a -> Scope b f a
pure a
a = f (Var b a) -> Scope b f a
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope (Var b a -> f (Var b a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Var b a
forall b a. a -> Var b a
F a
a))
{-# INLINE pure #-}
<*> :: Scope b f (a -> b) -> Scope b f a -> Scope b f b
(<*>) = Scope b f (a -> b) -> Scope b f a -> Scope b f b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
{-# INLINE (<*>) #-}
instance Monad f => Monad (Scope b f) where
#if __GLASGOW_HASKELL__ < 710
return a = Scope (return (F a))
{-# INLINE return #-}
#endif
Scope f (Var b a)
e >>= :: Scope b f a -> (a -> Scope b f b) -> Scope b f b
>>= a -> Scope b f b
f = f (Var b b) -> Scope b f b
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope (f (Var b b) -> Scope b f b) -> f (Var b b) -> Scope b f b
forall a b. (a -> b) -> a -> b
$ f (Var b a)
e f (Var b a) -> (Var b a -> f (Var b b)) -> f (Var b b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var b a
v -> case Var b a
v of
B b
b -> Var b b -> f (Var b b)
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Var b b
forall b a. b -> Var b a
B b
b)
F a
a -> Scope b f b -> f (Var b b)
forall b (f :: * -> *) a. Scope b f a -> f (Var b a)
unscope (a -> Scope b f b
f a
a)
{-# INLINE (>>=) #-}
substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a
substitute :: a -> f a -> f a -> f a
substitute a
a f a
p f a
w = f a
w f a -> (a -> f a) -> f a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then f a
p else a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return a
b
{-# INLINE substitute #-}
substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a
substituteVar :: a -> a -> f a -> f a
substituteVar a
a a
p = (a -> a) -> f a -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then a
p else a
b)
{-# INLINE substituteVar #-}
abstract :: Functor f => (a -> Maybe b) -> f a -> Scope b f a
abstract :: (a -> Maybe b) -> f a -> Scope b f a
abstract a -> Maybe b
f f a
e = f (Var b a) -> Scope b f a
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope ((a -> Var b a) -> f a -> f (Var b a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var b a
k f a
e) where
k :: a -> Var b a
k a
y = case a -> Maybe b
f a
y of
Just b
z -> b -> Var b a
forall b a. b -> Var b a
B b
z
Maybe b
Nothing -> a -> Var b a
forall b a. a -> Var b a
F a
y
{-# INLINE abstract #-}
abstract1 :: (Functor f, Eq a) => a -> f a -> Scope () f a
abstract1 :: a -> f a -> Scope () f a
abstract1 a
a = (a -> Maybe ()) -> f a -> Scope () f a
forall (f :: * -> *) a b.
Functor f =>
(a -> Maybe b) -> f a -> Scope b f a
abstract (\a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing)
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
instantiate :: (b -> f a) -> Scope b f a -> f a
instantiate b -> f a
k Scope b f a
e = Scope b f a -> f (Var b a)
forall b (f :: * -> *) a. Scope b f a -> f (Var b a)
unscope Scope b f a
e f (Var b a) -> (Var b a -> f a) -> f a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var b a
v -> case Var b a
v of
B b
b -> b -> f a
k b
b
F a
a -> a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
{-# INLINE instantiate #-}
instantiate1 :: Monad f => f a -> Scope n f a -> f a
instantiate1 :: f a -> Scope n f a -> f a
instantiate1 f a
e = (n -> f a) -> Scope n f a -> f a
forall (f :: * -> *) b a.
Monad f =>
(b -> f a) -> Scope b f a -> f a
instantiate (f a -> n -> f a
forall a b. a -> b -> a
const f a
e)
{-# INLINE instantiate1 #-}
hoistScope :: (f (Var b a) -> g (Var b a)) -> Scope b f a -> Scope b g a
hoistScope :: (f (Var b a) -> g (Var b a)) -> Scope b f a -> Scope b g a
hoistScope f (Var b a) -> g (Var b a)
f = g (Var b a) -> Scope b g a
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope (g (Var b a) -> Scope b g a)
-> (Scope b f a -> g (Var b a)) -> Scope b f a -> Scope b g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Var b a) -> g (Var b a)
f (f (Var b a) -> g (Var b a))
-> (Scope b f a -> f (Var b a)) -> Scope b f a -> g (Var b a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope b f a -> f (Var b a)
forall b (f :: * -> *) a. Scope b f a -> f (Var b a)
unscope
{-# INLINE hoistScope #-}
mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a
mapBound :: (b -> b') -> Scope b f a -> Scope b' f a
mapBound b -> b'
f (Scope f (Var b a)
s) = f (Var b' a) -> Scope b' f a
forall b (f :: * -> *) a. f (Var b a) -> Scope b f a
Scope ((Var b a -> Var b' a) -> f (Var b a) -> f (Var b' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var b a -> Var b' a
forall a. Var b a -> Var b' a
f' f (Var b a)
s) where
f' :: Var b a -> Var b' a
f' (B b
b) = b' -> Var b' a
forall b a. b -> Var b a
B (b -> b'
f b
b)
f' (F a
a) = a -> Var b' a
forall b a. a -> Var b a
F a
a
{-# INLINE mapBound #-}
bindings :: Foldable f => Scope b f a -> [b]
bindings :: Scope b f a -> [b]
bindings (Scope f (Var b a)
s) = (Var b a -> [b] -> [b]) -> [b] -> f (Var b a) -> [b]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var b a -> [b] -> [b]
forall a a. Var a a -> [a] -> [a]
f [] f (Var b a)
s where
f :: Var a a -> [a] -> [a]
f (B a
v) [a]
vs = a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
vs
f Var a a
_ [a]
vs = [a]
vs
{-# INLINE bindings #-}
closed :: Traversable f => f a -> Maybe (f b)
closed :: f a -> Maybe (f b)
closed = (a -> Maybe b) -> f a -> Maybe (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Maybe b -> a -> Maybe b
forall a b. a -> b -> a
const Maybe b
forall a. Maybe a
Nothing)
{-# INLINE closed #-}
isClosed :: Foldable f => f a -> Bool
isClosed :: f a -> Bool
isClosed = (a -> Bool) -> f a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
False)
{-# INLINE isClosed #-}