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
  { Goal -> GStatus
gStatus :: GStatus
  , Goal -> String
gName :: String }
  deriving (Goal -> Goal -> Bool
(Goal -> Goal -> Bool) -> (Goal -> Goal -> Bool) -> Eq Goal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Goal -> Goal -> Bool
$c/= :: Goal -> Goal -> Bool
== :: Goal -> Goal -> Bool
$c== :: Goal -> Goal -> Bool
Eq, Eq Goal
Eq Goal =>
(Goal -> Goal -> Ordering)
-> (Goal -> Goal -> Bool)
-> (Goal -> Goal -> Bool)
-> (Goal -> Goal -> Bool)
-> (Goal -> Goal -> Bool)
-> (Goal -> Goal -> Goal)
-> (Goal -> Goal -> Goal)
-> Ord Goal
Goal -> Goal -> Bool
Goal -> Goal -> Ordering
Goal -> Goal -> Goal
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Goal -> Goal -> Goal
$cmin :: Goal -> Goal -> Goal
max :: Goal -> Goal -> Goal
$cmax :: Goal -> Goal -> Goal
>= :: Goal -> Goal -> Bool
$c>= :: Goal -> Goal -> Bool
> :: Goal -> Goal -> Bool
$c> :: Goal -> Goal -> Bool
<= :: Goal -> Goal -> Bool
$c<= :: Goal -> Goal -> Bool
< :: Goal -> Goal -> Bool
$c< :: Goal -> Goal -> Bool
compare :: Goal -> Goal -> Ordering
$ccompare :: Goal -> Goal -> Ordering
$cp1Ord :: Eq Goal
Ord)

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

showGoal :: Goal -> String
showGoal :: Goal -> String
showGoal (Goal { gName :: Goal -> String
gName = String
n, gStatus :: Goal -> GStatus
gStatus = GStatus
s }) =
  GStatus -> String -> String
spanString GStatus
s (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ GStatus -> String
statusToPrefix GStatus
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n

data GStatus = GOpen
             | GTimeout
             | GDisproved
             | GInconsistent
             | GProved
             | GGuessed
             | GConjectured
             | GHandwritten
               deriving (GStatus -> GStatus -> Bool
(GStatus -> GStatus -> Bool)
-> (GStatus -> GStatus -> Bool) -> Eq GStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GStatus -> GStatus -> Bool
$c/= :: GStatus -> GStatus -> Bool
== :: GStatus -> GStatus -> Bool
$c== :: GStatus -> GStatus -> Bool
Eq, Eq GStatus
Eq GStatus =>
(GStatus -> GStatus -> Ordering)
-> (GStatus -> GStatus -> Bool)
-> (GStatus -> GStatus -> Bool)
-> (GStatus -> GStatus -> Bool)
-> (GStatus -> GStatus -> Bool)
-> (GStatus -> GStatus -> GStatus)
-> (GStatus -> GStatus -> GStatus)
-> Ord GStatus
GStatus -> GStatus -> Bool
GStatus -> GStatus -> Ordering
GStatus -> GStatus -> GStatus
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: GStatus -> GStatus -> GStatus
$cmin :: GStatus -> GStatus -> GStatus
max :: GStatus -> GStatus -> GStatus
$cmax :: GStatus -> GStatus -> GStatus
>= :: GStatus -> GStatus -> Bool
$c>= :: GStatus -> GStatus -> Bool
> :: GStatus -> GStatus -> Bool
$c> :: GStatus -> GStatus -> Bool
<= :: GStatus -> GStatus -> Bool
$c<= :: GStatus -> GStatus -> Bool
< :: GStatus -> GStatus -> Bool
$c< :: GStatus -> GStatus -> Bool
compare :: GStatus -> GStatus -> Ordering
$ccompare :: GStatus -> GStatus -> Ordering
$cp1Ord :: Eq GStatus
Ord)

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

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


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

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

spanString :: GStatus -> String -> String
spanString :: GStatus -> String -> String
spanString s :: GStatus
s m :: String
m = "<span color=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ GStatus -> String
statusToColor GStatus
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\">" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ "</span>"

-- | Converts a ProofStatus into a GStatus
proofStatusToGStatus :: ProofStatus a -> GStatus
proofStatusToGStatus :: ProofStatus a -> GStatus
proofStatusToGStatus p :: ProofStatus a
p = case ProofStatus a -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus ProofStatus a
p of
  Proved False -> GStatus
GInconsistent
  Proved True -> GStatus
GProved
  Disproved -> GStatus
GDisproved
  Open (Reason s :: [String]
s) ->
    if (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "timeout" (String -> Bool) -> (String -> String) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower) [String]
s then GStatus
GTimeout else GStatus
GOpen

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

-- | Converts a GenericConfig into a GStatus
genericConfigToGStatus :: GenericConfig a -> GStatus
genericConfigToGStatus :: GenericConfig a -> GStatus
genericConfigToGStatus cfg :: GenericConfig a
cfg = case ProofStatus a -> GStatus
forall a. ProofStatus a -> GStatus
proofStatusToGStatus (ProofStatus a -> GStatus) -> ProofStatus a -> GStatus
forall a b. (a -> b) -> a -> b
$ GenericConfig a -> ProofStatus a
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig a
cfg of
  GOpen -> if GenericConfig a -> Bool
forall proof_tree. GenericConfig proof_tree -> Bool
timeLimitExceeded GenericConfig a
cfg then GStatus
GTimeout else GStatus
GOpen
  s :: GStatus
s -> GStatus
s