{-# 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
(Int -> BaseTy -> ShowS)
-> (BaseTy -> String) -> ([BaseTy] -> ShowS) -> Show BaseTy
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
(BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool) -> Eq BaseTy
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
Eq BaseTy
-> (BaseTy -> BaseTy -> Ordering)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> BaseTy)
-> (BaseTy -> BaseTy -> BaseTy)
-> Ord 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
$cp1Ord :: Eq BaseTy
Ord, (forall x. BaseTy -> Rep BaseTy x)
-> (forall x. Rep BaseTy x -> BaseTy) -> Generic BaseTy
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
DataType
Constr
Typeable BaseTy
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy)
-> (BaseTy -> Constr)
-> (BaseTy -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> BaseTy -> BaseTy)
-> (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 u. (forall d. Data d => d -> u) -> BaseTy -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u)
-> (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 (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy)
-> Data BaseTy
BaseTy -> DataType
BaseTy -> Constr
(forall b. Data b => b -> b) -> BaseTy -> BaseTy
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cCtrList :: Constr
$cCtrBag :: Constr
$cCtrSet :: Constr
$cC :: Constr
$cQ :: Constr
$cF :: Constr
$cZ :: Constr
$cN :: Constr
$cP :: Constr
$cB :: Constr
$cUnit :: Constr
$cVoid :: Constr
$tBaseTy :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> BaseTy -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
gmapQ :: (forall d. Data d => d -> u) -> BaseTy -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable BaseTy
Data, Show BaseTy
Show BaseTy
-> (AlphaCtx -> BaseTy -> BaseTy -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BaseTy -> f BaseTy)
-> (AlphaCtx -> NamePatFind -> BaseTy -> BaseTy)
-> (AlphaCtx -> NthPatFind -> BaseTy -> BaseTy)
-> (BaseTy -> DisjointSet AnyName)
-> (BaseTy -> All)
-> (BaseTy -> Bool)
-> (BaseTy -> NthPatFind)
-> (BaseTy -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName))
-> (AlphaCtx -> BaseTy -> BaseTy -> Ordering)
-> Alpha 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' :: AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show BaseTy
Alpha, Subst BaseTy, Subst Atom, Subst UAtom, Subst Type)
instance Pretty BaseTy where
pretty :: BaseTy -> Sem r Doc
pretty = \case
BaseTy
Void -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Void"
BaseTy
Unit -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Unit"
BaseTy
B -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Bool"
BaseTy
P -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Prop"
BaseTy
N -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"ℕ"
BaseTy
Z -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"ℤ"
BaseTy
Q -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"ℚ"
BaseTy
F -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"𝔽"
BaseTy
C -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Char"
BaseTy
CtrList -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"List"
BaseTy
CtrBag -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Bag"
BaseTy
CtrSet -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Set"
isCtr :: BaseTy -> Bool
isCtr :: BaseTy -> Bool
isCtr = (BaseTy -> [BaseTy] -> Bool
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
(Ilk -> Ilk -> Bool) -> (Ilk -> Ilk -> Bool) -> Eq Ilk
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
Eq Ilk
-> (Ilk -> Ilk -> Ordering)
-> (Ilk -> Ilk -> Bool)
-> (Ilk -> Ilk -> Bool)
-> (Ilk -> Ilk -> Bool)
-> (Ilk -> Ilk -> Bool)
-> (Ilk -> Ilk -> Ilk)
-> (Ilk -> Ilk -> Ilk)
-> Ord 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
$cp1Ord :: Eq Ilk
Ord, ReadPrec [Ilk]
ReadPrec Ilk
Int -> ReadS Ilk
ReadS [Ilk]
(Int -> ReadS Ilk)
-> ReadS [Ilk] -> ReadPrec Ilk -> ReadPrec [Ilk] -> Read 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
(Int -> Ilk -> ShowS)
-> (Ilk -> String) -> ([Ilk] -> ShowS) -> Show Ilk
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. Ilk -> Rep Ilk x)
-> (forall x. Rep Ilk x -> Ilk) -> Generic Ilk
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
DataType
Constr
Typeable Ilk
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ilk -> c Ilk)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ilk)
-> (Ilk -> Constr)
-> (Ilk -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Ilk -> Ilk)
-> (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 u. (forall d. Data d => d -> u) -> Ilk -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Ilk -> u)
-> (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 (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk)
-> Data Ilk
Ilk -> DataType
Ilk -> Constr
(forall b. Data b => b -> b) -> Ilk -> Ilk
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ilk -> c Ilk
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cUnification :: Constr
$cSkolem :: Constr
$tIlk :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Ilk -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ilk -> u
gmapQ :: (forall d. Data d => d -> u) -> Ilk -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Ilk -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Ilk
Data, Show Ilk
Show Ilk
-> (AlphaCtx -> Ilk -> Ilk -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ilk -> f Ilk)
-> (AlphaCtx -> NamePatFind -> Ilk -> Ilk)
-> (AlphaCtx -> NthPatFind -> Ilk -> Ilk)
-> (Ilk -> DisjointSet AnyName)
-> (Ilk -> All)
-> (Ilk -> Bool)
-> (Ilk -> NthPatFind)
-> (Ilk -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Ilk -> Ilk)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Ilk -> (Ilk -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ilk -> m (Ilk, Perm AnyName))
-> (AlphaCtx -> Ilk -> Ilk -> Ordering)
-> Alpha 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' :: AlphaCtx -> Ilk -> m (Ilk, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ilk -> m (Ilk, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show Ilk
Alpha, Subst Atom, Subst Type)
instance Pretty Ilk where
pretty :: Ilk -> Sem r Doc
pretty = \case
Ilk
Skolem -> Sem r Doc
"S"
Ilk
Unification -> Sem r Doc
"U"
data Var where
V :: Ilk -> Name Type -> Var
deriving (Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
(Int -> Var -> ShowS)
-> (Var -> String) -> ([Var] -> ShowS) -> Show Var
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
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
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
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord 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
$cp1Ord :: Eq Var
Ord, (forall x. Var -> Rep Var x)
-> (forall x. Rep Var x -> Var) -> Generic Var
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
DataType
Constr
Typeable Var
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var -> c Var)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Var)
-> (Var -> Constr)
-> (Var -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Var -> Var)
-> (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 u. (forall d. Data d => d -> u) -> Var -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Var -> u)
-> (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 (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var -> m Var)
-> Data Var
Var -> DataType
Var -> Constr
(forall b. Data b => b -> b) -> Var -> Var
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var -> c Var
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cV :: Constr
$tVar :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Var -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Var -> u
gmapQ :: (forall d. Data d => d -> u) -> Var -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Var -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Var
Data, Show Var
Show Var
-> (AlphaCtx -> Var -> Var -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Var -> f Var)
-> (AlphaCtx -> NamePatFind -> Var -> Var)
-> (AlphaCtx -> NthPatFind -> Var -> Var)
-> (Var -> DisjointSet AnyName)
-> (Var -> All)
-> (Var -> Bool)
-> (Var -> NthPatFind)
-> (Var -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Var -> Var)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Var -> (Var -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Var -> m (Var, Perm AnyName))
-> (AlphaCtx -> Var -> Var -> Ordering)
-> Alpha 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' :: AlphaCtx -> Var -> m (Var, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Var -> m (Var, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show Var
Alpha, Subst Atom, Subst Type)
pattern U :: Name Type -> Var
pattern $bU :: Name Type -> Var
$mU :: forall r. Var -> (Name Type -> r) -> (Void# -> r) -> r
U v = V Unification v
pattern S :: Name Type -> Var
pattern $bS :: Name Type -> Var
$mS :: forall r. Var -> (Name Type -> r) -> (Void# -> 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
(Int -> Atom -> ShowS)
-> (Atom -> String) -> ([Atom] -> ShowS) -> Show Atom
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
(Atom -> Atom -> Bool) -> (Atom -> Atom -> Bool) -> Eq Atom
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
Eq Atom
-> (Atom -> Atom -> Ordering)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Atom)
-> (Atom -> Atom -> Atom)
-> Ord 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
$cp1Ord :: Eq Atom
Ord, (forall x. Atom -> Rep Atom x)
-> (forall x. Rep Atom x -> Atom) -> Generic Atom
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
DataType
Constr
Typeable Atom
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Atom -> c Atom)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Atom)
-> (Atom -> Constr)
-> (Atom -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Atom -> Atom)
-> (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 u. (forall d. Data d => d -> u) -> Atom -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Atom -> u)
-> (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 (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom)
-> Data Atom
Atom -> DataType
Atom -> Constr
(forall b. Data b => b -> b) -> Atom -> Atom
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Atom -> c Atom
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cABase :: Constr
$cAVar :: Constr
$tAtom :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Atom -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Atom -> u
gmapQ :: (forall d. Data d => d -> u) -> Atom -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Atom -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Atom
Data, Show Atom
Show Atom
-> (AlphaCtx -> Atom -> Atom -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Atom -> f Atom)
-> (AlphaCtx -> NamePatFind -> Atom -> Atom)
-> (AlphaCtx -> NthPatFind -> Atom -> Atom)
-> (Atom -> DisjointSet AnyName)
-> (Atom -> All)
-> (Atom -> Bool)
-> (Atom -> NthPatFind)
-> (Atom -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Atom -> Atom)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Atom -> (Atom -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Atom -> m (Atom, Perm AnyName))
-> (AlphaCtx -> Atom -> Atom -> Ordering)
-> Alpha 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' :: AlphaCtx -> Atom -> m (Atom, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Atom -> m (Atom, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show Atom
Alpha, Subst Type)
instance Subst Atom Atom where
isvar :: Atom -> Maybe (SubstName Atom Atom)
isvar (AVar (U Name Type
x)) = SubstName Atom Atom -> Maybe (SubstName Atom Atom)
forall a. a -> Maybe a
Just (Name Atom -> SubstName Atom Atom
forall a b. (a ~ b) => Name a -> SubstName a b
SubstName (Name Type -> Name Atom
coerce Name Type
x))
isvar Atom
_ = Maybe (SubstName Atom Atom)
forall a. Maybe a
Nothing
instance Pretty Atom where
pretty :: Atom -> Sem r Doc
pretty = \case
AVar (U Name Type
v) -> Name Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Type
v
AVar (S Name Type
v) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"$" Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Name Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Type
v
ABase BaseTy
b -> BaseTy -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
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 (Bool -> Bool) -> (Atom -> Bool) -> Atom -> Bool
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
(Int -> UAtom -> ShowS)
-> (UAtom -> String) -> ([UAtom] -> ShowS) -> Show UAtom
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
(UAtom -> UAtom -> Bool) -> (UAtom -> UAtom -> Bool) -> Eq UAtom
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
Eq UAtom
-> (UAtom -> UAtom -> Ordering)
-> (UAtom -> UAtom -> Bool)
-> (UAtom -> UAtom -> Bool)
-> (UAtom -> UAtom -> Bool)
-> (UAtom -> UAtom -> Bool)
-> (UAtom -> UAtom -> UAtom)
-> (UAtom -> UAtom -> UAtom)
-> Ord 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
$cp1Ord :: Eq UAtom
Ord, (forall x. UAtom -> Rep UAtom x)
-> (forall x. Rep UAtom x -> UAtom) -> Generic UAtom
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
Show UAtom
-> (AlphaCtx -> UAtom -> UAtom -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> UAtom -> f UAtom)
-> (AlphaCtx -> NamePatFind -> UAtom -> UAtom)
-> (AlphaCtx -> NthPatFind -> UAtom -> UAtom)
-> (UAtom -> DisjointSet AnyName)
-> (UAtom -> All)
-> (UAtom -> Bool)
-> (UAtom -> NthPatFind)
-> (UAtom -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> UAtom -> UAtom)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> UAtom -> (UAtom -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UAtom -> m (UAtom, Perm AnyName))
-> (AlphaCtx -> UAtom -> UAtom -> Ordering)
-> Alpha 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' :: AlphaCtx -> UAtom -> m (UAtom, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UAtom -> m (UAtom, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show UAtom
Alpha, Subst BaseTy)
instance Subst UAtom UAtom where
isvar :: UAtom -> Maybe (SubstName UAtom UAtom)
isvar (UV Name Type
x) = SubstName UAtom UAtom -> Maybe (SubstName UAtom UAtom)
forall a. a -> Maybe a
Just (Name UAtom -> SubstName UAtom UAtom
forall a b. (a ~ b) => Name a -> SubstName a b
SubstName (Name Type -> Name UAtom
coerce Name Type
x))
isvar UAtom
_ = Maybe (SubstName UAtom UAtom)
forall a. Maybe a
Nothing
instance Pretty UAtom where
pretty :: UAtom -> Sem r Doc
pretty (UB BaseTy
b) = BaseTy -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty BaseTy
b
pretty (UV Name Type
n) = Name Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
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) = BaseTy -> Either BaseTy (Name Type)
forall a b. a -> Either a b
Left BaseTy
b
uatomToEither (UV Name Type
v) = Name Type -> Either BaseTy (Name Type)
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
(Int -> Con -> ShowS)
-> (Con -> String) -> ([Con] -> ShowS) -> Show Con
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
(Con -> Con -> Bool) -> (Con -> Con -> Bool) -> Eq Con
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
Eq Con
-> (Con -> Con -> Ordering)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Con)
-> (Con -> Con -> Con)
-> Ord 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
$cp1Ord :: Eq Con
Ord, (forall x. Con -> Rep Con x)
-> (forall x. Rep Con x -> Con) -> Generic Con
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
DataType
Constr
Typeable Con
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Con)
-> (Con -> Constr)
-> (Con -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Con -> Con)
-> (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 u. (forall d. Data d => d -> u) -> Con -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Con -> u)
-> (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 (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con)
-> Data Con
Con -> DataType
Con -> Constr
(forall b. Data b => b -> b) -> Con -> Con
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cCUser :: Constr
$cCGraph :: Constr
$cCMap :: Constr
$cCContainer :: Constr
$cCSum :: Constr
$cCProd :: Constr
$cCArr :: Constr
$tCon :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Con -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Con -> u
gmapQ :: (forall d. Data d => d -> u) -> Con -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Con -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Con
Data, Show Con
Show Con
-> (AlphaCtx -> Con -> Con -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con)
-> (AlphaCtx -> NamePatFind -> Con -> Con)
-> (AlphaCtx -> NthPatFind -> Con -> Con)
-> (Con -> DisjointSet AnyName)
-> (Con -> All)
-> (Con -> Bool)
-> (Con -> NthPatFind)
-> (Con -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Con -> Con)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName))
-> (AlphaCtx -> Con -> Con -> Ordering)
-> Alpha 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' :: AlphaCtx -> Con -> m (Con, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show Con
Alpha)
instance Pretty Con where
pretty :: Con -> Sem r Doc
pretty = \case
Con
CMap -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Map"
Con
CGraph -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Graph"
CUser String
s -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
s
Con
CList -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"List"
Con
CBag -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Bag"
Con
CSet -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Set"
CContainer Atom
v -> Atom -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Atom
v
Con
c -> String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"Impossible: got Con " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Con -> String
forall a. Show a => a -> String
show Con
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in pretty @Con"
pattern CList :: Con
pattern $bCList :: Con
$mCList :: forall r. Con -> (Void# -> r) -> (Void# -> r) -> r
CList = CContainer (ABase CtrList)
pattern CBag :: Con
pattern $bCBag :: Con
$mCBag :: forall r. Con -> (Void# -> r) -> (Void# -> r) -> r
CBag = CContainer (ABase CtrBag)
pattern CSet :: Con
pattern $bCSet :: Con
$mCSet :: forall r. Con -> (Void# -> r) -> (Void# -> 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
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
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
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
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
Eq Type
-> (Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord 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
$cp1Ord :: Eq Type
Ord, (forall x. Type -> Rep Type x)
-> (forall x. Rep Type x -> Type) -> Generic Type
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
DataType
Constr
Typeable Type
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type)
-> (Type -> Constr)
-> (Type -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Type -> Type)
-> (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 u. (forall d. Data d => d -> u) -> Type -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Type -> u)
-> (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 (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type)
-> Data Type
Type -> DataType
Type -> Constr
(forall b. Data b => b -> b) -> Type -> Type
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cTyCon :: Constr
$cTyAtom :: Constr
$tType :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Type -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
gmapQ :: (forall d. Data d => d -> u) -> Type -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Type
Data, Show Type
Show Type
-> (AlphaCtx -> Type -> Type -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Type -> f Type)
-> (AlphaCtx -> NamePatFind -> Type -> Type)
-> (AlphaCtx -> NthPatFind -> Type -> Type)
-> (Type -> DisjointSet AnyName)
-> (Type -> All)
-> (Type -> Bool)
-> (Type -> NthPatFind)
-> (Type -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Type -> Type)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName))
-> (AlphaCtx -> Type -> Type -> Ordering)
-> Alpha 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' :: AlphaCtx -> Type -> m (Type, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show Type
Alpha)
instance Pretty Type where
pretty :: Type -> Sem r Doc
pretty (TyAtom Atom
a) = Atom -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Atom
a
pretty (Type
ty1 :->: Type
ty2) = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
tarrPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"→" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2)
pretty (Type
ty1 :*: Type
ty2) = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
tmulPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"×" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2)
pretty (Type
ty1 :+: Type
ty2) = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
taddPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"+" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2)
pretty (TyCon Con
c []) = Con -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Con
c
pretty (TyCon Con
c [Type]
tys) = do
[Sem r Doc]
ds <- PA -> Sem r [Sem r Doc] -> Sem r [Sem r Doc]
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r [Sem r Doc] -> Sem r [Sem r Doc])
-> Sem r [Sem r Doc] -> Sem r [Sem r Doc]
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Type -> Sem r Doc) -> [Type] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Type]
tys)
Con -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Con
c Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)
instance Subst Type Qualifier
instance Subst Type Rational where
subst :: Name Type -> Type -> Rational -> Rational
subst Name Type
_ Type
_ = Rational -> Rational
forall a. a -> a
id
substs :: [(Name Type, Type)] -> Rational -> Rational
substs [(Name Type, Type)]
_ = Rational -> Rational
forall a. a -> a
id
instance Subst Type Void where
subst :: Name Type -> Type -> Void -> Void
subst Name Type
_ Type
_ = Void -> Void
forall a. a -> a
id
substs :: [(Name Type, Type)] -> Void -> Void
substs [(Name Type, Type)]
_ = Void -> Void
forall a. a -> a
id
instance Subst Type Con where
isCoerceVar :: Con -> Maybe (SubstCoerce Con Type)
isCoerceVar (CContainer (AVar (U Name Type
x)))
= SubstCoerce Con Type -> Maybe (SubstCoerce Con Type)
forall a. a -> Maybe a
Just (Name Type -> (Type -> Maybe Con) -> SubstCoerce Con Type
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) = Con -> Maybe Con
forall a. a -> Maybe a
Just (Atom -> Con
CContainer Atom
a)
substCtrTy Type
_ = Maybe Con
forall a. Maybe a
Nothing
isCoerceVar Con
_ = Maybe (SubstCoerce Con Type)
forall a. Maybe a
Nothing
instance Subst Type Type where
isvar :: Type -> Maybe (SubstName Type Type)
isvar (TyAtom (AVar (U Name Type
x))) = SubstName Type Type -> Maybe (SubstName Type Type)
forall a. a -> Maybe a
Just (Name Type -> SubstName Type Type
forall a b. (a ~ b) => Name a -> SubstName a b
SubstName Name Type
x)
isvar Type
_ = Maybe (SubstName Type Type)
forall a. Maybe a
Nothing
pattern TyVar :: Name Type -> Type
pattern $bTyVar :: Name Type -> Type
$mTyVar :: forall r. Type -> (Name Type -> r) -> (Void# -> 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) -> (Void# -> r) -> r
TySkolem v = TyAtom (AVar (S v))
pattern TyVoid :: Type
pattern $bTyVoid :: Type
$mTyVoid :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyVoid = TyAtom (ABase Void)
pattern TyUnit :: Type
pattern $bTyUnit :: Type
$mTyUnit :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyUnit = TyAtom (ABase Unit)
pattern TyBool :: Type
pattern $bTyBool :: Type
$mTyBool :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyBool = TyAtom (ABase B)
pattern TyProp :: Type
pattern $bTyProp :: Type
$mTyProp :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyProp = TyAtom (ABase P)
pattern TyN :: Type
pattern $bTyN :: Type
$mTyN :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyN = TyAtom (ABase N)
pattern TyZ :: Type
pattern $bTyZ :: Type
$mTyZ :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyZ = TyAtom (ABase Z)
pattern TyF :: Type
pattern $bTyF :: Type
$mTyF :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyF = TyAtom (ABase F)
pattern TyQ :: Type
pattern $bTyQ :: Type
$mTyQ :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyQ = TyAtom (ABase Q)
pattern TyC :: Type
pattern $bTyC :: Type
$mTyC :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyC = TyAtom (ABase C)
infixr 5 :->:
pattern (:->:) :: Type -> Type -> Type
pattern $b:->: :: Type -> Type -> Type
$m:->: :: forall r. Type -> (Type -> Type -> r) -> (Void# -> 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) -> (Void# -> 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) -> (Void# -> r) -> r
(:+:) ty1 ty2 = TyCon CSum [ty1, ty2]
pattern TyList :: Type -> Type
pattern $bTyList :: Type -> Type
$mTyList :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
TyList elTy = TyCon CList [elTy]
pattern TyBag :: Type -> Type
pattern $bTyBag :: Type -> Type
$mTyBag :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
TyBag elTy = TyCon CBag [elTy]
pattern TySet :: Type -> Type
pattern $bTySet :: Type -> Type
$mTySet :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
TySet elTy = TyCon CSet [elTy]
pattern TyContainer :: Atom -> Type -> Type
pattern $bTyContainer :: Atom -> Type -> Type
$mTyContainer :: forall r. Type -> (Atom -> Type -> r) -> (Void# -> r) -> r
TyContainer c elTy = TyCon (CContainer c) [elTy]
pattern TyGraph :: Type -> Type
pattern $bTyGraph :: Type -> Type
$mTyGraph :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
TyGraph elTy = TyCon CGraph [elTy]
pattern TyMap :: Type -> Type -> Type
pattern $bTyMap :: Type -> Type -> Type
$mTyMap :: forall r. Type -> (Type -> Type -> r) -> (Void# -> 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) -> (Void# -> r) -> r
TyUser nm args = TyCon (CUser nm) args
pattern TyString :: Type
pattern $bTyString :: Type
$mTyString :: forall r. Type -> (Void# -> r) -> (Void# -> 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 = (a -> a) -> Set a -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (Name t -> t -> a -> a
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 = (a -> a) -> Set a -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map ([(Name t, t)] -> a -> a
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 = (a -> a) -> Map k a -> Map k a
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Name t -> t -> a -> a
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 = (a -> a) -> Map k a -> Map k a
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ([(Name t, t)] -> a -> a
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 :: (String, TyDefBody) -> Sem r Doc
pretty (String
tyName, TyDefBody [String]
ps [Type] -> Type
body)
= Sem r Doc
"type" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
tyName Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> [String] -> Sem r Doc
prettyArgs [String]
ps) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"=" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty ([Type] -> Type
body ((String -> Type) -> [String] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Type
TyVar (Name Type -> Type) -> (String -> Name Type) -> String -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name Type
forall a. String -> Name a
string2Name) [String]
ps))
where
prettyArgs :: [String] -> Sem r Doc
prettyArgs [] = Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
empty
prettyArgs [String]
_ = do
[Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((String -> Sem r Doc) -> [String] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
ps)
Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)
newtype PolyType = Forall (Bind [Name Type] Type)
deriving (Int -> PolyType -> ShowS
[PolyType] -> ShowS
PolyType -> String
(Int -> PolyType -> ShowS)
-> (PolyType -> String) -> ([PolyType] -> ShowS) -> Show PolyType
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. PolyType -> Rep PolyType x)
-> (forall x. Rep PolyType x -> PolyType) -> Generic PolyType
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
DataType
Constr
Typeable PolyType
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PolyType)
-> (PolyType -> Constr)
-> (PolyType -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> PolyType -> PolyType)
-> (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 u. (forall d. Data d => d -> u) -> PolyType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u)
-> (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 (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType)
-> Data PolyType
PolyType -> DataType
PolyType -> Constr
(forall b. Data b => b -> b) -> PolyType -> PolyType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cForall :: Constr
$tPolyType :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> PolyType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u
gmapQ :: (forall d. Data d => d -> u) -> PolyType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PolyType -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable PolyType
Data, Show PolyType
Show PolyType
-> (AlphaCtx -> PolyType -> PolyType -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType)
-> (AlphaCtx -> NamePatFind -> PolyType -> PolyType)
-> (AlphaCtx -> NthPatFind -> PolyType -> PolyType)
-> (PolyType -> DisjointSet AnyName)
-> (PolyType -> All)
-> (PolyType -> Bool)
-> (PolyType -> NthPatFind)
-> (PolyType -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> PolyType -> PolyType)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName))
-> (AlphaCtx -> PolyType -> PolyType -> Ordering)
-> Alpha 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' :: AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show PolyType
Alpha, Subst Type)
instance Pretty PolyType where
pretty :: PolyType -> Sem r Doc
pretty (Forall Bind [Name Type] Type
bnd) = Bind [Name Type] Type
-> (([Name Type], Type) -> Sem r Doc) -> Sem r Doc
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 ((([Name Type], Type) -> Sem r Doc) -> Sem r Doc)
-> (([Name Type], Type) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
\([Name Type]
_, Type
body) -> Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
body
toPolyType :: Type -> PolyType
toPolyType :: Type -> PolyType
toPolyType Type
ty = Bind [Name Type] Type -> PolyType
Forall ([Name Type] -> Type -> Bind [Name Type] Type
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 ([Name Type] -> Type -> Bind [Name Type] Type
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([Name Type] -> [Name Type]
forall a. Eq a => [a] -> [a]
nub ([Name Type] -> [Name Type]) -> [Name Type] -> [Name Type]
forall a b. (a -> b) -> a -> b
$ Getting (Endo [Name Type]) Type (Name Type) -> Type -> [Name Type]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [Name Type]) Type (Name Type)
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 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
countType Type
TyUnit = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
countType Type
TyBool = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
2
countType Type
TyC = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
17 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
16 :: Integer))
countType (Type
ty1 :+: Type
ty2) = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty1 Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
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 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
| Type -> Bool
isEmptyTy Type
ty2 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
| Bool
otherwise = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty1 Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
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
_) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
(Maybe Integer
_, Just Integer
0) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
(Maybe Integer
_, Just Integer
1) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
(Maybe Integer
c1, Maybe Integer
c2) -> Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
(^) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
c2 Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
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 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
| Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing
countType (TyBag Type
ty)
| Type -> Bool
isEmptyTy Type
ty = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
| Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing
countType (TySet Type
ty) = (Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty
countType (TyGraph Type
ty) =
(\Integer
t -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer) -> [Integer] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (\Integer
n -> (Integer
t Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`choose` Integer
n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
n)) [Integer
0 .. Integer
t]) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
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 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
| Type -> Bool
isEmptyTy Type
tyValue = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
| Bool
otherwise = (\Integer
k Integer
v -> (Integer
vInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
k) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
tyKey Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Integer
countType Type
tyValue
countType Type
_ = Maybe Integer
forall a. Maybe a
Nothing
isNumTy :: Type -> Bool
isNumTy :: Type -> Bool
isNumTy Type
ty = Type
ty Type -> [Type] -> Bool
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
(Strictness -> Strictness -> Bool)
-> (Strictness -> Strictness -> Bool) -> Eq Strictness
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
(Int -> Strictness -> ShowS)
-> (Strictness -> String)
-> ([Strictness] -> ShowS)
-> Show Strictness
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. Strictness -> Rep Strictness x)
-> (forall x. Rep Strictness x -> Strictness) -> Generic Strictness
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
Show Strictness
-> (AlphaCtx -> Strictness -> Strictness -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Strictness -> f Strictness)
-> (AlphaCtx -> NamePatFind -> Strictness -> Strictness)
-> (AlphaCtx -> NthPatFind -> Strictness -> Strictness)
-> (Strictness -> DisjointSet AnyName)
-> (Strictness -> All)
-> (Strictness -> Bool)
-> (Strictness -> NthPatFind)
-> (Strictness -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Strictness -> Strictness)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Strictness -> (Strictness -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Strictness -> m (Strictness, Perm AnyName))
-> (AlphaCtx -> Strictness -> Strictness -> Ordering)
-> Alpha 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' :: AlphaCtx -> Strictness -> m (Strictness, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Strictness -> m (Strictness, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show Strictness
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 Type -> [Type] -> [Type]
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 = (Atom -> Type) -> Substitution Atom -> Substitution Type
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 (Substitution Atom -> Substitution Type)
-> (Substitution UAtom -> Substitution Atom)
-> Substitution UAtom
-> Substitution Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UAtom -> Atom) -> Substitution UAtom -> Substitution Atom
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 Name Type -> Set (Name Type) -> Set (Name Type)
forall a. Ord a => a -> Set a -> Set a
`S.insert` (Type -> Set (Name Type)) -> [Type] -> Set (Name Type)
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) = (Type -> Set (Name Type)) -> [Type] -> Set (Name Type)
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Set (Name Type)
containerVars [Type]
tys
containerVars Type
_ = Set (Name Type)
forall a. Set a
S.empty
class HasType t where
getType :: t -> Type
setType :: Type -> t -> t
setType Type
_ = t -> t
forall a. a -> a
id