{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Disco.Types (
BaseTy (..),
isCtr,
Var (..),
Ilk (..),
pattern U,
pattern S,
Atom (..),
isVar,
isBase,
isSkolem,
UAtom (..),
uisVar,
uatomToAtom,
uatomToEither,
Con (..),
pattern CList,
pattern CBag,
pattern CSet,
Type (..),
pattern TyVar,
pattern TySkolem,
pattern TyVoid,
pattern TyUnit,
pattern TyBool,
pattern TyProp,
pattern TyN,
pattern TyZ,
pattern TyF,
pattern TyQ,
pattern TyC,
pattern (:->:),
pattern (:*:),
pattern (:+:),
pattern TyList,
pattern TyBag,
pattern TySet,
pattern TyGraph,
pattern TyMap,
pattern TyContainer,
pattern TyUser,
pattern TyString,
PolyType (..),
toPolyType,
closeType,
isNumTy,
isEmptyTy,
isFiniteTy,
isSearchable,
Substitution,
atomToTypeSubst,
uatomToTypeSubst,
Strictness (..),
strictness,
isTyVar,
containerVars,
countType,
unpair,
S,
TyDefBody (..),
TyDefCtx,
HasType (..),
)
where
import Data.Coerce
import Data.Data (Data)
import Disco.Data ()
import GHC.Generics (Generic)
import Unbound.Generics.LocallyNameless hiding (lunbind)
import Control.Lens (toListOf)
import Data.List (nub)
import Data.Map (Map)
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
import Data.Void
import Math.Combinatorics.Exact.Binomial (choose)
import Disco.Effects.LFresh
import Disco.Pretty hiding ((<>))
import Disco.Subst (Substitution)
import Disco.Types.Qualifiers
data BaseTy where
Void :: BaseTy
Unit :: BaseTy
B :: BaseTy
P :: BaseTy
N :: BaseTy
Z :: BaseTy
F :: BaseTy
Q :: BaseTy
C :: BaseTy
CtrSet :: BaseTy
CtrBag :: BaseTy
CtrList :: BaseTy
deriving (Int -> BaseTy -> ShowS
[BaseTy] -> ShowS
BaseTy -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BaseTy] -> ShowS
$cshowList :: [BaseTy] -> ShowS
show :: BaseTy -> String
$cshow :: BaseTy -> String
showsPrec :: Int -> BaseTy -> ShowS
$cshowsPrec :: Int -> BaseTy -> ShowS
Show, BaseTy -> BaseTy -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BaseTy -> BaseTy -> Bool
$c/= :: BaseTy -> BaseTy -> Bool
== :: BaseTy -> BaseTy -> Bool
$c== :: BaseTy -> BaseTy -> Bool
Eq, Eq BaseTy
BaseTy -> BaseTy -> Bool
BaseTy -> BaseTy -> Ordering
BaseTy -> BaseTy -> BaseTy
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 :: BaseTy -> BaseTy -> BaseTy
$cmin :: BaseTy -> BaseTy -> BaseTy
max :: BaseTy -> BaseTy -> BaseTy
$cmax :: BaseTy -> BaseTy -> BaseTy
>= :: BaseTy -> BaseTy -> Bool
$c>= :: BaseTy -> BaseTy -> Bool
> :: BaseTy -> BaseTy -> Bool
$c> :: BaseTy -> BaseTy -> Bool
<= :: BaseTy -> BaseTy -> Bool
$c<= :: BaseTy -> BaseTy -> Bool
< :: BaseTy -> BaseTy -> Bool
$c< :: BaseTy -> BaseTy -> Bool
compare :: BaseTy -> BaseTy -> Ordering
$ccompare :: BaseTy -> BaseTy -> Ordering
Ord, forall x. Rep BaseTy x -> BaseTy
forall x. BaseTy -> Rep BaseTy x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BaseTy x -> BaseTy
$cfrom :: forall x. BaseTy -> Rep BaseTy x
Generic, Typeable BaseTy
BaseTy -> DataType
BaseTy -> Constr
(forall b. Data b => b -> b) -> BaseTy -> BaseTy
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) -> BaseTy -> u
forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
gmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
$cgmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
dataTypeOf :: BaseTy -> DataType
$cdataTypeOf :: BaseTy -> DataType
toConstr :: BaseTy -> Constr
$ctoConstr :: BaseTy -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
Data, Show BaseTy
AlphaCtx -> NthPatFind -> BaseTy -> BaseTy
AlphaCtx -> NamePatFind -> BaseTy -> BaseTy
AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy
AlphaCtx -> BaseTy -> BaseTy -> Bool
AlphaCtx -> BaseTy -> BaseTy -> Ordering
BaseTy -> Bool
BaseTy -> All
BaseTy -> DisjointSet AnyName
BaseTy -> NthPatFind
BaseTy -> 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) -> BaseTy -> f BaseTy
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> BaseTy -> BaseTy -> Ordering
$cacompare' :: AlphaCtx -> BaseTy -> BaseTy -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy
$cswaps' :: AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy
namePatFind :: BaseTy -> NamePatFind
$cnamePatFind :: BaseTy -> NamePatFind
nthPatFind :: BaseTy -> NthPatFind
$cnthPatFind :: BaseTy -> NthPatFind
isEmbed :: BaseTy -> Bool
$cisEmbed :: BaseTy -> Bool
isTerm :: BaseTy -> All
$cisTerm :: BaseTy -> All
isPat :: BaseTy -> DisjointSet AnyName
$cisPat :: BaseTy -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> BaseTy -> BaseTy
$copen :: AlphaCtx -> NthPatFind -> BaseTy -> BaseTy
close :: AlphaCtx -> NamePatFind -> BaseTy -> BaseTy
$cclose :: AlphaCtx -> NamePatFind -> BaseTy -> BaseTy
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BaseTy -> f BaseTy
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BaseTy -> f BaseTy
aeq' :: AlphaCtx -> BaseTy -> BaseTy -> Bool
$caeq' :: AlphaCtx -> BaseTy -> BaseTy -> Bool
Alpha, Subst BaseTy, Subst Atom, Subst UAtom, Subst Type)
instance Pretty BaseTy where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
BaseTy -> Sem r (Doc ann)
pretty = \case
BaseTy
Void -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Void"
BaseTy
Unit -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Unit"
BaseTy
B -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Bool"
BaseTy
P -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Prop"
BaseTy
N -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"ℕ"
BaseTy
Z -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"ℤ"
BaseTy
Q -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"ℚ"
BaseTy
F -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"𝔽"
BaseTy
C -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Char"
BaseTy
CtrList -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"List"
BaseTy
CtrBag -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Bag"
BaseTy
CtrSet -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Set"
isCtr :: BaseTy -> Bool
isCtr :: BaseTy -> Bool
isCtr = (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BaseTy
CtrSet, BaseTy
CtrBag, BaseTy
CtrList])
data Ilk = Skolem | Unification
deriving (Ilk -> Ilk -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ilk -> Ilk -> Bool
$c/= :: Ilk -> Ilk -> Bool
== :: Ilk -> Ilk -> Bool
$c== :: Ilk -> Ilk -> Bool
Eq, Eq Ilk
Ilk -> Ilk -> Bool
Ilk -> Ilk -> Ordering
Ilk -> Ilk -> Ilk
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 :: Ilk -> Ilk -> Ilk
$cmin :: Ilk -> Ilk -> Ilk
max :: Ilk -> Ilk -> Ilk
$cmax :: Ilk -> Ilk -> Ilk
>= :: Ilk -> Ilk -> Bool
$c>= :: Ilk -> Ilk -> Bool
> :: Ilk -> Ilk -> Bool
$c> :: Ilk -> Ilk -> Bool
<= :: Ilk -> Ilk -> Bool
$c<= :: Ilk -> Ilk -> Bool
< :: Ilk -> Ilk -> Bool
$c< :: Ilk -> Ilk -> Bool
compare :: Ilk -> Ilk -> Ordering
$ccompare :: Ilk -> Ilk -> Ordering
Ord, ReadPrec [Ilk]
ReadPrec Ilk
Int -> ReadS Ilk
ReadS [Ilk]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Ilk]
$creadListPrec :: ReadPrec [Ilk]
readPrec :: ReadPrec Ilk
$creadPrec :: ReadPrec Ilk
readList :: ReadS [Ilk]
$creadList :: ReadS [Ilk]
readsPrec :: Int -> ReadS Ilk
$creadsPrec :: Int -> ReadS Ilk
Read, Int -> Ilk -> ShowS
[Ilk] -> ShowS
Ilk -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ilk] -> ShowS
$cshowList :: [Ilk] -> ShowS
show :: Ilk -> String
$cshow :: Ilk -> String
showsPrec :: Int -> Ilk -> ShowS
$cshowsPrec :: Int -> Ilk -> ShowS
Show, forall x. Rep Ilk x -> Ilk
forall x. Ilk -> Rep Ilk x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Ilk x -> Ilk
$cfrom :: forall x. Ilk -> Rep Ilk x
Generic, Typeable Ilk
Ilk -> DataType
Ilk -> Constr
(forall b. Data b => b -> b) -> Ilk -> Ilk
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) -> Ilk -> u
forall u. (forall d. Data d => d -> u) -> Ilk -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ilk
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ilk -> c Ilk
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ilk)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ilk)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ilk -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ilk -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Ilk -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Ilk -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
gmapT :: (forall b. Data b => b -> b) -> Ilk -> Ilk
$cgmapT :: (forall b. Data b => b -> b) -> Ilk -> Ilk
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ilk)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ilk)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ilk)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ilk)
dataTypeOf :: Ilk -> DataType
$cdataTypeOf :: Ilk -> DataType
toConstr :: Ilk -> Constr
$ctoConstr :: Ilk -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ilk
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ilk
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ilk -> c Ilk
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ilk -> c Ilk
Data, Show Ilk
AlphaCtx -> NthPatFind -> Ilk -> Ilk
AlphaCtx -> NamePatFind -> Ilk -> Ilk
AlphaCtx -> Perm AnyName -> Ilk -> Ilk
AlphaCtx -> Ilk -> Ilk -> Bool
AlphaCtx -> Ilk -> Ilk -> Ordering
Ilk -> Bool
Ilk -> All
Ilk -> DisjointSet AnyName
Ilk -> NthPatFind
Ilk -> 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) -> Ilk -> f Ilk
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ilk -> m (Ilk, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Ilk -> (Ilk -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Ilk -> Ilk -> Ordering
$cacompare' :: AlphaCtx -> Ilk -> Ilk -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ilk -> m (Ilk, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ilk -> m (Ilk, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Ilk -> (Ilk -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Ilk -> (Ilk -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Ilk -> Ilk
$cswaps' :: AlphaCtx -> Perm AnyName -> Ilk -> Ilk
namePatFind :: Ilk -> NamePatFind
$cnamePatFind :: Ilk -> NamePatFind
nthPatFind :: Ilk -> NthPatFind
$cnthPatFind :: Ilk -> NthPatFind
isEmbed :: Ilk -> Bool
$cisEmbed :: Ilk -> Bool
isTerm :: Ilk -> All
$cisTerm :: Ilk -> All
isPat :: Ilk -> DisjointSet AnyName
$cisPat :: Ilk -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Ilk -> Ilk
$copen :: AlphaCtx -> NthPatFind -> Ilk -> Ilk
close :: AlphaCtx -> NamePatFind -> Ilk -> Ilk
$cclose :: AlphaCtx -> NamePatFind -> Ilk -> Ilk
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ilk -> f Ilk
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ilk -> f Ilk
aeq' :: AlphaCtx -> Ilk -> Ilk -> Bool
$caeq' :: AlphaCtx -> Ilk -> Ilk -> Bool
Alpha, Subst Atom, Subst Type)
instance Pretty Ilk where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Ilk -> Sem r (Doc ann)
pretty = \case
Ilk
Skolem -> Sem r (Doc ann)
"S"
Ilk
Unification -> Sem r (Doc ann)
"U"
data Var where
V :: Ilk -> Name Type -> Var
deriving (Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show, Var -> Var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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 :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
Ord, forall x. Rep Var x -> Var
forall x. Var -> Rep Var x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Var x -> Var
$cfrom :: forall x. Var -> Rep Var x
Generic, Typeable Var
Var -> DataType
Var -> Constr
(forall b. Data b => b -> b) -> Var -> Var
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) -> Var -> u
forall u. (forall d. Data d => d -> u) -> Var -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Var -> m Var
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var -> m Var
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Var
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var -> c Var
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Var)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var -> m Var
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var -> m Var
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var -> m Var
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var -> m Var
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Var -> m Var
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Var -> m Var
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Var -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Var -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Var -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Var -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
gmapT :: (forall b. Data b => b -> b) -> Var -> Var
$cgmapT :: (forall b. Data b => b -> b) -> Var -> Var
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Var)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Var)
dataTypeOf :: Var -> DataType
$cdataTypeOf :: Var -> DataType
toConstr :: Var -> Constr
$ctoConstr :: Var -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Var
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Var
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var -> c Var
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var -> c Var
Data, Show Var
AlphaCtx -> NthPatFind -> Var -> Var
AlphaCtx -> NamePatFind -> Var -> Var
AlphaCtx -> Perm AnyName -> Var -> Var
AlphaCtx -> Var -> Var -> Bool
AlphaCtx -> Var -> Var -> Ordering
Var -> Bool
Var -> All
Var -> DisjointSet AnyName
Var -> NthPatFind
Var -> 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) -> Var -> f Var
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Var -> m (Var, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Var -> (Var -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Var -> Var -> Ordering
$cacompare' :: AlphaCtx -> Var -> Var -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Var -> m (Var, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Var -> m (Var, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Var -> (Var -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Var -> (Var -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Var -> Var
$cswaps' :: AlphaCtx -> Perm AnyName -> Var -> Var
namePatFind :: Var -> NamePatFind
$cnamePatFind :: Var -> NamePatFind
nthPatFind :: Var -> NthPatFind
$cnthPatFind :: Var -> NthPatFind
isEmbed :: Var -> Bool
$cisEmbed :: Var -> Bool
isTerm :: Var -> All
$cisTerm :: Var -> All
isPat :: Var -> DisjointSet AnyName
$cisPat :: Var -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Var -> Var
$copen :: AlphaCtx -> NthPatFind -> Var -> Var
close :: AlphaCtx -> NamePatFind -> Var -> Var
$cclose :: AlphaCtx -> NamePatFind -> Var -> Var
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Var -> f Var
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Var -> f Var
aeq' :: AlphaCtx -> Var -> Var -> Bool
$caeq' :: AlphaCtx -> Var -> Var -> Bool
Alpha, Subst Atom, Subst Type)
pattern U :: Name Type -> Var
pattern $bU :: Name Type -> Var
$mU :: forall {r}. Var -> (Name Type -> r) -> ((# #) -> r) -> r
U v = V Unification v
pattern S :: Name Type -> Var
pattern $bS :: Name Type -> Var
$mS :: forall {r}. Var -> (Name Type -> r) -> ((# #) -> r) -> r
S v = V Skolem v
{-# COMPLETE U, S #-}
data Atom where
AVar :: Var -> Atom
ABase :: BaseTy -> Atom
deriving (Int -> Atom -> ShowS
[Atom] -> ShowS
Atom -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Atom] -> ShowS
$cshowList :: [Atom] -> ShowS
show :: Atom -> String
$cshow :: Atom -> String
showsPrec :: Int -> Atom -> ShowS
$cshowsPrec :: Int -> Atom -> ShowS
Show, Atom -> Atom -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Atom -> Atom -> Bool
$c/= :: Atom -> Atom -> Bool
== :: Atom -> Atom -> Bool
$c== :: Atom -> Atom -> Bool
Eq, Eq Atom
Atom -> Atom -> Bool
Atom -> Atom -> Ordering
Atom -> Atom -> Atom
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 :: Atom -> Atom -> Atom
$cmin :: Atom -> Atom -> Atom
max :: Atom -> Atom -> Atom
$cmax :: Atom -> Atom -> Atom
>= :: Atom -> Atom -> Bool
$c>= :: Atom -> Atom -> Bool
> :: Atom -> Atom -> Bool
$c> :: Atom -> Atom -> Bool
<= :: Atom -> Atom -> Bool
$c<= :: Atom -> Atom -> Bool
< :: Atom -> Atom -> Bool
$c< :: Atom -> Atom -> Bool
compare :: Atom -> Atom -> Ordering
$ccompare :: Atom -> Atom -> Ordering
Ord, forall x. Rep Atom x -> Atom
forall x. Atom -> Rep Atom x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Atom x -> Atom
$cfrom :: forall x. Atom -> Rep Atom x
Generic, Typeable Atom
Atom -> DataType
Atom -> Constr
(forall b. Data b => b -> b) -> Atom -> Atom
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) -> Atom -> u
forall u. (forall d. Data d => d -> u) -> Atom -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Atom
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Atom -> c Atom
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Atom)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Atom)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Atom -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Atom -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Atom -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Atom -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
gmapT :: (forall b. Data b => b -> b) -> Atom -> Atom
$cgmapT :: (forall b. Data b => b -> b) -> Atom -> Atom
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Atom)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Atom)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Atom)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Atom)
dataTypeOf :: Atom -> DataType
$cdataTypeOf :: Atom -> DataType
toConstr :: Atom -> Constr
$ctoConstr :: Atom -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Atom
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Atom
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Atom -> c Atom
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Atom -> c Atom
Data, Show Atom
AlphaCtx -> NthPatFind -> Atom -> Atom
AlphaCtx -> NamePatFind -> Atom -> Atom
AlphaCtx -> Perm AnyName -> Atom -> Atom
AlphaCtx -> Atom -> Atom -> Bool
AlphaCtx -> Atom -> Atom -> Ordering
Atom -> Bool
Atom -> All
Atom -> DisjointSet AnyName
Atom -> NthPatFind
Atom -> 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) -> Atom -> f Atom
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Atom -> m (Atom, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Atom -> (Atom -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Atom -> Atom -> Ordering
$cacompare' :: AlphaCtx -> Atom -> Atom -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Atom -> m (Atom, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Atom -> m (Atom, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Atom -> (Atom -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Atom -> (Atom -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Atom -> Atom
$cswaps' :: AlphaCtx -> Perm AnyName -> Atom -> Atom
namePatFind :: Atom -> NamePatFind
$cnamePatFind :: Atom -> NamePatFind
nthPatFind :: Atom -> NthPatFind
$cnthPatFind :: Atom -> NthPatFind
isEmbed :: Atom -> Bool
$cisEmbed :: Atom -> Bool
isTerm :: Atom -> All
$cisTerm :: Atom -> All
isPat :: Atom -> DisjointSet AnyName
$cisPat :: Atom -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Atom -> Atom
$copen :: AlphaCtx -> NthPatFind -> Atom -> Atom
close :: AlphaCtx -> NamePatFind -> Atom -> Atom
$cclose :: AlphaCtx -> NamePatFind -> Atom -> Atom
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Atom -> f Atom
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Atom -> f Atom
aeq' :: AlphaCtx -> Atom -> Atom -> Bool
$caeq' :: AlphaCtx -> Atom -> Atom -> Bool
Alpha, Subst Type)
instance Subst Atom Atom where
isvar :: Atom -> Maybe (SubstName Atom Atom)
isvar (AVar (U Name Type
x)) = forall a. a -> Maybe a
Just (forall a b. (a ~ b) => Name a -> SubstName a b
SubstName (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
x))
isvar Atom
_ = forall a. Maybe a
Nothing
instance Pretty Atom where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Atom -> Sem r (Doc ann)
pretty = \case
AVar (U Name Type
v) -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Type
v
AVar (S Name Type
v) -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"$" forall a. Semigroup a => a -> a -> a
<> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Type
v
ABase BaseTy
b -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty BaseTy
b
isVar :: Atom -> Bool
isVar :: Atom -> Bool
isVar (AVar Var
_) = Bool
True
isVar Atom
_ = Bool
False
isBase :: Atom -> Bool
isBase :: Atom -> Bool
isBase = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom -> Bool
isVar
isSkolem :: Atom -> Bool
isSkolem :: Atom -> Bool
isSkolem (AVar (S Name Type
_)) = Bool
True
isSkolem Atom
_ = Bool
False
data UAtom where
UB :: BaseTy -> UAtom
UV :: Name Type -> UAtom
deriving (Int -> UAtom -> ShowS
[UAtom] -> ShowS
UAtom -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UAtom] -> ShowS
$cshowList :: [UAtom] -> ShowS
show :: UAtom -> String
$cshow :: UAtom -> String
showsPrec :: Int -> UAtom -> ShowS
$cshowsPrec :: Int -> UAtom -> ShowS
Show, UAtom -> UAtom -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UAtom -> UAtom -> Bool
$c/= :: UAtom -> UAtom -> Bool
== :: UAtom -> UAtom -> Bool
$c== :: UAtom -> UAtom -> Bool
Eq, Eq UAtom
UAtom -> UAtom -> Bool
UAtom -> UAtom -> Ordering
UAtom -> UAtom -> UAtom
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 :: UAtom -> UAtom -> UAtom
$cmin :: UAtom -> UAtom -> UAtom
max :: UAtom -> UAtom -> UAtom
$cmax :: UAtom -> UAtom -> UAtom
>= :: UAtom -> UAtom -> Bool
$c>= :: UAtom -> UAtom -> Bool
> :: UAtom -> UAtom -> Bool
$c> :: UAtom -> UAtom -> Bool
<= :: UAtom -> UAtom -> Bool
$c<= :: UAtom -> UAtom -> Bool
< :: UAtom -> UAtom -> Bool
$c< :: UAtom -> UAtom -> Bool
compare :: UAtom -> UAtom -> Ordering
$ccompare :: UAtom -> UAtom -> Ordering
Ord, forall x. Rep UAtom x -> UAtom
forall x. UAtom -> Rep UAtom x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep UAtom x -> UAtom
$cfrom :: forall x. UAtom -> Rep UAtom x
Generic, Show UAtom
AlphaCtx -> NthPatFind -> UAtom -> UAtom
AlphaCtx -> NamePatFind -> UAtom -> UAtom
AlphaCtx -> Perm AnyName -> UAtom -> UAtom
AlphaCtx -> UAtom -> UAtom -> Bool
AlphaCtx -> UAtom -> UAtom -> Ordering
UAtom -> Bool
UAtom -> All
UAtom -> DisjointSet AnyName
UAtom -> NthPatFind
UAtom -> 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) -> UAtom -> f UAtom
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UAtom -> m (UAtom, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> UAtom -> (UAtom -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> UAtom -> UAtom -> Ordering
$cacompare' :: AlphaCtx -> UAtom -> UAtom -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UAtom -> m (UAtom, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UAtom -> m (UAtom, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> UAtom -> (UAtom -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> UAtom -> (UAtom -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> UAtom -> UAtom
$cswaps' :: AlphaCtx -> Perm AnyName -> UAtom -> UAtom
namePatFind :: UAtom -> NamePatFind
$cnamePatFind :: UAtom -> NamePatFind
nthPatFind :: UAtom -> NthPatFind
$cnthPatFind :: UAtom -> NthPatFind
isEmbed :: UAtom -> Bool
$cisEmbed :: UAtom -> Bool
isTerm :: UAtom -> All
$cisTerm :: UAtom -> All
isPat :: UAtom -> DisjointSet AnyName
$cisPat :: UAtom -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> UAtom -> UAtom
$copen :: AlphaCtx -> NthPatFind -> UAtom -> UAtom
close :: AlphaCtx -> NamePatFind -> UAtom -> UAtom
$cclose :: AlphaCtx -> NamePatFind -> UAtom -> UAtom
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> UAtom -> f UAtom
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> UAtom -> f UAtom
aeq' :: AlphaCtx -> UAtom -> UAtom -> Bool
$caeq' :: AlphaCtx -> UAtom -> UAtom -> Bool
Alpha, Subst BaseTy)
instance Subst UAtom UAtom where
isvar :: UAtom -> Maybe (SubstName UAtom UAtom)
isvar (UV Name Type
x) = forall a. a -> Maybe a
Just (forall a b. (a ~ b) => Name a -> SubstName a b
SubstName (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
x))
isvar UAtom
_ = forall a. Maybe a
Nothing
instance Pretty UAtom where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
UAtom -> Sem r (Doc ann)
pretty (UB BaseTy
b) = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty BaseTy
b
pretty (UV Name Type
n) = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Type
n
uisVar :: UAtom -> Bool
uisVar :: UAtom -> Bool
uisVar (UV Name Type
_) = Bool
True
uisVar UAtom
_ = Bool
False
uatomToAtom :: UAtom -> Atom
uatomToAtom :: UAtom -> Atom
uatomToAtom (UB BaseTy
b) = BaseTy -> Atom
ABase BaseTy
b
uatomToAtom (UV Name Type
x) = Var -> Atom
AVar (Name Type -> Var
U Name Type
x)
uatomToEither :: UAtom -> Either BaseTy (Name Type)
uatomToEither :: UAtom -> Either BaseTy (Name Type)
uatomToEither (UB BaseTy
b) = forall a b. a -> Either a b
Left BaseTy
b
uatomToEither (UV Name Type
v) = forall a b. b -> Either a b
Right Name Type
v
data Con where
CArr :: Con
CProd :: Con
CSum :: Con
CContainer :: Atom -> Con
CMap :: Con
CGraph :: Con
CUser :: String -> Con
deriving (Int -> Con -> ShowS
[Con] -> ShowS
Con -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Con] -> ShowS
$cshowList :: [Con] -> ShowS
show :: Con -> String
$cshow :: Con -> String
showsPrec :: Int -> Con -> ShowS
$cshowsPrec :: Int -> Con -> ShowS
Show, Con -> Con -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Con -> Con -> Bool
$c/= :: Con -> Con -> Bool
== :: Con -> Con -> Bool
$c== :: Con -> Con -> Bool
Eq, Eq Con
Con -> Con -> Bool
Con -> Con -> Ordering
Con -> Con -> Con
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 :: Con -> Con -> Con
$cmin :: Con -> Con -> Con
max :: Con -> Con -> Con
$cmax :: Con -> Con -> Con
>= :: Con -> Con -> Bool
$c>= :: Con -> Con -> Bool
> :: Con -> Con -> Bool
$c> :: Con -> Con -> Bool
<= :: Con -> Con -> Bool
$c<= :: Con -> Con -> Bool
< :: Con -> Con -> Bool
$c< :: Con -> Con -> Bool
compare :: Con -> Con -> Ordering
$ccompare :: Con -> Con -> Ordering
Ord, forall x. Rep Con x -> Con
forall x. Con -> Rep Con x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Con x -> Con
$cfrom :: forall x. Con -> Rep Con x
Generic, Typeable Con
Con -> DataType
Con -> Constr
(forall b. Data b => b -> b) -> Con -> Con
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) -> Con -> u
forall u. (forall d. Data d => d -> u) -> Con -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Con -> m Con
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Con
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Con)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Con -> m Con
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Con -> m Con
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Con -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Con -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Con -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Con -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
gmapT :: (forall b. Data b => b -> b) -> Con -> Con
$cgmapT :: (forall b. Data b => b -> b) -> Con -> Con
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Con)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Con)
dataTypeOf :: Con -> DataType
$cdataTypeOf :: Con -> DataType
toConstr :: Con -> Constr
$ctoConstr :: Con -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Con
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Con
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con
Data, Show Con
AlphaCtx -> NthPatFind -> Con -> Con
AlphaCtx -> NamePatFind -> Con -> Con
AlphaCtx -> Perm AnyName -> Con -> Con
AlphaCtx -> Con -> Con -> Bool
AlphaCtx -> Con -> Con -> Ordering
Con -> Bool
Con -> All
Con -> DisjointSet AnyName
Con -> NthPatFind
Con -> 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) -> Con -> f Con
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Con -> Con -> Ordering
$cacompare' :: AlphaCtx -> Con -> Con -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Con -> Con
$cswaps' :: AlphaCtx -> Perm AnyName -> Con -> Con
namePatFind :: Con -> NamePatFind
$cnamePatFind :: Con -> NamePatFind
nthPatFind :: Con -> NthPatFind
$cnthPatFind :: Con -> NthPatFind
isEmbed :: Con -> Bool
$cisEmbed :: Con -> Bool
isTerm :: Con -> All
$cisTerm :: Con -> All
isPat :: Con -> DisjointSet AnyName
$cisPat :: Con -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Con -> Con
$copen :: AlphaCtx -> NthPatFind -> Con -> Con
close :: AlphaCtx -> NamePatFind -> Con -> Con
$cclose :: AlphaCtx -> NamePatFind -> Con -> Con
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con
aeq' :: AlphaCtx -> Con -> Con -> Bool
$caeq' :: AlphaCtx -> Con -> Con -> Bool
Alpha)
instance Pretty Con where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Con -> Sem r (Doc ann)
pretty = \case
Con
CMap -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Map"
Con
CGraph -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Graph"
CUser String
s -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s
Con
CList -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"List"
Con
CBag -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Bag"
Con
CSet -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Set"
CContainer Atom
v -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Atom
v
Con
c -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible: got Con " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Con
c forall a. [a] -> [a] -> [a]
++ String
" in pretty @Con"
pattern CList :: Con
pattern $bCList :: Con
$mCList :: forall {r}. Con -> ((# #) -> r) -> ((# #) -> r) -> r
CList = CContainer (ABase CtrList)
pattern CBag :: Con
pattern $bCBag :: Con
$mCBag :: forall {r}. Con -> ((# #) -> r) -> ((# #) -> r) -> r
CBag = CContainer (ABase CtrBag)
pattern CSet :: Con
pattern $bCSet :: Con
$mCSet :: forall {r}. Con -> ((# #) -> r) -> ((# #) -> r) -> r
CSet = CContainer (ABase CtrSet)
{-# COMPLETE CArr, CProd, CSum, CList, CBag, CSet, CGraph, CMap, CUser #-}
data Type where
TyAtom :: Atom -> Type
TyCon :: Con -> [Type] -> Type
deriving (Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show, Type -> Type -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq, Eq Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
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 :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c< :: Type -> Type -> Bool
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
Ord, forall x. Rep Type x -> Type
forall x. Type -> Rep Type x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Type x -> Type
$cfrom :: forall x. Type -> Rep Type x
Generic, Typeable Type
Type -> DataType
Type -> Constr
(forall b. Data b => b -> b) -> Type -> Type
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) -> Type -> u
forall u. (forall d. Data d => d -> u) -> Type -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapT :: (forall b. Data b => b -> b) -> Type -> Type
$cgmapT :: (forall b. Data b => b -> b) -> Type -> Type
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
dataTypeOf :: Type -> DataType
$cdataTypeOf :: Type -> DataType
toConstr :: Type -> Constr
$ctoConstr :: Type -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
Data, Show Type
AlphaCtx -> NthPatFind -> Type -> Type
AlphaCtx -> NamePatFind -> Type -> Type
AlphaCtx -> Perm AnyName -> Type -> Type
AlphaCtx -> Type -> Type -> Bool
AlphaCtx -> Type -> Type -> Ordering
Type -> Bool
Type -> All
Type -> DisjointSet AnyName
Type -> NthPatFind
Type -> 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) -> Type -> f Type
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Type -> Type -> Ordering
$cacompare' :: AlphaCtx -> Type -> Type -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Type -> Type
$cswaps' :: AlphaCtx -> Perm AnyName -> Type -> Type
namePatFind :: Type -> NamePatFind
$cnamePatFind :: Type -> NamePatFind
nthPatFind :: Type -> NthPatFind
$cnthPatFind :: Type -> NthPatFind
isEmbed :: Type -> Bool
$cisEmbed :: Type -> Bool
isTerm :: Type -> All
$cisTerm :: Type -> All
isPat :: Type -> DisjointSet AnyName
$cisPat :: Type -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Type -> Type
$copen :: AlphaCtx -> NthPatFind -> Type -> Type
close :: AlphaCtx -> NamePatFind -> Type -> Type
$cclose :: AlphaCtx -> NamePatFind -> Type -> Type
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Type -> f Type
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Type -> f Type
aeq' :: AlphaCtx -> Type -> Type -> Bool
$caeq' :: AlphaCtx -> Type -> Type -> Bool
Alpha)
instance Pretty Type where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
pretty (TyAtom Atom
a) = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Atom
a
pretty (Type
ty1 :->: Type
ty2) =
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
tarrPA forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"→" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2)
pretty (Type
ty1 :*: Type
ty2) =
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
tmulPA forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"×" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2)
pretty (Type
ty1 :+: Type
ty2) =
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
taddPA forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"+" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2)
pretty (TyCon Con
c []) = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Con
c
pretty (TyCon Con
c [Type]
tys) = do
[Sem r (Doc ann)]
ds <- forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Type]
tys)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Con
c forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds)
instance Subst Type Qualifier
instance Subst Type Rational where
subst :: Name Type -> Type -> Rational -> Rational
subst Name Type
_ Type
_ = forall a. a -> a
id
substs :: [(Name Type, Type)] -> Rational -> Rational
substs [(Name Type, Type)]
_ = forall a. a -> a
id
instance Subst Type Void where
subst :: Name Type -> Type -> Void -> Void
subst Name Type
_ Type
_ = forall a. a -> a
id
substs :: [(Name Type, Type)] -> Void -> Void
substs [(Name Type, Type)]
_ = forall a. a -> a
id
instance Subst Type Con where
isCoerceVar :: Con -> Maybe (SubstCoerce Con Type)
isCoerceVar (CContainer (AVar (U Name Type
x))) =
forall a. a -> Maybe a
Just (forall b a. Name b -> (b -> Maybe a) -> SubstCoerce a b
SubstCoerce Name Type
x Type -> Maybe Con
substCtrTy)
where
substCtrTy :: Type -> Maybe Con
substCtrTy (TyAtom Atom
a) = forall a. a -> Maybe a
Just (Atom -> Con
CContainer Atom
a)
substCtrTy Type
_ = forall a. Maybe a
Nothing
isCoerceVar Con
_ = forall a. Maybe a
Nothing
instance Subst Type Type where
isvar :: Type -> Maybe (SubstName Type Type)
isvar (TyAtom (AVar (U Name Type
x))) = forall a. a -> Maybe a
Just (forall a b. (a ~ b) => Name a -> SubstName a b
SubstName Name Type
x)
isvar Type
_ = forall a. Maybe a
Nothing
pattern TyVar :: Name Type -> Type
pattern $bTyVar :: Name Type -> Type
$mTyVar :: forall {r}. Type -> (Name Type -> r) -> ((# #) -> r) -> r
TyVar v = TyAtom (AVar (U v))
pattern TySkolem :: Name Type -> Type
pattern $bTySkolem :: Name Type -> Type
$mTySkolem :: forall {r}. Type -> (Name Type -> r) -> ((# #) -> r) -> r
TySkolem v = TyAtom (AVar (S v))
pattern TyVoid :: Type
pattern $bTyVoid :: Type
$mTyVoid :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyVoid = TyAtom (ABase Void)
pattern TyUnit :: Type
pattern $bTyUnit :: Type
$mTyUnit :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyUnit = TyAtom (ABase Unit)
pattern TyBool :: Type
pattern $bTyBool :: Type
$mTyBool :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyBool = TyAtom (ABase B)
pattern TyProp :: Type
pattern $bTyProp :: Type
$mTyProp :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyProp = TyAtom (ABase P)
pattern TyN :: Type
pattern $bTyN :: Type
$mTyN :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyN = TyAtom (ABase N)
pattern TyZ :: Type
pattern $bTyZ :: Type
$mTyZ :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyZ = TyAtom (ABase Z)
pattern TyF :: Type
pattern $bTyF :: Type
$mTyF :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyF = TyAtom (ABase F)
pattern TyQ :: Type
pattern $bTyQ :: Type
$mTyQ :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyQ = TyAtom (ABase Q)
pattern TyC :: Type
pattern $bTyC :: Type
$mTyC :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyC = TyAtom (ABase C)
infixr 5 :->:
pattern (:->:) :: Type -> Type -> Type
pattern $b:->: :: Type -> Type -> Type
$m:->: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
(:->:) ty1 ty2 = TyCon CArr [ty1, ty2]
infixr 7 :*:
pattern (:*:) :: Type -> Type -> Type
pattern $b:*: :: Type -> Type -> Type
$m:*: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
(:*:) ty1 ty2 = TyCon CProd [ty1, ty2]
infixr 6 :+:
pattern (:+:) :: Type -> Type -> Type
pattern $b:+: :: Type -> Type -> Type
$m:+: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
(:+:) ty1 ty2 = TyCon CSum [ty1, ty2]
pattern TyList :: Type -> Type
pattern $bTyList :: Type -> Type
$mTyList :: forall {r}. Type -> (Type -> r) -> ((# #) -> r) -> r
TyList elTy = TyCon CList [elTy]
pattern TyBag :: Type -> Type
pattern $bTyBag :: Type -> Type
$mTyBag :: forall {r}. Type -> (Type -> r) -> ((# #) -> r) -> r
TyBag elTy = TyCon CBag [elTy]
pattern TySet :: Type -> Type
pattern $bTySet :: Type -> Type
$mTySet :: forall {r}. Type -> (Type -> r) -> ((# #) -> r) -> r
TySet elTy = TyCon CSet [elTy]
pattern TyContainer :: Atom -> Type -> Type
pattern $bTyContainer :: Atom -> Type -> Type
$mTyContainer :: forall {r}. Type -> (Atom -> Type -> r) -> ((# #) -> r) -> r
TyContainer c elTy = TyCon (CContainer c) [elTy]
pattern TyGraph :: Type -> Type
pattern $bTyGraph :: Type -> Type
$mTyGraph :: forall {r}. Type -> (Type -> r) -> ((# #) -> r) -> r
TyGraph elTy = TyCon CGraph [elTy]
pattern TyMap :: Type -> Type -> Type
pattern $bTyMap :: Type -> Type -> Type
$mTyMap :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
TyMap tyKey tyValue = TyCon CMap [tyKey, tyValue]
pattern TyUser :: String -> [Type] -> Type
pattern $bTyUser :: String -> [Type] -> Type
$mTyUser :: forall {r}. Type -> (String -> [Type] -> r) -> ((# #) -> r) -> r
TyUser nm args = TyCon (CUser nm) args
pattern TyString :: Type
pattern $bTyString :: Type
$mTyString :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyString = TyList TyC
{-# COMPLETE
TyVar
, TySkolem
, TyVoid
, TyUnit
, TyBool
, TyProp
, TyN
, TyZ
, TyF
, TyQ
, TyC
, (:->:)
, (:*:)
, (:+:)
, TyList
, TyBag
, TySet
, TyGraph
, TyMap
, TyUser
#-}
isTyVar :: Type -> Bool
isTyVar :: Type -> Bool
isTyVar (TyAtom (AVar Var
_)) = Bool
True
isTyVar Type
_ = Bool
False
instance (Ord a, Subst t a) => Subst t (Set a) where
subst :: Name t -> t -> Set a -> Set a
subst Name t
x t
t = forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (forall b a. Subst b a => Name b -> b -> a -> a
subst Name t
x t
t)
substs :: [(Name t, t)] -> Set a -> Set a
substs [(Name t, t)]
s = forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (forall b a. Subst b a => [(Name b, b)] -> a -> a
substs [(Name t, t)]
s)
instance (Ord k, Subst t a) => Subst t (Map k a) where
subst :: Name t -> t -> Map k a -> Map k a
subst Name t
x t
t = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall b a. Subst b a => Name b -> b -> a -> a
subst Name t
x t
t)
substs :: [(Name t, t)] -> Map k a -> Map k a
substs [(Name t, t)]
s = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall b a. Subst b a => [(Name b, b)] -> a -> a
substs [(Name t, t)]
s)
data TyDefBody = TyDefBody [String] ([Type] -> Type)
instance Show TyDefBody where
show :: TyDefBody -> String
show TyDefBody
_ = String
"<tydef>"
type TyDefCtx = M.Map String TyDefBody
instance Pretty (String, TyDefBody) where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
(String, TyDefBody) -> Sem r (Doc ann)
pretty (String
tyName, TyDefBody [String]
ps [Type] -> Type
body) =
Sem r (Doc ann)
"type" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
tyName forall a. Semigroup a => a -> a -> a
<> [String] -> Sem r (Doc ann)
prettyArgs [String]
ps) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty ([Type] -> Type
body (forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Type
TyVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> Name a
string2Name) [String]
ps))
where
prettyArgs :: [String] -> Sem r (Doc ann)
prettyArgs [] = forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty
prettyArgs [String]
_ = do
[Sem r (Doc ann)]
ds <- forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text [String]
ps)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds)
newtype PolyType = Forall (Bind [Name Type] Type)
deriving (Int -> PolyType -> ShowS
[PolyType] -> ShowS
PolyType -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PolyType] -> ShowS
$cshowList :: [PolyType] -> ShowS
show :: PolyType -> String
$cshow :: PolyType -> String
showsPrec :: Int -> PolyType -> ShowS
$cshowsPrec :: Int -> PolyType -> ShowS
Show, forall x. Rep PolyType x -> PolyType
forall x. PolyType -> Rep PolyType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PolyType x -> PolyType
$cfrom :: forall x. PolyType -> Rep PolyType x
Generic, Typeable PolyType
PolyType -> DataType
PolyType -> Constr
(forall b. Data b => b -> b) -> PolyType -> PolyType
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) -> PolyType -> u
forall u. (forall d. Data d => d -> u) -> PolyType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PolyType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PolyType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> PolyType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PolyType -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
gmapT :: (forall b. Data b => b -> b) -> PolyType -> PolyType
$cgmapT :: (forall b. Data b => b -> b) -> PolyType -> PolyType
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PolyType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PolyType)
dataTypeOf :: PolyType -> DataType
$cdataTypeOf :: PolyType -> DataType
toConstr :: PolyType -> Constr
$ctoConstr :: PolyType -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PolyType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PolyType
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType
Data, Show PolyType
AlphaCtx -> NthPatFind -> PolyType -> PolyType
AlphaCtx -> NamePatFind -> PolyType -> PolyType
AlphaCtx -> Perm AnyName -> PolyType -> PolyType
AlphaCtx -> PolyType -> PolyType -> Bool
AlphaCtx -> PolyType -> PolyType -> Ordering
PolyType -> Bool
PolyType -> All
PolyType -> DisjointSet AnyName
PolyType -> NthPatFind
PolyType -> 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) -> PolyType -> f PolyType
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> PolyType -> PolyType -> Ordering
$cacompare' :: AlphaCtx -> PolyType -> PolyType -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> PolyType -> PolyType
$cswaps' :: AlphaCtx -> Perm AnyName -> PolyType -> PolyType
namePatFind :: PolyType -> NamePatFind
$cnamePatFind :: PolyType -> NamePatFind
nthPatFind :: PolyType -> NthPatFind
$cnthPatFind :: PolyType -> NthPatFind
isEmbed :: PolyType -> Bool
$cisEmbed :: PolyType -> Bool
isTerm :: PolyType -> All
$cisTerm :: PolyType -> All
isPat :: PolyType -> DisjointSet AnyName
$cisPat :: PolyType -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> PolyType -> PolyType
$copen :: AlphaCtx -> NthPatFind -> PolyType -> PolyType
close :: AlphaCtx -> NamePatFind -> PolyType -> PolyType
$cclose :: AlphaCtx -> NamePatFind -> PolyType -> PolyType
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType
aeq' :: AlphaCtx -> PolyType -> PolyType -> Bool
$caeq' :: AlphaCtx -> PolyType -> PolyType -> Bool
Alpha, Subst Type)
instance Pretty PolyType where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
PolyType -> Sem r (Doc ann)
pretty (Forall Bind [Name Type] Type
bnd) = forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Name Type] Type
bnd forall a b. (a -> b) -> a -> b
$
\([Name Type]
_, Type
body) -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
body
toPolyType :: Type -> PolyType
toPolyType :: Type -> PolyType
toPolyType Type
ty = Bind [Name Type] Type -> PolyType
Forall (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [] Type
ty)
closeType :: Type -> PolyType
closeType :: Type -> PolyType
closeType Type
ty = Bind [Name Type] Type -> PolyType
Forall (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *) b.
(Alpha a, Typeable b, Contravariant f, Applicative f) =>
(Name b -> f (Name b)) -> a -> f a
fv Type
ty) Type
ty)
countType :: Type -> Maybe Integer
countType :: Type -> Maybe Integer
countType Type
TyVoid = forall a. a -> Maybe a
Just Integer
0
countType Type
TyUnit = forall a. a -> Maybe a
Just Integer
1
countType Type
TyBool = forall a. a -> Maybe a
Just Integer
2
countType Type
TyC = forall a. a -> Maybe a
Just (Integer
17 forall a. Num a => a -> a -> a
* Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
16 :: Integer))
countType (Type
ty1 :+: Type
ty2) = forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Integer
countType Type
ty2
countType (Type
ty1 :*: Type
ty2)
| Type -> Bool
isEmptyTy Type
ty1 = forall a. a -> Maybe a
Just Integer
0
| Type -> Bool
isEmptyTy Type
ty2 = forall a. a -> Maybe a
Just Integer
0
| Bool
otherwise = forall a. Num a => a -> a -> a
(*) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Integer
countType Type
ty2
countType (Type
ty1 :->: Type
ty2) =
case (Type -> Maybe Integer
countType Type
ty1, Type -> Maybe Integer
countType Type
ty2) of
(Just Integer
0, Maybe Integer
_) -> forall a. a -> Maybe a
Just Integer
1
(Maybe Integer
_, Just Integer
0) -> forall a. a -> Maybe a
Just Integer
0
(Maybe Integer
_, Just Integer
1) -> forall a. a -> Maybe a
Just Integer
1
(Maybe Integer
c1, Maybe Integer
c2) -> forall a b. (Num a, Integral b) => a -> b -> a
(^) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
c2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Integer
c1
countType (TyList Type
ty)
| Type -> Bool
isEmptyTy Type
ty = forall a. a -> Maybe a
Just Integer
1
| Bool
otherwise = forall a. Maybe a
Nothing
countType (TyBag Type
ty)
| Type -> Bool
isEmptyTy Type
ty = forall a. a -> Maybe a
Just Integer
1
| Bool
otherwise = forall a. Maybe a
Nothing
countType (TySet Type
ty) = (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty
countType (TyGraph Type
ty) =
(\Integer
t -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Integer
n -> (Integer
t forall a. Integral a => a -> a -> a
`choose` Integer
n) forall a. Num a => a -> a -> a
* Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
n forall a. Num a => a -> a -> a
* Integer
n)) [Integer
0 .. Integer
t])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty
countType (TyMap Type
tyKey Type
tyValue)
| Type -> Bool
isEmptyTy Type
tyKey = forall a. a -> Maybe a
Just Integer
1
| Type -> Bool
isEmptyTy Type
tyValue = forall a. a -> Maybe a
Just Integer
1
| Bool
otherwise = (\Integer
k Integer
v -> (Integer
v forall a. Num a => a -> a -> a
+ Integer
1) forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
k) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
tyKey forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Integer
countType Type
tyValue
countType Type
_ = forall a. Maybe a
Nothing
isNumTy :: Type -> Bool
isNumTy :: Type -> Bool
isNumTy Type
ty = Type
ty forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type
TyN, Type
TyZ, Type
TyF, Type
TyQ]
isEmptyTy :: Type -> Bool
isEmptyTy :: Type -> Bool
isEmptyTy Type
ty
| Just Integer
0 <- Type -> Maybe Integer
countType Type
ty = Bool
True
| Bool
otherwise = Bool
False
isFiniteTy :: Type -> Bool
isFiniteTy :: Type -> Bool
isFiniteTy Type
ty
| Just Integer
_ <- Type -> Maybe Integer
countType Type
ty = Bool
True
| Bool
otherwise = Bool
False
isSearchable :: Type -> Bool
isSearchable :: Type -> Bool
isSearchable Type
TyProp = Bool
False
isSearchable Type
ty
| Type -> Bool
isNumTy Type
ty = Bool
True
| Type -> Bool
isFiniteTy Type
ty = Bool
True
isSearchable (TyList Type
ty) = Type -> Bool
isSearchable Type
ty
isSearchable (TySet Type
ty) = Type -> Bool
isSearchable Type
ty
isSearchable (Type
ty1 :+: Type
ty2) = Type -> Bool
isSearchable Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isSearchable Type
ty2
isSearchable (Type
ty1 :*: Type
ty2) = Type -> Bool
isSearchable Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isSearchable Type
ty2
isSearchable (Type
ty1 :->: Type
ty2) = Type -> Bool
isFiniteTy Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isSearchable Type
ty2
isSearchable Type
_ = Bool
False
data Strictness = Strict | Lazy
deriving (Strictness -> Strictness -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Strictness -> Strictness -> Bool
$c/= :: Strictness -> Strictness -> Bool
== :: Strictness -> Strictness -> Bool
$c== :: Strictness -> Strictness -> Bool
Eq, Int -> Strictness -> ShowS
[Strictness] -> ShowS
Strictness -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Strictness] -> ShowS
$cshowList :: [Strictness] -> ShowS
show :: Strictness -> String
$cshow :: Strictness -> String
showsPrec :: Int -> Strictness -> ShowS
$cshowsPrec :: Int -> Strictness -> ShowS
Show, forall x. Rep Strictness x -> Strictness
forall x. Strictness -> Rep Strictness x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Strictness x -> Strictness
$cfrom :: forall x. Strictness -> Rep Strictness x
Generic, Show Strictness
AlphaCtx -> NthPatFind -> Strictness -> Strictness
AlphaCtx -> NamePatFind -> Strictness -> Strictness
AlphaCtx -> Perm AnyName -> Strictness -> Strictness
AlphaCtx -> Strictness -> Strictness -> Bool
AlphaCtx -> Strictness -> Strictness -> Ordering
Strictness -> Bool
Strictness -> All
Strictness -> DisjointSet AnyName
Strictness -> NthPatFind
Strictness -> 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) -> Strictness -> f Strictness
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Strictness -> m (Strictness, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Strictness -> (Strictness -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Strictness -> Strictness -> Ordering
$cacompare' :: AlphaCtx -> Strictness -> Strictness -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Strictness -> m (Strictness, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Strictness -> m (Strictness, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Strictness -> (Strictness -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Strictness -> (Strictness -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Strictness -> Strictness
$cswaps' :: AlphaCtx -> Perm AnyName -> Strictness -> Strictness
namePatFind :: Strictness -> NamePatFind
$cnamePatFind :: Strictness -> NamePatFind
nthPatFind :: Strictness -> NthPatFind
$cnthPatFind :: Strictness -> NthPatFind
isEmbed :: Strictness -> Bool
$cisEmbed :: Strictness -> Bool
isTerm :: Strictness -> All
$cisTerm :: Strictness -> All
isPat :: Strictness -> DisjointSet AnyName
$cisPat :: Strictness -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Strictness -> Strictness
$copen :: AlphaCtx -> NthPatFind -> Strictness -> Strictness
close :: AlphaCtx -> NamePatFind -> Strictness -> Strictness
$cclose :: AlphaCtx -> NamePatFind -> Strictness -> Strictness
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Strictness -> f Strictness
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Strictness -> f Strictness
aeq' :: AlphaCtx -> Strictness -> Strictness -> Bool
$caeq' :: AlphaCtx -> Strictness -> Strictness -> Bool
Alpha)
strictness :: Type -> Strictness
strictness :: Type -> Strictness
strictness Type
ty
| Type -> Bool
isNumTy Type
ty = Strictness
Strict
| Bool
otherwise = Strictness
Lazy
unpair :: Type -> [Type]
unpair :: Type -> [Type]
unpair (Type
ty1 :*: Type
ty2) = Type
ty1 forall a. a -> [a] -> [a]
: Type -> [Type]
unpair Type
ty2
unpair Type
ty = [Type
ty]
type S = Substitution Type
atomToTypeSubst :: Substitution Atom -> Substitution Type
atomToTypeSubst :: Substitution Atom -> Substitution Type
atomToTypeSubst = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Atom -> Type
TyAtom
uatomToTypeSubst :: Substitution UAtom -> Substitution Type
uatomToTypeSubst :: Substitution UAtom -> Substitution Type
uatomToTypeSubst = Substitution Atom -> Substitution Type
atomToTypeSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UAtom -> Atom
uatomToAtom
containerVars :: Type -> Set (Name Type)
containerVars :: Type -> Set (Name Type)
containerVars (TyCon (CContainer (AVar (U Name Type
x))) [Type]
tys) =
Name Type
x forall a. Ord a => a -> Set a -> Set a
`S.insert` forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Set (Name Type)
containerVars [Type]
tys
containerVars (TyCon Con
_ [Type]
tys) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Set (Name Type)
containerVars [Type]
tys
containerVars Type
_ = forall a. Set a
S.empty
class HasType t where
getType :: t -> Type
setType :: Type -> t -> t
setType Type
_ = forall a. a -> a
id