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)

data Constraint = LRT TcPolicyRec TcPolicy TcPolicy
  deriving Show

type ConstraintWMsg = (Constraint, String)


type WeakConstraint = (TcPolicy, TcPolicy)

type Map = Map.Map

--Check if a given constraint p<=q verifies that q is an unknown policy of a variable
isCstrVar :: WeakConstraint -> IO Bool
isCstrVar (_, (TcPolicy _))    = return False
isCstrVar (_, (TcPolicyVar (TcMetaVar _ ref))) = do
  mpol <- readIORef ref
  case mpol of
    Nothing -> return True --do lift $ writeIORef ref (Just pF)
    Just _  -> return False                                    
isCstrVar (_, (TcJoin _ _))    = panic "Right-side of a constrain shouldn't be a join !" "" 
isCstrVar (_, (TcMeet _ _))    = panic "Right-side of a constrain shouldn't be a meet !" "" 
isCstrVar _                    = fail "TcThis and TcRigidVar not handled at that point"


partitionM :: (WeakConstraint -> IO Bool) -> [WeakConstraint] -> IO([WeakConstraint], [WeakConstraint])
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 :: (WeakConstraint -> IO Bool) -> [WeakConstraint] -> IO([WeakConstraint])
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 TcMetaVar [TcPolicy]) -> WeakConstraint -> (Map TcMetaVar [TcPolicy])
linker m (p, TcPolicyVar x) = case (Map.lookup x m) of
                                Nothing -> Map.insert x [p] m
                                Just ps -> Map.insert x (p:ps) m
linker _ _                  = panic "linker shouldn't be called on a non-variable constraint" ""


-- Substitutes a TcPolicy policy to a TcMetaVar in a TcPolicy
substPol :: TcMetaVar -> TcPolicy -> TcPolicy -> TcPolicy
substPol x px p@(TcPolicyVar y) = 
    case (x == y) of
      True  -> px
      False -> p
substPol x px (TcJoin p q) = (TcJoin (substPol x px p) (substPol x px q))
substPol x px (TcMeet p q) = (TcMeet (substPol x px p) (substPol x px q))
substPol _ _ p             = p

-- Substitutes a TcPolicy to a TcMetaVar in a list of TcPolicy and add the ones which have actually been modified.
substitution :: TcMetaVar -> TcPolicy -> [WeakConstraint] -> [WeakConstraint]
substitution _ _ [] = []
substitution x px ((p,q):cs) = 
    let psubst = substPol x px p in
    case (psubst == p) of
      True  -> (p,q):(substitution x px cs)
      False -> (psubst, q):(substitution x px cs)