{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE LambdaCase #-}

module Intensional.Types
  ( RVar,
    Domain,
    Refined (..),
    DataType (..),
    Type,
    TypeGen (..),
    -- inj,
    decompType,
    subTyVar,
    tyconOf,
  )
where

import Binary
import Data.Bifunctor
import Data.Hashable
import qualified Data.IntSet as I
import Data.Map (Map)
import GHC.Generics hiding (prec)
import GhcPlugins hiding ((<>), Expr (..), Type)
import IfaceType

type RVar = Int

type Domain = I.IntSet

-- The class of objects containing refinement variables
class Refined t where
  domain :: t -> Domain
  rename :: RVar -> RVar -> t -> t
  prpr   :: (RVar -> SDoc) -> t -> SDoc

instance Refined b => Refined (Map a b) where
  domain :: Map a b -> Domain
domain = (b -> Domain) -> Map a b -> Domain
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> Domain
forall t. Refined t => t -> Domain
domain
  rename :: RVar -> RVar -> Map a b -> Map a b
rename x :: RVar
x y :: RVar
y = (b -> b) -> Map a b -> Map a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RVar -> RVar -> b -> b
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y)
  prpr :: (RVar -> SDoc) -> Map a b -> SDoc
prpr m :: RVar -> SDoc
m = (b -> SDoc -> SDoc) -> SDoc -> Map a b -> SDoc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SDoc -> SDoc -> SDoc
($$) (SDoc -> SDoc -> SDoc) -> (b -> SDoc) -> b -> SDoc -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RVar -> SDoc) -> b -> SDoc
forall t. Refined t => (RVar -> SDoc) -> t -> SDoc
prpr RVar -> SDoc
m) SDoc
empty

