-- | Define the behaviors of 'Player'
--
-- TODO
--
-- * adoption of concept of front/back
--
-- * indirect speed control based of acceleration parameter
--
{-# LANGUAGE
	GADTs
      , MultiParamTypeClasses
      , ViewPatterns
  #-}
module Satter.PlayerSAT
       (
         newIntentionBySAT
       , fromContext
       , makeLiterals
       , toBools
       , theRule
       , cnfInfo
       , dumpTheRule
       , dumpTheCNF
       , callSolver'
         -- * for internal development and debug
--       , SLit (..)
--       , ActionTarget (..)
       ) where

import Control.Applicative
import Control.Lens
import Control.Monad
-- import Control.Parallel.Strategies
import Data.IORef
import Data.List
import Data.Ord
import System.IO.Unsafe
import Satter.TwoD
import Satter.Field
import Satter.Types
import Satter.Ball
import SAT.Mios.Util.DIMACS ((-|-), (-&-), (->-), neg)
import qualified SAT.Mios.Util.DIMACS as CNF
import qualified SAT.Mios as Mios

viewResolutionX, viewResolutionY :: Int
viewResolutionX = 4
viewResolutionY = 4

numOfGrid :: Int
numOfGrid = viewResolutionX * viewResolutionY

type Rule = CNF.BoolForm

-- | Application level symbols corresponding to literals in CNF
--
-- the number of SLit is 4 * numOfGrid + 12 + 5 + 6 + numOfGrid = 5 * numOfGrid + 23, f.e:
--
-- * (3, 4) grid =>  83 literals
-- * (5, 6) gird => 173 literals
--
data SLit where
  -- + the environment part :: direction = input [1 .. 4 * numOfGrid + 12]
  MyZone :: Int -> SLit
  BallZone :: Int -> SLit
  MateZone :: Int -> SLit
  EnemyZone :: Int -> SLit
  -- + 12 literals to designate the player's rank about the distance to the ball
  BallDist :: Int -> SLit       -- Note: 0 in 0 to 11 ([1 .. 12]) means I'M-KEEPING-THE-BALL
  -- + 2 misc input literal part
  OurBall :: SLit               --  the 4 * numOfGrid + 13th
  CloseToEnemy :: SLit                 -- the 4 * numOfGrid + 14th as the last input literal
  -- + 3 intention literal part :: direction = output
  IntMove :: SLit
  IntKick :: SLit
  IntDribble :: SLit
  -- + (6 + numOfGrid) target literal part :: direction = output
  Target :: ActionTarget -> SLit
  deriving (Eq, Ord, Read, Show)

instance Enum SLit where
  fromEnum (MyZone n) = 0 + n
  fromEnum (BallZone n) = 1 * numOfGrid + n
  fromEnum (MateZone n) = 2 * numOfGrid + n
  fromEnum (EnemyZone n) = 3 * numOfGrid + n
  fromEnum (BallDist n) = 4 * numOfGrid + 1 + n -- 0 based
  fromEnum OurBall = 4 * numOfGrid + 12 + 1
  fromEnum CloseToEnemy = 4 * numOfGrid + 12 + 2
  fromEnum IntMove = 4 * numOfGrid + 12 + 3
  fromEnum IntKick = 4 * numOfGrid + 12 + 4
  fromEnum IntDribble = 4 * numOfGrid + 12 + 5
  fromEnum (Target t) = 4 * numOfGrid + 12 + 6 + fromEnum t -- ActionTarget is 0 base (started from TargetBall)
  toEnum n
    | abs n <= 1 * numOfGrid = MyZone $ val n 0
    | abs n <= 2 * numOfGrid = BallZone $ val n (1 * numOfGrid)
    | abs n <= 3 * numOfGrid = MateZone $ val n (2 * numOfGrid)
    | abs n <= 4 * numOfGrid = EnemyZone $ val n (3 * numOfGrid)
    | abs n <= gBlock = BallDist $ val n (4 * numOfGrid + 1)
    | abs n == gBlock + 1 = OurBall
    | abs n == gBlock + 2 = CloseToEnemy
    | abs n == gBlock + 3 = IntMove
    | abs n == gBlock + 4 = IntKick
    | abs n == gBlock + 5 = IntDribble
    | abs n <= gBlock + 5 + fromEnum DefenceLine + 1 = Target . toEnum $ val n (gBlock + 5 + 1)
    | abs n <= gBlock + 5 + numOfGrid = Target . TargetGrid theGrid $ val n (gBlock + 5 + fromEnum DefenceLine + 1)
    | otherwise = error "invalid arg to toEnum :: Int -> SLit"
    where
      val x k = abs x - k
      gBlock = 4 * numOfGrid + 12

-- | minBound :: SLit == 1, maxBound :: SLit == 80
instance CNF.BoolComponent SLit where
  toBF = CNF.toBF . fromEnum
--  fromBF = undefined

asSym :: Int -> String
asSym n
  | n < 0 = "!" ++ show (toEnum n :: SLit)
  | otherwise = show (toEnum n :: SLit)

newIntentionBySAT :: GameContext -> Maybe Ball -> Player -> IO Intention
newIntentionBySAT g b p@(_property -> _roll -> PlayerSAT) = do
  let env = makeLiterals g b p
  case b of
    Just _ | elem (fromEnum (BallDist 0)) env -> return ()
    Nothing | notElem (fromEnum (BallDist 0)) env -> return ()
    _ -> error $ show (fromEnum( BallDist 0), b, env)
  -- TODO: select action based on Directorintention
  {-- debug -}
  ans <- callSolver' (g ^. solverIteration) env
  case filter (fromEnum CloseToEnemy <) <$> ans of
    Just [] -> do
      -- CNF.toFile "dump.cnf" $ buildCNF env
      -- error $ "no action:" ++ show env ++ "\n" ++ literalsToEnv env
      return NoPlan
    Just outLits -> do
      let (Just ans') = ans
      when (g ^. debug && mod (g ^. time) 2 == 0) $ writeIORef (g ^. satAssignments) $ map (0 <) ans'
      let actions = map toEnum $ filter (\n -> fromEnum IntMove <= n && n <= fromEnum IntDribble) outLits
      let targets = map toEnum $ filter (fromEnum (Target (minBound:: ActionTarget)) <=) outLits
      case targets of
        [] | null actions -> putStrLn "NoAction" >> return NoPlan
        [] -> error $ "no action target:" ++ show (env, actions, targets) ++ "\n" ++ literalsToEnv env
        (Target t:_) | elem IntMove actions -> return (GoFor 1.3 t)
        (Target t:_) | elem IntKick actions && b /= Nothing -> return (KickTo 2.4 t)
        (Target t:_) | elem IntKick actions -> error $ "strange decision: " ++ show (b, p, t)
        (Target t:_) | elem IntDribble actions && b /= Nothing -> return (DribblingTo 1.25 t)
        (Target t:_) | elem IntDribble actions -> error $ "strange decision: " ++ show (b, p, t)
        _ | null actions -> return NoPlan
    Nothing -> do
      -- CNF.toFile "dump.cnf" $ buildCNF env
      error $ "unsolvable: " ++ show env ++ "\n" ++ literalsToEnv env

fromContext :: GameContext -> Player -> [[Int]]
fromContext _ _ = []

-- fromAssigns :: ??-> [Bool]
-- 62 literals
toBools :: [GameContext -> Maybe Ball -> Player -> [Bool]]
toBools =
  [
    mapOfMe               -- my position category (1- 12: 12 literals) [mapMeZone1 .. mapMeZone12]
  , mapOfBall              -- ball position category (13 - 24: 12 literals) [mapBallZone1 .. mapBallzone12]
  , mapOfMates           -- (36- 47: 12 literals) [mapMateZone1 .. mapMateZone12]
  , mapOfEnemies         -- (48-59: 12 literals) [mapEnemyZone1 .. mapEnemyZone12]
  , positionToBall       -- order of distance to ball (60-72: 12 literals) [ballDist0 .. ballDist11]
  , ourBall
  , closeToEnemy
  ]

makeLiterals :: GameContext -> Maybe Ball -> Player -> [Int]
makeLiterals g b p = zipWith (\n p -> if p then n else negate n) [1 ..] . concat {- . withStrategy rpar -} $ map (\f -> f g b p) toBools

literalsToEnv :: [Int] -> String
literalsToEnv env = intercalate "\n" [me, ball, ourBall, mates, enemies, ord]
  where
    me = check "my position" 0 $ sublist 0 numOfGrid
    ball = check "ball position" numOfGrid $ sublist numOfGrid (2 * numOfGrid)
    mates = "mates positions: " ++ (show . map (subtract (2 * numOfGrid)) . filter (0 <) $ sublist (2 * numOfGrid) (3 * numOfGrid))
    enemies = "enemies positions: " ++ (show . map (subtract (2 * numOfGrid)) . filter (0 <) $ sublist (3 * numOfGrid) (4 * numOfGrid))
    ord = check "distance order" (4 * numOfGrid + 1) $ sublist (4 * numOfGrid) (5 * numOfGrid)
    ourBall = if elem (fromEnum OurBall) env then "our ball" else "not our ball"
    check mes k l =
      if length (filter (0 <) l) == 1
        then mes ++ ": " ++ show (subtract k <$> find (0 <) l)
        else "calculation of " ++ mes ++ " was wrong"
    sublist f t = take (t - f) . drop f $ env

mapOfMe :: GameContext -> Maybe Ball -> Player -> [Bool]
mapOfMe _ _ p@(_property -> _team -> t) = positionLiterals preds (p ^. geometrics_p . position)
  where preds = (if t == Team1 then gridViewOfTeam1 else gridViewOfTeam2) (viewResolutionX, viewResolutionY)

mapOfBall :: GameContext -> Maybe Ball -> Player -> [Bool]
mapOfBall (_ball -> b) _ (_property -> _team -> t) = positionLiterals preds (positionOf b)
  where preds = (if t == Team1 then gridViewOfTeam1 else gridViewOfTeam2) (viewResolutionX, viewResolutionY)

-- | 12 literals: whether i have ball : /n/th literal is on if the player is the /n/th closest player to ball
positionToBall :: GameContext -> Maybe Ball -> Player -> [Bool]
positionToBall g (Just b) p = take 12 $ True : repeat False
  -- check the geometric condition
--  unless (near2 30 (p ^. geometrics_p . position) (positionOf b)) $
--    error $ show ("strange distance conditio", p, b)

positionToBall g Nothing p
  | positionOf b == (p ^. geometrics_p . position) = take 12 $ True : repeat False  -- i'm on ball, i didn't know!
--  | distance (positionOf b) (p ^. geometrics_p . position) < 3 = take 12 $ True : repeat False  -- i'm on ball, i didn't know!
  | otherwise = (False :) . map (myID ==) $ nears
  where
    myID = p ^. property . idNumber
    tc = getTeamContext g p
    b = g ^. ball
    t = expectedTime b (p ^. geometrics_p . position) (p ^. geometrics_p . velocity)
    nears = (map _idNumber . nearestPlayers (positionOf (b <!! t))) $ getTeammatePositions g p False

nearestPlayers :: TwoD -> [(PlayerProperty, TwoD)] -> [PlayerProperty]
nearestPlayers (x, y) assoc = map fst $ sortBy (comparing (dist . snd)) assoc
  where dist (x1, y1) = sqrt $ (x1 -x) ** 2 + (y1 - y) ** 2

mapOfMates :: GameContext -> Maybe Ball -> Player -> [Bool]
mapOfMates g _ p = map (flip any mates) preds
  where
    mates = map snd . filter (((p ^. property . idNumber) /=) . _idNumber . fst) $ getTeammatePositions g p False
    preds = (if p ^. property . team == Team1 then gridViewOfTeam1 else gridViewOfTeam2) (viewResolutionX, viewResolutionY)

mapOfEnemies :: GameContext -> Maybe Ball -> Player -> [Bool]
mapOfEnemies g b p = map (flip any enmies) preds
  where
    enmies = map snd $ getEnemyPositions g p
    preds = (if p ^. property . team == Team1 then gridViewOfTeam1 else gridViewOfTeam2) (viewResolutionX, viewResolutionY)

ourBall :: GameContext -> Maybe Ball -> Player -> [Bool]
ourBall g@(_ball -> _holdBy -> holder) _ p =
  (: []) $ case holder of { Nothing -> False; Just x -> elem x (_teammates (getTeamContext g p)) }

closeToEnemy :: GameContext -> Maybe Ball -> Player -> [Bool]
closeToEnemy g _ p@(_geometrics_p -> _position -> pos) = [Nothing /= find ((< 20) . (<-> pos) . snd) (getEnemyPositions g p)]

--------------------------------------------------------------------------------
-- SAT rules
--------------------------------------------------------------------------------

theGrid :: (Int, Int)
theGrid = (viewResolutionX, viewResolutionY)

zones :: [Int]
zones = [1 .. numOfGrid]

targets :: [SLit]
targets = map Target [TargetBall .. TargetZone numOfGrid]

anywhere :: (Int -> SLit) -> Int -> Int -> Rule
anywhere sym from to = foldr (\n exp -> exp -|- sym n) (CNF.toBF from) [from + 1 .. to]

andAll :: [Rule] -> Rule
andAll (x:l) =foldr (-&-) x l

orAll :: [Rule] -> Rule
orAll (x:l) =foldr (-|-) x l

toCNF :: CNF.BoolComponent a => a -> CNF.BoolForm
toCNF = CNF.toBF

--------------------------------------------------------------------------------
-- | primary actions
irrational_behaviors :: Rule
irrational_behaviors = neg (IntKick -&- Target TargetBall)
                       -&- neg (IntKick -&- Target TargetDefaultPosition)
                       -&- neg (IntDribble -&- Target TargetBall)
                       -&- neg (IntMove -&- Target TargetMate)
                       -&- neg (IntDribble -&- Target TargetMate)

i_need_an_action :: Rule
i_need_an_action = (IntMove -|- IntKick -|- IntDribble) -&- orAll [toCNF t | t <- targets]

default_position_is_the_last_option :: Rule
default_position_is_the_last_option = orAll [toCNF t | t <-targets, t /= Target TargetDefaultPosition] ->- neg (toCNF (Target TargetDefaultPosition))

zone_is_better_than_offsideline = anywhere (Target . TargetZone) 1 numOfGrid
                                  ->- (neg (orAll [toCNF (Target t) | t <- [TargetOffsideLine .. DefenceLine]]))

zone_is_exclusive = andAll [ toCNF (Target (TargetZone z)) ->- andAll [neg (Target (TargetZone z')) | z' <- [1 .. numOfGrid], z /= z'] | z <- [1 .. numOfGrid]]

out_of_field =  (neg (anywhere MyZone 1 numOfGrid)) ->- (IntMove -&- Target TargetDefaultPosition)

i_have_ball :: Rule
i_have_ball = BallDist 0 ->- neg IntMove

i_dont_keep_ball :: Rule
i_dont_keep_ball = neg (BallDist 0) ->- (neg IntKick -&- neg IntDribble)

i_have_ball0 :: Rule
i_have_ball0 = andAll [(MyZone r -&- BallDist 0 -&- (neg (MateZone 1) -|- neg (MateZone 2) -|- neg (MateZone 3))) ->- (IntDribble -&- Target TargetGoal) | r <- [4 .. 6]]

i_have_ball1 :: Rule
i_have_ball1 = andAll [(MyZone r -&- BallDist 0 -&- MateZone r') ->- (IntKick -&- Target (TargetGrid theGrid r'))
                      | r <- [1 + viewResolutionX * 2 * div viewResolutionY 4 .. viewResolutionY * 3 * div viewResolutionY 4]
                      , r' <- [1 .. viewResolutionX * div viewResolutionY 4]]

i_have_ball2 :: Rule
i_have_ball2 = andAll [(MyZone r -&- BallDist 0) ->- (IntKick -&- Target TargetMate)
                      | r <- [1 + viewResolutionX * 3 * div viewResolutionX 4 .. numOfGrid]]

i_have_ball3 :: Rule
i_have_ball3 = andAll [(MyZone r -&- BallDist 0) ->- (IntKick -&- Target TargetGoal)
                      | r <- [1 .. viewResolutionX * div viewResolutionX 4]]

i_must_get_ball :: Rule
i_must_get_ball = (neg OurBall -&- (BallDist 1 -|- BallDist 2)) ->- (IntMove -&- Target TargetBall)

-- I'm in offside position
im_in_offside_position :: Rule
im_in_offside_position =
  ((neg OurBall -&- (anywhere MyZone frontL frontR) -&- (anywhere BallZone (frontR + 1) numOfGrid)) ->- (IntMove -&- Target TargetBall))
  -&- ((neg OurBall -&- (anywhere MyZone frontL (2 * frontR)) -&- (anywhere BallZone (2 * frontR + 1) numOfGrid)) ->- (IntMove -&- Target TargetBall))
  where
    frontL = 1
    frontR = viewResolutionX

im_nearest_to_ball :: Rule
im_nearest_to_ball = andAll [(neg OurBall -&- neg (BallDist 0) -&- MyZone r -&- BallZone r) ->- (IntMove -&- Target TargetBall) | r <- zones]

i_must_shoot :: Rule
i_must_shoot = (MyZone 2 -&- BallDist 0) ->- (IntKick -&- Target TargetGoal)

im_top_and_near_goal :: Rule
im_top_and_near_goal = andAll [ (MyZone r -&- BallDist 0 -&- (neg (EnemyZone r))) ->- (IntKick -&- Target TargetGoal)
                              | r <- [1 .. viewResolutionX]]

up_to_reverse_side :: Rule
up_to_reverse_side = andAll [(OurBall -&- MyZone r -&- BallZone r' -&- MateZone r' -&- MateZone r -&- neg (MateZone r'') -&- neg (BallDist 1) -&- neg (BallDist 2)) ->- (IntMove -&- Target (TargetGrid theGrid r'')) | r <- [4 .. 9], (r', r'') <- [(4,3), (5,1), (5,3), (6, 1)]]

push_forward :: Rule
push_forward = andAll [(MyZone r -&- BallZone r' -&- neg (BallDist 1) -&- neg (BallDist 2)) ->- (IntMove -&- Target (TargetGrid theGrid 2)) | r <- [frontR + 1 .. numOfGrid], r' <- [1..frontR]]
  where
    frontR = 2 * viewResolutionX

push_forward2 = (anywhere MyZone 7 numOfGrid -&- anywhere BallZone 1 6 -&- neg (BallDist 1) -&- neg (BallDist 2) -&- neg (BallDist 3)) ->- (IntMove -&- Target (TargetGrid theGrid 2))

push_forward3 = andAll [(MyZone r -&- BallZone r' -&- neg (MateZone 2)) ->- (IntMove -&- Target (TargetGrid theGrid 2)) | r <- [1,viewResolutionX], r' <- [viewResolutionX + 1 .. 2 * viewResolutionX]]

not_to_dribble_near_enemy = CloseToEnemy ->- neg IntDribble

-- | the rule
-- Note: use following commands to display
--
-- >>> CNF.asList theRule
--
-- >>> CNF.asLatex theRule
--
-- >>> CNF.toFile "filename.cnf" (CNF.asList theRule)
--
-- >>> CNF.toCNFString (CNF.asList theRule)

theRule :: Rule
theRule =
  andAll
  [
    irrational_behaviors
--  , out_of_field
  , i_need_an_action
--  , zone_is_better_than_offsideline
  , zone_is_exclusive
  , default_position_is_the_last_option
  , i_have_ball
  , i_have_ball0
  , i_have_ball1
  , i_have_ball2
  , i_dont_keep_ball
  , i_must_get_ball
  , im_in_offside_position
  , im_nearest_to_ball
  , i_must_shoot
  , im_top_and_near_goal
  , up_to_reverse_side
  , push_forward
  , push_forward2
  , push_forward3
  , not_to_dribble_near_enemy
  ]

theCNF :: [[Int]]
theCNF = CNF.asList theRule

-- | the number of input literals, the number of literals, the number of clauses
cnfInfo :: (Int, Int, Int)
cnfInfo = (fromEnum CloseToEnemy, maximum . map abs . concat $ theCNF, length (CNF.asList theRule))

-- | With the given [Int] that represents the environment, return valid actions by a SAT solver
callSolver :: [Int] -> IO (Maybe [Int])
callSolver lst = Just <$> Mios.solveSAT (Mios.CNFDescription ls (cs + length lst) Nothing) (map (:[]) lst ++ theCNF)
  where (_, ls, cs) = cnfInfo

callSolver' :: Int -> [Int] -> IO (Maybe [Int])
callSolver' 1 lst = do
  -- putStrLn $ "O(SAT) = " ++ show [elem (fromEnum (BallDist 0)) lst, elem (fromEnum (BallDist 1)) lst, elem (fromEnum (BallDist 2)) lst] ++ " : " ++ literalsToEnv lst
  callSolver lst

callSolver' n lst = do
  res <- callSolver lst
  case res of
    ans@(Just lit') -> do
      res' <- callSolver' (n -1) $ lst ++ map negate (firstIntention lit')
      case res' of
        Nothing -> return ans
        next -> return next
    _ -> return Nothing
  where
    firstIntention l
      | null (filter (fromEnum IntDribble <) l) = error $ "strange: " ++ show l
      | elem (fromEnum IntMove) l = [fromEnum IntMove, head (filter (fromEnum IntDribble <) l)]
      | elem (fromEnum IntKick) l = [fromEnum IntKick, head (filter (fromEnum IntDribble <) l)]
      | elem (fromEnum IntDribble) l = [fromEnum IntDribble, head (filter (fromEnum IntDribble <) l)]
      | otherwise = error $ show l

-- | for debugging
buildCNF :: [Int] -> [[Int]]
buildCNF lst = map (:[]) lst ++ theCNF

dumpTheRule :: FilePath -> IO ()
dumpTheRule filename = CNF.toFile filename theCNF

dumpTheCNF :: FilePath -> GameContext -> IO ()
dumpTheCNF filename g = CNF.toFile filename $ buildCNF $ makeLiterals g Nothing (nthPlayer g 1)
