module Language.Java.Paragon.TypeCheck.Containment (lrt) where

import Language.Java.Paragon.Parser
import Language.Java.Paragon.Syntax
import Language.Java.Paragon.TypeCheck.Actors
import Language.Java.Paragon.TypeCheck.Constraints
import Language.Java.Paragon.TypeCheck.Locks
import Language.Java.Paragon.TypeCheck.Policy

import qualified Data.Map as M

--import Debug.Trace

-- ensuring Datalog-equivalance by having an atom for something being an actor
actorAtomString :: String
actorAtomString = "$ACTOR$"

-- to be joined with the policies in question, to have that every variable in
-- the head of a rule is bounded on the right hand side as well
bindActors :: TcPolicy
bindActors = TcPolicy [TcClause (TcVar (Ident "x")) [TcAtom (Name [Ident actorAtomString]) [TcVar (Ident "x")]]]

-- We need to add the $ACTOR$ atom to all clauses in the recursive (global)
-- policy. Since join is not defined for recursive policies, it is easier to
-- just add this explicitly for all the actors in the heads of a rule (only for
-- $FLOW$ rules)
bindActorsRec :: [TcClause TcAtom] -> [TcClause TcAtom]
bindActorsRec [] = []
bindActorsRec (TcClause head@(TcAtom (Name [Ident flowAtomString]) actors) body:rst) = TcClause head nbody:rst
  where nbody = map (\x -> TcAtom (Name [Ident actorAtomString]) [x]) actors ++ body
bindActorsRec (_:rst) = bindActorsRec rst


-- Less restrictive than with recursive policies:
-- Global policy -> p -> q -> (p lrt q)
lrt :: TcPolicyRec -> TcPolicy -> TcPolicy -> Either Bool Constraint
-- If both are policies, we can actually perform the check
lrt (TcPolicyRec g) polp@(TcPolicy _) polq@(TcPolicy _) = Left $ all (\d -> canDerive d (bound_g ++ rp)) rq
  where bound_g          = bindActorsRec g
        (TcPolicyRec rp) = toRecPolicy (join polp bindActors)
        (TcPolicyRec rq) = toRecPolicy (join polq bindActors)
        canDerive d p    = derivable p (substEl tau ruleHead) (subst tau ruleBody ++ allAreActors)
          where m   = foldl (\y x -> max (maxActorId (aliasToFresh x)) y) 0 p
                SubstM tau maxID = groundSubst m d 
                (TcClause ruleHead ruleBody) = d
                -- include facts to database that all concrete values are actors:
                allAreActors = map (\x -> TcAtom (Name [Ident actorAtomString]) [TcActor (Fresh x)]) [0..maxID]

-- For joins and meets, we want to try all the candidates.
-- We have that 
--  * p1 `join` p2 <= p  <=>  p1 <= p /\ p2 <= p
--  * p <= p1 `meet` p2  <=>  p <= p1 /\ p <= p2
lrt g p1@(TcJoin p11 p12) p2 = --traceShow (p1, p11, p12, p2) $
    case (lrt g p11 p2, lrt g p12 p2) of
      (Right _, Right _) -> Right (LRT g p1 p2)
      (Right l, Left b) 
          | b -> Right l
          | not b -> Left b
      (Left b, Right l)
          | b -> Right l
          | not b -> Left b
      (Left b1, Left b2) -> Left $ b1 && b2
lrt g p1 p2@(TcMeet p21 p22) =
    case (lrt g p1 p21, lrt g p2 p22) of
      (Right _, Right _) -> Right (LRT g p1 p2)
      (Right l, Left b) 
          | b -> Right l
          | not b -> Left b
      (Left b, Right l)
          | b -> Right l
          | not b -> Left b
      (Left b1, Left b2) -> Left $ b1 && b2

