module Language.Java.Paragon.TypeCheck.Constraints where


import qualified Data.Map as Map

import Language.Java.Paragon.TypeCheck.Policy
--import Language.Java.Paragon.TypeCheck.Containment
import Language.Java.Paragon.TypeCheck.Locks
--import Language.Java.Paragon.TypeCheck.Monad.TcCont
import Language.Java.Paragon.Interaction
import Data.IORef
import Data.List (partition, union)
import Language.Java.Paragon.Monad.Base (orM)
--import Control.Monad (filterM)

constraintsModule :: String
constraintsModule = typeCheckerBase ++ ".Constraints"

data Constraint = LRT [TcClause TcAtom] [TcLock] (TcPolicy TcActor) (TcPolicy TcActor)
  deriving (Show, Eq)

type ConstraintWMsg = (Constraint, String)


splitCstrs :: Constraint -> [Constraint]
splitCstrs (LRT g ls p q) = map (\x -> LRT g ls x q) (disjoin p)
    where disjoin :: (TcPolicy TcActor) -> [TcPolicy TcActor]
          disjoin (Join p1 p2) = (disjoin p1)++(disjoin p2)
          disjoin p' = [p']




--Check if a given constraint p<=q verifies that q is an unknown policy of a variable
isCstrVar :: Constraint -> IO Bool
isCstrVar (LRT _ _ _ (RealPolicy _))    = return False
isCstrVar (LRT _ _ _ (VarPolicy (TcMetaVar _ ref))) = do
  mpol <- readIORef ref
  case mpol of
    Nothing -> return True 
    Just _  -> panic "MetaVar assigned to a Policy : shouldn't occur here." ""
isCstrVar (LRT _ _ _ (Join _ _)) 
    = panic (constraintsModule ++ ".isCstrVar") 
      "Right-side of a constrain shouldn't be a join !"

--Check if a given constraint p<=q verifies that q is an unknown policy of a variable
noVarLeft :: Constraint -> IO Bool
noVarLeft (LRT _ _ (RealPolicy _) _)    = return True
noVarLeft (LRT _ _ (VarPolicy (TcMetaVar _ ref)) _) = do
  mpol <- readIORef ref
  case mpol of
    Nothing -> return False
    Just _  -> panic "MetaVar assigned to a Policy : shouldn't occur here." ""
noVarLeft (LRT g ls (Join p q) r) = (noVarLeft (LRT g ls p r)) `orM` (noVarLeft (LRT g ls q r))

partitionM :: (Constraint -> IO Bool) -> [Constraint] -> IO([Constraint], [Constraint])
partitionM f xs = do
  xs' <- mapM (\x -> do 
                 b <- f x 
                 return (b, x)) 
         xs
  xs'' <- return $ partition fst xs'
  return $ ((map snd $ fst xs''), (map snd $ snd xs''))

{-
filterM :: (Constraint -> IO Bool) -> [Constraint] -> IO([Constraint])
filterM f xs = do
  xs' <- mapM (\x -> do 
                 b <- f x 
                 return (b, x)) 
         xs
  xs'' <- return $ filter fst xs'
  return $ (map snd $ xs'')
-}

linker :: (Map.Map (TcMetaVar TcActor) [([TcLock], (TcPolicy TcActor))]) -> Constraint -> (Map.Map (TcMetaVar TcActor) [([TcLock], (TcPolicy TcActor))])
linker m (LRT _ ls p (VarPolicy x)) = case (Map.lookup x m) of
                                        Nothing -> Map.insert x [(ls, p)] m
                                        Just ps -> Map.insert x ((ls, p):ps) m
linker _ _                          = panic "linker shouldn't be called on a non-variable constraint" ""


-- Given (ls, p) and (ls',q) s.t. (ls, p) <= X, returns (ls `union` ls', p) if q=X, (ls, p) either
substPol :: (TcMetaVar TcActor) -> ([TcLock], (TcPolicy TcActor)) -> (([TcLock], TcPolicy TcActor)) -> ([TcLock], (TcPolicy TcActor))
substPol x (ls, px) (ls', p@(VarPolicy y)) = 
    case (x == y) of
      True  -> ((ls `union` ls'), px)
      False -> (ls', p)
substPol _ _ (_, (Join _ _)) = panic "substPol called on a Join !" ""
substPol _ _ p             = p

-- Add to a set of constraints the ones obtained by substituting a policy to a MetaVariable
substitution :: (TcMetaVar TcActor) -> ([TcLock], (TcPolicy TcActor)) -> [Constraint] -> [Constraint]
substitution _ _ [] = []
substitution x (ls, px) ((c@(LRT g ls' p q)):cs) = 
    let (ls'', psubst) = substPol x (ls, px) (ls',p) in
    case ((psubst == p) && (ls'' == ls')) of
      True  -> c:(substitution x (ls, px) cs)
      False -> (LRT g ls'' psubst q):c:(substitution x (ls, px) cs)