{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}

-- The Hashable instances for Unique and Name are orphans
-- but should eventually be removed when hashtables are
-- replaced in the ConstraintSet representation.
{-# OPTIONS_GHC -Wno-orphans #-} 

module Intensional.Constructors
  ( Side (..),
    K (..),
    ConL,
    ConR,
    toAtomic,
    getLocation
  )
where

import Binary
import Data.Hashable
import GhcPlugins hiding (L)
import Intensional.Types
import Unique

instance Hashable Unique where
  hashWithSalt :: Int -> Unique -> Int
hashWithSalt s :: Int
s = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int -> Int) -> (Unique -> Int) -> Unique -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> Int
getKey

instance Hashable Name where
  hashWithSalt :: Int -> Name -> Int
hashWithSalt s :: Int
s = Int -> Unique -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Unique -> Int) -> (Name -> Unique) -> Name -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Unique
forall a. Uniquable a => a -> Unique
getUnique

data Side = L | R

-- A constructor set with a location tag
-- We include the srcSpan as part of the
-- identity so that multiple errors with 
-- the same constructor in different program
-- locations are treated seperately.
data K (s :: Side) where
  Dom :: DataType Name -> K s
  Con :: Name -> SrcSpan -> K 'L
  Set :: UniqSet Name -> SrcSpan -> K 'R

type ConL = K 'L
type ConR = K 'R

-- Don't disregard location in comparison
-- i.e. distinguish between different sources
-- and sinks
instance Eq (K s) where
  Dom d :: DataType Name
d == :: K s -> K s -> Bool
== Dom d' :: DataType Name
d' = DataType Name
d DataType Name -> DataType Name -> Bool
forall a. Eq a => a -> a -> Bool
== DataType Name
d'
  Con k :: Name
k l :: SrcSpan
l == Con k' :: Name
k' l' :: SrcSpan
l' = Name
k Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
k' Bool -> Bool -> Bool
&& SrcSpan
l SrcSpan -> SrcSpan -> Bool
forall a. Eq a => a -> a -> Bool
== SrcSpan
l'
  Set s :: UniqSet Name
s l :: SrcSpan
l == Set s' :: UniqSet Name
s' l' :: SrcSpan
l' = UniqSet Name
s UniqSet Name -> UniqSet Name -> Bool
forall a. Eq a => a -> a -> Bool
== UniqSet Name
s' Bool -> Bool -> Bool
&& SrcSpan
l SrcSpan -> SrcSpan -> Bool
forall a. Eq a => a -> a -> Bool
== SrcSpan
l'
  _ == _ = Bool
False

instance Hashable (K s) where
  hashWithSalt :: Int -> K s -> Int
hashWithSalt s :: Int
s (Dom d :: DataType Name
d) = Int -> DataType Name -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s DataType Name
d
  hashWithSalt s :: Int
s (Con k :: Name
k _) = Int -> Name -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Name
k
  hashWithSalt s :: Int
s (Set ks :: UniqSet Name
ks _) = Int -> [Unique] -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (UniqSet Name -> [Unique]
forall elt. UniqSet elt -> [Unique]
nonDetKeysUniqSet UniqSet Name
ks)

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