-- But only
--  * p <= p1 `join` p2  <==  p <= p1 \/ p <= p2
--  * p1 `meet` p2 <= p  <==  p1 <= p \/ p2 <= p
lrt g p1 p2@(TcJoin p21 p22) =
    case (lrt g p1 p21, lrt g p2 p22) of
      (Right _, Right _) -> Right (LRT g p1 p2)
      (Right l, Left b) 
          | b -> Left b
          | not b -> Right (LRT g p1 p2)
      (Left b, Right l)
          | b -> Left b
          | not b -> Right (LRT g p1 p2)
      (Left b1, Left b2) -> Left $ b1 || b2
lrt g p1@(TcMeet p11 p12) p2 =
    case (lrt g p11 p2, lrt g p12 p2) of
      (Right _, Right _) -> Right (LRT g p1 p2)
      (Right l, Left b) 
          | b -> Left b
          | not b -> Right (LRT g p1 p2)
      (Left b, Right l)
          | b -> Left b
          | not b -> Right (LRT g p1 p2)
      (Left b1, Left b2) -> Left $ b1 || b2

-- If both are rigid variables, the only way they can possibly fit
-- is if they are in fact the same rigid variable
lrt g (TcRigidVar i1) (TcRigidVar i2) = Left $ i1 == i2

-- If either is a rigid variable, we need to be very strict
-- only trivial constraints can be discharged.
lrt g p1@(TcRigidVar _) p2 = 
    case lrt g top p2 of
      Right (LRT _ _ _) -> Right (LRT g p1 p2)
      l -> l
lrt g p1 p2@(TcRigidVar _) =
    case lrt g p1 bottom of
      Right (LRT _ _ _) -> Right (LRT g p1 p2)
      l -> l

lrt g p1 p2 = Right $ LRT g p1 p2



-------------------------- 
-- Substitution functions

type Subst = M.Map Ident TcActor

-- Assisting type containg the maximal actor-id as an informative value
data SubstM = SubstM Subst Int

emptysub :: Subst
emptysub = M.empty

add :: Subst -> Ident -> TcActor -> Subst
add s a b = M.insert a b s

lookupSubst :: (Ord k) => k -> M.Map k a -> Maybe a
lookupSubst = M.lookup

substAct :: Subst -> TcActor -> TcActor
substAct sub (TcVar id) = 
  case (lookupSubst id sub) of
  (Just a) -> a
  Nothing -> (TcVar id)
substAct sub a = a

substEl :: Subst -> TcAtom -> TcAtom
substEl sub (TcAtom name actors) = TcAtom name (map (substAct sub) actors)

subst :: Subst -> [TcAtom] -> [TcAtom]
subst s = map (substEl s)
--------------------------

--------------------------
-- Preparing the database for the (uniform) containment check

groundSubst :: Int -> TcClause TcAtom -> SubstM
groundSubst maxIDProg rule@(TcClause ruleHead ruleBody) = afterBody
  where maxID     = max (maxActorId (aliasToFresh rule)) maxIDProg
        sub       = SubstM emptysub maxID
        afterHead = freshSubstAtom sub ruleHead
        afterBody = foldl freshSubstAtom afterHead ruleBody

-- Using the assumption that fresh-ints are distinct from alias-ints
-- Converts all aliases to fresh actors
aliasToFresh :: TcClause TcAtom -> TcClause TcAtom
aliasToFresh (TcClause ruleHead ruleBody) = TcClause rh rb
  where rh = aliasToFreshAtom ruleHead               
        rb = map aliasToFreshAtom ruleBody
        aliasToFreshAtom (TcAtom name actors) = TcAtom name (map aliasToFreshActor actors)
	aliasToFreshActor (TcActor (Alias i)) = TcActor (Fresh i)
        aliasToFreshActor x = x

