{-# 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
[Telescope b] -> ShowS
Telescope b -> String
(Int -> Telescope b -> ShowS)
-> (Telescope b -> String)
-> ([Telescope b] -> ShowS)
-> Show (Telescope b)
forall b. Show b => Int -> Telescope b -> ShowS
forall b. Show b => [Telescope b] -> ShowS
forall b. Show b => Telescope b -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Telescope b] -> ShowS
$cshowList :: forall b. Show b => [Telescope b] -> ShowS
show :: Telescope b -> String
$cshow :: forall b. Show b => Telescope b -> String
showsPrec :: Int -> Telescope b -> ShowS
$cshowsPrec :: forall b. Show b => Int -> Telescope b -> ShowS
Show, (forall x. Telescope b -> Rep (Telescope b) x)
-> (forall x. Rep (Telescope b) x -> Telescope b)
-> Generic (Telescope b)
forall x. Rep (Telescope b) x -> Telescope b
forall x. Telescope b -> Rep (Telescope b) x
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, Show (Telescope b)
Show (Telescope b)
-> (AlphaCtx -> Telescope b -> Telescope b -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b))
-> (AlphaCtx -> NamePatFind -> Telescope b -> Telescope b)
-> (AlphaCtx -> NthPatFind -> Telescope b -> Telescope b)
-> (Telescope b -> DisjointSet AnyName)
-> (Telescope b -> All)
-> (Telescope b -> Bool)
-> (Telescope b -> NthPatFind)
-> (Telescope b -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName))
-> (AlphaCtx -> Telescope b -> Telescope b -> Ordering)
-> Alpha (Telescope b)
AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
AlphaCtx -> Telescope b -> Telescope b -> Bool
AlphaCtx -> Telescope b -> Telescope b -> Ordering
Telescope b -> Bool
Telescope b -> All
Telescope b -> DisjointSet AnyName
Telescope b -> NthPatFind
Telescope b -> 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 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
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)
forall (m :: * -> *) 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' :: 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' :: 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' :: 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
$cp1Alpha :: forall b. Alpha b => Show (Telescope b)
Alpha, Subst t, Typeable (Telescope b)
DataType
Constr
Typeable (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 (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b))
-> (Telescope b -> Constr)
-> (Telescope b -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Telescope b)))
-> ((forall b. Data b => b -> b) -> Telescope b -> Telescope b)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r)
-> (forall u. (forall d. Data d => d -> u) -> Telescope b -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Telescope b -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b))
-> Data (Telescope b)
Telescope b -> DataType
Telescope b -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
(forall b. Data b => b -> b) -> Telescope b -> Telescope b
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> c (Telescope b)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b)
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 u. Int -> (forall d. Data d => d -> u) -> Telescope b -> u
forall u. (forall d. Data d => d -> u) -> Telescope b -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Telescope b))
$cTelCons :: Constr
$cTelEmpty :: Constr
$tTelescope :: DataType
gmapMo :: (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 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 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 :: 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 d. Data d => d -> u) -> Telescope b -> [u]
$cgmapQ :: forall b u.
Data b =>
(forall d. Data d => d -> u) -> Telescope b -> [u]
gmapQr :: (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 :: (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 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 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 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 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)
$cp1Data :: forall b. Data b => Typeable (Telescope b)
Data)
telCons :: Alpha b => b -> Telescope b -> Telescope b
telCons :: b -> Telescope b -> Telescope b
telCons b
b Telescope b
tb = Rebind b (Telescope b) -> Telescope b
forall b. Rebind b (Telescope b) -> Telescope b
TelCons (b -> Telescope b -> Rebind b (Telescope b)
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 :: (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 (Rebind b (Telescope b) -> (b, Telescope b)
forall p1 p2. (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
unrebind -> (b
b,Telescope b
bs))) = b -> r -> r
f b
b ((b -> r -> r) -> r -> Telescope b -> r
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 :: (a -> b) -> Telescope a -> Telescope b
mapTelescope a -> b
f = [b] -> Telescope b
forall b. Alpha b => [b] -> Telescope b
toTelescope ([b] -> Telescope b)
-> (Telescope a -> [b]) -> Telescope a -> Telescope b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f ([a] -> [b]) -> (Telescope a -> [a]) -> Telescope a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope a -> [a]
forall b. Alpha b => Telescope b -> [b]
fromTelescope
traverseTelescope
:: (Applicative f, Alpha a, Alpha b)
=> (a -> f b) -> Telescope a -> f (Telescope b)
traverseTelescope :: (a -> f b) -> Telescope a -> f (Telescope b)
traverseTelescope a -> f b
f = (a -> f (Telescope b) -> f (Telescope b))
-> f (Telescope b) -> Telescope a -> f (Telescope b)
forall b r. Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope (\a
a f (Telescope b)
ftb -> b -> Telescope b -> Telescope b
forall b. Alpha b => b -> Telescope b -> Telescope b
telCons (b -> Telescope b -> Telescope b)
-> f b -> f (Telescope b -> Telescope b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
a f (Telescope b -> Telescope b)
-> f (Telescope b) -> f (Telescope b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Telescope b)
ftb) (Telescope b -> f (Telescope b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Telescope b
forall b. Telescope b
TelEmpty)
toTelescope :: Alpha b => [b] -> Telescope b
toTelescope :: [b] -> Telescope b
toTelescope = (b -> Telescope b -> Telescope b)
-> Telescope b -> [b] -> Telescope b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr b -> Telescope b -> Telescope b
forall b. Alpha b => b -> Telescope b -> Telescope b
telCons Telescope b
forall b. Telescope b
TelEmpty
fromTelescope :: Alpha b => Telescope b -> [b]
fromTelescope :: Telescope b -> [b]
fromTelescope = (b -> [b] -> [b]) -> [b] -> Telescope b -> [b]
forall b r. Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope (:) []
data Side = L | R
deriving (Int -> Side -> ShowS
[Side] -> ShowS
Side -> String
(Int -> Side -> ShowS)
-> (Side -> String) -> ([Side] -> ShowS) -> Show Side
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Side] -> ShowS
$cshowList :: [Side] -> ShowS
show :: Side -> String
$cshow :: Side -> String
showsPrec :: Int -> Side -> ShowS
$cshowsPrec :: Int -> Side -> ShowS
Show, Side -> Side -> Bool
(Side -> Side -> Bool) -> (Side -> Side -> Bool) -> Eq Side
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
Eq Side
-> (Side -> Side -> Ordering)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Side)
-> (Side -> Side -> Side)
-> Ord 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
$cp1Ord :: Eq Side
Ord, Int -> Side
Side -> Int
Side -> [Side]
Side -> Side
Side -> Side -> [Side]
Side -> Side -> Side -> [Side]
(Side -> Side)
-> (Side -> Side)
-> (Int -> Side)
-> (Side -> Int)
-> (Side -> [Side])
-> (Side -> Side -> [Side])
-> (Side -> Side -> [Side])
-> (Side -> Side -> Side -> [Side])
-> Enum 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
Side -> Side -> Bounded Side
forall a. a -> a -> Bounded a
maxBound :: Side
$cmaxBound :: Side
minBound :: Side
$cminBound :: Side
Bounded, (forall x. Side -> Rep Side x)
-> (forall x. Rep Side x -> Side) -> Generic Side
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
DataType
Constr
Typeable Side
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Side)
-> (Side -> Constr)
-> (Side -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Side -> Side)
-> (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 u. (forall d. Data d => d -> u) -> Side -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Side -> u)
-> (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 (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side)
-> Data Side
Side -> DataType
Side -> Constr
(forall b. Data b => b -> b) -> Side -> Side
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cR :: Constr
$cL :: Constr
$tSide :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Side -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Side -> u
gmapQ :: (forall d. Data d => d -> u) -> Side -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Side -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Side
Data, Show Side
Show Side
-> (AlphaCtx -> Side -> Side -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side)
-> (AlphaCtx -> NamePatFind -> Side -> Side)
-> (AlphaCtx -> NthPatFind -> Side -> Side)
-> (Side -> DisjointSet AnyName)
-> (Side -> All)
-> (Side -> Bool)
-> (Side -> NthPatFind)
-> (Side -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Side -> Side)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Side -> m (Side, Perm AnyName))
-> (AlphaCtx -> Side -> Side -> Ordering)
-> Alpha 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' :: AlphaCtx -> Side -> m (Side, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Side -> m (Side, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show Side
Alpha, Subst t)
instance Pretty Side where
pretty :: Side -> Sem r Doc
pretty = \case
Side
L -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"left"
Side
R -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"right"
selectSide :: Side -> a -> a -> a
selectSide :: 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 = Side -> Bool -> Bool -> Bool
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 -> String
(Int -> Container -> ShowS)
-> (Container -> String)
-> ([Container] -> ShowS)
-> Show Container
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Container] -> ShowS
$cshowList :: [Container] -> ShowS
show :: Container -> String
$cshow :: Container -> String
showsPrec :: Int -> Container -> ShowS
$cshowsPrec :: Int -> Container -> ShowS
Show, Container -> Container -> Bool
(Container -> Container -> Bool)
-> (Container -> Container -> Bool) -> Eq Container
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]
(Container -> Container)
-> (Container -> Container)
-> (Int -> Container)
-> (Container -> Int)
-> (Container -> [Container])
-> (Container -> Container -> [Container])
-> (Container -> Container -> [Container])
-> (Container -> Container -> Container -> [Container])
-> Enum 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. Container -> Rep Container x)
-> (forall x. Rep Container x -> Container) -> Generic Container
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
DataType
Constr
Typeable Container
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Container)
-> (Container -> Constr)
-> (Container -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Container -> Container)
-> (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 u. (forall d. Data d => d -> u) -> Container -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Container -> u)
-> (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 (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container)
-> Data Container
Container -> DataType
Container -> Constr
(forall b. Data b => b -> b) -> Container -> Container
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cSetContainer :: Constr
$cBagContainer :: Constr
$cListContainer :: Constr
$tContainer :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Container -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Container -> u
gmapQ :: (forall d. Data d => d -> u) -> Container -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Container -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Container
Data, Show Container
Show Container
-> (AlphaCtx -> Container -> Container -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Container -> f Container)
-> (AlphaCtx -> NamePatFind -> Container -> Container)
-> (AlphaCtx -> NthPatFind -> Container -> Container)
-> (Container -> DisjointSet AnyName)
-> (Container -> All)
-> (Container -> Bool)
-> (Container -> NthPatFind)
-> (Container -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Container -> Container)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Container -> m (Container, Perm AnyName))
-> (AlphaCtx -> Container -> Container -> Ordering)
-> Alpha 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' :: AlphaCtx -> Container -> m (Container, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Container -> m (Container, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show Container
Alpha, Subst t)
data Ellipsis t where
Until :: t -> Ellipsis t
deriving (Int -> Ellipsis t -> ShowS
[Ellipsis t] -> ShowS
Ellipsis t -> String
(Int -> Ellipsis t -> ShowS)
-> (Ellipsis t -> String)
-> ([Ellipsis t] -> ShowS)
-> Show (Ellipsis t)
forall t. Show t => Int -> Ellipsis t -> ShowS
forall t. Show t => [Ellipsis t] -> ShowS
forall t. Show t => Ellipsis t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ellipsis t] -> ShowS
$cshowList :: forall t. Show t => [Ellipsis t] -> ShowS
show :: Ellipsis t -> String
$cshow :: forall t. Show t => Ellipsis t -> String
showsPrec :: Int -> Ellipsis t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Ellipsis t -> ShowS
Show, (forall x. Ellipsis t -> Rep (Ellipsis t) x)
-> (forall x. Rep (Ellipsis t) x -> Ellipsis t)
-> Generic (Ellipsis t)
forall x. Rep (Ellipsis t) x -> Ellipsis t
forall x. Ellipsis t -> Rep (Ellipsis t) x
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, a -> Ellipsis b -> Ellipsis a
(a -> b) -> Ellipsis a -> Ellipsis b
(forall a b. (a -> b) -> Ellipsis a -> Ellipsis b)
-> (forall a b. a -> Ellipsis b -> Ellipsis a) -> Functor Ellipsis
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
<$ :: a -> Ellipsis b -> Ellipsis a
$c<$ :: forall a b. a -> Ellipsis b -> Ellipsis a
fmap :: (a -> b) -> Ellipsis a -> Ellipsis b
$cfmap :: forall a b. (a -> b) -> Ellipsis a -> Ellipsis b
Functor, Ellipsis a -> Bool
(a -> m) -> Ellipsis a -> m
(a -> b -> b) -> b -> Ellipsis a -> b
(forall m. Monoid m => Ellipsis m -> m)
-> (forall m a. Monoid m => (a -> m) -> Ellipsis a -> m)
-> (forall m a. Monoid m => (a -> m) -> Ellipsis a -> m)
-> (forall a b. (a -> b -> b) -> b -> Ellipsis a -> b)
-> (forall a b. (a -> b -> b) -> b -> Ellipsis a -> b)
-> (forall b a. (b -> a -> b) -> b -> Ellipsis a -> b)
-> (forall b a. (b -> a -> b) -> b -> Ellipsis a -> b)
-> (forall a. (a -> a -> a) -> Ellipsis a -> a)
-> (forall a. (a -> a -> a) -> Ellipsis a -> a)
-> (forall a. Ellipsis a -> [a])
-> (forall a. Ellipsis a -> Bool)
-> (forall a. Ellipsis a -> Int)
-> (forall a. Eq a => a -> Ellipsis a -> Bool)
-> (forall a. Ord a => Ellipsis a -> a)
-> (forall a. Ord a => Ellipsis a -> a)
-> (forall a. Num a => Ellipsis a -> a)
-> (forall a. Num a => Ellipsis a -> a)
-> Foldable Ellipsis
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 :: Ellipsis a -> a
$cproduct :: forall a. Num a => Ellipsis a -> a
sum :: Ellipsis a -> a
$csum :: forall a. Num a => Ellipsis a -> a
minimum :: Ellipsis a -> a
$cminimum :: forall a. Ord a => Ellipsis a -> a
maximum :: Ellipsis a -> a
$cmaximum :: forall a. Ord a => Ellipsis a -> a
elem :: a -> Ellipsis a -> Bool
$celem :: forall a. Eq a => a -> Ellipsis a -> Bool
length :: Ellipsis a -> Int
$clength :: forall a. Ellipsis a -> Int
null :: Ellipsis a -> Bool
$cnull :: forall a. Ellipsis a -> Bool
toList :: Ellipsis a -> [a]
$ctoList :: forall a. Ellipsis a -> [a]
foldl1 :: (a -> a -> a) -> Ellipsis a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
foldr1 :: (a -> a -> a) -> Ellipsis a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
foldl' :: (b -> a -> b) -> b -> Ellipsis a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
foldl :: (b -> a -> b) -> b -> Ellipsis a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
foldr' :: (a -> b -> b) -> b -> Ellipsis a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
foldr :: (a -> b -> b) -> b -> Ellipsis a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
foldMap' :: (a -> m) -> Ellipsis a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
foldMap :: (a -> m) -> Ellipsis a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
fold :: Ellipsis m -> m
$cfold :: forall m. Monoid m => Ellipsis m -> m
Foldable, Functor Ellipsis
Foldable Ellipsis
Functor Ellipsis
-> Foldable Ellipsis
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ellipsis a -> f (Ellipsis b))
-> (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 (m :: * -> *) a.
Monad m =>
Ellipsis (m a) -> m (Ellipsis a))
-> Traversable Ellipsis
(a -> f b) -> Ellipsis a -> f (Ellipsis 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 => 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 :: Ellipsis (m a) -> m (Ellipsis a)
$csequence :: forall (m :: * -> *) a. Monad m => Ellipsis (m a) -> m (Ellipsis a)
mapM :: (a -> m b) -> Ellipsis a -> m (Ellipsis b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ellipsis a -> m (Ellipsis b)
sequenceA :: Ellipsis (f a) -> f (Ellipsis a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Ellipsis (f a) -> f (Ellipsis a)
traverse :: (a -> f b) -> Ellipsis a -> f (Ellipsis b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ellipsis a -> f (Ellipsis b)
$cp2Traversable :: Foldable Ellipsis
$cp1Traversable :: Functor Ellipsis
Traversable, Show (Ellipsis t)
Show (Ellipsis t)
-> (AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t))
-> (AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t)
-> (AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t)
-> (Ellipsis t -> DisjointSet AnyName)
-> (Ellipsis t -> All)
-> (Ellipsis t -> Bool)
-> (Ellipsis t -> NthPatFind)
-> (Ellipsis t -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName))
-> (AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering)
-> Alpha (Ellipsis t)
AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
Ellipsis t -> Bool
Ellipsis t -> All
Ellipsis t -> DisjointSet AnyName
Ellipsis t -> NthPatFind
Ellipsis t -> 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 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
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)
forall (m :: * -> *) b.
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' :: 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' :: 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' :: 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
$cp1Alpha :: forall t. Alpha t => Show (Ellipsis t)
Alpha, Subst a, Typeable (Ellipsis t)
DataType
Constr
Typeable (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 (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t))
-> (Ellipsis t -> Constr)
-> (Ellipsis t -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ellipsis t)))
-> ((forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r)
-> (forall u. (forall d. Data d => d -> u) -> Ellipsis t -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t))
-> Data (Ellipsis t)
Ellipsis t -> DataType
Ellipsis t -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
(forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t)
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 u. Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u
forall u. (forall d. Data d => d -> u) -> Ellipsis t -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ellipsis t))
$cUntil :: Constr
$tEllipsis :: DataType
gmapMo :: (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 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 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 :: 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 d. Data d => d -> u) -> Ellipsis t -> [u]
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> Ellipsis t -> [u]
gmapQr :: (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 :: (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 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 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 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 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)
$cp1Data :: forall t. Data t => Typeable (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 x. Term_ e -> Rep (Term_ e) x)
-> (forall x. Rep (Term_ e) x -> Term_ e) -> Generic (Term_ e)
forall x. Rep (Term_ e) x -> Term_ e
forall x. Term_ e -> Rep (Term_ e) x
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 :: (Term_ e -> f (Term_ e)) -> Term_ e -> f (Term_ e)
plate = (Term_ e -> f (Term_ e)) -> Term_ e -> f (Term_ e)
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 x. Link_ e -> Rep (Link_ e) x)
-> (forall x. Rep (Link_ e) x -> Link_ e) -> Generic (Link_ e)
forall x. Rep (Link_ e) x -> Link_ e
forall x. Link_ e -> Rep (Link_ e) x
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 x. Qual_ e -> Rep (Qual_ e) x)
-> (forall x. Rep (Qual_ e) x -> Qual_ e) -> Generic (Qual_ e)
forall x. Rep (Qual_ e) x -> Qual_ e
forall x. Qual_ e -> Rep (Qual_ e) x
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 x. Binding_ e -> Rep (Binding_ e) x)
-> (forall x. Rep (Binding_ e) x -> Binding_ e)
-> Generic (Binding_ e)
forall x. Rep (Binding_ e) x -> Binding_ e
forall x. Binding_ e -> Rep (Binding_ e) x
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 x. Guard_ e -> Rep (Guard_ e) x)
-> (forall x. Rep (Guard_ e) x -> Guard_ e) -> Generic (Guard_ e)
forall x. Rep (Guard_ e) x -> Guard_ e
forall x. Guard_ e -> Rep (Guard_ e) x
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
XPattern_ :: X_Pattern e -> Pattern_ e
deriving ((forall x. Pattern_ e -> Rep (Pattern_ e) x)
-> (forall x. Rep (Pattern_ e) x -> Pattern_ e)
-> Generic (Pattern_ e)
forall x. Rep (Pattern_ e) x -> Pattern_ e
forall x. Pattern_ e -> Rep (Pattern_ e) x
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. Quantifier -> Rep Quantifier x)
-> (forall x. Rep Quantifier x -> Quantifier) -> Generic Quantifier
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
DataType
Constr
Typeable Quantifier
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quantifier -> c Quantifier)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quantifier)
-> (Quantifier -> Constr)
-> (Quantifier -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Quantifier -> Quantifier)
-> (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 u. (forall d. Data d => d -> u) -> Quantifier -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Quantifier -> u)
-> (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 (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quantifier -> m Quantifier)
-> Data Quantifier
Quantifier -> DataType
Quantifier -> Constr
(forall b. Data b => b -> b) -> Quantifier -> Quantifier
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quantifier -> c Quantifier
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cAll :: Constr
$cEx :: Constr
$cLam :: Constr
$tQuantifier :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Quantifier -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quantifier -> u
gmapQ :: (forall d. Data d => d -> u) -> Quantifier -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Quantifier -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Quantifier
Data, Quantifier -> Quantifier -> Bool
(Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool) -> Eq Quantifier
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
Eq Quantifier
-> (Quantifier -> Quantifier -> Ordering)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Quantifier)
-> (Quantifier -> Quantifier -> Quantifier)
-> Ord 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
$cp1Ord :: Eq Quantifier
Ord, Int -> Quantifier -> ShowS
[Quantifier] -> ShowS
Quantifier -> String
(Int -> Quantifier -> ShowS)
-> (Quantifier -> String)
-> ([Quantifier] -> ShowS)
-> Show Quantifier
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Quantifier] -> ShowS
$cshowList :: [Quantifier] -> ShowS
show :: Quantifier -> String
$cshow :: Quantifier -> String
showsPrec :: Int -> Quantifier -> ShowS
$cshowsPrec :: Int -> Quantifier -> ShowS
Show, Show Quantifier
Show Quantifier
-> (AlphaCtx -> Quantifier -> Quantifier -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Quantifier -> f Quantifier)
-> (AlphaCtx -> NamePatFind -> Quantifier -> Quantifier)
-> (AlphaCtx -> NthPatFind -> Quantifier -> Quantifier)
-> (Quantifier -> DisjointSet AnyName)
-> (Quantifier -> All)
-> (Quantifier -> Bool)
-> (Quantifier -> NthPatFind)
-> (Quantifier -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Quantifier -> Quantifier)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Quantifier -> (Quantifier -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Quantifier -> m (Quantifier, Perm AnyName))
-> (AlphaCtx -> Quantifier -> Quantifier -> Ordering)
-> Alpha 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' :: AlphaCtx -> Quantifier -> m (Quantifier, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Quantifier -> m (Quantifier, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show Quantifier
Alpha, Subst Type)
type Property_ e = Term_ e
instance Alpha Void