{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Disco.AST.Generic (
Telescope (..),
telCons,
foldTelescope,
mapTelescope,
traverseTelescope,
toTelescope,
fromTelescope,
Side (..),
selectSide,
fromSide,
Container (..),
Ellipsis (..),
Term_ (..),
X_TVar,
X_TPrim,
X_TLet,
X_TParens,
X_TUnit,
X_TBool,
X_TNat,
X_TRat,
X_TChar,
X_TString,
X_TAbs,
X_TApp,
X_TTup,
X_TCase,
X_TChain,
X_TTyOp,
X_TContainer,
X_TContainerComp,
X_TAscr,
X_Term,
ForallTerm,
Link_ (..),
X_TLink,
ForallLink,
Qual_ (..),
X_QBind,
X_QGuard,
ForallQual,
Binding_ (..),
Branch_,
Guard_ (..),
X_GBool,
X_GPat,
X_GLet,
ForallGuard,
Pattern_ (..),
X_PVar,
X_PWild,
X_PAscr,
X_PUnit,
X_PBool,
X_PTup,
X_PInj,
X_PNat,
X_PChar,
X_PString,
X_PCons,
X_PList,
X_PAdd,
X_PMul,
X_PSub,
X_PNeg,
X_PFrac,
X_Pattern,
ForallPattern,
Quantifier (..),
Binder_,
X_Binder,
Property_,
)
where
import Control.Lens.Plated
import Data.Data (Data)
import Data.Data.Lens (uniplate)
import Data.Typeable
import GHC.Exts (Constraint)
import GHC.Generics (Generic)
import Data.Void
import Unbound.Generics.LocallyNameless
import Disco.Pretty
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Types
data Telescope b where
TelEmpty :: Telescope b
TelCons :: Rebind b (Telescope b) -> Telescope b
deriving (Int -> Telescope b -> ShowS
forall b. Show b => Int -> Telescope b -> ShowS
forall b. Show b => [Telescope b] -> ShowS
forall b. Show b => Telescope b -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Telescope b] -> ShowS
$cshowList :: forall b. Show b => [Telescope b] -> ShowS
show :: Telescope b -> [Char]
$cshow :: forall b. Show b => Telescope b -> [Char]
showsPrec :: Int -> Telescope b -> ShowS
$cshowsPrec :: forall b. Show b => Int -> Telescope b -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall b x. Rep (Telescope b) x -> Telescope b
forall b x. Telescope b -> Rep (Telescope b) x
$cto :: forall b x. Rep (Telescope b) x -> Telescope b
$cfrom :: forall b x. Telescope b -> Rep (Telescope b) x
Generic, forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall {b}. Alpha b => Show (Telescope b)
forall b.
Alpha b =>
AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
forall b.
Alpha b =>
AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
forall b.
Alpha b =>
AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
forall b. Alpha b => AlphaCtx -> Telescope b -> Telescope b -> Bool
forall b.
Alpha b =>
AlphaCtx -> Telescope b -> Telescope b -> Ordering
forall b. Alpha b => Telescope b -> Bool
forall b. Alpha b => Telescope b -> All
forall b. Alpha b => Telescope b -> DisjointSet AnyName
forall b. Alpha b => Telescope b -> NthPatFind
forall b. Alpha b => Telescope b -> NamePatFind
forall b (f :: * -> *).
(Alpha b, Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)
forall b (m :: * -> *).
(Alpha b, Fresh m) =>
AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)
forall b (m :: * -> *) b.
(Alpha b, LFresh m) =>
AlphaCtx
-> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Telescope b -> Telescope b -> Ordering
$cacompare' :: forall b.
Alpha b =>
AlphaCtx -> Telescope b -> Telescope b -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)
$cfreshen' :: forall b (m :: * -> *).
(Alpha b, Fresh m) =>
AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall b (m :: * -> *) b.
(Alpha b, LFresh m) =>
AlphaCtx
-> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
$cswaps' :: forall b.
Alpha b =>
AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
namePatFind :: Telescope b -> NamePatFind
$cnamePatFind :: forall b. Alpha b => Telescope b -> NamePatFind
nthPatFind :: Telescope b -> NthPatFind
$cnthPatFind :: forall b. Alpha b => Telescope b -> NthPatFind
isEmbed :: Telescope b -> Bool
$cisEmbed :: forall b. Alpha b => Telescope b -> Bool
isTerm :: Telescope b -> All
$cisTerm :: forall b. Alpha b => Telescope b -> All
isPat :: Telescope b -> DisjointSet AnyName
$cisPat :: forall b. Alpha b => Telescope b -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
$copen :: forall b.
Alpha b =>
AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
close :: AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
$cclose :: forall b.
Alpha b =>
AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)
$cfvAny' :: forall b (f :: * -> *).
(Alpha b, Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)
aeq' :: AlphaCtx -> Telescope b -> Telescope b -> Bool
$caeq' :: forall b. Alpha b => AlphaCtx -> Telescope b -> Telescope b -> Bool
Alpha, Subst t, Telescope b -> DataType
Telescope b -> Constr
forall {b}. Data b => Typeable (Telescope b)
forall b. Data b => Telescope b -> DataType
forall b. Data b => Telescope b -> Constr
forall b.
Data b =>
(forall b. Data b => b -> b) -> Telescope b -> Telescope b
forall b u.
Data b =>
Int -> (forall d. Data d => d -> u) -> Telescope b -> u
forall b u.
Data b =>
(forall d. Data d => d -> u) -> Telescope b -> [u]
forall b r r'.
Data b =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
forall b r r'.
Data b =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
forall b (m :: * -> *).
(Data b, Monad m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
forall b (m :: * -> *).
(Data b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
forall b (c :: * -> *).
Data b =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b)
forall b (c :: * -> *).
Data b =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> c (Telescope b)
forall b (t :: * -> *) (c :: * -> *).
(Data b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
forall b (t :: * -> * -> *) (c :: * -> *).
(Data b, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Telescope b))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> c (Telescope b)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
$cgmapMo :: forall b (m :: * -> *).
(Data b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
$cgmapMp :: forall b (m :: * -> *).
(Data b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
$cgmapM :: forall b (m :: * -> *).
(Data b, Monad m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Telescope b -> u
$cgmapQi :: forall b u.
Data b =>
Int -> (forall d. Data d => d -> u) -> Telescope b -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Telescope b -> [u]
$cgmapQ :: forall b u.
Data b =>
(forall d. Data d => d -> u) -> Telescope b -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
$cgmapQr :: forall b r r'.
Data b =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
$cgmapQl :: forall b r r'.
Data b =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
gmapT :: (forall b. Data b => b -> b) -> Telescope b -> Telescope b
$cgmapT :: forall b.
Data b =>
(forall b. Data b => b -> b) -> Telescope b -> Telescope b
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Telescope b))
$cdataCast2 :: forall b (t :: * -> * -> *) (c :: * -> *).
(Data b, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Telescope b))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
$cdataCast1 :: forall b (t :: * -> *) (c :: * -> *).
(Data b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
dataTypeOf :: Telescope b -> DataType
$cdataTypeOf :: forall b. Data b => Telescope b -> DataType
toConstr :: Telescope b -> Constr
$ctoConstr :: forall b. Data b => Telescope b -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b)
$cgunfold :: forall b (c :: * -> *).
Data b =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> c (Telescope b)
$cgfoldl :: forall b (c :: * -> *).
Data b =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> c (Telescope b)
Data)
telCons :: Alpha b => b -> Telescope b -> Telescope b
telCons :: forall b. Alpha b => b -> Telescope b -> Telescope b
telCons b
b Telescope b
tb = forall b. Rebind b (Telescope b) -> Telescope b
TelCons (forall p1 p2. (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
rebind b
b Telescope b
tb)
foldTelescope :: Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope :: forall b r. Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope b -> r -> r
_ r
z Telescope b
TelEmpty = r
z
foldTelescope b -> r -> r
f r
z (TelCons (forall p1 p2. (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
unrebind -> (b
b, Telescope b
bs))) = b -> r -> r
f b
b (forall b r. Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope b -> r -> r
f r
z Telescope b
bs)
mapTelescope :: (Alpha a, Alpha b) => (a -> b) -> Telescope a -> Telescope b
mapTelescope :: forall a b.
(Alpha a, Alpha b) =>
(a -> b) -> Telescope a -> Telescope b
mapTelescope a -> b
f = forall b. Alpha b => [b] -> Telescope b
toTelescope forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. Alpha b => Telescope b -> [b]
fromTelescope
traverseTelescope ::
(Applicative f, Alpha a, Alpha b) =>
(a -> f b) ->
Telescope a ->
f (Telescope b)
traverseTelescope :: forall (f :: * -> *) a b.
(Applicative f, Alpha a, Alpha b) =>
(a -> f b) -> Telescope a -> f (Telescope b)
traverseTelescope a -> f b
f = forall b r. Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope (\a
a f (Telescope b)
ftb -> forall b. Alpha b => b -> Telescope b -> Telescope b
telCons forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Telescope b)
ftb) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b. Telescope b
TelEmpty)
toTelescope :: Alpha b => [b] -> Telescope b
toTelescope :: forall b. Alpha b => [b] -> Telescope b
toTelescope = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b. Alpha b => b -> Telescope b -> Telescope b
telCons forall b. Telescope b
TelEmpty
fromTelescope :: Alpha b => Telescope b -> [b]
fromTelescope :: forall b. Alpha b => Telescope b -> [b]
fromTelescope = forall b r. Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope (:) []
data Side = L | R
deriving (Int -> Side -> ShowS
[Side] -> ShowS
Side -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Side] -> ShowS
$cshowList :: [Side] -> ShowS
show :: Side -> [Char]
$cshow :: Side -> [Char]
showsPrec :: Int -> Side -> ShowS
$cshowsPrec :: Int -> Side -> ShowS
Show, Side -> Side -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Side -> Side -> Bool
$c/= :: Side -> Side -> Bool
== :: Side -> Side -> Bool
$c== :: Side -> Side -> Bool
Eq, Eq Side
Side -> Side -> Bool
Side -> Side -> Ordering
Side -> Side -> Side
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Side -> Side -> Side
$cmin :: Side -> Side -> Side
max :: Side -> Side -> Side
$cmax :: Side -> Side -> Side
>= :: Side -> Side -> Bool
$c>= :: Side -> Side -> Bool
> :: Side -> Side -> Bool
$c> :: Side -> Side -> Bool
<= :: Side -> Side -> Bool
$c<= :: Side -> Side -> Bool
< :: Side -> Side -> Bool
$c< :: Side -> Side -> Bool
compare :: Side -> Side -> Ordering
$ccompare :: Side -> Side -> Ordering
Ord, Int -> Side
Side -> Int
Side -> [Side]
Side -> Side
Side -> Side -> [Side]
Side -> Side -> Side -> [Side]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Side -> Side -> Side -> [Side]
$cenumFromThenTo :: Side -> Side -> Side -> [Side]
enumFromTo :: Side -> Side -> [Side]
$cenumFromTo :: Side -> Side -> [Side]
enumFromThen :: Side -> Side -> [Side]
$cenumFromThen :: Side -> Side -> [Side]
enumFrom :: Side -> [Side]
$cenumFrom :: Side -> [Side]
fromEnum :: Side -> Int
$cfromEnum :: Side -> Int
toEnum :: Int -> Side
$ctoEnum :: Int -> Side
pred :: Side -> Side
$cpred :: Side -> Side
succ :: Side -> Side
$csucc :: Side -> Side
Enum, Side
forall a. a -> a -> Bounded a
maxBound :: Side
$cmaxBound :: Side
minBound :: Side
$cminBound :: Side
Bounded, forall x. Rep Side x -> Side
forall x. Side -> Rep Side x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Side x -> Side
$cfrom :: forall x. Side -> Rep Side x
Generic, Typeable Side
Side -> DataType
Side -> Constr
(forall b. Data b => b -> b) -> Side -> Side
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Side -> u
forall u. (forall d. Data d => d -> u) -> Side -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Side -> m Side
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Side
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Side)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Side -> m Side
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Side -> m Side
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Side -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Side -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Side -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Side -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
gmapT :: (forall b. Data b => b -> b) -> Side -> Side
$cgmapT :: (forall b. Data b => b -> b) -> Side -> Side
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Side)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Side)
dataTypeOf :: Side -> DataType
$cdataTypeOf :: Side -> DataType
toConstr :: Side -> Constr
$ctoConstr :: Side -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Side
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Side
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side
Data, Show Side
AlphaCtx -> NthPatFind -> Side -> Side
AlphaCtx -> NamePatFind -> Side -> Side
AlphaCtx -> Perm AnyName -> Side -> Side
AlphaCtx -> Side -> Side -> Bool
AlphaCtx -> Side -> Side -> Ordering
Side -> Bool
Side -> All
Side -> DisjointSet AnyName
Side -> NthPatFind
Side -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Side -> m (Side, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Side -> Side -> Ordering
$cacompare' :: AlphaCtx -> Side -> Side -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Side -> m (Side, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Side -> m (Side, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Side -> Side
$cswaps' :: AlphaCtx -> Perm AnyName -> Side -> Side
namePatFind :: Side -> NamePatFind
$cnamePatFind :: Side -> NamePatFind
nthPatFind :: Side -> NthPatFind
$cnthPatFind :: Side -> NthPatFind
isEmbed :: Side -> Bool
$cisEmbed :: Side -> Bool
isTerm :: Side -> All
$cisTerm :: Side -> All
isPat :: Side -> DisjointSet AnyName
$cisPat :: Side -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Side -> Side
$copen :: AlphaCtx -> NthPatFind -> Side -> Side
close :: AlphaCtx -> NamePatFind -> Side -> Side
$cclose :: AlphaCtx -> NamePatFind -> Side -> Side
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side
aeq' :: AlphaCtx -> Side -> Side -> Bool
$caeq' :: AlphaCtx -> Side -> Side -> Bool
Alpha, Subst t)
instance Pretty Side where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Side -> Sem r (Doc ann)
pretty = \case
Side
L -> forall (m :: * -> *) ann. Applicative m => [Char] -> m (Doc ann)
text [Char]
"left"
Side
R -> forall (m :: * -> *) ann. Applicative m => [Char] -> m (Doc ann)
text [Char]
"right"
selectSide :: Side -> a -> a -> a
selectSide :: forall a. Side -> a -> a -> a
selectSide Side
L a
a a
_ = a
a
selectSide Side
R a
_ a
b = a
b
fromSide :: Side -> Bool
fromSide :: Side -> Bool
fromSide Side
s = forall a. Side -> a -> a -> a
selectSide Side
s Bool
False Bool
True
data Container where
ListContainer :: Container
BagContainer :: Container
SetContainer :: Container
deriving (Int -> Container -> ShowS
[Container] -> ShowS
Container -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Container] -> ShowS
$cshowList :: [Container] -> ShowS
show :: Container -> [Char]
$cshow :: Container -> [Char]
showsPrec :: Int -> Container -> ShowS
$cshowsPrec :: Int -> Container -> ShowS
Show, Container -> Container -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Container -> Container -> Bool
$c/= :: Container -> Container -> Bool
== :: Container -> Container -> Bool
$c== :: Container -> Container -> Bool
Eq, Int -> Container
Container -> Int
Container -> [Container]
Container -> Container
Container -> Container -> [Container]
Container -> Container -> Container -> [Container]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Container -> Container -> Container -> [Container]
$cenumFromThenTo :: Container -> Container -> Container -> [Container]
enumFromTo :: Container -> Container -> [Container]
$cenumFromTo :: Container -> Container -> [Container]
enumFromThen :: Container -> Container -> [Container]
$cenumFromThen :: Container -> Container -> [Container]
enumFrom :: Container -> [Container]
$cenumFrom :: Container -> [Container]
fromEnum :: Container -> Int
$cfromEnum :: Container -> Int
toEnum :: Int -> Container
$ctoEnum :: Int -> Container
pred :: Container -> Container
$cpred :: Container -> Container
succ :: Container -> Container
$csucc :: Container -> Container
Enum, forall x. Rep Container x -> Container
forall x. Container -> Rep Container x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Container x -> Container
$cfrom :: forall x. Container -> Rep Container x
Generic, Typeable Container
Container -> DataType
Container -> Constr
(forall b. Data b => b -> b) -> Container -> Container
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Container -> u
forall u. (forall d. Data d => d -> u) -> Container -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Container -> m Container
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Container
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Container)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Container)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Container -> m Container
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Container -> m Container
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Container -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Container -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Container -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Container -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
gmapT :: (forall b. Data b => b -> b) -> Container -> Container
$cgmapT :: (forall b. Data b => b -> b) -> Container -> Container
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Container)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Container)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Container)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Container)
dataTypeOf :: Container -> DataType
$cdataTypeOf :: Container -> DataType
toConstr :: Container -> Constr
$ctoConstr :: Container -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Container
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Container
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container
Data, Show Container
AlphaCtx -> NthPatFind -> Container -> Container
AlphaCtx -> NamePatFind -> Container -> Container
AlphaCtx -> Perm AnyName -> Container -> Container
AlphaCtx -> Container -> Container -> Bool
AlphaCtx -> Container -> Container -> Ordering
Container -> Bool
Container -> All
Container -> DisjointSet AnyName
Container -> NthPatFind
Container -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Container -> f Container
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Container -> m (Container, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Container -> Container -> Ordering
$cacompare' :: AlphaCtx -> Container -> Container -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Container -> m (Container, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Container -> m (Container, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Container -> Container
$cswaps' :: AlphaCtx -> Perm AnyName -> Container -> Container
namePatFind :: Container -> NamePatFind
$cnamePatFind :: Container -> NamePatFind
nthPatFind :: Container -> NthPatFind
$cnthPatFind :: Container -> NthPatFind
isEmbed :: Container -> Bool
$cisEmbed :: Container -> Bool
isTerm :: Container -> All
$cisTerm :: Container -> All
isPat :: Container -> DisjointSet AnyName
$cisPat :: Container -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Container -> Container
$copen :: AlphaCtx -> NthPatFind -> Container -> Container
close :: AlphaCtx -> NamePatFind -> Container -> Container
$cclose :: AlphaCtx -> NamePatFind -> Container -> Container
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Container -> f Container
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Container -> f Container
aeq' :: AlphaCtx -> Container -> Container -> Bool
$caeq' :: AlphaCtx -> Container -> Container -> Bool
Alpha, Subst t)
data Ellipsis t where
Until :: t -> Ellipsis t
deriving (Int -> Ellipsis t -> ShowS
forall t. Show t => Int -> Ellipsis t -> ShowS
forall t. Show t => [Ellipsis t] -> ShowS
forall t. Show t => Ellipsis t -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Ellipsis t] -> ShowS
$cshowList :: forall t. Show t => [Ellipsis t] -> ShowS
show :: Ellipsis t -> [Char]
$cshow :: forall t. Show t => Ellipsis t -> [Char]
showsPrec :: Int -> Ellipsis t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Ellipsis t -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (Ellipsis t) x -> Ellipsis t
forall t x. Ellipsis t -> Rep (Ellipsis t) x
$cto :: forall t x. Rep (Ellipsis t) x -> Ellipsis t
$cfrom :: forall t x. Ellipsis t -> Rep (Ellipsis t) x
Generic, forall a b. a -> Ellipsis b -> Ellipsis a
forall a b. (a -> b) -> Ellipsis a -> Ellipsis 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 -> Ellipsis b -> Ellipsis a
$c<$ :: forall a b. a -> Ellipsis b -> Ellipsis a
fmap :: forall a b. (a -> b) -> Ellipsis a -> Ellipsis b
$cfmap :: forall a b. (a -> b) -> Ellipsis a -> Ellipsis b
Functor, forall a. Eq a => a -> Ellipsis a -> Bool
forall a. Num a => Ellipsis a -> a
forall a. Ord a => Ellipsis a -> a
forall m. Monoid m => Ellipsis m -> m
forall a. Ellipsis a -> Bool
forall a. Ellipsis a -> Int
forall a. Ellipsis a -> [a]
forall a. (a -> a -> a) -> Ellipsis a -> a
forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
forall a b. (a -> b -> b) -> b -> Ellipsis 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 => Ellipsis a -> a
$cproduct :: forall a. Num a => Ellipsis a -> a
sum :: forall a. Num a => Ellipsis a -> a
$csum :: forall a. Num a => Ellipsis a -> a
minimum :: forall a. Ord a => Ellipsis a -> a
$cminimum :: forall a. Ord a => Ellipsis a -> a
maximum :: forall a. Ord a => Ellipsis a -> a
$cmaximum :: forall a. Ord a => Ellipsis a -> a
elem :: forall a. Eq a => a -> Ellipsis a -> Bool
$celem :: forall a. Eq a => a -> Ellipsis a -> Bool
length :: forall a. Ellipsis a -> Int
$clength :: forall a. Ellipsis a -> Int
null :: forall a. Ellipsis a -> Bool
$cnull :: forall a. Ellipsis a -> Bool
toList :: forall a. Ellipsis a -> [a]
$ctoList :: forall a. Ellipsis a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
foldr1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
fold :: forall m. Monoid m => Ellipsis m -> m
$cfold :: forall m. Monoid m => Ellipsis m -> m
Foldable, Functor Ellipsis
Foldable Ellipsis
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 => Ellipsis (m a) -> m (Ellipsis a)
forall (f :: * -> *) a.
Applicative f =>
Ellipsis (f a) -> f (Ellipsis a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ellipsis a -> m (Ellipsis b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ellipsis a -> f (Ellipsis b)
sequence :: forall (m :: * -> *) a. Monad m => Ellipsis (m a) -> m (Ellipsis a)
$csequence :: forall (m :: * -> *) a. Monad m => Ellipsis (m a) -> m (Ellipsis a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ellipsis a -> m (Ellipsis b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ellipsis a -> m (Ellipsis b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Ellipsis (f a) -> f (Ellipsis a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Ellipsis (f a) -> f (Ellipsis a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ellipsis a -> f (Ellipsis b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ellipsis a -> f (Ellipsis b)
Traversable, forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall {t}. Alpha t => Show (Ellipsis t)
forall t.
Alpha t =>
AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
forall t.
Alpha t =>
AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
forall t.
Alpha t =>
AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
forall t. Alpha t => AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
forall t.
Alpha t =>
AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
forall t. Alpha t => Ellipsis t -> Bool
forall t. Alpha t => Ellipsis t -> All
forall t. Alpha t => Ellipsis t -> DisjointSet AnyName
forall t. Alpha t => Ellipsis t -> NthPatFind
forall t. Alpha t => Ellipsis t -> NamePatFind
forall t (f :: * -> *).
(Alpha t, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)
forall t (m :: * -> *).
(Alpha t, Fresh m) =>
AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)
forall t (m :: * -> *) b.
(Alpha t, LFresh m) =>
AlphaCtx
-> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
$cacompare' :: forall t.
Alpha t =>
AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)
$cfreshen' :: forall t (m :: * -> *).
(Alpha t, Fresh m) =>
AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall t (m :: * -> *) b.
(Alpha t, LFresh m) =>
AlphaCtx
-> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
$cswaps' :: forall t.
Alpha t =>
AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
namePatFind :: Ellipsis t -> NamePatFind
$cnamePatFind :: forall t. Alpha t => Ellipsis t -> NamePatFind
nthPatFind :: Ellipsis t -> NthPatFind
$cnthPatFind :: forall t. Alpha t => Ellipsis t -> NthPatFind
isEmbed :: Ellipsis t -> Bool
$cisEmbed :: forall t. Alpha t => Ellipsis t -> Bool
isTerm :: Ellipsis t -> All
$cisTerm :: forall t. Alpha t => Ellipsis t -> All
isPat :: Ellipsis t -> DisjointSet AnyName
$cisPat :: forall t. Alpha t => Ellipsis t -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
$copen :: forall t.
Alpha t =>
AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
close :: AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
$cclose :: forall t.
Alpha t =>
AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)
$cfvAny' :: forall t (f :: * -> *).
(Alpha t, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)
aeq' :: AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
$caeq' :: forall t. Alpha t => AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
Alpha, Subst a, Ellipsis t -> DataType
Ellipsis t -> Constr
forall {t}. Data t => Typeable (Ellipsis t)
forall t. Data t => Ellipsis t -> DataType
forall t. Data t => Ellipsis t -> Constr
forall t.
Data t =>
(forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u
forall t u.
Data t =>
(forall d. Data d => d -> u) -> Ellipsis t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ellipsis t))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Ellipsis t -> [u]
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> Ellipsis t -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
gmapT :: (forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ellipsis t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ellipsis t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
dataTypeOf :: Ellipsis t -> DataType
$cdataTypeOf :: forall t. Data t => Ellipsis t -> DataType
toConstr :: Ellipsis t -> Constr
$ctoConstr :: forall t. Data t => Ellipsis t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)
Data)
type family X_TVar e
type family X_TPrim e
type family X_TLet e
type family X_TParens e
type family X_TUnit e
type family X_TBool e
type family X_TNat e
type family X_TRat e
type family X_TChar e
type family X_TString e
type family X_TAbs e
type family X_TApp e
type family X_TTup e
type family X_TCase e
type family X_TChain e
type family X_TTyOp e
type family X_TContainer e
type family X_TContainerComp e
type family X_TAscr e
type family X_Term e
data Term_ e where
TVar_ :: X_TVar e -> Name (Term_ e) -> Term_ e
TPrim_ :: X_TPrim e -> Prim -> Term_ e
TLet_ :: X_TLet e -> Bind (Telescope (Binding_ e)) (Term_ e) -> Term_ e
TParens_ :: X_TParens e -> Term_ e -> Term_ e
TUnit_ :: X_TUnit e -> Term_ e
TBool_ :: X_TBool e -> Bool -> Term_ e
TNat_ :: X_TNat e -> Integer -> Term_ e
TRat_ :: X_TRat e -> Rational -> Term_ e
TChar_ :: X_TChar e -> Char -> Term_ e
TString_ :: X_TString e -> [Char] -> Term_ e
TAbs_ :: Quantifier -> X_TAbs e -> Binder_ e (Term_ e) -> Term_ e
TApp_ :: X_TApp e -> Term_ e -> Term_ e -> Term_ e
TTup_ :: X_TTup e -> [Term_ e] -> Term_ e
TCase_ :: X_TCase e -> [Branch_ e] -> Term_ e
TChain_ :: X_TChain e -> Term_ e -> [Link_ e] -> Term_ e
TTyOp_ :: X_TTyOp e -> TyOp -> Type -> Term_ e
TContainer_ :: X_TContainer e -> Container -> [(Term_ e, Maybe (Term_ e))] -> Maybe (Ellipsis (Term_ e)) -> Term_ e
TContainerComp_ :: X_TContainerComp e -> Container -> Bind (Telescope (Qual_ e)) (Term_ e) -> Term_ e
TAscr_ :: X_TAscr e -> Term_ e -> PolyType -> Term_ e
XTerm_ :: X_Term e -> Term_ e
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Term_ e) x -> Term_ e
forall e x. Term_ e -> Rep (Term_ e) x
$cto :: forall e x. Rep (Term_ e) x -> Term_ e
$cfrom :: forall e x. Term_ e -> Rep (Term_ e) x
Generic)
type ForallTerm (a :: * -> Constraint) e =
( a (X_TVar e)
, a (X_TPrim e)
, a (X_TLet e)
, a (X_TParens e)
, a (X_TUnit e)
, a (X_TBool e)
, a (X_TNat e)
, a (X_TRat e)
, a (X_TChar e)
, a (X_TString e)
, a (X_TAbs e)
, a (X_TApp e)
, a (X_TCase e)
, a (X_TTup e)
, a (X_TChain e)
, a (X_TTyOp e)
, a (X_TContainer e)
, a (X_TContainerComp e)
, a (X_TAscr e)
, a (X_Term e)
, a (Qual_ e)
, a (Guard_ e)
, a (Link_ e)
, a (Binding_ e)
, a (Pattern_ e)
, a (Binder_ e (Term_ e))
)
deriving instance ForallTerm Show e => Show (Term_ e)
instance
( Typeable e
, ForallTerm (Subst Type) e
, ForallTerm Alpha e
) =>
Subst Type (Term_ e)
instance (Typeable e, ForallTerm Alpha e) => Alpha (Term_ e)
deriving instance (Data e, Typeable e, ForallTerm Data e) => Data (Term_ e)
instance (Data e, ForallTerm Data e) => Plated (Term_ e) where
plate :: Traversal' (Term_ e) (Term_ e)
plate = forall a. Data a => Traversal' a a
uniplate
type family X_TLink e
data Link_ e where
TLink_ :: X_TLink e -> BOp -> Term_ e -> Link_ e
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Link_ e) x -> Link_ e
forall e x. Link_ e -> Rep (Link_ e) x
$cto :: forall e x. Rep (Link_ e) x -> Link_ e
$cfrom :: forall e x. Link_ e -> Rep (Link_ e) x
Generic)
type ForallLink (a :: * -> Constraint) e =
( a (X_TLink e)
, a (Term_ e)
)
deriving instance ForallLink Show e => Show (Link_ e)
instance ForallLink (Subst Type) e => Subst Type (Link_ e)
instance (Typeable e, Show (Link_ e), ForallLink Alpha e) => Alpha (Link_ e)
deriving instance (Typeable e, Data e, ForallLink Data e) => Data (Link_ e)
type family X_QBind e
type family X_QGuard e
data Qual_ e where
QBind_ :: X_QBind e -> Name (Term_ e) -> Embed (Term_ e) -> Qual_ e
QGuard_ :: X_QGuard e -> Embed (Term_ e) -> Qual_ e
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Qual_ e) x -> Qual_ e
forall e x. Qual_ e -> Rep (Qual_ e) x
$cto :: forall e x. Rep (Qual_ e) x -> Qual_ e
$cfrom :: forall e x. Qual_ e -> Rep (Qual_ e) x
Generic)
type ForallQual (a :: * -> Constraint) e =
( a (X_QBind e)
, a (X_QGuard e)
, a (Term_ e)
)
deriving instance ForallQual Show e => Show (Qual_ e)
instance ForallQual (Subst Type) e => Subst Type (Qual_ e)
instance (Typeable e, ForallQual Alpha e) => Alpha (Qual_ e)
deriving instance (Typeable e, Data e, ForallQual Data e) => Data (Qual_ e)
data Binding_ e = Binding_ (Maybe (Embed PolyType)) (Name (Term_ e)) (Embed (Term_ e))
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Binding_ e) x -> Binding_ e
forall e x. Binding_ e -> Rep (Binding_ e) x
$cto :: forall e x. Rep (Binding_ e) x -> Binding_ e
$cfrom :: forall e x. Binding_ e -> Rep (Binding_ e) x
Generic)
deriving instance ForallTerm Show e => Show (Binding_ e)
instance Subst Type (Term_ e) => Subst Type (Binding_ e)
instance (Typeable e, Show (Binding_ e), Alpha (Term_ e)) => Alpha (Binding_ e)
deriving instance (Typeable e, Data e, ForallTerm Data e) => Data (Binding_ e)
type Branch_ e = Bind (Telescope (Guard_ e)) (Term_ e)
type family X_GBool e
type family X_GPat e
type family X_GLet e
data Guard_ e where
GBool_ :: X_GBool e -> Embed (Term_ e) -> Guard_ e
GPat_ :: X_GPat e -> Embed (Term_ e) -> Pattern_ e -> Guard_ e
GLet_ :: X_GLet e -> Binding_ e -> Guard_ e
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Guard_ e) x -> Guard_ e
forall e x. Guard_ e -> Rep (Guard_ e) x
$cto :: forall e x. Rep (Guard_ e) x -> Guard_ e
$cfrom :: forall e x. Guard_ e -> Rep (Guard_ e) x
Generic)
type ForallGuard (a :: * -> Constraint) e =
( a (X_GBool e)
, a (X_GPat e)
, a (X_GLet e)
, a (Term_ e)
, a (Pattern_ e)
, a (Binding_ e)
)
deriving instance ForallGuard Show e => Show (Guard_ e)
instance ForallGuard (Subst Type) e => Subst Type (Guard_ e)
instance (Typeable e, Show (Guard_ e), ForallGuard Alpha e) => Alpha (Guard_ e)
deriving instance (Typeable e, Data e, ForallGuard Data e) => Data (Guard_ e)
type family X_PVar e
type family X_PWild e
type family X_PAscr e
type family X_PUnit e
type family X_PBool e
type family X_PTup e
type family X_PInj e
type family X_PNat e
type family X_PChar e
type family X_PString e
type family X_PCons e
type family X_PList e
type family X_PAdd e
type family X_PMul e
type family X_PSub e
type family X_PNeg e
type family X_PFrac e
type family X_Pattern e
data Pattern_ e where
PVar_ :: X_PVar e -> Name (Term_ e) -> Pattern_ e
PWild_ :: X_PWild e -> Pattern_ e
PAscr_ :: X_PAscr e -> Pattern_ e -> Type -> Pattern_ e
PUnit_ :: X_PUnit e -> Pattern_ e
PBool_ :: X_PBool e -> Bool -> Pattern_ e
PTup_ :: X_PTup e -> [Pattern_ e] -> Pattern_ e
PInj_ :: X_PInj e -> Side -> Pattern_ e -> Pattern_ e
PNat_ :: X_PNat e -> Integer -> Pattern_ e
PChar_ :: X_PChar e -> Char -> Pattern_ e
PString_ :: X_PString e -> String -> Pattern_ e
PCons_ :: X_PCons e -> Pattern_ e -> Pattern_ e -> Pattern_ e
PList_ :: X_PList e -> [Pattern_ e] -> Pattern_ e
PAdd_ :: X_PAdd e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e
PMul_ :: X_PMul e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e
PSub_ :: X_PSub e -> Pattern_ e -> Term_ e -> Pattern_ e
PNeg_ :: X_PNeg e -> Pattern_ e -> Pattern_ e
PFrac_ :: X_PFrac e -> Pattern_ e -> Pattern_ e -> Pattern_ e
PNonlinear_ :: Embed (Pattern_ e) -> Name (Term_ e) -> Pattern_ e
XPattern_ :: X_Pattern e -> Pattern_ e
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Pattern_ e) x -> Pattern_ e
forall e x. Pattern_ e -> Rep (Pattern_ e) x
$cto :: forall e x. Rep (Pattern_ e) x -> Pattern_ e
$cfrom :: forall e x. Pattern_ e -> Rep (Pattern_ e) x
Generic)
type ForallPattern (a :: * -> Constraint) e =
( a (X_PVar e)
, a (X_PWild e)
, a (X_PAscr e)
, a (X_PUnit e)
, a (X_PBool e)
, a (X_PNat e)
, a (X_PChar e)
, a (X_PString e)
, a (X_PTup e)
, a (X_PInj e)
, a (X_PCons e)
, a (X_PList e)
, a (X_PAdd e)
, a (X_PMul e)
, a (X_PSub e)
, a (X_PNeg e)
, a (X_PFrac e)
, a (X_Pattern e)
, a (Term_ e)
)
deriving instance ForallPattern Show e => Show (Pattern_ e)
instance ForallPattern (Subst Type) e => Subst Type (Pattern_ e)
instance (Typeable e, Show (Pattern_ e), ForallPattern Alpha e) => Alpha (Pattern_ e)
deriving instance (Typeable e, Data e, ForallPattern Data e) => Data (Pattern_ e)
type family X_Binder e
type Binder_ e a = Bind (X_Binder e) a
data Quantifier = Lam | Ex | All
deriving (forall x. Rep Quantifier x -> Quantifier
forall x. Quantifier -> Rep Quantifier x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Quantifier x -> Quantifier
$cfrom :: forall x. Quantifier -> Rep Quantifier x
Generic, Typeable Quantifier
Quantifier -> DataType
Quantifier -> Constr
(forall b. Data b => b -> b) -> Quantifier -> Quantifier
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Quantifier -> u
forall u. (forall d. Data d => d -> u) -> Quantifier -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Quantifier -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Quantifier -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quantifier -> m Quantifier
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quantifier -> m Quantifier
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quantifier
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quantifier -> c Quantifier
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quantifier)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantifier)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quantifier -> m Quantifier
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quantifier -> m Quantifier
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quantifier -> m Quantifier
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quantifier -> m Quantifier
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quantifier -> m Quantifier
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quantifier -> m Quantifier
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quantifier -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quantifier -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Quantifier -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Quantifier -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Quantifier -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Quantifier -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Quantifier -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Quantifier -> r
gmapT :: (forall b. Data b => b -> b) -> Quantifier -> Quantifier
$cgmapT :: (forall b. Data b => b -> b) -> Quantifier -> Quantifier
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantifier)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantifier)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quantifier)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quantifier)
dataTypeOf :: Quantifier -> DataType
$cdataTypeOf :: Quantifier -> DataType
toConstr :: Quantifier -> Constr
$ctoConstr :: Quantifier -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quantifier
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quantifier
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quantifier -> c Quantifier
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quantifier -> c Quantifier
Data, Quantifier -> Quantifier -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Quantifier -> Quantifier -> Bool
$c/= :: Quantifier -> Quantifier -> Bool
== :: Quantifier -> Quantifier -> Bool
$c== :: Quantifier -> Quantifier -> Bool
Eq, Eq Quantifier
Quantifier -> Quantifier -> Bool
Quantifier -> Quantifier -> Ordering
Quantifier -> Quantifier -> Quantifier
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Quantifier -> Quantifier -> Quantifier
$cmin :: Quantifier -> Quantifier -> Quantifier
max :: Quantifier -> Quantifier -> Quantifier
$cmax :: Quantifier -> Quantifier -> Quantifier
>= :: Quantifier -> Quantifier -> Bool
$c>= :: Quantifier -> Quantifier -> Bool
> :: Quantifier -> Quantifier -> Bool
$c> :: Quantifier -> Quantifier -> Bool
<= :: Quantifier -> Quantifier -> Bool
$c<= :: Quantifier -> Quantifier -> Bool
< :: Quantifier -> Quantifier -> Bool
$c< :: Quantifier -> Quantifier -> Bool
compare :: Quantifier -> Quantifier -> Ordering
$ccompare :: Quantifier -> Quantifier -> Ordering
Ord, Int -> Quantifier -> ShowS
[Quantifier] -> ShowS
Quantifier -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Quantifier] -> ShowS
$cshowList :: [Quantifier] -> ShowS
show :: Quantifier -> [Char]
$cshow :: Quantifier -> [Char]
showsPrec :: Int -> Quantifier -> ShowS
$cshowsPrec :: Int -> Quantifier -> ShowS
Show, Show Quantifier
AlphaCtx -> NthPatFind -> Quantifier -> Quantifier
AlphaCtx -> NamePatFind -> Quantifier -> Quantifier
AlphaCtx -> Perm AnyName -> Quantifier -> Quantifier
AlphaCtx -> Quantifier -> Quantifier -> Bool
AlphaCtx -> Quantifier -> Quantifier -> Ordering
Quantifier -> Bool
Quantifier -> All
Quantifier -> DisjointSet AnyName
Quantifier -> NthPatFind
Quantifier -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Quantifier -> f Quantifier
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Quantifier -> m (Quantifier, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Quantifier -> (Quantifier -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Quantifier -> Quantifier -> Ordering
$cacompare' :: AlphaCtx -> Quantifier -> Quantifier -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Quantifier -> m (Quantifier, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Quantifier -> m (Quantifier, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Quantifier -> (Quantifier -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Quantifier -> (Quantifier -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Quantifier -> Quantifier
$cswaps' :: AlphaCtx -> Perm AnyName -> Quantifier -> Quantifier
namePatFind :: Quantifier -> NamePatFind
$cnamePatFind :: Quantifier -> NamePatFind
nthPatFind :: Quantifier -> NthPatFind
$cnthPatFind :: Quantifier -> NthPatFind
isEmbed :: Quantifier -> Bool
$cisEmbed :: Quantifier -> Bool
isTerm :: Quantifier -> All
$cisTerm :: Quantifier -> All
isPat :: Quantifier -> DisjointSet AnyName
$cisPat :: Quantifier -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Quantifier -> Quantifier
$copen :: AlphaCtx -> NthPatFind -> Quantifier -> Quantifier
close :: AlphaCtx -> NamePatFind -> Quantifier -> Quantifier
$cclose :: AlphaCtx -> NamePatFind -> Quantifier -> Quantifier
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Quantifier -> f Quantifier
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Quantifier -> f Quantifier
aeq' :: AlphaCtx -> Quantifier -> Quantifier -> Bool
$caeq' :: AlphaCtx -> Quantifier -> Quantifier -> Bool
Alpha, Subst Type)
type Property_ e = Term_ e
instance Alpha Void