{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

-- for the Data IntVar instance

-- |
-- Module      :  Swarm.Language.Types
-- Copyright   :  Brent Yorgey
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Types for the Swarm programming language and related utilities.
module Swarm.Language.Types (
  -- * Basic definitions
  BaseTy (..),
  Var,
  TypeF (..),

  -- * @Type@
  Type,
  tyVars,
  pattern TyBase,
  pattern TyVar,
  pattern TyVoid,
  pattern TyUnit,
  pattern TyInt,
  pattern TyText,
  pattern TyDir,
  pattern TyBool,
  pattern TyRobot,
  pattern (:+:),
  pattern (:*:),
  pattern (:->:),
  pattern TyCmd,
  pattern TyDelay,

  -- * @UType@
  UType,
  pattern UTyBase,
  pattern UTyVar,
  pattern UTyVoid,
  pattern UTyUnit,
  pattern UTyInt,
  pattern UTyText,
  pattern UTyDir,
  pattern UTyBool,
  pattern UTyRobot,
  pattern UTySum,
  pattern UTyProd,
  pattern UTyFun,
  pattern UTyCmd,
  pattern UTyDelay,

  -- ** Utilities
  ucata,
  mkVarName,

  -- * Polytypes
  Poly (..),
  Polytype,
  pattern PolyUnit,
  UPolytype,

  -- * Contexts
  TCtx,
  UCtx,

  -- * Modules
  Module (..),
  TModule,
  UModule,
  trivMod,

  -- * The 'WithU' class
  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

------------------------------------------------------------
-- Types
------------------------------------------------------------

-- | Base types.
data BaseTy
  = -- | The void type, with no inhabitants.
    BVoid
  | -- | The unit type, with a single inhabitant.
    BUnit
  | -- | Signed, arbitrary-size integers.
    BInt
  | -- | Unicode strings.
    BText
  | -- | Directions.
    BDir
  | -- | Booleans.
    BBool
  | -- | Robots.
    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)

-- | A "structure functor" encoding the shape of type expressions.
--   Actual types are then represented by taking a fixed point of this
--   functor.  We represent types in this way, via a "two-level type",
--   so that we can work with the @unification-fd@ package (see
--   https://byorgey.wordpress.com/2021/09/08/implementing-hindley-milner-with-the-unification-fd-library/).
data TypeF t
  = -- | A base type.
    TyBaseF BaseTy
  | -- | A type variable.
    TyVarF Var
  | -- | Commands, with return type.  Note that
    --   commands form a monad.
    TyCmdF t
  | -- | Type of delayed computations.
    TyDelayF t
  | -- | Sum type.
    TySumF t t
  | -- | Product type.
    TyProdF t t
  | -- | Function type.
    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@ is now defined as the fixed point of 'TypeF'.  It would be
--   annoying to manually apply and match against 'Fix' constructors
--   everywhere, so we provide pattern synonyms that allow us to work
--   with 'Type' as if it were defined in a directly recursive way.
type Type = Fix TypeF

-- | Get all the type variables contained in a 'Type'.
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)

-- The derived Data instance is so we can make a quasiquoter for types.
deriving instance Data Type

-- | 'UType's are like 'Type's, but also contain unification
--   variables.  'UType' is defined via 'UTerm', which is also a kind
--   of fixed point (in fact, 'UType' is the /free monad/ over 'TypeF').
--
--   Just as with 'Type', we provide a bunch of pattern synonyms for
--   working with 'UType' as if it were defined directly.
type UType = UTerm TypeF IntVar

-- The derived Data instances are so we can make a quasiquoter for
-- types.
deriving instance Data UType
deriving instance Data IntVar

-- | A generic /fold/ for things defined via 'UTerm' (including, in
--   particular, 'UType').  This probably belongs in the
--   @unification-fd@ package, but since it doesn't provide one, we
--   define it here.
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)

-- | A quick-and-dirty method for turning an 'IntVar' (used internally
--   as a unification variable) into a unique variable name, by
--   appending a number to the given name.
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)))

-- | For convenience, so we can write /e.g./ @"a"@ instead of @TyVar "a"@.
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)

------------------------------------------------------------
-- Contexts
------------------------------------------------------------

-- | A @TCtx@ is a mapping from variables to polytypes.  We generally
--   get one of these at the end of the type inference process.
type TCtx = Ctx Polytype

-- | A @UCtx@ is a mapping from variables to polytypes with
--   unification variables.  We generally have one of these while we
--   are in the midst of the type inference process.
type UCtx = Ctx UPolytype

------------------------------------------------------------
-- Polytypes
------------------------------------------------------------

-- | A @Poly t@ is a universally quantified @t@.  The variables in the
--   list are bound inside the @t@.  For example, the type @forall
--   a. a -> a@ would be represented as @Forall ["a"] (TyFun "a" "a")@.
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)

-- | A polytype without unification variables.
type Polytype = Poly Type

-- | A polytype with unification variables.
type UPolytype = Poly UType

------------------------------------------------------------
-- Modules
------------------------------------------------------------

-- | A module generally represents the result of performing type
--   inference on a top-level expression, which in particular can
--   contain definitions ('Swarm.Language.Syntax.TDef').  A module
--   contains the overall type of the expression, as well as the
--   context giving the types of any defined variables.
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)

-- | A 'TModule' is the final result of the type inference process on
--   an expression: we get a polytype for the expression, and a
--   context of polytypes for the defined variables.
type TModule = Module Polytype Polytype

-- | A 'UModule' represents the type of an expression at some
--   intermediate stage during the type inference process.  We get a
--   'UType' (/not/ a 'UPolytype') for the expression, which may
--   contain some free unification or type variables, as well as a
--   context of 'UPolytype's for any defined variables.
type UModule = Module UType UPolytype

-- | The trivial module for a given @s@, with the empty context.
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

------------------------------------------------------------
-- WithU
------------------------------------------------------------

-- | In several cases we have two versions of something: a "normal"
--   version, and a @U@ version with unification variables in it
--   (/e.g./ 'Type' vs 'UType', 'Polytype' vs 'UPolytype', 'TCtx' vs
--   'UCtx'). This class abstracts over the process of converting back
--   and forth between them.
--
--   In particular, @'WithU' t@ represents the fact that the type @t@
--   also has a @U@ counterpart, with a way to convert back and forth.
--   Note, however, that converting back may be "unsafe" in the sense
--   that it requires an extra burden of proof to guarantee that it is
--   used only on inputs that are safe.
class WithU t where
  -- | The associated "@U@-version" of the type @t@.
  type U t :: *

  -- | Convert from @t@ to its associated "@U@-version".  This
  --   direction is always safe (we simply have no unification
  --   variables even though the type allows it).
  toU :: t -> U t

  -- | Convert from the associated "@U@-version" back to @t@.
  --   Generally, this direction requires somehow knowing that there
  --   are no longer any unification variables in the value being
  --   converted.
  fromU :: U t -> t

-- | 'Type' is an instance of 'WithU', with associated type 'UType'.
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

-- | A 'WithU' instance can be lifted through any functor (including,
--   in particular, 'Ctx' and 'Poly').
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 synonyms
------------------------------------------------------------

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 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 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 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)

pattern PolyUnit :: Polytype
pattern $bPolyUnit :: Polytype
$mPolyUnit :: forall {r}. Polytype -> ((# #) -> r) -> ((# #) -> r) -> r
PolyUnit = Forall [] (TyCmd TyUnit)

-- Derive aeson instances for type serialization
deriving instance Generic Type
deriving instance ToJSON Type
deriving instance FromJSON Type