{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Swarm.Language.Types (
BaseTy (..),
Var,
TypeF (..),
Type,
tyVars,
pattern TyBase,
pattern TyVar,
pattern TyUnit,
pattern TyInt,
pattern TyText,
pattern TyDir,
pattern TyBool,
pattern TyRobot,
pattern (:+:),
pattern (:*:),
pattern (:->:),
pattern TyCmd,
pattern TyDelay,
UType,
pattern UTyBase,
pattern UTyVar,
pattern UTyUnit,
pattern UTyInt,
pattern UTyText,
pattern UTyDir,
pattern UTyBool,
pattern UTyRobot,
pattern UTySum,
pattern UTyProd,
pattern UTyFun,
pattern UTyCmd,
pattern UTyDelay,
ucata,
mkVarName,
Poly (..),
Polytype,
UPolytype,
TCtx,
UCtx,
Module (..),
TModule,
UModule,
trivMod,
WithU (..),
) where
import Control.Unification
import Control.Unification.IntVar
import Data.Aeson (FromJSON, ToJSON)
import Data.Data (Data)
import Data.Foldable (fold)
import Data.Functor.Fixedpoint
import Data.Maybe (fromJust)
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
=
BUnit
|
BInt
|
BText
|
BDir
|
BBool
|
BRobot
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
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)
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, 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
data Module s t = Module {forall s t. Module s t -> s
moduleTy :: s, forall s t. Module s t -> Ctx t
moduleCtx :: Ctx t}
deriving (Int -> Module s t -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s t. (Show s, Show t) => Int -> Module s t -> ShowS
forall s t. (Show s, Show t) => [Module s t] -> ShowS
forall s t. (Show s, Show t) => Module s t -> String
showList :: [Module s t] -> ShowS
$cshowList :: forall s t. (Show s, Show t) => [Module s t] -> ShowS
show :: Module s t -> String
$cshow :: forall s t. (Show s, Show t) => Module s t -> String
showsPrec :: Int -> Module s t -> ShowS
$cshowsPrec :: forall s t. (Show s, Show t) => Int -> Module s t -> ShowS
Show, Module s t -> Module s t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s t. (Eq s, Eq t) => Module s t -> Module s t -> Bool
/= :: Module s t -> Module s t -> Bool
$c/= :: forall s t. (Eq s, Eq t) => Module s t -> Module s t -> Bool
== :: Module s t -> Module s t -> Bool
$c== :: forall s t. (Eq s, Eq t) => Module s t -> Module s t -> Bool
Eq, forall a b. a -> Module s b -> Module s a
forall a b. (a -> b) -> Module s a -> Module s b
forall s a b. a -> Module s b -> Module s a
forall s a b. (a -> b) -> Module s a -> Module s 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 -> Module s b -> Module s a
$c<$ :: forall s a b. a -> Module s b -> Module s a
fmap :: forall a b. (a -> b) -> Module s a -> Module s b
$cfmap :: forall s a b. (a -> b) -> Module s a -> Module s b
Functor, Module s t -> DataType
Module s t -> Constr
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 {s} {t}. (Data s, Data t) => Typeable (Module s t)
forall s t. (Data s, Data t) => Module s t -> DataType
forall s t. (Data s, Data t) => Module s t -> Constr
forall s t.
(Data s, Data t) =>
(forall b. Data b => b -> b) -> Module s t -> Module s t
forall s t u.
(Data s, Data t) =>
Int -> (forall d. Data d => d -> u) -> Module s t -> u
forall s t u.
(Data s, Data t) =>
(forall d. Data d => d -> u) -> Module s t -> [u]
forall s t r r'.
(Data s, Data t) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
forall s t r r'.
(Data s, Data t) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
forall s t (m :: * -> *).
(Data s, Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
forall s t (m :: * -> *).
(Data s, Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
forall s t (c :: * -> *).
(Data s, Data t) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Module s t)
forall s t (c :: * -> *).
(Data s, Data t) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Module s t -> c (Module s t)
forall s t (t :: * -> *) (c :: * -> *).
(Data s, Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Module s t))
forall s t (t :: * -> * -> *) (c :: * -> *).
(Data s, Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Module s t))
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Module s t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Module s t -> c (Module s t)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Module s t))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
$cgmapMo :: forall s t (m :: * -> *).
(Data s, Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
$cgmapMp :: forall s t (m :: * -> *).
(Data s, Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
$cgmapM :: forall s t (m :: * -> *).
(Data s, Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Module s t -> u
$cgmapQi :: forall s t u.
(Data s, Data t) =>
Int -> (forall d. Data d => d -> u) -> Module s t -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Module s t -> [u]
$cgmapQ :: forall s t u.
(Data s, Data t) =>
(forall d. Data d => d -> u) -> Module s t -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
$cgmapQr :: forall s t r r'.
(Data s, Data t) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
$cgmapQl :: forall s t r r'.
(Data s, Data t) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
gmapT :: (forall b. Data b => b -> b) -> Module s t -> Module s t
$cgmapT :: forall s t.
(Data s, Data t) =>
(forall b. Data b => b -> b) -> Module s t -> Module s t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Module s t))
$cdataCast2 :: forall s t (t :: * -> * -> *) (c :: * -> *).
(Data s, Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Module s t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Module s t))
$cdataCast1 :: forall s t (t :: * -> *) (c :: * -> *).
(Data s, Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Module s t))
dataTypeOf :: Module s t -> DataType
$cdataTypeOf :: forall s t. (Data s, Data t) => Module s t -> DataType
toConstr :: Module s t -> Constr
$ctoConstr :: forall s t. (Data s, Data t) => Module s t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Module s t)
$cgunfold :: forall s t (c :: * -> *).
(Data s, Data t) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Module s t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Module s t -> c (Module s t)
$cgfoldl :: forall s t (c :: * -> *).
(Data s, Data t) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Module s t -> c (Module s t)
Data, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s t x. Rep (Module s t) x -> Module s t
forall s t x. Module s t -> Rep (Module s t) x
$cto :: forall s t x. Rep (Module s t) x -> Module s t
$cfrom :: forall s t x. Module s t -> Rep (Module s t) x
Generic, forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
forall s t.
(FromJSON s, FromJSON t) =>
Value -> Parser [Module s t]
forall s t.
(FromJSON s, FromJSON t) =>
Value -> Parser (Module s t)
parseJSONList :: Value -> Parser [Module s t]
$cparseJSONList :: forall s t.
(FromJSON s, FromJSON t) =>
Value -> Parser [Module s t]
parseJSON :: Value -> Parser (Module s t)
$cparseJSON :: forall s t.
(FromJSON s, FromJSON t) =>
Value -> Parser (Module s t)
FromJSON, forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
forall s t. (ToJSON t, ToJSON s) => [Module s t] -> Encoding
forall s t. (ToJSON t, ToJSON s) => [Module s t] -> Value
forall s t. (ToJSON t, ToJSON s) => Module s t -> Encoding
forall s t. (ToJSON t, ToJSON s) => Module s t -> Value
toEncodingList :: [Module s t] -> Encoding
$ctoEncodingList :: forall s t. (ToJSON t, ToJSON s) => [Module s t] -> Encoding
toJSONList :: [Module s t] -> Value
$ctoJSONList :: forall s t. (ToJSON t, ToJSON s) => [Module s t] -> Value
toEncoding :: Module s t -> Encoding
$ctoEncoding :: forall s t. (ToJSON t, ToJSON s) => Module s t -> Encoding
toJSON :: Module s t -> Value
$ctoJSON :: forall s t. (ToJSON t, ToJSON s) => Module s t -> Value
ToJSON)
type TModule = Module Polytype Polytype
type UModule = Module UType UPolytype
trivMod :: s -> Module s t
trivMod :: forall s t. s -> Module s t
trivMod s
t = forall s t. s -> Ctx t -> Module s t
Module s
t forall t. Ctx t
empty
class WithU t where
type U t :: *
toU :: t -> U t
fromU :: U t -> 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 -> Type
fromU = forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) v. Traversable t => UTerm t v -> Maybe (Fix t)
freeze
instance (WithU t, Functor 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) -> f t
fromU = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. WithU t => U t -> 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 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 TyRobot :: Type
pattern $bTyRobot :: Type
$mTyRobot :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
TyRobot = Fix (TyBaseF BRobot)
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 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 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 UTyRobot :: UType
pattern $bUTyRobot :: UType
$mUTyRobot :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
UTyRobot = UTerm (TyBaseF BRobot)
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 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)
deriving instance Generic Type
deriving instance ToJSON Type
deriving instance FromJSON Type