instance Binary (K 'L) where
  put_ :: BinHandle -> K 'L -> IO ()
put_ bh :: BinHandle
bh (Dom d :: DataType Name
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 -> DataType Name -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh DataType Name
d
  put_ bh :: BinHandle
bh (Con k :: Name
k l :: SrcSpan
l) = 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 -> Name -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh Name
k IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> SrcSpan -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh SrcSpan
l

  get :: BinHandle -> IO (K 'L)
get bh :: BinHandle
bh =
    BinHandle -> IO Bool
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh IO Bool -> (Bool -> IO (K 'L)) -> IO (K 'L)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      False -> DataType Name -> K 'L
forall (s :: Side). DataType Name -> K s
Dom (DataType Name -> K 'L) -> IO (DataType Name) -> IO (K 'L)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO (DataType Name)
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      True -> Name -> SrcSpan -> K 'L
Con (Name -> SrcSpan -> K 'L) -> IO Name -> IO (SrcSpan -> K 'L)
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 (SrcSpan -> K 'L) -> IO SrcSpan -> IO (K 'L)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BinHandle -> IO SrcSpan
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh

instance Binary (K 'R) where
  put_ :: BinHandle -> K 'R -> IO ()
put_ bh :: BinHandle
bh (Dom d :: DataType Name
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 -> DataType Name -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh DataType Name
d
  put_ bh :: BinHandle
bh (Set s :: UniqSet Name
s l :: SrcSpan
l) = 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 -> [Name] -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh (UniqSet Name -> [Name]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet UniqSet Name
s) IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BinHandle -> SrcSpan -> IO ()
forall a. Binary a => BinHandle -> a -> IO ()
put_ BinHandle
bh SrcSpan
l

  get :: BinHandle -> IO (K 'R)
get bh :: BinHandle
bh =
    BinHandle -> IO Bool
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh IO Bool -> (Bool -> IO (K 'R)) -> IO (K 'R)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      False -> DataType Name -> K 'R
forall (s :: Side). DataType Name -> K s
Dom (DataType Name -> K 'R) -> IO (DataType Name) -> IO (K 'R)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinHandle -> IO (DataType Name)
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
      True -> do
        UniqSet Name
s <- [Name] -> UniqSet Name
forall a. Uniquable a => [a] -> UniqSet a
mkUniqSet ([Name] -> UniqSet Name) -> IO [Name] -> IO (UniqSet Name)
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
        SrcSpan
l <- BinHandle -> IO SrcSpan
forall a. Binary a => BinHandle -> IO a
get BinHandle
bh
        K 'R -> IO (K 'R)
forall (m :: * -> *) a. Monad m => a -> m a
return (UniqSet Name -> SrcSpan -> K 'R
Set UniqSet Name
s SrcSpan
l)

instance Refined (K l) where
  domain :: K l -> Domain
domain (Dom d :: DataType Name
d) = DataType Name -> Domain
forall t. Refined t => t -> Domain
domain DataType Name
d
  domain _ = Domain
forall a. Monoid a => a
mempty

  rename :: Int -> Int -> K l -> K l
rename x :: Int
x y :: Int
y (Dom d :: DataType Name
d) = DataType Name -> K l
forall (s :: Side). DataType Name -> K s
Dom (Int -> Int -> DataType Name -> DataType Name
forall t. Refined t => Int -> Int -> t -> t
rename Int
x Int
y DataType Name
d)
  rename _ _ s :: K l
s = K l
s

  prpr :: (Int -> SDoc) -> K l -> SDoc
prpr m :: Int -> SDoc
m (Dom (Inj x :: Int
x d :: Name
d)) = Int -> SDoc
m Int
x SDoc -> SDoc -> SDoc
GhcPlugins.<> SDoc -> SDoc
parens (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
d)
  prpr _ (Dom (Base _))  = [Char] -> SDoc
forall a. HasCallStack => [Char] -> a
error "Base in constraint."
  prpr _ (Con k :: Name
k _) = Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
k
  prpr _ (Set ks :: UniqSet Name
ks _) = [SDoc] -> SDoc
hcat [Char -> SDoc
char '{', (Name -> SDoc) -> [Name] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithBars Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr (UniqSet Name -> [Name]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet UniqSet Name
ks), Char -> SDoc
char '}']

{-|
    Assuming @k@ is either a @Con@ or @Set@ atom, 
    @getLocation k@ is the associated span.
-}
getLocation :: K a -> SrcSpan 
getLocation :: K a -> SrcSpan
getLocation (Con _ s :: SrcSpan
s) = SrcSpan
s
getLocation (Set _ s :: SrcSpan
s) = SrcSpan
s
getLocation _         = [Char] -> SrcSpan
forall a. HasCallStack => [Char] -> a
error "Dom constructors have no location."

-- Convert constraint to atomic form
toAtomic :: K l -> K r -> [(K 'L, K 'R)]
toAtomic :: K l -> K r -> [(K 'L, K 'R)]
toAtomic (Dom d :: DataType Name
d) (Dom d' :: DataType Name
d')
  | DataType Name
d DataType Name -> DataType Name -> Bool
forall a. Eq a => a -> a -> Bool
== DataType Name
d' = []
  | Bool
otherwise = [(DataType Name -> K 'L
forall (s :: Side). DataType Name -> K s
Dom DataType Name
d, DataType Name -> K 'R
forall (s :: Side). DataType Name -> K s
Dom DataType Name
d')]
toAtomic (Dom d :: DataType Name
d) (Con k :: Name
k l :: SrcSpan
l) =
  [(DataType Name -> K 'L
forall (s :: Side). DataType Name -> K s
Dom DataType Name
d, UniqSet Name -> SrcSpan -> K 'R
Set (Name -> UniqSet Name
forall a. Uniquable a => a -> UniqSet a
unitUniqSet Name
k) SrcSpan
l)]
toAtomic (Dom d :: DataType Name
d) (Set ks :: UniqSet Name
ks l :: SrcSpan
l) =
  [(DataType Name -> K 'L
forall (s :: Side). DataType Name -> K s
Dom DataType Name
d, UniqSet Name -> SrcSpan -> K 'R
Set UniqSet Name
ks SrcSpan
l)]
toAtomic (Con k :: Name
k l :: SrcSpan
l) (Dom d :: DataType Name
d) =
  [(Name -> SrcSpan -> K 'L
Con Name
k SrcSpan
l, DataType Name -> K 'R
forall (s :: Side). DataType Name -> K s
Dom DataType Name
d)]
toAtomic (Con k :: Name
k l :: SrcSpan
l) (Con k' :: Name
k' l' :: SrcSpan
l')
  | Name
k Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
k' = []
  | Bool
otherwise = [(Name -> SrcSpan -> K 'L
Con Name
k SrcSpan
l, UniqSet Name -> SrcSpan -> K 'R
Set UniqSet Name
forall a. UniqSet a
emptyUniqSet SrcSpan
l')]
toAtomic (Con k :: Name
k l :: SrcSpan
l) (Set ks :: UniqSet Name
ks l' :: SrcSpan
l')
  | Name -> UniqSet Name -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
elementOfUniqSet Name
k UniqSet Name
ks = []
  | Bool
otherwise = [(Name -> SrcSpan -> K 'L
Con Name
k SrcSpan
l, UniqSet Name -> SrcSpan -> K 'R
Set UniqSet Name
forall a. UniqSet a
emptyUniqSet SrcSpan
l')]
toAtomic (Set ks :: UniqSet Name
ks l :: SrcSpan
l) (Dom d :: DataType Name
d) =
  [(Name -> SrcSpan -> K 'L
Con Name
k SrcSpan
l, DataType Name -> K 'R
forall (s :: Side). DataType Name -> K s
Dom DataType Name
d) | Name
k <- UniqSet Name -> [Name]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet UniqSet Name
ks]
toAtomic (Set ks :: UniqSet Name
ks l :: SrcSpan
l) (Con k :: Name
k l' :: SrcSpan
l') =
  [(Name -> SrcSpan -> K 'L
Con Name
k SrcSpan
l, UniqSet Name -> SrcSpan -> K 'R
Set UniqSet Name
forall a. UniqSet a
emptyUniqSet SrcSpan
l') | Name
k' <- UniqSet Name -> [Name]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet UniqSet Name
ks, Name
k' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
k]
toAtomic (Set ks :: UniqSet Name
ks l :: SrcSpan
l) (Set ks' :: UniqSet Name
ks' l' :: SrcSpan
l') =
  [(Name -> SrcSpan -> K 'L
Con Name
k SrcSpan
l, UniqSet Name -> SrcSpan -> K 'R
Set UniqSet Name
forall a. UniqSet a
emptyUniqSet SrcSpan
l') | Name
k <- UniqSet Name -> [Name]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet UniqSet Name
ks, Bool -> Bool
not (Name -> UniqSet Name -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
elementOfUniqSet Name
k UniqSet Name
ks')]