-- A datatype identifier
-- d is TyCon, IfaceTyCon or Name
data DataType d
  = Base d
  | Inj RVar d -- Extended datatypes from the canonical environment
  deriving (DataType d -> DataType d -> Bool
(DataType d -> DataType d -> Bool)
-> (DataType d -> DataType d -> Bool) -> Eq (DataType d)
forall d. Eq d => DataType d -> DataType d -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataType d -> DataType d -> Bool
$c/= :: forall d. Eq d => DataType d -> DataType d -> Bool
== :: DataType d -> DataType d -> Bool
$c== :: forall d. Eq d => DataType d -> DataType d -> Bool
Eq, a -> DataType b -> DataType a
(a -> b) -> DataType a -> DataType b
(forall a b. (a -> b) -> DataType a -> DataType b)
-> (forall a b. a -> DataType b -> DataType a) -> Functor DataType
forall a b. a -> DataType b -> DataType a
forall a b. (a -> b) -> DataType a -> DataType b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> DataType b -> DataType a
$c<$ :: forall a b. a -> DataType b -> DataType a
fmap :: (a -> b) -> DataType a -> DataType b
$cfmap :: forall a b. (a -> b) -> DataType a -> DataType b
Functor, DataType a -> Bool
(a -> m) -> DataType a -> m
(a -> b -> b) -> b -> DataType a -> b
(forall m. Monoid m => DataType m -> m)
-> (forall m a. Monoid m => (a -> m) -> DataType a -> m)
-> (forall m a. Monoid m => (a -> m) -> DataType a -> m)
-> (forall a b. (a -> b -> b) -> b -> DataType a -> b)
-> (forall a b. (a -> b -> b) -> b -> DataType a -> b)
-> (forall b a. (b -> a -> b) -> b -> DataType a -> b)
-> (forall b a. (b -> a -> b) -> b -> DataType a -> b)
-> (forall a. (a -> a -> a) -> DataType a -> a)
-> (forall a. (a -> a -> a) -> DataType a -> a)
-> (forall a. DataType a -> [a])
-> (forall a. DataType a -> Bool)
-> (forall a. DataType a -> RVar)
-> (forall a. Eq a => a -> DataType a -> Bool)
-> (forall a. Ord a => DataType a -> a)
-> (forall a. Ord a => DataType a -> a)
-> (forall a. Num a => DataType a -> a)
-> (forall a. Num a => DataType a -> a)
-> Foldable DataType
forall a. Eq a => a -> DataType a -> Bool
forall a. Num a => DataType a -> a
forall a. Ord a => DataType a -> a
forall m. Monoid m => DataType m -> m
forall a. DataType a -> Bool
forall a. DataType a -> RVar
forall a. DataType a -> [a]
forall a. (a -> a -> a) -> DataType a -> a
forall m a. Monoid m => (a -> m) -> DataType a -> m
forall b a. (b -> a -> b) -> b -> DataType a -> b
forall a b. (a -> b -> b) -> b -> DataType 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 -> RVar)
-> (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 :: DataType a -> a
$cproduct :: forall a. Num a => DataType a -> a
sum :: DataType a -> a
$csum :: forall a. Num a => DataType a -> a
minimum :: DataType a -> a
$cminimum :: forall a. Ord a => DataType a -> a
maximum :: DataType a -> a
$cmaximum :: forall a. Ord a => DataType a -> a
elem :: a -> DataType a -> Bool
$celem :: forall a. Eq a => a -> DataType a -> Bool
length :: DataType a -> RVar
$clength :: forall a. DataType a -> RVar
null :: DataType a -> Bool
$cnull :: forall a. DataType a -> Bool
toList :: DataType a -> [a]
$ctoList :: forall a. DataType a -> [a]
foldl1 :: (a -> a -> a) -> DataType a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> DataType a -> a
foldr1 :: (a -> a -> a) -> DataType a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> DataType a -> a
foldl' :: (b -> a -> b) -> b -> DataType a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> DataType a -> b
foldl :: (b -> a -> b) -> b -> DataType a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> DataType a -> b
foldr' :: (a -> b -> b) -> b -> DataType a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> DataType a -> b
foldr :: (a -> b -> b) -> b -> DataType a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> DataType a -> b
foldMap' :: (a -> m) -> DataType a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> DataType a -> m
foldMap :: (a -> m) -> DataType a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> DataType a -> m
fold :: DataType m -> m
$cfold :: forall m. Monoid m => DataType m -> m
Foldable, (forall x. DataType d -> Rep (DataType d) x)
-> (forall x. Rep (DataType d) x -> DataType d)
-> Generic (DataType d)
forall x. Rep (DataType d) x -> DataType d
forall x. DataType d -> Rep (DataType d) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall d x. Rep (DataType d) x -> DataType d
forall d x. DataType d -> Rep (DataType d) x
$cto :: forall d x. Rep (DataType d) x -> DataType d
$cfrom :: forall d x. DataType d -> Rep (DataType d) x
Generic, Functor DataType
Foldable DataType
(Functor DataType, Foldable DataType) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> DataType a -> f (DataType b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    DataType (f a) -> f (DataType a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> DataType a -> m (DataType b))
-> (forall (m :: * -> *) a.
    Monad m =>
    DataType (m a) -> m (DataType a))
-> Traversable DataType
(a -> f b) -> DataType a -> f (DataType b)
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 => DataType (m a) -> m (DataType a)
forall (f :: * -> *) a.
Applicative f =>
DataType (f a) -> f (DataType a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> DataType a -> m (DataType b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> DataType a -> f (DataType b)
sequence :: DataType (m a) -> m (DataType a)
$csequence :: forall (m :: * -> *) a. Monad m => DataType (m a) -> m (DataType a)
mapM :: (a -> m b) -> DataType a -> m (DataType b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> DataType a -> m (DataType b)
sequenceA :: DataType (f a) -> f (DataType a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
DataType (f a) -> f (DataType a)
traverse :: (a -> f b) -> DataType a -> f (DataType b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> DataType a -> f (DataType b)
$cp2Traversable :: Foldable DataType
$cp1Traversable :: Functor DataType
Traversable)

instance Hashable d => Hashable (DataType d)

instance Outputable d => Outputable (DataType d) where
  ppr :: DataType d -> SDoc
ppr = (RVar -> SDoc) -> DataType d -> SDoc
forall t. Refined t => (RVar -> SDoc) -> t -> SDoc
prpr RVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr 

instance Binary d => Binary (DataType d) where
  put_ :: BinHandle -> DataType d -> IO ()
put_ bh :: BinHandle
bh (Base d :: d
d) = BinHandle -> Bool -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh Bool
False IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> d -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh d
d
  put_ bh :: BinHandle
bh (Inj x :: RVar
x d :: d
d) =  BinHandle -> Bool -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh Bool
True IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> RVar -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh RVar
x IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> d -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh d
d
  get :: BinHandle -> IO (DataType d)
get bh :: BinHandle
bh =
    BinHandle -> IO Bool
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh IO Bool -> (Bool -> IO (DataType d)) -> IO (DataType d)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      False -> d -> DataType d
forall d. d -> DataType d
Base (d -> DataType d) -> IO d -> IO (DataType d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO d
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      True -> RVar -> d -> DataType d
forall d. RVar -> d -> DataType d
Inj (RVar -> d -> DataType d) -> IO RVar -> IO (d -> DataType d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO RVar
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh IO (d -> DataType d) -> IO d -> IO (DataType d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BinHandle -> IO d
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh

instance Outputable d => Refined (DataType d) where
  domain :: DataType d -> Domain
domain (Base _) = Domain
I.empty
  domain (Inj x :: RVar
x _) = RVar -> Domain
I.singleton RVar
x

  rename :: RVar -> RVar -> DataType d -> DataType d
rename x :: RVar
x y :: RVar
y (Inj z :: RVar
z d :: d
d)
    | RVar
x RVar -> RVar -> Bool
forall a. Eq a => a -> a -> Bool
== RVar
z = RVar -> d -> DataType d
forall d. RVar -> d -> DataType d
Inj RVar
y d
d
  rename _ _ d :: DataType d
d = DataType d
d

  prpr :: (RVar -> SDoc) -> DataType d -> SDoc
prpr _ (Base d :: d
d) = d -> SDoc
forall a. Outputable a => a -> SDoc
ppr d
d
  prpr m :: RVar -> SDoc
m (Inj x :: RVar
x d :: d
d) = [SDoc] -> SDoc
hcat [String -> SDoc
text "inj_", RVar -> SDoc
m RVar
x] SDoc -> SDoc -> SDoc
<+> d -> SDoc
forall a. Outputable a => a -> SDoc
ppr d
d

-- Check if a core datatype contains covariant arguments
-- covariant :: TyCon -> Bool
-- covariant = all pos . concatMap dataConOrigArgTys . tyConDataCons
--   where
--     pos, neg :: Type -> Bool
--     pos (FunTy t1 t2) = neg t1 && pos t2
--     pos _ = True
--     neg (FunTy t1 t2) = pos t1 && neg t2
--     neg (TyConApp _ _) = False -- These cases are overapproximate
--     neg (TyVarTy _) = False
--     neg _ = True



-- Get the tycon from a datatype
tyconOf :: DataType d -> d
tyconOf :: DataType d -> d
tyconOf (Base d :: d
d) = d
d
tyconOf (Inj _ d :: d
d) = d
d

type Type = TypeGen TyCon

-- Monomorphic types parameterised by type constructors
data TypeGen d
  = Var Name
  | App (TypeGen d) (TypeGen d)
  | Data (DataType d) [TypeGen d]
  | TypeGen d :=> TypeGen d
  | Lit IfaceTyLit
  | Ambiguous -- Ambiguous hides higher-ranked types and casts
  deriving (a -> TypeGen b -> TypeGen a
(a -> b) -> TypeGen a -> TypeGen b
(forall a b. (a -> b) -> TypeGen a -> TypeGen b)
-> (forall a b. a -> TypeGen b -> TypeGen a) -> Functor TypeGen
forall a b. a -> TypeGen b -> TypeGen a
forall a b. (a -> b) -> TypeGen a -> TypeGen b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> TypeGen b -> TypeGen a
$c<$ :: forall a b. a -> TypeGen b -> TypeGen a
fmap :: (a -> b) -> TypeGen a -> TypeGen b
$cfmap :: forall a b. (a -> b) -> TypeGen a -> TypeGen b
Functor, TypeGen a -> Bool
(a -> m) -> TypeGen a -> m
(a -> b -> b) -> b -> TypeGen a -> b
(forall m. Monoid m => TypeGen m -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeGen a -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeGen a -> m)
-> (forall a b. (a -> b -> b) -> b -> TypeGen a -> b)
-> (forall a b. (a -> b -> b) -> b -> TypeGen a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeGen a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeGen a -> b)
-> (forall a. (a -> a -> a) -> TypeGen a -> a)
-> (forall a. (a -> a -> a) -> TypeGen a -> a)
-> (forall a. TypeGen a -> [a])
-> (forall a. TypeGen a -> Bool)
-> (forall a. TypeGen a -> RVar)
-> (forall a. Eq a => a -> TypeGen a -> Bool)
-> (forall a. Ord a => TypeGen a -> a)
-> (forall a. Ord a => TypeGen a -> a)
-> (forall a. Num a => TypeGen a -> a)
-> (forall a. Num a => TypeGen a -> a)
-> Foldable TypeGen
forall a. Eq a => a -> TypeGen a -> Bool
forall a. Num a => TypeGen a -> a
forall a. Ord a => TypeGen a -> a
forall m. Monoid m => TypeGen m -> m
forall a. TypeGen a -> Bool
forall a. TypeGen a -> RVar
forall a. TypeGen a -> [a]
forall a. (a -> a -> a) -> TypeGen a -> a
forall m a. Monoid m => (a -> m) -> TypeGen a -> m
forall b a. (b -> a -> b) -> b -> TypeGen a -> b
forall a b. (a -> b -> b) -> b -> TypeGen 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 -> RVar)
-> (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 :: TypeGen a -> a
$cproduct :: forall a. Num a => TypeGen a -> a
sum :: TypeGen a -> a
$csum :: forall a. Num a => TypeGen a -> a
minimum :: TypeGen a -> a
$cminimum :: forall a. Ord a => TypeGen a -> a
maximum :: TypeGen a -> a
$cmaximum :: forall a. Ord a => TypeGen a -> a
elem :: a -> TypeGen a -> Bool
$celem :: forall a. Eq a => a -> TypeGen a -> Bool
length :: TypeGen a -> RVar
$clength :: forall a. TypeGen a -> RVar
null :: TypeGen a -> Bool
$cnull :: forall a. TypeGen a -> Bool
toList :: TypeGen a -> [a]
$ctoList :: forall a. TypeGen a -> [a]
foldl1 :: (a -> a -> a) -> TypeGen a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeGen a -> a
foldr1 :: (a -> a -> a) -> TypeGen a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> TypeGen a -> a
foldl' :: (b -> a -> b) -> b -> TypeGen a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypeGen a -> b
foldl :: (b -> a -> b) -> b -> TypeGen a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypeGen a -> b
foldr' :: (a -> b -> b) -> b -> TypeGen a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypeGen a -> b
foldr :: (a -> b -> b) -> b -> TypeGen a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeGen a -> b
foldMap' :: (a -> m) -> TypeGen a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypeGen a -> m
foldMap :: (a -> m) -> TypeGen a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeGen a -> m
fold :: TypeGen m -> m
$cfold :: forall m. Monoid m => TypeGen m -> m
Foldable, Functor TypeGen
Foldable TypeGen
(Functor TypeGen, Foldable TypeGen) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TypeGen a -> f (TypeGen b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TypeGen (f a) -> f (TypeGen a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TypeGen a -> m (TypeGen b))
-> (forall (m :: * -> *) a.
    Monad m =>
    TypeGen (m a) -> m (TypeGen a))
-> Traversable TypeGen
(a -> f b) -> TypeGen a -> f (TypeGen b)
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 => TypeGen (m a) -> m (TypeGen a)
forall (f :: * -> *) a.
Applicative f =>
TypeGen (f a) -> f (TypeGen a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeGen a -> m (TypeGen b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeGen a -> f (TypeGen b)
sequence :: TypeGen (m a) -> m (TypeGen a)
$csequence :: forall (m :: * -> *) a. Monad m => TypeGen (m a) -> m (TypeGen a)
mapM :: (a -> m b) -> TypeGen a -> m (TypeGen b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeGen a -> m (TypeGen b)
sequenceA :: TypeGen (f a) -> f (TypeGen a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypeGen (f a) -> f (TypeGen a)
traverse :: (a -> f b) -> TypeGen a -> f (TypeGen b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeGen a -> f (TypeGen b)
$cp2Traversable :: Foldable TypeGen
$cp1Traversable :: Functor TypeGen
Traversable)

-- Clone of a Outputable Core.Type
instance Outputable d => Outputable (TypeGen d) where
  ppr :: TypeGen d -> SDoc
ppr = (RVar -> SDoc) -> TypeGen d -> SDoc
forall t. Refined t => (RVar -> SDoc) -> t -> SDoc
prpr RVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr
      
instance Binary d => Binary (TypeGen d) where
  put_ :: BinHandle -> TypeGen d -> IO ()
put_ bh :: BinHandle
bh (Var a :: Name
a) = BinHandle -> RVar -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (0 :: Int) IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> Name -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh Name
a
  put_ bh :: BinHandle
bh (App a :: TypeGen d
a b :: TypeGen d
b) = BinHandle -> RVar -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (1 :: Int) IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> TypeGen d -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh TypeGen d
a IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> TypeGen d -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh TypeGen d
b
  put_ bh :: BinHandle
bh (Data d :: DataType d
d as :: [TypeGen d]
as) = BinHandle -> RVar -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (2 :: Int) IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> DataType d -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh DataType d
d IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> [TypeGen d] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh [TypeGen d]
as
  put_ bh :: BinHandle
bh (a :: TypeGen d
a :=> b :: TypeGen d
b) = BinHandle -> RVar -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (3 :: Int) IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> TypeGen d -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh TypeGen d
a IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> TypeGen d -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh TypeGen d
b
  put_ bh :: BinHandle
bh (Lit l :: IfaceTyLit
l) = BinHandle -> RVar -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (4 :: Int) IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> IfaceTyLit -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh IfaceTyLit
l
  put_ bh :: BinHandle
bh Ambiguous = BinHandle -> RVar -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (5 :: Int)

  get :: BinHandle -> IO (TypeGen d)
get bh :: BinHandle
bh = do
    RVar
n <- BinHandle -> IO RVar
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
    case RVar
n :: Int of
      0 -> Name -> TypeGen d
forall d. Name -> TypeGen d
Var (Name -> TypeGen d) -> IO Name -> IO (TypeGen d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO Name
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      1 -> TypeGen d -> TypeGen d -> TypeGen d
forall d. TypeGen d -> TypeGen d -> TypeGen d
App (TypeGen d -> TypeGen d -> TypeGen d)
-> IO (TypeGen d) -> IO (TypeGen d -> TypeGen d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO (TypeGen d)
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh IO (TypeGen d -> TypeGen d) -> IO (TypeGen d) -> IO (TypeGen d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BinHandle -> IO (TypeGen d)
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      2 -> DataType d -> [TypeGen d] -> TypeGen d
forall d. DataType d -> [TypeGen d] -> TypeGen d
Data (DataType d -> [TypeGen d] -> TypeGen d)
-> IO (DataType d) -> IO ([TypeGen d] -> TypeGen d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO (DataType d)
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh IO ([TypeGen d] -> TypeGen d) -> IO [TypeGen d] -> IO (TypeGen d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BinHandle -> IO [TypeGen d]
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      3 -> TypeGen d -> TypeGen d -> TypeGen d
forall d. TypeGen d -> TypeGen d -> TypeGen d
(:=>) (TypeGen d -> TypeGen d -> TypeGen d)
-> IO (TypeGen d) -> IO (TypeGen d -> TypeGen d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO (TypeGen d)
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh IO (TypeGen d -> TypeGen d) -> IO (TypeGen d) -> IO (TypeGen d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BinHandle -> IO (TypeGen d)
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      4 -> IfaceTyLit -> TypeGen d
forall d. IfaceTyLit -> TypeGen d
Lit (IfaceTyLit -> TypeGen d) -> IO IfaceTyLit -> IO (TypeGen d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO IfaceTyLit
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      5 -> TypeGen d -> IO (TypeGen d)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeGen d
forall d. TypeGen d
Ambiguous
      _ -> String -> SDoc -> IO (TypeGen d)
forall a. HasCallStack => String -> SDoc -> a
pprPanic "Invalid binary file!" (SDoc -> IO (TypeGen d)) -> SDoc -> IO (TypeGen d)
forall a b. (a -> b) -> a -> b
$ RVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr RVar
n

instance Outputable d => Refined (TypeGen d) where
  domain :: TypeGen d -> Domain
domain (App a :: TypeGen d
a b :: TypeGen d
b) = TypeGen d -> Domain
forall t. Refined t => t -> Domain
domain TypeGen d
a Domain -> Domain -> Domain
forall a. Semigroup a => a -> a -> a
<> TypeGen d -> Domain
forall t. Refined t => t -> Domain
domain TypeGen d
b
  domain (Data d :: DataType d
d as :: [TypeGen d]
as) = DataType d -> Domain
forall t. Refined t => t -> Domain
domain DataType d
d Domain -> Domain -> Domain
forall a. Semigroup a => a -> a -> a
<> (TypeGen d -> Domain) -> [TypeGen d] -> Domain
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TypeGen d -> Domain
forall t. Refined t => t -> Domain
domain [TypeGen d]
as
  domain (a :: TypeGen d
a :=> b :: TypeGen d
b) = TypeGen d -> Domain
forall t. Refined t => t -> Domain
domain TypeGen d
a Domain -> Domain -> Domain
forall a. Semigroup a => a -> a -> a
<> TypeGen d -> Domain
forall t. Refined t => t -> Domain
domain TypeGen d
b
  domain _ = Domain
forall a. Monoid a => a
mempty

  rename :: RVar -> RVar -> TypeGen d -> TypeGen d
rename x :: RVar
x y :: RVar
y (App a :: TypeGen d
a b :: TypeGen d
b) = TypeGen d -> TypeGen d -> TypeGen d
forall d. TypeGen d -> TypeGen d -> TypeGen d
App (RVar -> RVar -> TypeGen d -> TypeGen d
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y TypeGen d
a) (RVar -> RVar -> TypeGen d -> TypeGen d
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y TypeGen d
b)
  rename x :: RVar
x y :: RVar
y (Data d :: DataType d
d as :: [TypeGen d]
as) = DataType d -> [TypeGen d] -> TypeGen d
forall d. DataType d -> [TypeGen d] -> TypeGen d
Data (RVar -> RVar -> DataType d -> DataType d
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y DataType d
d) (RVar -> RVar -> TypeGen d -> TypeGen d
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y (TypeGen d -> TypeGen d) -> [TypeGen d] -> [TypeGen d]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TypeGen d]
as)
  rename x :: RVar
x y :: RVar
y (a :: TypeGen d
a :=> b :: TypeGen d
b) = RVar -> RVar -> TypeGen d -> TypeGen d
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y TypeGen d
a TypeGen d -> TypeGen d -> TypeGen d
forall d. TypeGen d -> TypeGen d -> TypeGen d
:=> RVar -> RVar -> TypeGen d -> TypeGen d
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y TypeGen d
b
  rename _ _ t :: TypeGen d
t = TypeGen d
t

  prpr :: (RVar -> SDoc) -> TypeGen d -> SDoc
prpr m :: RVar -> SDoc
m = PprPrec -> TypeGen d -> SDoc
forall d. Outputable d => PprPrec -> TypeGen d -> SDoc
pprTy PprPrec
topPrec
    where
      pprTy :: Outputable d => PprPrec -> TypeGen d -> SDoc
      pprTy :: PprPrec -> TypeGen d -> SDoc
pprTy _ (Var a :: Name
a) = Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
a
      pprTy prec :: PprPrec
prec (App t1 :: TypeGen d
t1 t2 :: TypeGen d
t2) = SDoc -> RVar -> SDoc -> SDoc
hang (PprPrec -> TypeGen d -> SDoc
forall d. Outputable d => PprPrec -> TypeGen d -> SDoc
pprTy PprPrec
prec TypeGen d
t1) 2 (PprPrec -> TypeGen d -> SDoc
forall d. Outputable d => PprPrec -> TypeGen d -> SDoc
pprTy PprPrec
appPrec TypeGen d
t2)
      pprTy _ (Data d :: DataType d
d as :: [TypeGen d]
as) = SDoc -> RVar -> SDoc -> SDoc
hang ((RVar -> SDoc) -> DataType d -> SDoc
forall t. Refined t => (RVar -> SDoc) -> t -> SDoc
prpr RVar -> SDoc
m DataType d
d) 2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep [[SDoc] -> SDoc
hcat [String -> SDoc
text "@", PprPrec -> TypeGen d -> SDoc
forall d. Outputable d => PprPrec -> TypeGen d -> SDoc
pprTy PprPrec
appPrec TypeGen d
a] | TypeGen d
a <- [TypeGen d]
as]
      pprTy prec :: PprPrec
prec (t1 :: TypeGen d
t1 :=> t2 :: TypeGen d
t2) = PprPrec -> PprPrec -> SDoc -> SDoc
maybeParen PprPrec
prec PprPrec
funPrec (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep [PprPrec -> TypeGen d -> SDoc
forall d. Outputable d => PprPrec -> TypeGen d -> SDoc
pprTy PprPrec
funPrec TypeGen d
t1, SDoc
arrow, PprPrec -> TypeGen d -> SDoc
forall d. Outputable d => PprPrec -> TypeGen d -> SDoc
pprTy PprPrec
prec TypeGen d
t2]
      pprTy _ (Lit l :: IfaceTyLit
l) = IfaceTyLit -> SDoc
forall a. Outputable a => a -> SDoc
ppr IfaceTyLit
l
      pprTy _ Ambiguous = String -> SDoc
text "<?>"

-- Inject a sort into a refinement environment
-- inj :: Int -> TypeGen d -> TypeGen d
-- inj _ (Var a) = Var a
-- inj x (App a b) = App (inj x a) (inj x b)
-- inj x (Data (Base b) as) = Data (Base b) (inj x <$> as)
-- inj x (Data (Inj _ d) as) = Data (Inj x d) (inj x <$> as)
-- inj x (a :=> b) = inj x a :=> inj x b
-- inj _ (Lit l) = Lit l
-- inj _ Ambiguous = Ambiguous

-- Decompose a functions into its arguments and eventual return type
decompType :: TypeGen d -> ([TypeGen d], TypeGen d)
decompType :: TypeGen d -> ([TypeGen d], TypeGen d)
decompType (a :: TypeGen d
a :=> b :: TypeGen d
b) = ([TypeGen d] -> [TypeGen d])
-> ([TypeGen d], TypeGen d) -> ([TypeGen d], TypeGen d)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([TypeGen d] -> [TypeGen d] -> [TypeGen d]
forall a. [a] -> [a] -> [a]
++ [TypeGen d
a]) (TypeGen d -> ([TypeGen d], TypeGen d)
forall d. TypeGen d -> ([TypeGen d], TypeGen d)
decompType TypeGen d
b)
decompType a :: TypeGen d
a = ([], TypeGen d
a)

-- Type variable substitution
subTyVar :: Outputable d => Name -> TypeGen d -> TypeGen d -> TypeGen d
subTyVar :: Name -> TypeGen d -> TypeGen d -> TypeGen d
subTyVar a :: Name
a t :: TypeGen d
t (Var a' :: Name
a')
  | Name
a Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
a' = TypeGen d
t
  | Bool
otherwise = Name -> TypeGen d
forall d. Name -> TypeGen d
Var Name
a'
subTyVar a :: Name
a t :: TypeGen d
t (App x :: TypeGen d
x y :: TypeGen d
y) = TypeGen d -> TypeGen d -> TypeGen d
forall d. Outputable d => TypeGen d -> TypeGen d -> TypeGen d
applyType (Name -> TypeGen d -> TypeGen d -> TypeGen d
forall d.
Outputable d =>
Name -> TypeGen d -> TypeGen d -> TypeGen d
subTyVar Name
a TypeGen d
t TypeGen d
x) (Name -> TypeGen d -> TypeGen d -> TypeGen d
forall d.
Outputable d =>
Name -> TypeGen d -> TypeGen d -> TypeGen d
subTyVar Name
a TypeGen d
t TypeGen d
y)
subTyVar a :: Name
a t :: TypeGen d
t (Data d :: DataType d
d as :: [TypeGen d]
as) = DataType d -> [TypeGen d] -> TypeGen d
forall d. DataType d -> [TypeGen d] -> TypeGen d
Data DataType d
d (Name -> TypeGen d -> TypeGen d -> TypeGen d
forall d.
Outputable d =>
Name -> TypeGen d -> TypeGen d -> TypeGen d
subTyVar Name
a TypeGen d
t (TypeGen d -> TypeGen d) -> [TypeGen d] -> [TypeGen d]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TypeGen d]
as)
subTyVar a :: Name
a t :: TypeGen d
t (x :: TypeGen d
x :=> y :: TypeGen d
y) = Name -> TypeGen d -> TypeGen d -> TypeGen d
forall d.
Outputable d =>
Name -> TypeGen d -> TypeGen d -> TypeGen d
subTyVar Name
a TypeGen d
t TypeGen d
x TypeGen d -> TypeGen d -> TypeGen d
forall d. TypeGen d -> TypeGen d -> TypeGen d
:=> Name -> TypeGen d -> TypeGen d -> TypeGen d
forall d.
Outputable d =>
Name -> TypeGen d -> TypeGen d -> TypeGen d
subTyVar Name
a TypeGen d
t TypeGen d
y
subTyVar _ _ t :: TypeGen d
t = TypeGen d
t

-- Unsaturated type application
applyType :: Outputable d => TypeGen d -> TypeGen d -> TypeGen d
applyType :: TypeGen d -> TypeGen d -> TypeGen d
applyType (Var a :: Name
a) t :: TypeGen d
t = TypeGen d -> TypeGen d -> TypeGen d
forall d. TypeGen d -> TypeGen d -> TypeGen d
App (Name -> TypeGen d
forall d. Name -> TypeGen d
Var Name
a) TypeGen d
t
applyType (App a :: TypeGen d
a b :: TypeGen d
b) t :: TypeGen d
t = TypeGen d -> TypeGen d -> TypeGen d
forall d. TypeGen d -> TypeGen d -> TypeGen d
App (TypeGen d -> TypeGen d -> TypeGen d
forall d. TypeGen d -> TypeGen d -> TypeGen d
App TypeGen d
a TypeGen d
b) TypeGen d
t
applyType (Data d :: DataType d
d as :: [TypeGen d]
as) t :: TypeGen d
t = DataType d -> [TypeGen d] -> TypeGen d
forall d. DataType d -> [TypeGen d] -> TypeGen d
Data DataType d
d ([TypeGen d]
as [TypeGen d] -> [TypeGen d] -> [TypeGen d]
forall a. [a] -> [a] -> [a]
++ [TypeGen d
t])
applyType Ambiguous _ = TypeGen d
forall d. TypeGen d
Ambiguous
applyType a :: TypeGen d
a b :: TypeGen d
b = String -> SDoc -> TypeGen d
forall a. HasCallStack => String -> SDoc -> a
pprPanic "The type is already saturated!" (SDoc -> TypeGen d) -> SDoc -> TypeGen d
forall a b. (a -> b) -> a -> b
$ (TypeGen d, TypeGen d) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TypeGen d
a, TypeGen d
b)