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

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

import Language.Java.Paragon.Syntax

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)

(<++>) :: 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
openedBy xs x = any (opens x) xs
  where opens (TcLock n1 aids1) (TcLock n2 aids2) =
            n1 == n2 && and (zipWith (==) aids1 aids2)


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