-- Returns the highest integer found as actorID
maxActorId :: TcClause TcAtom -> Int
maxActorId (TcClause ruleHead ruleBody) = max h b
  where h = getHeighestActorId ruleHead
        b = foldl (\t atom -> max (getHeighestActorId atom) t) 0 ruleBody
        getHeighestActorId (TcAtom name actors) = foldl (\t actor -> max (acc actor) t ) 0 actors
        acc (TcActor (Fresh i)) = i
        acc _                   = 0

-- Returns an extended substitution mapping all variables in TcAtom
-- to fresh constants not occurring in the first two arguments
freshSubstAtom :: SubstM -> TcAtom -> SubstM
freshSubstAtom sub (TcAtom _ actors) = foldl freshSubstActor sub actors

-- Adds a mapping to the substitution if the provided actor is a variable
freshSubstActor :: SubstM -> TcActor -> SubstM
freshSubstActor sub@(SubstM mapping maxId) (TcVar id) = 
  case lookupSubst id mapping of
  Just _  -> sub -- already mapped to a constant
  Nothing -> SubstM (add mapping id (TcActor (Fresh (maxId + 1)))) (maxId + 1)
freshSubstActor sub                        _          = sub


--------------------------

--------------------------
-- Functions for Datalog evaluation

-- Returns list of possible substitutions making the second argument a
-- ground list of actors, based on facts in the first ones
matchSubst :: [[TcActor]] -> [TcActor] -> [Subst]
matchSubst [] a = []
matchSubst (d:db) a = 
  case findsubstAct d a of -- can we make a substitution from Atom a to become Atom d
  Just subst -> subst : matchSubst db a
  Nothing    -> matchSubst db a
  where findsubstAct [] [] = Just emptysub
        findsubstAct [] _  = Nothing -- not same number of actors
        findsubstAct _  [] = Nothing -- not same number of actors
        findsubstAct (TcActor ida : actsa) (TcActor idb : actsb) = -- same concrete actor
          if ida == idb then findsubstAct actsa actsb else Nothing
        findsubstAct (ac:actsa) (TcVar id : actsb) = -- variable can be substituted, continue on tail
          case (findsubstAct actsa (map (substAct (M.singleton id ac)) actsb)) of
          Nothing -> Nothing
          Just s -> Just (add s id ac)


-- Returns list of substitutions that satisfy the atom in
-- the present database
satisfyAtom :: [TcAtom] -> TcAtom -> [Subst]
satisfyAtom db at@(TcAtom name _) = 
  matchSubst (map getActors (filter (\x -> getName x == name ) db)) (getActors at)
  where getActors (TcAtom _ acts) = acts
        getName (TcAtom n _) = n


-- Given a database, head of a rule, unsatisfied part of the body of a rule,
-- return list of new derived facts on the head of the rule
deriveOneRule :: [TcAtom] -> TcAtom -> [TcAtom] -> [TcAtom]
deriveOneRule db ruleHead [] = -- head must be ground now (given that we use the $ACTOR$ atom everywhere)
  if ruleHead `elem` db 
   then []
   else [ruleHead] -- only new facts
deriveOneRule db ruleHead (atom:aBody) = 
  foldl (\atoml s -> deriveOneRule db (substEl s ruleHead) (subst s aBody) ++ atoml) [] r
  where r = satisfyAtom db atom

-- Performs one step of fact derivation
deriveOne :: [TcClause TcAtom] -> [TcAtom] -> [TcAtom]
deriveOne rules database = foldl (\list (TcClause hd tl) -> deriveOneRule database hd tl ++ list) [] rules

-- Returns all possible derivable facts
deriveAll :: [TcClause TcAtom] -> [TcAtom] -> [TcAtom]
deriveAll program database =
  case deriveOne program database of
  []   -> database
  list -> deriveAll program (list ++ database)

-- Returns true if it can derive the requested atom from the provided database
-- of atoms
derivable :: [TcClause TcAtom] -> TcAtom -> [TcAtom] -> Bool
derivable program fact database = fact `elem` deriveAll program database