content: 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
  