module Common.GtkGoal where

import Data.List (isInfixOf)
import Data.Char (toLower)

import Interfaces.GenericATPState

import Logic.Prover

import Static.GTheory

-- * Datatypes and functions for prover

data Goal = Goal
  { gStatus :: GStatus
  , gName :: String }
  deriving (Eq, Ord)

toGtkGoal :: (String, Maybe BasicProof) -> Goal
toGtkGoal (n, st) =
          Goal { gName = n
               , gStatus = maybe GOpen basicProofToGStatus st }

showGoal :: Goal -> String
showGoal (Goal { gName = n, gStatus = s }) =
  spanString s $ statusToPrefix s ++ n

data GStatus = GOpen
             | GTimeout
             | GDisproved
             | GInconsistent
             | GProved
             | GGuessed
             | GConjectured
             | GHandwritten
               deriving (Eq, Ord)

instance Show GStatus where
  show GProved       = spanString GProved       "Proved"
  show GInconsistent = spanString GInconsistent "Inconsistent"
  show GDisproved    = spanString GDisproved    "Disproved"
  show GOpen         = spanString GOpen         "Open"
  show GTimeout      = spanString GTimeout      "Open (Timeout!)"
  show GGuessed      = spanString GGuessed      "Guessed"
  show GConjectured  = spanString GConjectured  "Conjectured"
  show GHandwritten  = spanString GHandwritten  "Handwritten"

showSimple :: GStatus -> String
showSimple gs = case gs of
  GProved       -> "Proved"
  GInconsistent -> "Inconsistent"
  GDisproved    -> "Disproved"
  GOpen         -> "Open"
  GTimeout      -> "Open (Timeout!)"
  GGuessed      -> "Guessed"
  GConjectured  -> "Conjectured"
  GHandwritten  -> "Handwritten"


statusToColor :: GStatus -> String
statusToColor s = case s of
  GOpen         -> "black"
  GProved       -> "green"
  GDisproved    -> "red"
  GTimeout      -> "blue"
  GInconsistent -> "orange"
  GGuessed      -> "darkgreen"
  GConjectured  -> "darkgreen"
  GHandwritten  -> "darkgreen"

statusToPrefix :: GStatus -> String
statusToPrefix s = case s of
  GOpen         -> "[ ] "
  GProved       -> "[+] "
  GDisproved    -> "[-] "
  GTimeout      -> "[t] "
  GInconsistent -> "[*] "
  GGuessed      -> "[.] "
  GConjectured  -> "[:] "
  GHandwritten  -> "[/] "

spanString :: GStatus -> String -> String
spanString s m = "<span color=\"" ++ statusToColor s ++ "\">" ++ m ++ "</span>"

-- | Converts a ProofStatus into a GStatus
proofStatusToGStatus :: ProofStatus a -> GStatus
proofStatusToGStatus p = case goalStatus p  of
  Proved False -> GInconsistent
  Proved True  -> GProved
  Disproved    -> GDisproved
  Open (Reason s) ->
    if any (isInfixOf "timeout" . map toLower) s then GTimeout else GOpen

-- | Converts a BasicProof into a GStatus
basicProofToGStatus :: BasicProof -> GStatus
basicProofToGStatus p = case p of
  BasicProof _ st -> proofStatusToGStatus st
  Guessed         -> GGuessed
  Conjectured     -> GConjectured
  Handwritten     -> GHandwritten

-- | Converts a GenericConfig into a GStatus
genericConfigToGStatus :: GenericConfig a -> GStatus
genericConfigToGStatus cfg = case proofStatusToGStatus $ proofStatus cfg of
  GOpen -> if timeLimitExceeded cfg then GTimeout else GOpen
  s     -> s
