{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Swarm.Language.Types (
BaseTy (..),
Var,
TypeF (..),
Type,
tyVars,
pattern TyBase,
pattern TyVar,
pattern TyVoid,
pattern TyUnit,
pattern TyInt,
pattern TyText,
pattern TyDir,
pattern TyBool,
pattern TyActor,
pattern TyKey,
pattern (:+:),
pattern (:*:),
pattern (:->:),
pattern TyRcd,
pattern TyCmd,
pattern TyDelay,
UType,
pattern UTyBase,
pattern UTyVar,
pattern UTyVoid,
pattern UTyUnit,
pattern UTyInt,
pattern UTyText,
pattern UTyDir,
pattern UTyBool,
pattern UTyActor,
pattern UTyKey,
pattern UTySum,
pattern UTyProd,
pattern UTyFun,
pattern UTyRcd,
pattern UTyCmd,
pattern UTyDelay,
ucata,
mkVarName,
Poly (..),
Polytype,
pattern PolyUnit,
UPolytype,
TCtx,
UCtx,
WithU (..),
) where
import Control.Monad (guard)
import Control.Unification
import Control.Unification.IntVar
import Data.Aeson (FromJSON, ToJSON)
import Data.Data (Data)
import Data.Foldable (fold)
import Data.Function (on)
import Data.Functor.Fixedpoint
import Data.Kind qualified
import Data.Map.Merge.Strict qualified as M
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as M
import Data.Set (Set)
import Data.Set qualified as S
import Data.String (IsString (..))
import Data.Text (Text)
import Data.Text qualified as T
import GHC.Generics (Generic, Generic1)
import Swarm.Language.Context
import Witch
data BaseTy
=
BVoid
|
BUnit
|
BInt
|
BText
|
BDir
|
BBool
|
BActor
|
BKey
deriving (BaseTy -> BaseTy -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BaseTy -> BaseTy -> Bool
$c/= :: BaseTy -> BaseTy -> Bool
== :: BaseTy -> BaseTy -> Bool
$c== :: BaseTy -> BaseTy -> Bool
Eq, Eq BaseTy
BaseTy -> BaseTy -> Bool
BaseTy -> BaseTy -> Ordering
BaseTy -> BaseTy -> BaseTy
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BaseTy -> BaseTy -> BaseTy
$cmin :: BaseTy -> BaseTy -> BaseTy
max :: BaseTy -> BaseTy -> BaseTy
$cmax :: BaseTy -> BaseTy -> BaseTy
>= :: BaseTy -> BaseTy -> Bool
$c>= :: BaseTy -> BaseTy -> Bool
> :: BaseTy -> BaseTy -> Bool
$c> :: BaseTy -> BaseTy -> Bool
<= :: BaseTy -> BaseTy -> Bool
$c<= :: BaseTy -> BaseTy -> Bool
< :: BaseTy -> BaseTy -> Bool
$c< :: BaseTy -> BaseTy -> Bool
compare :: BaseTy -> BaseTy -> Ordering
$ccompare :: BaseTy -> BaseTy -> Ordering
Ord, Int -> BaseTy -> ShowS
[BaseTy] -> ShowS
BaseTy -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BaseTy] -> ShowS
$cshowList :: [BaseTy] -> ShowS
show :: BaseTy -> String
$cshow :: BaseTy -> String
showsPrec :: Int -> BaseTy -> ShowS
$cshowsPrec :: Int -> BaseTy -> ShowS
Show, Typeable BaseTy
BaseTy -> DataType
BaseTy -> Constr
(forall b. Data b => b -> b) -> BaseTy -> BaseTy
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
gmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
$cgmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
dataTypeOf :: BaseTy -> DataType
$cdataTypeOf :: BaseTy -> DataType
toConstr :: BaseTy -> Constr
$ctoConstr :: BaseTy -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
Data, 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, Value -> Parser [BaseTy]
Value -> Parser BaseTy
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [BaseTy]
$cparseJSONList :: Value -> Parser [BaseTy]
parseJSON :: Value -> Parser BaseTy
$cparseJSON :: Value -> Parser BaseTy
FromJSON, [BaseTy] -> Encoding
[BaseTy] -> Value
BaseTy -> Encoding
BaseTy -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [BaseTy] -> Encoding
$ctoEncodingList :: [BaseTy] -> Encoding
toJSONList :: [BaseTy] -> Value
$ctoJSONList :: [BaseTy] -> Value
toEncoding :: BaseTy -> Encoding
$ctoEncoding :: BaseTy -> Encoding
toJSON :: BaseTy -> Value
$ctoJSON :: BaseTy -> Value
ToJSON)
data TypeF t
=
TyBaseF BaseTy
|
TyVarF Var
|
TyCmdF t
|
TyDelayF t
|
TySumF t t
|
TyProdF t t
|
TyFunF t t
|
TyRcdF (Map Var t)
deriving (Int -> TypeF t -> ShowS
forall t. Show t => Int -> TypeF t -> ShowS
forall t. Show t => [TypeF t] -> ShowS
forall t. Show t => TypeF t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeF t] -> ShowS
$cshowList :: forall t. Show t => [TypeF t] -> ShowS
show :: TypeF t -> String
$cshow :: forall t. Show t => TypeF t -> String
showsPrec :: Int -> TypeF t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> TypeF t -> ShowS
Show, TypeF t -> TypeF t -> Bool
forall t. Eq t => TypeF t -> TypeF t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeF t -> TypeF t -> Bool
$c/= :: forall t. Eq t => TypeF t -> TypeF t -> Bool
== :: TypeF t -> TypeF t -> Bool
$c== :: forall t. Eq t => TypeF t -> TypeF t -> Bool
Eq, forall a b. a -> TypeF b -> TypeF a
forall a b. (a -> b) -> TypeF a -> TypeF b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TypeF b -> TypeF a
$c<$ :: forall a b. a -> TypeF b -> TypeF a
fmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
$cfmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
Functor, forall a. Eq a => a -> TypeF a -> Bool
forall a. Num a => TypeF a -> a
forall a. Ord a => TypeF a -> a
forall m. Monoid m => TypeF m -> m
forall a. TypeF a -> Bool
forall a. TypeF a -> Int
forall a. TypeF a -> [a]
forall a. (a -> a -> a) -> TypeF a -> a
forall m a. Monoid m => (a -> m) -> TypeF a -> m
forall b a. (b -> a -> b) -> b -> TypeF a -> b
forall a b. (a -> b -> b) -> b -> TypeF a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => TypeF a -> a
$cproduct :: forall a. Num a => TypeF a -> a
sum :: forall a. Num a => TypeF a -> a
$csum :: forall a. Num a => TypeF a -> a
minimum :: forall a. Ord a => TypeF a -> a
$cminimum :: forall a. Ord a => TypeF a -> a
maximum :: forall a. Ord a => TypeF a -> a
$cmaximum :: forall a. Ord a => TypeF a -> a
elem :: forall a. Eq a => a -> TypeF a -> Bool
$celem :: forall a. Eq a => a -> TypeF a -> Bool
length :: forall a. TypeF a -> Int
$clength :: forall a. TypeF a -> Int
null :: forall a. TypeF a -> Bool
$cnull :: forall a. TypeF a -> Bool
toList :: forall a. TypeF a -> [a]
$ctoList :: forall a. TypeF a -> [a]
foldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
fold :: forall m. Monoid m => TypeF m -> m
$cfold :: forall m. Monoid m => TypeF m -> m
Foldable, Functor TypeF
Foldable TypeF
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
sequence :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
$csequence :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
sequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (TypeF t) x -> TypeF t
forall t x. TypeF t -> Rep (TypeF t) x
$cto :: forall t x. Rep (TypeF t) x -> TypeF t
$cfrom :: forall t x. TypeF t -> Rep (TypeF t) x
Generic, forall a. Rep1 TypeF a -> TypeF a
forall a. TypeF a -> Rep1 TypeF a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall a. Rep1 TypeF a -> TypeF a
$cfrom1 :: forall a. TypeF a -> Rep1 TypeF a
Generic1, Traversable TypeF
forall a. TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a)))
forall (t :: * -> *).
Traversable t
-> (forall a. t a -> t a -> Maybe (t (Either a (a, a))))
-> Unifiable t
zipMatch :: forall a. TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a)))
$czipMatch :: forall a. TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a)))
Unifiable, TypeF t -> DataType
TypeF t -> Constr
forall {t}. Data t => Typeable (TypeF t)
forall t. Data t => TypeF t -> DataType
forall t. Data t => TypeF t -> Constr
forall t.
Data t =>
(forall b. Data b => b -> b) -> TypeF t -> TypeF t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> TypeF t -> u
forall t u.
Data t =>
(forall d. Data d => d -> u) -> TypeF t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeF t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeF t -> c (TypeF t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeF t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypeF t))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeF t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeF t -> c (TypeF t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeF t))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TypeF t -> u
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> TypeF t -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> TypeF t -> [u]
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> TypeF t -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
gmapT :: (forall b. Data b => b -> b) -> TypeF t -> TypeF t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> TypeF t -> TypeF t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypeF t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypeF t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeF t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeF t))
dataTypeOf :: TypeF t -> DataType
$cdataTypeOf :: forall t. Data t => TypeF t -> DataType
toConstr :: TypeF t -> Constr
$ctoConstr :: forall t. Data t => TypeF t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeF t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeF t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeF t -> c (TypeF t)
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeF t -> c (TypeF t)
Data, forall t. FromJSON t => Value -> Parser [TypeF t]
forall t. FromJSON t => Value -> Parser (TypeF t)
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [TypeF t]
$cparseJSONList :: forall t. FromJSON t => Value -> Parser [TypeF t]
parseJSON :: Value -> Parser (TypeF t)
$cparseJSON :: forall t. FromJSON t => Value -> Parser (TypeF t)
FromJSON, forall t. ToJSON t => [TypeF t] -> Encoding
forall t. ToJSON t => [TypeF t] -> Value
forall t. ToJSON t => TypeF t -> Encoding
forall t. ToJSON t => TypeF t -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [TypeF t] -> Encoding
$ctoEncodingList :: forall t. ToJSON t => [TypeF t] -> Encoding
toJSONList :: [TypeF t] -> Value
$ctoJSONList :: forall t. ToJSON t => [TypeF t] -> Value
toEncoding :: TypeF t -> Encoding
$ctoEncoding :: forall t. ToJSON t => TypeF t -> Encoding
toJSON :: TypeF t -> Value
$ctoJSON :: forall t. ToJSON t => TypeF t -> Value
ToJSON)
instance Ord k => Unifiable (Map k) where
zipMatch :: forall a. Map k a -> Map k a -> Maybe (Map k (Either a (a, a)))
zipMatch Map k a
m1 Map k a
m2 = do
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall k a. Map k a -> Set k
M.keysSet) Map k a
m1 Map k a
m2
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge forall (f :: * -> *) k x y. Applicative f => WhenMissing f k x y
M.dropMissing forall (f :: * -> *) k x y. Applicative f => WhenMissing f k x y
M.dropMissing (forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched (\k
_ a
a1 a
a2 -> forall a b. b -> Either a b
Right (a
a1, a
a2))) Map k a
m1 Map k a
m2
type Type = Fix TypeF
tyVars :: Type -> Set Var
tyVars :: Type -> Set Var
tyVars = forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
cata (\case TyVarF Var
x -> forall a. a -> Set a
S.singleton Var
x; TypeF (Set Var)
f -> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold TypeF (Set Var)
f)
deriving instance Data Type
type UType = UTerm TypeF IntVar
deriving instance Data UType
deriving instance Data IntVar
ucata :: Functor t => (v -> a) -> (t a -> a) -> UTerm t v -> a
ucata :: forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> UTerm t v -> a
ucata v -> a
f t a -> a
_ (UVar v
v) = v -> a
f v
v
ucata v -> a
f t a -> a
g (UTerm t (UTerm t v)
t) = t a -> a
g (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> UTerm t v -> a
ucata v -> a
f t a -> a
g) t (UTerm t v)
t)
mkVarName :: Text -> IntVar -> Var
mkVarName :: Var -> IntVar -> Var
mkVarName Var
nm (IntVar Int
v) = Var -> Var -> Var
T.append Var
nm (forall source target. From source target => source -> target
from @String (forall a. Show a => a -> String
show (Int
v forall a. Num a => a -> a -> a
+ (forall a. Bounded a => a
maxBound :: Int) forall a. Num a => a -> a -> a
+ Int
1)))
instance IsString Type where
fromString :: String -> Type
fromString String
x = Var -> Type
TyVar (forall source target. From source target => source -> target
from @String String
x)
instance IsString UType where
fromString :: String -> UType
fromString String
x = Var -> UType
UTyVar (forall source target. From source target => source -> target
from @String String
x)
type TCtx = Ctx Polytype
type UCtx = Ctx UPolytype
data Poly t = Forall [Var] t
deriving (Int -> Poly t -> ShowS
forall t. Show t => Int -> Poly t -> ShowS
forall t. Show t => [Poly t] -> ShowS
forall t. Show t => Poly t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Poly t] -> ShowS
$cshowList :: forall t. Show t => [Poly t] -> ShowS
show :: Poly t -> String
$cshow :: forall t. Show t => Poly t -> String
showsPrec :: Int -> Poly t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Poly t -> ShowS
Show, Poly t -> Poly t -> Bool
forall t. Eq t => Poly t -> Poly t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Poly t -> Poly t -> Bool
$c/= :: forall t. Eq t => Poly t -> Poly t -> Bool
== :: Poly t -> Poly t -> Bool
$c== :: forall t. Eq t => Poly t -> Poly t -> Bool
Eq, forall a b. a -> Poly b -> Poly a
forall a b. (a -> b) -> Poly a -> Poly b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Poly b -> Poly a
$c<$ :: forall a b. a -> Poly b -> Poly a
fmap :: forall a b. (a -> b) -> Poly a -> Poly b
$cfmap :: forall a b. (a -> b) -> Poly a -> Poly b
Functor, forall a. Eq a => a -> Poly a -> Bool
forall a. Num a => Poly a -> a
forall a. Ord a => Poly a -> a
forall m. Monoid m => Poly m -> m
forall a. Poly a -> Bool
forall a. Poly a -> Int
forall a. Poly a -> [a]
forall a. (a -> a -> a) -> Poly a -> a
forall m a. Monoid m => (a -> m) -> Poly a -> m
forall b a. (b -> a -> b) -> b -> Poly a -> b
forall a b. (a -> b -> b) -> b -> Poly a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Poly a -> a
$cproduct :: forall a. Num a => Poly a -> a
sum :: forall a. Num a => Poly a -> a
$csum :: forall a. Num a => Poly a -> a
minimum :: forall a. Ord a => Poly a -> a
$cminimum :: forall a. Ord a => Poly a -> a
maximum :: forall a. Ord a => Poly a -> a
$cmaximum :: forall a. Ord a => Poly a -> a
elem :: forall a. Eq a => a -> Poly a -> Bool
$celem :: forall a. Eq a => a -> Poly a -> Bool
length :: forall a. Poly a -> Int
$clength :: forall a. Poly a -> Int
null :: forall a. Poly a -> Bool
$cnull :: forall a. Poly a -> Bool
toList :: forall a. Poly a -> [a]
$ctoList :: forall a. Poly a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Poly a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Poly a -> a
foldr1 :: forall a. (a -> a -> a) -> Poly a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Poly a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Poly a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Poly a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Poly a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Poly a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Poly a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Poly a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Poly a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Poly a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Poly a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Poly a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Poly a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Poly a -> m
fold :: forall m. Monoid m => Poly m -> m
$cfold :: forall m. Monoid m => Poly m -> m
Foldable, Functor Poly
Foldable Poly
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Poly (m a) -> m (Poly a)
forall (f :: * -> *) a. Applicative f => Poly (f a) -> f (Poly a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly a -> m (Poly b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Poly a -> f (Poly b)
sequence :: forall (m :: * -> *) a. Monad m => Poly (m a) -> m (Poly a)
$csequence :: forall (m :: * -> *) a. Monad m => Poly (m a) -> m (Poly a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly a -> m (Poly b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly a -> m (Poly b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Poly (f a) -> f (Poly a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Poly (f a) -> f (Poly a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Poly a -> f (Poly b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Poly a -> f (Poly b)
Traversable, Poly t -> DataType
Poly t -> Constr
forall {t}. Data t => Typeable (Poly t)
forall t. Data t => Poly t -> DataType
forall t. Data t => Poly t -> Constr
forall t.
Data t =>
(forall b. Data b => b -> b) -> Poly t -> Poly t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Poly t -> u
forall t u. Data t => (forall d. Data d => d -> u) -> Poly t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
forall t r r'.
Data t =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly t -> c (Poly t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly t))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly t -> c (Poly t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly t))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Poly t -> u
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Poly t -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Poly t -> [u]
$cgmapQ :: forall t u. Data t => (forall d. Data d => d -> u) -> Poly t -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
gmapT :: (forall b. Data b => b -> b) -> Poly t -> Poly t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> Poly t -> Poly t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly t))
dataTypeOf :: Poly t -> DataType
$cdataTypeOf :: forall t. Data t => Poly t -> DataType
toConstr :: Poly t -> Constr
$ctoConstr :: forall t. Data t => Poly t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly t -> c (Poly t)
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly t -> c (Poly t)
Data, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (Poly t) x -> Poly t
forall t x. Poly t -> Rep (Poly t) x
$cto :: forall t x. Rep (Poly t) x -> Poly t
$cfrom :: forall t x. Poly t -> Rep (Poly t) x
Generic, forall t. FromJSON t => Value -> Parser [Poly t]
forall t. FromJSON t => Value -> Parser (Poly t)
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [Poly t]
$cparseJSONList :: forall t. FromJSON t => Value -> Parser [Poly t]
parseJSON :: Value -> Parser (Poly t)
$cparseJSON :: forall t. FromJSON t => Value -> Parser (Poly t)
FromJSON, forall t. ToJSON t => [Poly t] -> Encoding
forall t. ToJSON t => [Poly t] -> Value
forall t. ToJSON t => Poly t -> Encoding
forall t. ToJSON t => Poly t -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [Poly t] -> Encoding
$ctoEncodingList :: forall t. ToJSON t => [Poly t] -> Encoding
toJSONList :: [Poly t] -> Value
$ctoJSONList :: forall t. ToJSON t => [Poly t] -> Value
toEncoding :: Poly t -> Encoding
$ctoEncoding :: forall t. ToJSON t => Poly t -> Encoding
toJSON :: Poly t -> Value
$ctoJSON :: forall t. ToJSON t => Poly t -> Value
ToJSON)
type Polytype = Poly Type
type UPolytype = Poly UType
class WithU t where
type U t :: Data.Kind.Type
toU :: t -> U t
fromU :: U t -> Maybe t
instance WithU Type where
type U Type = UType
toU :: Type -> U Type
toU = forall (t :: * -> *) v. Functor t => Fix t -> UTerm t v
unfreeze
fromU :: U Type -> Maybe Type
fromU = forall (t :: * -> *) v. Traversable t => UTerm t v -> Maybe (Fix t)
freeze
instance (WithU t, Traversable f) => WithU (f t) where
type U (f t) = f (U t)
toU :: f t -> U (f t)
toU = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. WithU t => t -> U t
toU
fromU :: U (f t) -> Maybe (f t)
fromU = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. WithU t => U t -> Maybe t
fromU
pattern TyBase :: BaseTy -> Type
pattern $bTyBase :: BaseTy -> Type
$mTyBase :: forall {r}. Type -> (BaseTy -> r) -> ((# #) -> r) -> r
TyBase b = Fix (TyBaseF b)
pattern TyVar :: Var -> Type
pattern $bTyVar :: Var -> Type
$mTyVar :: forall {r}. Type -> (Var -> r) -> ((# #) -> r) -> r
TyVar v = Fix (TyVarF v)
pattern TyVoid :: Type
pattern $bTyVoid :: Type
$mTyVoid :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyVoid = Fix (TyBaseF BVoid)
pattern TyUnit :: Type
pattern $bTyUnit :: Type
$mTyUnit :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyUnit = Fix (TyBaseF BUnit)
pattern TyInt :: Type
pattern $bTyInt :: Type
$mTyInt :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyInt = Fix (TyBaseF BInt)
pattern TyText :: Type
pattern $bTyText :: Type
$mTyText :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyText = Fix (TyBaseF BText)
pattern TyDir :: Type
pattern $bTyDir :: Type
$mTyDir :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyDir = Fix (TyBaseF BDir)
pattern TyBool :: Type
pattern $bTyBool :: Type
$mTyBool :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyBool = Fix (TyBaseF BBool)
pattern TyActor :: Type
pattern $bTyActor :: Type
$mTyActor :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyActor = Fix (TyBaseF BActor)
pattern TyKey :: Type
pattern $bTyKey :: Type
$mTyKey :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyKey = Fix (TyBaseF BKey)
infixr 5 :+:
pattern (:+:) :: Type -> Type -> Type
pattern ty1 $b:+: :: Type -> Type -> Type
$m:+: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
:+: ty2 = Fix (TySumF ty1 ty2)
infixr 6 :*:
pattern (:*:) :: Type -> Type -> Type
pattern ty1 $b:*: :: Type -> Type -> Type
$m:*: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
:*: ty2 = Fix (TyProdF ty1 ty2)
infixr 1 :->:
pattern (:->:) :: Type -> Type -> Type
pattern ty1 $b:->: :: Type -> Type -> Type
$m:->: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
:->: ty2 = Fix (TyFunF ty1 ty2)
pattern TyRcd :: Map Var Type -> Type
pattern $bTyRcd :: Map Var Type -> Type
$mTyRcd :: forall {r}. Type -> (Map Var Type -> r) -> ((# #) -> r) -> r
TyRcd m = Fix (TyRcdF m)
pattern TyCmd :: Type -> Type
pattern $bTyCmd :: Type -> Type
$mTyCmd :: forall {r}. Type -> (Type -> r) -> ((# #) -> r) -> r
TyCmd ty1 = Fix (TyCmdF ty1)
pattern TyDelay :: Type -> Type
pattern $bTyDelay :: Type -> Type
$mTyDelay :: forall {r}. Type -> (Type -> r) -> ((# #) -> r) -> r
TyDelay ty1 = Fix (TyDelayF ty1)
pattern UTyBase :: BaseTy -> UType
pattern $bUTyBase :: BaseTy -> UType
$mUTyBase :: forall {r}. UType -> (BaseTy -> r) -> ((# #) -> r) -> r
UTyBase b = UTerm (TyBaseF b)
pattern UTyVar :: Var -> UType
pattern $bUTyVar :: Var -> UType
$mUTyVar :: forall {r}. UType -> (Var -> r) -> ((# #) -> r) -> r
UTyVar v = UTerm (TyVarF v)
pattern UTyVoid :: UType
pattern $bUTyVoid :: UType
$mUTyVoid :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
UTyVoid = UTerm (TyBaseF BVoid)
pattern UTyUnit :: UType
pattern $bUTyUnit :: UType
$mUTyUnit :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
UTyUnit = UTerm (TyBaseF BUnit)
pattern UTyInt :: UType
pattern $bUTyInt :: UType
$mUTyInt :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
UTyInt = UTerm (TyBaseF BInt)
pattern UTyText :: UType
pattern $bUTyText :: UType
$mUTyText :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
UTyText = UTerm (TyBaseF BText)
pattern UTyDir :: UType
pattern $bUTyDir :: UType
$mUTyDir :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
UTyDir = UTerm (TyBaseF BDir)
pattern UTyBool :: UType
pattern $bUTyBool :: UType
$mUTyBool :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
UTyBool = UTerm (TyBaseF BBool)
pattern UTyActor :: UType
pattern $bUTyActor :: UType
$mUTyActor :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
UTyActor = UTerm (TyBaseF BActor)
pattern UTyKey :: UType
pattern $bUTyKey :: UType
$mUTyKey :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
UTyKey = UTerm (TyBaseF BKey)
pattern UTySum :: UType -> UType -> UType
pattern $bUTySum :: UType -> UType -> UType
$mUTySum :: forall {r}. UType -> (UType -> UType -> r) -> ((# #) -> r) -> r
UTySum ty1 ty2 = UTerm (TySumF ty1 ty2)
pattern UTyProd :: UType -> UType -> UType
pattern $bUTyProd :: UType -> UType -> UType
$mUTyProd :: forall {r}. UType -> (UType -> UType -> r) -> ((# #) -> r) -> r
UTyProd ty1 ty2 = UTerm (TyProdF ty1 ty2)
pattern UTyFun :: UType -> UType -> UType
pattern $bUTyFun :: UType -> UType -> UType
$mUTyFun :: forall {r}. UType -> (UType -> UType -> r) -> ((# #) -> r) -> r
UTyFun ty1 ty2 = UTerm (TyFunF ty1 ty2)
pattern UTyRcd :: Map Var UType -> UType
pattern $bUTyRcd :: Map Var UType -> UType
$mUTyRcd :: forall {r}. UType -> (Map Var UType -> r) -> ((# #) -> r) -> r
UTyRcd m = UTerm (TyRcdF m)
pattern UTyCmd :: UType -> UType
pattern $bUTyCmd :: UType -> UType
$mUTyCmd :: forall {r}. UType -> (UType -> r) -> ((# #) -> r) -> r
UTyCmd ty1 = UTerm (TyCmdF ty1)
pattern UTyDelay :: UType -> UType
pattern $bUTyDelay :: UType -> UType
$mUTyDelay :: forall {r}. UType -> (UType -> r) -> ((# #) -> r) -> r
UTyDelay ty1 = UTerm (TyDelayF ty1)
pattern PolyUnit :: Polytype
pattern $bPolyUnit :: Polytype
$mPolyUnit :: forall {r}. Polytype -> ((# #) -> r) -> ((# #) -> r) -> r
PolyUnit = Forall [] (TyCmd TyUnit)
deriving instance Generic Type
deriving instance ToJSON Type
deriving instance FromJSON Type