{-# LANGUAGE CPP, DeriveDataTypeable, FlexibleInstances #-}
module Language.Java.Paragon.TypeCheck.Locks where

import Data.List (intersect, union, (\\) )

import Language.Java.Paragon.Syntax
import Language.Java.Paragon.Pretty
import Language.Java.Paragon.Interaction

import Language.Java.Paragon.TypeCheck.Actors

#ifdef BASE4
import Data.Data
#else
import Data.Generics (Data(..),Typeable(..))
#endif

type LockMods = ([TcLock], [TcLock])

noMods :: LockMods
noMods = ([],[])

--data TcLockExp = TcLockExp [TcLock] | TcLockVar Ident
--  deriving (Eq, Ord, Show, Data, Typeable)

data TcLock = TcLock (Name ()) [ActorId] | TcLockVar (Ident ())
  deriving (Eq, Ord, Show, Data, Typeable)

instance Pretty TcLock where
  pretty (TcLock n aids) = pretty n <> 
    opt (not $ null aids) (parens (hcat (punctuate (char ',') $ map pretty aids)))
  pretty (TcLockVar i) = pretty i

instance Pretty [TcLock] where
  pretty ls = brackets $ hcat (punctuate (char ',') $ map pretty ls)


(<++>) :: LockMods -> LockMods -> LockMods
(c1,o1) <++> (c2,o2) = (c1 `union` c2, o1 `intersect` o2)

(||>>) :: LockMods -> LockMods -> LockMods
(c1,o1) ||>> (c2,o2) =
            let os = (filter (not . (closedBy c2)) o1) ++ o2
                cs = (filter (not . (openedBy o2)) c1) ++ c2
             in (cs,os)

closedBy, openedBy :: [TcLock] -> TcLock -> Bool
closedBy xs x = any (closes x) xs
  where closes (TcLock n1 aids1) (TcLock n2 aids2) =
            n1 == n2 && aids1 `unify` aids2
        closes _ _ = panic "TypeCheck.Locks.closedBy"
                     "TcLockVar should have been instantiated but isn't"
openedBy xs x = any (opens x) xs
  where opens (TcLock n1 aids1) (TcLock n2 aids2) =
            n1 == n2 && and (zipWith (==) aids1 aids2)
        opens  _ _ = panic "TypeCheck.Locks.openedBy"
                     "TcLockVar should have been instantiated but isn't"


models :: LockMods -> LockMods -> Bool
models (c1,o1) (c2,o2) = null (c2 \\ c1) && null (o1 \\ o2)