{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE PatternSynonyms #-}

module Intensional.Scheme
  ( Scheme,
    SchemeGen (..),
    pattern Forall,
    mono,
    Intensional.Scheme.unsats
  )
where

import Binary
import Intensional.Constraints as Constraints
import qualified Data.IntSet as I
import qualified Data.IntMap as IntMap
import GhcPlugins 
import Intensional.Types

type Scheme = SchemeGen TyCon

-- Constrained polymorphic types
data SchemeGen d
  = Scheme
      { SchemeGen d -> [Name]
tyvars :: [Name],
        SchemeGen d -> Domain
boundvs :: Domain,
        SchemeGen d -> TypeGen d
body :: TypeGen d,
        SchemeGen d -> ConstraintSet
constraints :: ConstraintSet
      }
  deriving (a -> SchemeGen b -> SchemeGen a
(a -> b) -> SchemeGen a -> SchemeGen b
(forall a b. (a -> b) -> SchemeGen a -> SchemeGen b)
-> (forall a b. a -> SchemeGen b -> SchemeGen a)
-> Functor SchemeGen
forall a b. a -> SchemeGen b -> SchemeGen a
forall a b. (a -> b) -> SchemeGen a -> SchemeGen b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SchemeGen b -> SchemeGen a
$c<$ :: forall a b. a -> SchemeGen b -> SchemeGen a
fmap :: (a -> b) -> SchemeGen a -> SchemeGen b
$cfmap :: forall a b. (a -> b) -> SchemeGen a -> SchemeGen b
Functor, SchemeGen a -> Bool
(a -> m) -> SchemeGen a -> m
(a -> b -> b) -> b -> SchemeGen a -> b
(forall m. Monoid m => SchemeGen m -> m)
-> (forall m a. Monoid m => (a -> m) -> SchemeGen a -> m)
-> (forall m a. Monoid m => (a -> m) -> SchemeGen a -> m)
-> (forall a b. (a -> b -> b) -> b -> SchemeGen a -> b)
-> (forall a b. (a -> b -> b) -> b -> SchemeGen a -> b)
-> (forall b a. (b -> a -> b) -> b -> SchemeGen a -> b)
-> (forall b a. (b -> a -> b) -> b -> SchemeGen a -> b)
-> (forall a. (a -> a -> a) -> SchemeGen a -> a)
-> (forall a. (a -> a -> a) -> SchemeGen a -> a)
-> (forall a. SchemeGen a -> [a])
-> (forall a. SchemeGen a -> Bool)
-> (forall a. SchemeGen a -> Int)
-> (forall a. Eq a => a -> SchemeGen a -> Bool)
-> (forall a. Ord a => SchemeGen a -> a)
-> (forall a. Ord a => SchemeGen a -> a)
-> (forall a. Num a => SchemeGen a -> a)
-> (forall a. Num a => SchemeGen a -> a)
-> Foldable SchemeGen
forall a. Eq a => a -> SchemeGen a -> Bool
forall a. Num a => SchemeGen a -> a
forall a. Ord a => SchemeGen a -> a
forall m. Monoid m => SchemeGen m -> m
forall a. SchemeGen a -> Bool
forall a. SchemeGen a -> Int
forall a. SchemeGen a -> [a]
forall a. (a -> a -> a) -> SchemeGen a -> a
forall m a. Monoid m => (a -> m) -> SchemeGen a -> m
forall b a. (b -> a -> b) -> b -> SchemeGen a -> b
forall a b. (a -> b -> b) -> b -> SchemeGen 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 :: SchemeGen a -> a
$cproduct :: forall a. Num a => SchemeGen a -> a
sum :: SchemeGen a -> a
$csum :: forall a. Num a => SchemeGen a -> a
minimum :: SchemeGen a -> a
$cminimum :: forall a. Ord a => SchemeGen a -> a
maximum :: SchemeGen a -> a
$cmaximum :: forall a. Ord a => SchemeGen a -> a
elem :: a -> SchemeGen a -> Bool
$celem :: forall a. Eq a => a -> SchemeGen a -> Bool
length :: SchemeGen a -> Int
$clength :: forall a. SchemeGen a -> Int
null :: SchemeGen a -> Bool
$cnull :: forall a. SchemeGen a -> Bool
toList :: SchemeGen a -> [a]
$ctoList :: forall a. SchemeGen a -> [a]
foldl1 :: (a -> a -> a) -> SchemeGen a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SchemeGen a -> a
foldr1 :: (a -> a -> a) -> SchemeGen a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SchemeGen a -> a
foldl' :: (b -> a -> b) -> b -> SchemeGen a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SchemeGen a -> b
foldl :: (b -> a -> b) -> b -> SchemeGen a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SchemeGen a -> b
foldr' :: (a -> b -> b) -> b -> SchemeGen a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SchemeGen a -> b
foldr :: (a -> b -> b) -> b -> SchemeGen a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> SchemeGen a -> b
foldMap' :: (a -> m) -> SchemeGen a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SchemeGen a -> m
foldMap :: (a -> m) -> SchemeGen a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SchemeGen a -> m
fold :: SchemeGen m -> m
$cfold :: forall m. Monoid m => SchemeGen m -> m
Foldable, Functor SchemeGen
Foldable SchemeGen
(Functor SchemeGen, Foldable SchemeGen) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> SchemeGen a -> f (SchemeGen b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    SchemeGen (f a) -> f (SchemeGen a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SchemeGen a -> m (SchemeGen b))
-> (forall (m :: * -> *) a.
    Monad m =>
    SchemeGen (m a) -> m (SchemeGen a))
-> Traversable SchemeGen
(a -> f b) -> SchemeGen a -> f (SchemeGen 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 =>
SchemeGen (m a) -> m (SchemeGen a)
forall (f :: * -> *) a.
Applicative f =>
SchemeGen (f a) -> f (SchemeGen a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SchemeGen a -> m (SchemeGen b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SchemeGen a -> f (SchemeGen b)
sequence :: SchemeGen (m a) -> m (SchemeGen a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
SchemeGen (m a) -> m (SchemeGen a)
mapM :: (a -> m b) -> SchemeGen a -> m (SchemeGen b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SchemeGen a -> m (SchemeGen b)
sequenceA :: SchemeGen (f a) -> f (SchemeGen a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
SchemeGen (f a) -> f (SchemeGen a)
traverse :: (a -> f b) -> SchemeGen a -> f (SchemeGen b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SchemeGen a -> f (SchemeGen b)
$cp2Traversable :: Foldable SchemeGen
$cp1Traversable :: Functor SchemeGen
Traversable)

{-# COMPLETE Forall #-}

pattern Forall :: [Name] -> TypeGen d -> SchemeGen d
pattern $bForall :: [Name] -> TypeGen d -> SchemeGen d
$mForall :: forall r d.
SchemeGen d -> ([Name] -> TypeGen d -> r) -> (Void# -> r) -> r
Forall as t <-
  Scheme as _ t _
  where
    Forall as :: [Name]
as t :: TypeGen d
t = [Name] -> Domain -> TypeGen d -> ConstraintSet -> SchemeGen d
forall d.
[Name] -> Domain -> TypeGen d -> ConstraintSet -> SchemeGen d
Scheme [Name]
as Domain
forall a. Monoid a => a
mempty TypeGen d
t ConstraintSet
forall a. Monoid a => a
mempty

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

instance Binary d => Binary (SchemeGen d) where
  put_ :: BinHandle -> SchemeGen d -> IO ()
put_ bh :: BinHandle
bh (Scheme as :: [Name]
as bs :: Domain
bs t :: TypeGen d
t cs :: ConstraintSet
cs) = BinHandle -> [Name] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh [Name]
as IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> [Int] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (Domain -> [Int]
I.toList Domain
bs) 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
t IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> ConstraintSet -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh ConstraintSet
cs

  get :: BinHandle -> IO (SchemeGen d)
get bh :: BinHandle
bh = [Name] -> Domain -> TypeGen d -> ConstraintSet -> SchemeGen d
forall d.
[Name] -> Domain -> TypeGen d -> ConstraintSet -> SchemeGen d
Scheme ([Name] -> Domain -> TypeGen d -> ConstraintSet -> SchemeGen d)
-> IO [Name]
-> IO (Domain -> TypeGen d -> ConstraintSet -> SchemeGen 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 IO (Domain -> TypeGen d -> ConstraintSet -> SchemeGen d)
-> IO Domain -> IO (TypeGen d -> ConstraintSet -> SchemeGen d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Int] -> Domain
I.fromList ([Int] -> Domain) -> IO [Int] -> IO Domain
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO [Int]
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh) IO (TypeGen d -> ConstraintSet -> SchemeGen d)
-> IO (TypeGen d) -> IO (ConstraintSet -> SchemeGen 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 IO (ConstraintSet -> SchemeGen d)
-> IO ConstraintSet -> IO (SchemeGen d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BinHandle -> IO ConstraintSet
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh

instance Outputable d => Refined (SchemeGen d) where
  domain :: SchemeGen d -> Domain
domain s :: SchemeGen d
s = (TypeGen d -> Domain
forall t. Refined t => t -> Domain
domain (SchemeGen d -> TypeGen d
forall d. SchemeGen d -> TypeGen d
body SchemeGen d
s) Domain -> Domain -> Domain
forall a. Semigroup a => a -> a -> a
Prelude.<> ConstraintSet -> Domain
forall t. Refined t => t -> Domain
domain (SchemeGen d -> ConstraintSet
forall d. SchemeGen d -> ConstraintSet
constraints SchemeGen d
s)) Domain -> Domain -> Domain
I.\\ SchemeGen d -> Domain
forall d. SchemeGen d -> Domain
boundvs SchemeGen d
s

  rename :: Int -> Int -> SchemeGen d -> SchemeGen d
rename x :: Int
x y :: Int
y s :: SchemeGen d
s
    | Int -> Domain -> Bool
I.member Int
x (SchemeGen d -> Domain
forall d. SchemeGen d -> Domain
boundvs SchemeGen d
s) = SchemeGen d
s
    | Int -> Domain -> Bool
I.member Int
y (SchemeGen d -> Domain
forall d. SchemeGen d -> Domain
boundvs SchemeGen d
s) = String -> SDoc -> SchemeGen d
forall a. HasCallStack => String -> SDoc -> a
pprPanic "Alpha renaming of polymorphic types is not implemented!" (SDoc -> SchemeGen d) -> SDoc -> SchemeGen d
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Int
x, Int
y)
    | Bool
otherwise =
      Scheme :: forall d.
[Name] -> Domain -> TypeGen d -> ConstraintSet -> SchemeGen d
Scheme
        { tyvars :: [Name]
tyvars = SchemeGen d -> [Name]
forall d. SchemeGen d -> [Name]
tyvars SchemeGen d
s,
          boundvs :: Domain
boundvs = SchemeGen d -> Domain
forall d. SchemeGen d -> Domain
boundvs SchemeGen d
s,
          body :: TypeGen d
body = Int -> Int -> TypeGen d -> TypeGen d
forall t. Refined t => Int -> Int -> t -> t
rename Int
x Int
y (SchemeGen d -> TypeGen d
forall d. SchemeGen d -> TypeGen d
body SchemeGen d
s),
          constraints :: ConstraintSet
constraints = Int -> Int -> ConstraintSet -> ConstraintSet
forall t. Refined t => Int -> Int -> t -> t
rename Int
x Int
y (SchemeGen d -> ConstraintSet
forall d. SchemeGen d -> ConstraintSet
constraints SchemeGen d
s)
        }
  
  prpr :: (Int -> SDoc) -> SchemeGen d -> SDoc
prpr _ scheme :: SchemeGen d
scheme 
    | SchemeGen d -> ConstraintSet
forall d. SchemeGen d -> ConstraintSet
constraints SchemeGen d
scheme ConstraintSet -> ConstraintSet -> Bool
forall a. Eq a => a -> a -> Bool
/= ConstraintSet
forall a. Monoid a => a
mempty =
      SDoc -> Int -> SDoc -> SDoc
hang
        ([SDoc] -> SDoc
hcat [SDoc
pprTyQuant, SDoc
pprConQuant, (Int -> SDoc) -> TypeGen d -> SDoc
forall t. Refined t => (Int -> SDoc) -> t -> SDoc
prpr Int -> SDoc
varMap (SchemeGen d -> TypeGen d
forall d. SchemeGen d -> TypeGen d
body SchemeGen d
scheme)])
        2
        (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "where") 2 ((Int -> SDoc) -> ConstraintSet -> SDoc
forall t. Refined t => (Int -> SDoc) -> t -> SDoc
prpr Int -> SDoc
varMap (SchemeGen d -> ConstraintSet
forall d. SchemeGen d -> ConstraintSet
constraints SchemeGen d
scheme)))
    | Bool
otherwise = [SDoc] -> SDoc
hcat [SDoc
pprTyQuant, SDoc
pprConQuant, (Int -> SDoc) -> TypeGen d -> SDoc
forall t. Refined t => (Int -> SDoc) -> t -> SDoc
prpr Int -> SDoc
varMap (SchemeGen d -> TypeGen d
forall d. SchemeGen d -> TypeGen d
body SchemeGen d
scheme)]
    where
      numVars :: Int
numVars = Domain -> Int
I.size (SchemeGen d -> Domain
forall d. SchemeGen d -> Domain
boundvs SchemeGen d
scheme)
      varNames :: [SDoc]
varNames =
        if Int
numVars Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3 then [ Char -> SDoc
char 'X' SDoc -> SDoc -> SDoc
GhcPlugins.<> Int -> SDoc
int Int
n | Int
n <- [1..Int
numVars] ] else [ Char -> SDoc
char Char
c | Char
c <- ['X', 'Y', 'Z'] ]
      varMap :: Int -> SDoc
varMap = \x :: Int
x -> IntMap SDoc
m IntMap SDoc -> Int -> SDoc
forall a. IntMap a -> Int -> a
IntMap.! Int
x
        where m :: IntMap SDoc
m = [(Int, SDoc)] -> IntMap SDoc
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, SDoc)] -> IntMap SDoc) -> [(Int, SDoc)] -> IntMap SDoc
forall a b. (a -> b) -> a -> b
$ [Int] -> [SDoc] -> [(Int, SDoc)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Domain -> [Int]
I.toAscList (SchemeGen d -> Domain
forall d. SchemeGen d -> Domain
boundvs SchemeGen d
scheme)) [SDoc]
varNames
      pprTyQuant :: SDoc
pprTyQuant
        | [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (SchemeGen d -> [Name]
forall d. SchemeGen d -> [Name]
tyvars SchemeGen d
scheme) = SDoc
empty
        | Bool
otherwise = [SDoc] -> SDoc
hcat [SDoc
forAllLit SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
fsep ((Name -> SDoc) -> [Name] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([Name] -> [SDoc]) -> [Name] -> [SDoc]
forall a b. (a -> b) -> a -> b
$ SchemeGen d -> [Name]
forall d. SchemeGen d -> [Name]
tyvars SchemeGen d
scheme), SDoc
dot]
      pprConQuant :: SDoc
pprConQuant
        | Domain -> Bool
I.null (SchemeGen d -> Domain
forall d. SchemeGen d -> Domain
boundvs SchemeGen d
scheme) = SDoc
empty
        | Bool
otherwise = [SDoc] -> SDoc
hcat [SDoc
forAllLit SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
fsep ((Int -> SDoc) -> [Int] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Int -> SDoc
varMap ([Int] -> [SDoc]) -> [Int] -> [SDoc]
forall a b. (a -> b) -> a -> b
$ Domain -> [Int]
I.toList (SchemeGen d -> Domain
forall d. SchemeGen d -> Domain
boundvs SchemeGen d
scheme)), SDoc
dot]

-- Demand a monomorphic type
mono :: SchemeGen d -> TypeGen d
mono :: SchemeGen d -> TypeGen d
mono (Forall [] t :: TypeGen d
t) = TypeGen d
t
mono _ = TypeGen d
forall d. TypeGen d
Ambiguous

{-|
    Given a scheme @s@, @unsats s@ is the constraint set containing
    just the trivially unsatisfiable constraints associated with @s@.
-}
unsats :: Scheme -> ConstraintSet
unsats :: Scheme -> ConstraintSet
unsats s :: Scheme
s = ConstraintSet -> ConstraintSet
Constraints.unsats (Scheme -> ConstraintSet
forall d. SchemeGen d -> ConstraintSet
constraints Scheme
s)