81d182b21020b815887e9057959228546cf61b6bChristian Maederimport Data.List (isInfixOf)
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maederimport Data.Char (toLower)
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder-- * Datatypes and functions for prover
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederdata Goal = Goal
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder { gStatus :: GStatus
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , gName :: String }
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder deriving (Eq, Ord)
05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedertoGtkGoal :: (String, Maybe BasicProof) -> Goal
05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedertoGtkGoal (n, st) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Goal { gName = n
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder , gStatus = maybe GOpen basicProofToGStatus st }
ad270004874ce1d0697fb30d7309f180553bb315Christian MaedershowGoal :: Goal -> String
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian MaedershowGoal (Goal { gName = n, gStatus = s }) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder spanString s $ statusToPrefix s ++ n
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata GStatus = GOpen
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | GInconsistent
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder | GConjectured
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder | GHandwritten
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder deriving (Eq, Ord)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Show GStatus where
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder show GProved = spanString GProved "Proved"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder show GInconsistent = spanString GInconsistent "Inconsistent"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder show GDisproved = spanString GDisproved "Disproved"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder show GOpen = spanString GOpen "Open"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder show GTimeout = spanString GTimeout "Open (Timeout!)"
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder show GGuessed = spanString GGuessed "Guessed"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder show GConjectured = spanString GConjectured "Conjectured"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder show GHandwritten = spanString GHandwritten "Handwritten"
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian MaedershowSimple :: GStatus -> String
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian MaedershowSimple gs = case gs of
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder GProved -> "Proved"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GInconsistent -> "Inconsistent"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GDisproved -> "Disproved"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GOpen -> "Open"
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder GTimeout -> "Open (Timeout!)"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GGuessed -> "Guessed"
07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maeder GConjectured -> "Conjectured"
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder GHandwritten -> "Handwritten"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederstatusToColor :: GStatus -> String
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederstatusToColor s = case s of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GOpen -> "black"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GProved -> "green"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GDisproved -> "red"
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder GTimeout -> "blue"
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder GInconsistent -> "orange"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GGuessed -> "darkgreen"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GConjectured -> "darkgreen"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GHandwritten -> "darkgreen"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederstatusToPrefix :: GStatus -> String
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederstatusToPrefix s = case s of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GOpen -> "[ ] "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GProved -> "[+] "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GDisproved -> "[-] "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GTimeout -> "[t] "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GInconsistent -> "[*] "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GGuessed -> "[.] "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GConjectured -> "[:] "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GHandwritten -> "[/] "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederspanString :: GStatus -> String -> String
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederspanString s m = "<span color=\"" ++ statusToColor s ++ "\">" ++ m ++ "</span>"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | Converts a ProofStatus into a GStatus
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederproofStatusToGStatus :: ProofStatus a -> GStatus
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederproofStatusToGStatus p = case goalStatus p of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Proved False -> GInconsistent
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Proved True -> GProved
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Disproved -> GDisproved
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Open (Reason s) ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if any (isInfixOf "timeout" . map toLower) s then GTimeout else GOpen
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | Converts a BasicProof into a GStatus
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederbasicProofToGStatus :: BasicProof -> GStatus
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederbasicProofToGStatus p = case p of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder BasicProof _ st -> proofStatusToGStatus st
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Guessed -> GGuessed
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Conjectured -> GConjectured
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder Handwritten -> GHandwritten
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | Converts a GenericConfig into a GStatus
81d182b21020b815887e9057959228546cf61b6bChristian MaedergenericConfigToGStatus :: GenericConfig a -> GStatus
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian MaedergenericConfigToGStatus cfg = case proofStatusToGStatus $ proofStatus cfg of
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder GOpen -> if timeLimitExceeded cfg then GTimeout else GOpen