{- |
Module      :  ./SoftFOL/MathServParsing.hs
Description :  Functions for parsing MathServ output as a MathServResponse
Copyright   :  (c) Rainer Grabbe, DFKI GmbH
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  unknown

Functions for parsing MathServ output into a MathServResponse structure.

-}

module SoftFOL.MathServParsing
  ( callMathServ
  , parseMathServOut
  , MathServServices (..)
  , MathServOperationTypes (..)
  , MathServCall (..)
  , MathServResponse (..)
  , MWFoAtpResult (..)
  , MWFormalProof (..)
  , MWStatus (..)
  , FoAtpStatus (..)
  , SolvedStatus (..)
  , UnsolvedStatus (..)
  , MWCalculus (..)
  , MWTimeResource (..)
  ) where

import Common.Utils (getEnvSave, readMaybe)

import Text.XML.Light
import Network.HTTP
import Network.HTTP.HandleStream as S

import Data.Char
import Data.List
import Data.Maybe
import Data.Time (TimeOfDay, timeToTimeOfDay)

-- * Datatypes for MathServ services

data ServerAddr = ServerAddr
    { ServerAddr -> String
serverName :: String
    , ServerAddr -> Int
portNumber :: Int }

instance Show ServerAddr where
    showsPrec :: Int -> ServerAddr -> ShowS
showsPrec _ sAdd :: ServerAddr
sAdd =
        (ServerAddr -> String
serverName ServerAddr
sAdd String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar ':' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Show a => a -> ShowS
shows (ServerAddr -> Int
portNumber ServerAddr
sAdd)

instance Read ServerAddr where
    readsPrec :: Int -> ReadS ServerAddr
readsPrec _ s :: String
s = let
        (n :: String
n, portRest :: String
portRest) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= ':') String
s
        (portS :: String
portS, rest :: String
rest) = case String
portRest of
          "" -> ("", "")
          _ : r :: String
r -> (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isDigit String
r
        portN :: Int
portN = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 8080 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
portS
       in [(ServerAddr :: String -> Int -> ServerAddr
ServerAddr { serverName :: String
serverName = String
n, portNumber :: Int
portNumber = Int
portN }, String
rest)]

defaultServer :: ServerAddr
defaultServer :: ServerAddr
defaultServer = ServerAddr :: String -> Int -> ServerAddr
ServerAddr
  { serverName :: String
serverName = "mathserv.informatik.uni-bremen.de"
  , portNumber :: Int
portNumber = 8080 }


{- |
  Record type for all needed data to do a MathServ call.
-}
data MathServCall = MathServCall {
    -- | Selected MathServ service
    MathServCall -> MathServServices
mathServService :: MathServServices,
    -- | Selected MathServ operation
    MathServCall -> MathServOperationTypes
mathServOperation :: MathServOperationTypes,
    -- | Problem to prove in TPTP format
    MathServCall -> String
problem :: String,
    -- | Time limit
    MathServCall -> Int
proverTimeLimit :: Int,
    -- | Extra options
    MathServCall -> Maybe String
extraOptions :: Maybe String
  }

{- |
  MathServ services to select.
-}
data MathServServices =
  -- | Broker service
    Broker
  -- | Vampire service
  | VampireService
  deriving Int -> MathServServices -> ShowS
[MathServServices] -> ShowS
MathServServices -> String
(Int -> MathServServices -> ShowS)
-> (MathServServices -> String)
-> ([MathServServices] -> ShowS)
-> Show MathServServices
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MathServServices] -> ShowS
$cshowList :: [MathServServices] -> ShowS
show :: MathServServices -> String
$cshow :: MathServServices -> String
showsPrec :: Int -> MathServServices -> ShowS
$cshowsPrec :: Int -> MathServServices -> ShowS
Show

{- |
  MathServ operation to select. These are only common types and will be
  translated into correct MathServOperations.
-}
data MathServOperationTypes =
  -- | stands for ProveProblemOpt
    ProblemOpt
  -- | stands for ProveProblemChoice
  | ProblemChoice
  -- | stands for ProveTPTPProblem or ProveTPTPProblemWithOptions
  | TPTPProblem
  -- | stands for ProveProblem
  | Problem
  deriving Int -> MathServOperationTypes -> ShowS
[MathServOperationTypes] -> ShowS
MathServOperationTypes -> String
(Int -> MathServOperationTypes -> ShowS)
-> (MathServOperationTypes -> String)
-> ([MathServOperationTypes] -> ShowS)
-> Show MathServOperationTypes
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MathServOperationTypes] -> ShowS
$cshowList :: [MathServOperationTypes] -> ShowS
show :: MathServOperationTypes -> String
$cshow :: MathServOperationTypes -> String
showsPrec :: Int -> MathServOperationTypes -> ShowS
$cshowsPrec :: Int -> MathServOperationTypes -> ShowS
Show

{- |
  A MathServ response structure to be filled by parsing all rdf-objects
  returned by MathServ.
-}
data MathServResponse =
       MathServResponse { MathServResponse -> Either String MWFoAtpResult
foAtpResult :: Either String MWFoAtpResult,
                          MathServResponse -> MWTimeResource
timeResource :: MWTimeResource
                          } deriving (MathServResponse -> MathServResponse -> Bool
(MathServResponse -> MathServResponse -> Bool)
-> (MathServResponse -> MathServResponse -> Bool)
-> Eq MathServResponse
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MathServResponse -> MathServResponse -> Bool
$c/= :: MathServResponse -> MathServResponse -> Bool
== :: MathServResponse -> MathServResponse -> Bool
$c== :: MathServResponse -> MathServResponse -> Bool
Eq, Eq MathServResponse
Eq MathServResponse =>
(MathServResponse -> MathServResponse -> Ordering)
-> (MathServResponse -> MathServResponse -> Bool)
-> (MathServResponse -> MathServResponse -> Bool)
-> (MathServResponse -> MathServResponse -> Bool)
-> (MathServResponse -> MathServResponse -> Bool)
-> (MathServResponse -> MathServResponse -> MathServResponse)
-> (MathServResponse -> MathServResponse -> MathServResponse)
-> Ord MathServResponse
MathServResponse -> MathServResponse -> Bool
MathServResponse -> MathServResponse -> Ordering
MathServResponse -> MathServResponse -> MathServResponse
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 :: MathServResponse -> MathServResponse -> MathServResponse
$cmin :: MathServResponse -> MathServResponse -> MathServResponse
max :: MathServResponse -> MathServResponse -> MathServResponse
$cmax :: MathServResponse -> MathServResponse -> MathServResponse
>= :: MathServResponse -> MathServResponse -> Bool
$c>= :: MathServResponse -> MathServResponse -> Bool
> :: MathServResponse -> MathServResponse -> Bool
$c> :: MathServResponse -> MathServResponse -> Bool
<= :: MathServResponse -> MathServResponse -> Bool
$c<= :: MathServResponse -> MathServResponse -> Bool
< :: MathServResponse -> MathServResponse -> Bool
$c< :: MathServResponse -> MathServResponse -> Bool
compare :: MathServResponse -> MathServResponse -> Ordering
$ccompare :: MathServResponse -> MathServResponse -> Ordering
$cp1Ord :: Eq MathServResponse
Ord, Int -> MathServResponse -> ShowS
[MathServResponse] -> ShowS
MathServResponse -> String
(Int -> MathServResponse -> ShowS)
-> (MathServResponse -> String)
-> ([MathServResponse] -> ShowS)
-> Show MathServResponse
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MathServResponse] -> ShowS
$cshowList :: [MathServResponse] -> ShowS
show :: MathServResponse -> String
$cshow :: MathServResponse -> String
showsPrec :: Int -> MathServResponse -> ShowS
$cshowsPrec :: Int -> MathServResponse -> ShowS
Show)

data MWFoAtpResult =
       MWFoAtpResult { MWFoAtpResult -> MWFormalProof
proof :: MWFormalProof,
                       MWFoAtpResult -> String
outputStr :: String,
                       MWFoAtpResult -> MWStatus
systemStatus :: MWStatus,
                       MWFoAtpResult -> String
systemStr :: String,
                       MWFoAtpResult -> MWTimeResource
time :: MWTimeResource
                       } deriving (MWFoAtpResult -> MWFoAtpResult -> Bool
(MWFoAtpResult -> MWFoAtpResult -> Bool)
-> (MWFoAtpResult -> MWFoAtpResult -> Bool) -> Eq MWFoAtpResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MWFoAtpResult -> MWFoAtpResult -> Bool
$c/= :: MWFoAtpResult -> MWFoAtpResult -> Bool
== :: MWFoAtpResult -> MWFoAtpResult -> Bool
$c== :: MWFoAtpResult -> MWFoAtpResult -> Bool
Eq, Eq MWFoAtpResult
Eq MWFoAtpResult =>
(MWFoAtpResult -> MWFoAtpResult -> Ordering)
-> (MWFoAtpResult -> MWFoAtpResult -> Bool)
-> (MWFoAtpResult -> MWFoAtpResult -> Bool)
-> (MWFoAtpResult -> MWFoAtpResult -> Bool)
-> (MWFoAtpResult -> MWFoAtpResult -> Bool)
-> (MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult)
-> (MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult)
-> Ord MWFoAtpResult
MWFoAtpResult -> MWFoAtpResult -> Bool
MWFoAtpResult -> MWFoAtpResult -> Ordering
MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult
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 :: MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult
$cmin :: MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult
max :: MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult
$cmax :: MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult
>= :: MWFoAtpResult -> MWFoAtpResult -> Bool
$c>= :: MWFoAtpResult -> MWFoAtpResult -> Bool
> :: MWFoAtpResult -> MWFoAtpResult -> Bool
$c> :: MWFoAtpResult -> MWFoAtpResult -> Bool
<= :: MWFoAtpResult -> MWFoAtpResult -> Bool
$c<= :: MWFoAtpResult -> MWFoAtpResult -> Bool
< :: MWFoAtpResult -> MWFoAtpResult -> Bool
$c< :: MWFoAtpResult -> MWFoAtpResult -> Bool
compare :: MWFoAtpResult -> MWFoAtpResult -> Ordering
$ccompare :: MWFoAtpResult -> MWFoAtpResult -> Ordering
$cp1Ord :: Eq MWFoAtpResult
Ord, Int -> MWFoAtpResult -> ShowS
[MWFoAtpResult] -> ShowS
MWFoAtpResult -> String
(Int -> MWFoAtpResult -> ShowS)
-> (MWFoAtpResult -> String)
-> ([MWFoAtpResult] -> ShowS)
-> Show MWFoAtpResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MWFoAtpResult] -> ShowS
$cshowList :: [MWFoAtpResult] -> ShowS
show :: MWFoAtpResult -> String
$cshow :: MWFoAtpResult -> String
showsPrec :: Int -> MWFoAtpResult -> ShowS
$cshowsPrec :: Int -> MWFoAtpResult -> ShowS
Show)

data MWFormalProof =
       TstpCnfRefutation { MWFormalProof -> String
formalProof :: String,
                           MWFormalProof -> MWProvingProblem
proofOf :: MWProvingProblem,
                           MWFormalProof -> MWCalculus
calculus :: MWCalculus,
                           MWFormalProof -> String
axioms :: String
                           } deriving (MWFormalProof -> MWFormalProof -> Bool
(MWFormalProof -> MWFormalProof -> Bool)
-> (MWFormalProof -> MWFormalProof -> Bool) -> Eq MWFormalProof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MWFormalProof -> MWFormalProof -> Bool
$c/= :: MWFormalProof -> MWFormalProof -> Bool
== :: MWFormalProof -> MWFormalProof -> Bool
$c== :: MWFormalProof -> MWFormalProof -> Bool
Eq, Eq MWFormalProof
Eq MWFormalProof =>
(MWFormalProof -> MWFormalProof -> Ordering)
-> (MWFormalProof -> MWFormalProof -> Bool)
-> (MWFormalProof -> MWFormalProof -> Bool)
-> (MWFormalProof -> MWFormalProof -> Bool)
-> (MWFormalProof -> MWFormalProof -> Bool)
-> (MWFormalProof -> MWFormalProof -> MWFormalProof)
-> (MWFormalProof -> MWFormalProof -> MWFormalProof)
-> Ord MWFormalProof
MWFormalProof -> MWFormalProof -> Bool
MWFormalProof -> MWFormalProof -> Ordering
MWFormalProof -> MWFormalProof -> MWFormalProof
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 :: MWFormalProof -> MWFormalProof -> MWFormalProof
$cmin :: MWFormalProof -> MWFormalProof -> MWFormalProof
max :: MWFormalProof -> MWFormalProof -> MWFormalProof
$cmax :: MWFormalProof -> MWFormalProof -> MWFormalProof
>= :: MWFormalProof -> MWFormalProof -> Bool
$c>= :: MWFormalProof -> MWFormalProof -> Bool
> :: MWFormalProof -> MWFormalProof -> Bool
$c> :: MWFormalProof -> MWFormalProof -> Bool
<= :: MWFormalProof -> MWFormalProof -> Bool
$c<= :: MWFormalProof -> MWFormalProof -> Bool
< :: MWFormalProof -> MWFormalProof -> Bool
$c< :: MWFormalProof -> MWFormalProof -> Bool
compare :: MWFormalProof -> MWFormalProof -> Ordering
$ccompare :: MWFormalProof -> MWFormalProof -> Ordering
$cp1Ord :: Eq MWFormalProof
Ord, Int -> MWFormalProof -> ShowS
[MWFormalProof] -> ShowS
MWFormalProof -> String
(Int -> MWFormalProof -> ShowS)
-> (MWFormalProof -> String)
-> ([MWFormalProof] -> ShowS)
-> Show MWFormalProof
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MWFormalProof] -> ShowS
$cshowList :: [MWFormalProof] -> ShowS
show :: MWFormalProof -> String
$cshow :: MWFormalProof -> String
showsPrec :: Int -> MWFormalProof -> ShowS
$cshowsPrec :: Int -> MWFormalProof -> ShowS
Show)

emptyMWFormalProof :: MWFormalProof
emptyMWFormalProof :: MWFormalProof
emptyMWFormalProof = TstpCnfRefutation :: String -> MWProvingProblem -> MWCalculus -> String -> MWFormalProof
TstpCnfRefutation
  { formalProof :: String
formalProof = ""
  , proofOf :: MWProvingProblem
proofOf = MWProvingProblem
UnknownProvingProblem
  , calculus :: MWCalculus
calculus = MWCalculus
UnknownCalc
  , axioms :: String
axioms = "" }


data MWStatus =
       MWStatus { MWStatus -> Bool
solved :: Bool,
                  MWStatus -> FoAtpStatus
foAtpStatus :: FoAtpStatus
                  } deriving (MWStatus -> MWStatus -> Bool
(MWStatus -> MWStatus -> Bool)
-> (MWStatus -> MWStatus -> Bool) -> Eq MWStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MWStatus -> MWStatus -> Bool
$c/= :: MWStatus -> MWStatus -> Bool
== :: MWStatus -> MWStatus -> Bool
$c== :: MWStatus -> MWStatus -> Bool
Eq, Eq MWStatus
Eq MWStatus =>
(MWStatus -> MWStatus -> Ordering)
-> (MWStatus -> MWStatus -> Bool)
-> (MWStatus -> MWStatus -> Bool)
-> (MWStatus -> MWStatus -> Bool)
-> (MWStatus -> MWStatus -> Bool)
-> (MWStatus -> MWStatus -> MWStatus)
-> (MWStatus -> MWStatus -> MWStatus)
-> Ord MWStatus
MWStatus -> MWStatus -> Bool
MWStatus -> MWStatus -> Ordering
MWStatus -> MWStatus -> MWStatus
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 :: MWStatus -> MWStatus -> MWStatus
$cmin :: MWStatus -> MWStatus -> MWStatus
max :: MWStatus -> MWStatus -> MWStatus
$cmax :: MWStatus -> MWStatus -> MWStatus
>= :: MWStatus -> MWStatus -> Bool
$c>= :: MWStatus -> MWStatus -> Bool
> :: MWStatus -> MWStatus -> Bool
$c> :: MWStatus -> MWStatus -> Bool
<= :: MWStatus -> MWStatus -> Bool
$c<= :: MWStatus -> MWStatus -> Bool
< :: MWStatus -> MWStatus -> Bool
$c< :: MWStatus -> MWStatus -> Bool
compare :: MWStatus -> MWStatus -> Ordering
$ccompare :: MWStatus -> MWStatus -> Ordering
$cp1Ord :: Eq MWStatus
Ord, Int -> MWStatus -> ShowS
[MWStatus] -> ShowS
MWStatus -> String
(Int -> MWStatus -> ShowS)
-> (MWStatus -> String) -> ([MWStatus] -> ShowS) -> Show MWStatus
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MWStatus] -> ShowS
$cshowList :: [MWStatus] -> ShowS
show :: MWStatus -> String
$cshow :: MWStatus -> String
showsPrec :: Int -> MWStatus -> ShowS
$cshowsPrec :: Int -> MWStatus -> ShowS
Show)

data FoAtpStatus =
       Solved SolvedStatus
     | Unsolved UnsolvedStatus
     deriving (FoAtpStatus -> FoAtpStatus -> Bool
(FoAtpStatus -> FoAtpStatus -> Bool)
-> (FoAtpStatus -> FoAtpStatus -> Bool) -> Eq FoAtpStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FoAtpStatus -> FoAtpStatus -> Bool
$c/= :: FoAtpStatus -> FoAtpStatus -> Bool
== :: FoAtpStatus -> FoAtpStatus -> Bool
$c== :: FoAtpStatus -> FoAtpStatus -> Bool
Eq, Eq FoAtpStatus
Eq FoAtpStatus =>
(FoAtpStatus -> FoAtpStatus -> Ordering)
-> (FoAtpStatus -> FoAtpStatus -> Bool)
-> (FoAtpStatus -> FoAtpStatus -> Bool)
-> (FoAtpStatus -> FoAtpStatus -> Bool)
-> (FoAtpStatus -> FoAtpStatus -> Bool)
-> (FoAtpStatus -> FoAtpStatus -> FoAtpStatus)
-> (FoAtpStatus -> FoAtpStatus -> FoAtpStatus)
-> Ord FoAtpStatus
FoAtpStatus -> FoAtpStatus -> Bool
FoAtpStatus -> FoAtpStatus -> Ordering
FoAtpStatus -> FoAtpStatus -> FoAtpStatus
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 :: FoAtpStatus -> FoAtpStatus -> FoAtpStatus
$cmin :: FoAtpStatus -> FoAtpStatus -> FoAtpStatus
max :: FoAtpStatus -> FoAtpStatus -> FoAtpStatus
$cmax :: FoAtpStatus -> FoAtpStatus -> FoAtpStatus
>= :: FoAtpStatus -> FoAtpStatus -> Bool
$c>= :: FoAtpStatus -> FoAtpStatus -> Bool
> :: FoAtpStatus -> FoAtpStatus -> Bool
$c> :: FoAtpStatus -> FoAtpStatus -> Bool
<= :: FoAtpStatus -> FoAtpStatus -> Bool
$c<= :: FoAtpStatus -> FoAtpStatus -> Bool
< :: FoAtpStatus -> FoAtpStatus -> Bool
$c< :: FoAtpStatus -> FoAtpStatus -> Bool
compare :: FoAtpStatus -> FoAtpStatus -> Ordering
$ccompare :: FoAtpStatus -> FoAtpStatus -> Ordering
$cp1Ord :: Eq FoAtpStatus
Ord, Int -> FoAtpStatus -> ShowS
[FoAtpStatus] -> ShowS
FoAtpStatus -> String
(Int -> FoAtpStatus -> ShowS)
-> (FoAtpStatus -> String)
-> ([FoAtpStatus] -> ShowS)
-> Show FoAtpStatus
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FoAtpStatus] -> ShowS
$cshowList :: [FoAtpStatus] -> ShowS
show :: FoAtpStatus -> String
$cshow :: FoAtpStatus -> String
showsPrec :: Int -> FoAtpStatus -> ShowS
$cshowsPrec :: Int -> FoAtpStatus -> ShowS
Show, ReadPrec [FoAtpStatus]
ReadPrec FoAtpStatus
Int -> ReadS FoAtpStatus
ReadS [FoAtpStatus]
(Int -> ReadS FoAtpStatus)
-> ReadS [FoAtpStatus]
-> ReadPrec FoAtpStatus
-> ReadPrec [FoAtpStatus]
-> Read FoAtpStatus
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [FoAtpStatus]
$creadListPrec :: ReadPrec [FoAtpStatus]
readPrec :: ReadPrec FoAtpStatus
$creadPrec :: ReadPrec FoAtpStatus
readList :: ReadS [FoAtpStatus]
$creadList :: ReadS [FoAtpStatus]
readsPrec :: Int -> ReadS FoAtpStatus
$creadsPrec :: Int -> ReadS FoAtpStatus
Read)

data SolvedStatus =
       CounterEquivalent
     | CounterSatisfiable
     | CounterTheorem
     | Equivalent
     | NoConsequence
     | Satisfiable
     | TautologousConclusion
     | Tautology
     | Theorem
     | Unsatisfiable
     | UnsatisfiableConclusion
     deriving (SolvedStatus -> SolvedStatus -> Bool
(SolvedStatus -> SolvedStatus -> Bool)
-> (SolvedStatus -> SolvedStatus -> Bool) -> Eq SolvedStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SolvedStatus -> SolvedStatus -> Bool
$c/= :: SolvedStatus -> SolvedStatus -> Bool
== :: SolvedStatus -> SolvedStatus -> Bool
$c== :: SolvedStatus -> SolvedStatus -> Bool
Eq, Eq SolvedStatus
Eq SolvedStatus =>
(SolvedStatus -> SolvedStatus -> Ordering)
-> (SolvedStatus -> SolvedStatus -> Bool)
-> (SolvedStatus -> SolvedStatus -> Bool)
-> (SolvedStatus -> SolvedStatus -> Bool)
-> (SolvedStatus -> SolvedStatus -> Bool)
-> (SolvedStatus -> SolvedStatus -> SolvedStatus)
-> (SolvedStatus -> SolvedStatus -> SolvedStatus)
-> Ord SolvedStatus
SolvedStatus -> SolvedStatus -> Bool
SolvedStatus -> SolvedStatus -> Ordering
SolvedStatus -> SolvedStatus -> SolvedStatus
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 :: SolvedStatus -> SolvedStatus -> SolvedStatus
$cmin :: SolvedStatus -> SolvedStatus -> SolvedStatus
max :: SolvedStatus -> SolvedStatus -> SolvedStatus
$cmax :: SolvedStatus -> SolvedStatus -> SolvedStatus
>= :: SolvedStatus -> SolvedStatus -> Bool
$c>= :: SolvedStatus -> SolvedStatus -> Bool
> :: SolvedStatus -> SolvedStatus -> Bool
$c> :: SolvedStatus -> SolvedStatus -> Bool
<= :: SolvedStatus -> SolvedStatus -> Bool
$c<= :: SolvedStatus -> SolvedStatus -> Bool
< :: SolvedStatus -> SolvedStatus -> Bool
$c< :: SolvedStatus -> SolvedStatus -> Bool
compare :: SolvedStatus -> SolvedStatus -> Ordering
$ccompare :: SolvedStatus -> SolvedStatus -> Ordering
$cp1Ord :: Eq SolvedStatus
Ord, Int -> SolvedStatus -> ShowS
[SolvedStatus] -> ShowS
SolvedStatus -> String
(Int -> SolvedStatus -> ShowS)
-> (SolvedStatus -> String)
-> ([SolvedStatus] -> ShowS)
-> Show SolvedStatus
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolvedStatus] -> ShowS
$cshowList :: [SolvedStatus] -> ShowS
show :: SolvedStatus -> String
$cshow :: SolvedStatus -> String
showsPrec :: Int -> SolvedStatus -> ShowS
$cshowsPrec :: Int -> SolvedStatus -> ShowS
Show, ReadPrec [SolvedStatus]
ReadPrec SolvedStatus
Int -> ReadS SolvedStatus
ReadS [SolvedStatus]
(Int -> ReadS SolvedStatus)
-> ReadS [SolvedStatus]
-> ReadPrec SolvedStatus
-> ReadPrec [SolvedStatus]
-> Read SolvedStatus
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SolvedStatus]
$creadListPrec :: ReadPrec [SolvedStatus]
readPrec :: ReadPrec SolvedStatus
$creadPrec :: ReadPrec SolvedStatus
readList :: ReadS [SolvedStatus]
$creadList :: ReadS [SolvedStatus]
readsPrec :: Int -> ReadS SolvedStatus
$creadsPrec :: Int -> ReadS SolvedStatus
Read)

data UnsolvedStatus =
       Assumed
     | GaveUp
     | InputError
     | MemoryOut
     | ResourceOut
     | Timeout
     | Unknown
     | NoStatus
     deriving (UnsolvedStatus -> UnsolvedStatus -> Bool
(UnsolvedStatus -> UnsolvedStatus -> Bool)
-> (UnsolvedStatus -> UnsolvedStatus -> Bool) -> Eq UnsolvedStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UnsolvedStatus -> UnsolvedStatus -> Bool
$c/= :: UnsolvedStatus -> UnsolvedStatus -> Bool
== :: UnsolvedStatus -> UnsolvedStatus -> Bool
$c== :: UnsolvedStatus -> UnsolvedStatus -> Bool
Eq, Eq UnsolvedStatus
Eq UnsolvedStatus =>
(UnsolvedStatus -> UnsolvedStatus -> Ordering)
-> (UnsolvedStatus -> UnsolvedStatus -> Bool)
-> (UnsolvedStatus -> UnsolvedStatus -> Bool)
-> (UnsolvedStatus -> UnsolvedStatus -> Bool)
-> (UnsolvedStatus -> UnsolvedStatus -> Bool)
-> (UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus)
-> (UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus)
-> Ord UnsolvedStatus
UnsolvedStatus -> UnsolvedStatus -> Bool
UnsolvedStatus -> UnsolvedStatus -> Ordering
UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus
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 :: UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus
$cmin :: UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus
max :: UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus
$cmax :: UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus
>= :: UnsolvedStatus -> UnsolvedStatus -> Bool
$c>= :: UnsolvedStatus -> UnsolvedStatus -> Bool
> :: UnsolvedStatus -> UnsolvedStatus -> Bool
$c> :: UnsolvedStatus -> UnsolvedStatus -> Bool
<= :: UnsolvedStatus -> UnsolvedStatus -> Bool
$c<= :: UnsolvedStatus -> UnsolvedStatus -> Bool
< :: UnsolvedStatus -> UnsolvedStatus -> Bool
$c< :: UnsolvedStatus -> UnsolvedStatus -> Bool
compare :: UnsolvedStatus -> UnsolvedStatus -> Ordering
$ccompare :: UnsolvedStatus -> UnsolvedStatus -> Ordering
$cp1Ord :: Eq UnsolvedStatus
Ord, Int -> UnsolvedStatus -> ShowS
[UnsolvedStatus] -> ShowS
UnsolvedStatus -> String
(Int -> UnsolvedStatus -> ShowS)
-> (UnsolvedStatus -> String)
-> ([UnsolvedStatus] -> ShowS)
-> Show UnsolvedStatus
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnsolvedStatus] -> ShowS
$cshowList :: [UnsolvedStatus] -> ShowS
show :: UnsolvedStatus -> String
$cshow :: UnsolvedStatus -> String
showsPrec :: Int -> UnsolvedStatus -> ShowS
$cshowsPrec :: Int -> UnsolvedStatus -> ShowS
Show, ReadPrec [UnsolvedStatus]
ReadPrec UnsolvedStatus
Int -> ReadS UnsolvedStatus
ReadS [UnsolvedStatus]
(Int -> ReadS UnsolvedStatus)
-> ReadS [UnsolvedStatus]
-> ReadPrec UnsolvedStatus
-> ReadPrec [UnsolvedStatus]
-> Read UnsolvedStatus
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [UnsolvedStatus]
$creadListPrec :: ReadPrec [UnsolvedStatus]
readPrec :: ReadPrec UnsolvedStatus
$creadPrec :: ReadPrec UnsolvedStatus
readList :: ReadS [UnsolvedStatus]
$creadList :: ReadS [UnsolvedStatus]
readsPrec :: Int -> ReadS UnsolvedStatus
$creadsPrec :: Int -> ReadS UnsolvedStatus
Read)

data MWProvingProblem =
       TstpFOFProblem
     | TstpProblem
     | UnknownProvingProblem
     deriving (MWProvingProblem -> MWProvingProblem -> Bool
(MWProvingProblem -> MWProvingProblem -> Bool)
-> (MWProvingProblem -> MWProvingProblem -> Bool)
-> Eq MWProvingProblem
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MWProvingProblem -> MWProvingProblem -> Bool
$c/= :: MWProvingProblem -> MWProvingProblem -> Bool
== :: MWProvingProblem -> MWProvingProblem -> Bool
$c== :: MWProvingProblem -> MWProvingProblem -> Bool
Eq, Eq MWProvingProblem
Eq MWProvingProblem =>
(MWProvingProblem -> MWProvingProblem -> Ordering)
-> (MWProvingProblem -> MWProvingProblem -> Bool)
-> (MWProvingProblem -> MWProvingProblem -> Bool)
-> (MWProvingProblem -> MWProvingProblem -> Bool)
-> (MWProvingProblem -> MWProvingProblem -> Bool)
-> (MWProvingProblem -> MWProvingProblem -> MWProvingProblem)
-> (MWProvingProblem -> MWProvingProblem -> MWProvingProblem)
-> Ord MWProvingProblem
MWProvingProblem -> MWProvingProblem -> Bool
MWProvingProblem -> MWProvingProblem -> Ordering
MWProvingProblem -> MWProvingProblem -> MWProvingProblem
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 :: MWProvingProblem -> MWProvingProblem -> MWProvingProblem
$cmin :: MWProvingProblem -> MWProvingProblem -> MWProvingProblem
max :: MWProvingProblem -> MWProvingProblem -> MWProvingProblem
$cmax :: MWProvingProblem -> MWProvingProblem -> MWProvingProblem
>= :: MWProvingProblem -> MWProvingProblem -> Bool
$c>= :: MWProvingProblem -> MWProvingProblem -> Bool
> :: MWProvingProblem -> MWProvingProblem -> Bool
$c> :: MWProvingProblem -> MWProvingProblem -> Bool
<= :: MWProvingProblem -> MWProvingProblem -> Bool
$c<= :: MWProvingProblem -> MWProvingProblem -> Bool
< :: MWProvingProblem -> MWProvingProblem -> Bool
$c< :: MWProvingProblem -> MWProvingProblem -> Bool
compare :: MWProvingProblem -> MWProvingProblem -> Ordering
$ccompare :: MWProvingProblem -> MWProvingProblem -> Ordering
$cp1Ord :: Eq MWProvingProblem
Ord, Int -> MWProvingProblem -> ShowS
[MWProvingProblem] -> ShowS
MWProvingProblem -> String
(Int -> MWProvingProblem -> ShowS)
-> (MWProvingProblem -> String)
-> ([MWProvingProblem] -> ShowS)
-> Show MWProvingProblem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MWProvingProblem] -> ShowS
$cshowList :: [MWProvingProblem] -> ShowS
show :: MWProvingProblem -> String
$cshow :: MWProvingProblem -> String
showsPrec :: Int -> MWProvingProblem -> ShowS
$cshowsPrec :: Int -> MWProvingProblem -> ShowS
Show)

data MWCalculus =
       AprosNDCalculus
     | OmegaNDCalculus
     | EpResCalc
     | SpassResCalc
     | StandardRes
     | OtterCalc
     | VampireResCalc
     | ZenonCalc
     | UnknownCalc
     deriving (MWCalculus -> MWCalculus -> Bool
(MWCalculus -> MWCalculus -> Bool)
-> (MWCalculus -> MWCalculus -> Bool) -> Eq MWCalculus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MWCalculus -> MWCalculus -> Bool
$c/= :: MWCalculus -> MWCalculus -> Bool
== :: MWCalculus -> MWCalculus -> Bool
$c== :: MWCalculus -> MWCalculus -> Bool
Eq, Eq MWCalculus
Eq MWCalculus =>
(MWCalculus -> MWCalculus -> Ordering)
-> (MWCalculus -> MWCalculus -> Bool)
-> (MWCalculus -> MWCalculus -> Bool)
-> (MWCalculus -> MWCalculus -> Bool)
-> (MWCalculus -> MWCalculus -> Bool)
-> (MWCalculus -> MWCalculus -> MWCalculus)
-> (MWCalculus -> MWCalculus -> MWCalculus)
-> Ord MWCalculus
MWCalculus -> MWCalculus -> Bool
MWCalculus -> MWCalculus -> Ordering
MWCalculus -> MWCalculus -> MWCalculus
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 :: MWCalculus -> MWCalculus -> MWCalculus
$cmin :: MWCalculus -> MWCalculus -> MWCalculus
max :: MWCalculus -> MWCalculus -> MWCalculus
$cmax :: MWCalculus -> MWCalculus -> MWCalculus
>= :: MWCalculus -> MWCalculus -> Bool
$c>= :: MWCalculus -> MWCalculus -> Bool
> :: MWCalculus -> MWCalculus -> Bool
$c> :: MWCalculus -> MWCalculus -> Bool
<= :: MWCalculus -> MWCalculus -> Bool
$c<= :: MWCalculus -> MWCalculus -> Bool
< :: MWCalculus -> MWCalculus -> Bool
$c< :: MWCalculus -> MWCalculus -> Bool
compare :: MWCalculus -> MWCalculus -> Ordering
$ccompare :: MWCalculus -> MWCalculus -> Ordering
$cp1Ord :: Eq MWCalculus
Ord, Int -> MWCalculus -> ShowS
[MWCalculus] -> ShowS
MWCalculus -> String
(Int -> MWCalculus -> ShowS)
-> (MWCalculus -> String)
-> ([MWCalculus] -> ShowS)
-> Show MWCalculus
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MWCalculus] -> ShowS
$cshowList :: [MWCalculus] -> ShowS
show :: MWCalculus -> String
$cshow :: MWCalculus -> String
showsPrec :: Int -> MWCalculus -> ShowS
$cshowsPrec :: Int -> MWCalculus -> ShowS
Show, ReadPrec [MWCalculus]
ReadPrec MWCalculus
Int -> ReadS MWCalculus
ReadS [MWCalculus]
(Int -> ReadS MWCalculus)
-> ReadS [MWCalculus]
-> ReadPrec MWCalculus
-> ReadPrec [MWCalculus]
-> Read MWCalculus
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [MWCalculus]
$creadListPrec :: ReadPrec [MWCalculus]
readPrec :: ReadPrec MWCalculus
$creadPrec :: ReadPrec MWCalculus
readList :: ReadS [MWCalculus]
$creadList :: ReadS [MWCalculus]
readsPrec :: Int -> ReadS MWCalculus
$creadsPrec :: Int -> ReadS MWCalculus
Read)

data MWTimeResource =
       MWTimeResource { MWTimeResource -> TimeOfDay
cpuTime :: TimeOfDay,
                        MWTimeResource -> TimeOfDay
wallClockTime :: TimeOfDay
                        } deriving (MWTimeResource -> MWTimeResource -> Bool
(MWTimeResource -> MWTimeResource -> Bool)
-> (MWTimeResource -> MWTimeResource -> Bool) -> Eq MWTimeResource
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MWTimeResource -> MWTimeResource -> Bool
$c/= :: MWTimeResource -> MWTimeResource -> Bool
== :: MWTimeResource -> MWTimeResource -> Bool
$c== :: MWTimeResource -> MWTimeResource -> Bool
Eq, Eq MWTimeResource
Eq MWTimeResource =>
(MWTimeResource -> MWTimeResource -> Ordering)
-> (MWTimeResource -> MWTimeResource -> Bool)
-> (MWTimeResource -> MWTimeResource -> Bool)
-> (MWTimeResource -> MWTimeResource -> Bool)
-> (MWTimeResource -> MWTimeResource -> Bool)
-> (MWTimeResource -> MWTimeResource -> MWTimeResource)
-> (MWTimeResource -> MWTimeResource -> MWTimeResource)
-> Ord MWTimeResource
MWTimeResource -> MWTimeResource -> Bool
MWTimeResource -> MWTimeResource -> Ordering
MWTimeResource -> MWTimeResource -> MWTimeResource
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 :: MWTimeResource -> MWTimeResource -> MWTimeResource
$cmin :: MWTimeResource -> MWTimeResource -> MWTimeResource
max :: MWTimeResource -> MWTimeResource -> MWTimeResource
$cmax :: MWTimeResource -> MWTimeResource -> MWTimeResource
>= :: MWTimeResource -> MWTimeResource -> Bool
$c>= :: MWTimeResource -> MWTimeResource -> Bool
> :: MWTimeResource -> MWTimeResource -> Bool
$c> :: MWTimeResource -> MWTimeResource -> Bool
<= :: MWTimeResource -> MWTimeResource -> Bool
$c<= :: MWTimeResource -> MWTimeResource -> Bool
< :: MWTimeResource -> MWTimeResource -> Bool
$c< :: MWTimeResource -> MWTimeResource -> Bool
compare :: MWTimeResource -> MWTimeResource -> Ordering
$ccompare :: MWTimeResource -> MWTimeResource -> Ordering
$cp1Ord :: Eq MWTimeResource
Ord, Int -> MWTimeResource -> ShowS
[MWTimeResource] -> ShowS
MWTimeResource -> String
(Int -> MWTimeResource -> ShowS)
-> (MWTimeResource -> String)
-> ([MWTimeResource] -> ShowS)
-> Show MWTimeResource
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MWTimeResource] -> ShowS
$cshowList :: [MWTimeResource] -> ShowS
show :: MWTimeResource -> String
$cshow :: MWTimeResource -> String
showsPrec :: Int -> MWTimeResource -> ShowS
$cshowsPrec :: Int -> MWTimeResource -> ShowS
Show)

toCData :: String -> CData
toCData :: String -> CData
toCData s :: String
s = CData
blank_cdata { cdData :: String
cdData = String
s }

mkProveProblemElem :: MathServCall -- ^ needed data to do a MathServ call
                   -> Element -- ^ resulting XML element
mkProveProblemElem :: MathServCall -> Element
mkProveProblemElem call :: MathServCall
call = let extOpt :: Maybe String
extOpt = MathServCall -> Maybe String
extraOptions MathServCall
call in
     String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode ("Prove" String -> ShowS
forall a. [a] -> [a] -> [a]
++ MathServOperationTypes -> String
forall a. Show a => a -> String
show (MathServCall -> MathServOperationTypes
mathServOperation MathServCall
call)
           String -> ShowS
forall a. [a] -> [a] -> [a]
++ if Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
extOpt then "WithOptions" else "")
       ([ String -> CData -> Element
forall t. Node t => String -> t -> Element
unode "in0" (CData -> Element) -> (String -> CData) -> String -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> CData
toCData (String -> CData) -> ShowS -> String -> CData
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
filter Char -> Bool
isAscii (String -> Element) -> String -> Element
forall a b. (a -> b) -> a -> b
$ MathServCall -> String
problem MathServCall
call
        , String -> CData -> Element
forall t. Node t => String -> t -> Element
unode "in1" (CData -> Element) -> (Int -> CData) -> Int -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> CData
toCData (String -> CData) -> (Int -> String) -> Int -> CData
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> Element) -> Int -> Element
forall a b. (a -> b) -> a -> b
$ MathServCall -> Int
proverTimeLimit MathServCall
call]
        [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ case Maybe String
extOpt of
             Nothing -> []
             Just o2 :: String
o2 -> [String -> CData -> Element
forall t. Node t => String -> t -> Element
unode "in2" (CData -> Element) -> CData -> Element
forall a b. (a -> b) -> a -> b
$ String -> CData
toCData String
o2])

-- ** functions for handling with soap

soapenvS :: String
soapenvS :: String
soapenvS = "soapenv"

bodyS :: String
bodyS :: String
bodyS = "Body"

soapEnvQName :: String -> QName
soapEnvQName :: String -> QName
soapEnvQName s :: String
s = (String -> QName
unqual String
s) { qPrefix :: Maybe String
qPrefix = String -> Maybe String
forall a. a -> Maybe a
Just String
soapenvS }

xmlnsQName :: String -> QName
xmlnsQName :: String -> QName
xmlnsQName s :: String
s = (String -> QName
unqual String
s) { qPrefix :: Maybe String
qPrefix = String -> Maybe String
forall a. a -> Maybe a
Just "xmlns" }

envUri :: String
envUri :: String
envUri = "http://schemas.xmlsoap.org/soap/envelope/"

bodyQ :: QName
bodyQ :: QName
bodyQ = (String -> QName
soapEnvQName String
bodyS) { qURI :: Maybe String
qURI = String -> Maybe String
forall a. a -> Maybe a
Just String
envUri }

mkEnvelope :: Element -> Element
mkEnvelope :: Element -> Element
mkEnvelope = [Attr] -> Element -> Element
add_attrs
  [ QName -> String -> Attr
Attr (String -> QName
unqual "encodingStyle") "http://schemas.xmlsoap.org/soap/encoding/"
  , QName -> String -> Attr
Attr (String -> QName
xmlnsQName "xsd") "http://www.w3.org/2001/XMLSchema"
  , QName -> String -> Attr
Attr (String -> QName
xmlnsQName String
soapenvS) String
envUri
  ] (Element -> Element) -> (Element -> Element) -> Element -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Element -> Element
forall t. Node t => QName -> t -> Element
node (String -> QName
soapEnvQName "Envelope")

mkSoapRequest :: MathServCall -> ServerAddr -> Request_String
mkSoapRequest :: MathServCall -> ServerAddr -> Request_String
mkSoapRequest call :: MathServCall
call serverPort :: ServerAddr
serverPort =
  let b :: String
b = Element -> String
showElement (Element -> String) -> Element -> String
forall a b. (a -> b) -> a -> b
$ Element -> Element
mkEnvelope (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ QName -> Element -> Element
forall t. Node t => QName -> t -> Element
node QName
bodyQ (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ MathServCall -> Element
mkProveProblemElem MathServCall
call
      r0 :: Request_String
r0 = String -> Request_String
postRequest (String -> Request_String) -> String -> Request_String
forall a b. (a -> b) -> a -> b
$ "http://" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ServerAddr -> String
forall a. Show a => a -> String
show ServerAddr
serverPort String -> ShowS
forall a. [a] -> [a] -> [a]
++ "/axis/services/"
           String -> ShowS
forall a. [a] -> [a] -> [a]
++ MathServServices -> String
forall a. Show a => a -> String
show (MathServCall -> MathServServices
mathServService MathServCall
call)
      r1 :: Request_String
r1 = HeaderSetter Request_String
forall a. HasHeaders a => HeaderSetter a
insertHeader (String -> HeaderName
HdrCustom "SOAPAction") "" Request_String
r0 { rqBody :: String
rqBody = String
b }
      r2 :: Request_String
r2 = HeaderSetter Request_String
forall a. HasHeaders a => HeaderSetter a
replaceHeader HeaderName
HdrUserAgent "hets" Request_String
r1
      r3 :: Request_String
r3 = HeaderSetter Request_String
forall a. HasHeaders a => HeaderSetter a
replaceHeader HeaderName
HdrContentLength (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
b) Request_String
r2
  in HeaderSetter Request_String
forall a. HasHeaders a => HeaderSetter a
insertHeader HeaderName
HdrContentType "text/xml" Request_String
r3

testQnameSuffix :: String -> QName -> Bool
testQnameSuffix :: String -> QName -> Bool
testQnameSuffix s :: String
s q :: QName
q = let l :: String
l = QName -> String
qName QName
q in
  Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing (QName -> Maybe String
qPrefix QName
q) Bool -> Bool -> Bool
&& String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "Prove" String
l Bool -> Bool -> Bool
&& String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf String
s String
l

unpackSoapEnvelope :: Either String String -> Either String String
unpackSoapEnvelope :: Either String String -> Either String String
unpackSoapEnvelope rsp :: Either String String
rsp = case Either String String
rsp of
  Left s :: String
s -> String -> Either String String
forall a b. a -> Either a b
Left String
s
  Right r :: String
r -> case String -> Maybe Element
forall s. XmlSource s => s -> Maybe Element
parseXMLDoc String
r of
    Nothing -> String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ "server returned illegal xml\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
r
    Just x :: Element
x -> case (QName -> Bool) -> Element -> Maybe Element
filterElementName (QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
bodyQ) Element
x of
     Nothing -> String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ "no soap Body found\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Element -> String
ppElement Element
x
     Just b :: Element
b -> case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
testQnameSuffix "Response") Element
b of
      Nothing -> String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ "no Prove Response found\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Element -> String
ppElement Element
b
      Just t :: Element
t -> case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
testQnameSuffix "Return") Element
t of
       Nothing -> String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ "no Prove Return value found\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Element -> String
ppElement Element
t
       Just v :: Element
v -> case Element -> String
strContent Element
v of
        "" -> String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ "no returned content found\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Element -> String
ppElement Element
v
        ts :: String
ts -> String -> Either String String
forall a b. b -> Either a b
Right String
ts

-- ** functions for handling with MathServ services

{- |
  Sends a problem in TPTP format to MathServ using a given time limit.
  Either MathServ output is returned or a simple error message (no XML).
-}
callMathServ :: MathServCall -- ^ needed data to do a MathServ call
             -> IO (Either String String )
             -- ^ Left (SOAP error) or Right (MathServ output or error message)
callMathServ :: MathServCall -> IO (Either String String)
callMathServ call :: MathServCall
call =
    do
       ServerAddr
serverPort <- ServerAddr
-> String -> (String -> Maybe ServerAddr) -> IO ServerAddr
forall a. a -> String -> (String -> Maybe a) -> IO a
getEnvSave ServerAddr
defaultServer "HETS_MATHSERVE" String -> Maybe ServerAddr
forall a. Read a => String -> Maybe a
readMaybe
       let r :: Request_String
r = MathServCall -> ServerAddr -> Request_String
mkSoapRequest MathServCall
call ServerAddr
serverPort
       Result (Response String)
res <- Request_String -> IO (Result (Response String))
forall ty. HStream ty => Request ty -> IO (Result (Response ty))
S.simpleHTTP Request_String
r
       Either String String -> IO (Either String String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String String -> IO (Either String String))
-> Either String String -> IO (Either String String)
forall a b. (a -> b) -> a -> b
$ case Result (Response String)
res of
                  Left mErr :: ConnError
mErr -> String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ ConnError -> String
forall a. Show a => a -> String
show ConnError
mErr
                  Right resp :: Response String
resp -> Either String String -> Either String String
unpackSoapEnvelope (Either String String -> Either String String)
-> Either String String -> Either String String
forall a b. (a -> b) -> a -> b
$ String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ Response String -> String
forall a. Response a -> a
rspBody Response String
resp

isMWnode :: String -> QName -> Bool
isMWnode :: String -> QName -> Bool
isMWnode s :: String
s q :: QName
q = QName -> String
qName QName
q String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s Bool -> Bool -> Bool
&& QName -> Maybe String
qPrefix QName
q Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Maybe String
forall a. a -> Maybe a
Just "mw"

getElemText :: String -> Element -> String
getElemText :: String -> Element -> String
getElemText s :: String
s = String -> (Element -> String) -> Maybe Element -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" Element -> String
strContent (Maybe Element -> String)
-> (Element -> Maybe Element) -> Element -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
isMWnode String
s)

{- |
  Full parsing of RDF-objects returned by MathServ and putting the results
  into a MathServResponse data-structure.
-}
parseMathServOut :: Either String String
       -- ^ Left (SOAP error) or Right (MathServ output or error message)
                 -> IO (Either String MathServResponse)
       -- ^ parsed rdf-objects in record
parseMathServOut :: Either String String -> IO (Either String MathServResponse)
parseMathServOut = Either String MathServResponse
-> IO (Either String MathServResponse)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String MathServResponse
 -> IO (Either String MathServResponse))
-> (Either String String -> Either String MathServResponse)
-> Either String String
-> IO (Either String MathServResponse)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either String String -> Either String MathServResponse
parseResponse

parseResponse :: Either String String -> Either String MathServResponse
parseResponse :: Either String String -> Either String MathServResponse
parseResponse eMathServOut :: Either String String
eMathServOut = do
   String
mathServOut <- Either String String
eMathServOut
   case String -> Maybe Element
forall s. XmlSource s => s -> Maybe Element
parseXMLDoc String
mathServOut of
     Nothing -> String -> Either String MathServResponse
forall a b. a -> Either a b
Left "illegal rdf xml tree"
     Just rdf :: Element
rdf -> do
        let mr :: Either String MWFoAtpResult
mr = case Element -> Maybe String
parseFailure Element
rdf of
              Just str :: String
str -> String -> Either String MWFoAtpResult
forall a b. a -> Either a b
Left String
str
              Nothing -> Element -> Either String MWFoAtpResult
parseResult Element
rdf
        MWTimeResource
t <- Element -> Either String MWTimeResource
parseTimeResource Element
rdf
        MathServResponse -> Either String MathServResponse
forall (m :: * -> *) a. Monad m => a -> m a
return MathServResponse :: Either String MWFoAtpResult -> MWTimeResource -> MathServResponse
MathServResponse
          { foAtpResult :: Either String MWFoAtpResult
foAtpResult = Either String MWFoAtpResult
mr
          , timeResource :: MWTimeResource
timeResource = MWTimeResource
t }

parseFailure :: Element -> Maybe String
parseFailure :: Element -> Maybe String
parseFailure e :: Element
e = case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
isMWnode "Failure") Element
e of
  Nothing -> Maybe String
forall a. Maybe a
Nothing
  Just f :: Element
f -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String -> Element -> String
getElemText "message" Element
f

parseResult :: Element -> Either String MWFoAtpResult
parseResult :: Element -> Either String MWFoAtpResult
parseResult rdf :: Element
rdf = case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
isMWnode "FoAtpResult") Element
rdf of
       Nothing -> String -> Either String MWFoAtpResult
forall a b. a -> Either a b
Left "no FoAtpResult found"
       Just e :: Element
e -> do
         MWStatus
stat <- Element -> Either String MWStatus
parseStatus Element
e
         MWTimeResource
tm <- case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
isMWnode "time") Element
e of
           Nothing -> String -> Either String MWTimeResource
forall a b. a -> Either a b
Left "no time element found"
           Just t :: Element
t -> Element -> Either String MWTimeResource
parseTimeResource Element
t
         let pr :: MWFormalProof
pr = Element -> MWFormalProof
parseProof Element
e
             out :: String
out = String -> Element -> String
getElemText "output" Element
e
             sys :: String
sys = String -> Element -> String
getElemText "system" Element
e
         MWFoAtpResult -> Either String MWFoAtpResult
forall (m :: * -> *) a. Monad m => a -> m a
return MWFoAtpResult :: MWFormalProof
-> String -> MWStatus -> String -> MWTimeResource -> MWFoAtpResult
MWFoAtpResult
           { proof :: MWFormalProof
proof = MWFormalProof
pr
           , outputStr :: String
outputStr = String
out
           , systemStatus :: MWStatus
systemStatus = MWStatus
stat
           , systemStr :: String
systemStr = String
sys
           , time :: MWTimeResource
time = MWTimeResource
tm }

parseProof :: Element -> MWFormalProof
parseProof :: Element -> MWFormalProof
parseProof e :: Element
e = case (QName -> Bool) -> Element -> Maybe Element
filterElementName
  (\ q :: QName
q -> String -> QName -> Bool
isMWnode "proof" QName
q Bool -> Bool -> Bool
|| String -> QName -> Bool
isMWnode "saturation" QName
q) Element
e of
  Nothing -> MWFormalProof
emptyMWFormalProof
  Just pr :: Element
pr -> case (QName -> Bool) -> Element -> Maybe Element
filterElementName (\ q :: QName
q -> String -> QName -> Bool
isMWnode "TstpCnfRefutation" QName
q
    Bool -> Bool -> Bool
|| String -> QName -> Bool
isMWnode "TstpCnfSaturation" QName
q) Element
pr of
    Nothing -> MWFormalProof
emptyMWFormalProof
    Just p :: Element
p -> let
        fp0 :: String
fp0 = String -> Element -> String
getElemText "formalProof" Element
p
        fp :: String
fp = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
fp0 then String -> Element -> String
getElemText "formalSaturation" Element
p else String
fp0
        prob :: MWProvingProblem
prob = case Element -> String -> MWProvingProblem
getProblem Element
p "proofOf" of
          UnknownProvingProblem -> Element -> String -> MWProvingProblem
getProblem Element
p "saturationOf"
          pa :: MWProvingProblem
pa -> MWProvingProblem
pa
        cal :: MWCalculus
cal = case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
isMWnode "calculus") Element
p of
                Nothing -> MWCalculus
UnknownCalc
                Just c :: Element
c -> Element -> MWCalculus
getCalcAttr Element
c
        axs :: String
axs = String -> Element -> String
getElemText "axioms" Element
p
       in TstpCnfRefutation :: String -> MWProvingProblem -> MWCalculus -> String -> MWFormalProof
TstpCnfRefutation
       { formalProof :: String
formalProof = String
fp
       , proofOf :: MWProvingProblem
proofOf = MWProvingProblem
prob
       , calculus :: MWCalculus
calculus = MWCalculus
cal
       , axioms :: String
axioms = String
axs }

isRdfResource :: QName -> Bool
isRdfResource :: QName -> Bool
isRdfResource q :: QName
q = QName -> String
qName QName
q String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "resource" Bool -> Bool -> Bool
&& QName -> Maybe String
qPrefix QName
q Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Maybe String
forall a. a -> Maybe a
Just "rdf"

{- |
  Removes first part of string until @#@ (including @#@).
-}
getAnchor :: String -- ^ in-string
          -> String -- ^ part of string after first occurence of @#@
getAnchor :: ShowS
getAnchor s :: String
s = case (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '#') String
s of
    [] -> []
    _ : r :: String
r -> String
r

getRdfResource :: Element -> String
getRdfResource :: Element -> String
getRdfResource e :: Element
e = case (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([String] -> [String])
-> ([Attr] -> [String]) -> [Attr] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Attr -> String) -> [Attr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
getAnchor ShowS -> (Attr -> String) -> Attr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attr -> String
attrVal)
  ([Attr] -> [String]) -> ([Attr] -> [Attr]) -> [Attr] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Attr -> Bool) -> [Attr] -> [Attr]
forall a. (a -> Bool) -> [a] -> [a]
filter (QName -> Bool
isRdfResource (QName -> Bool) -> (Attr -> QName) -> Attr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attr -> QName
attrKey) ([Attr] -> [String]) -> [Attr] -> [String]
forall a b. (a -> b) -> a -> b
$ Element -> [Attr]
elAttribs Element
e of
  str :: String
str : _ -> String
str
  _ -> ""

getProblem :: Element -> String -> MWProvingProblem
getProblem :: Element -> String -> MWProvingProblem
getProblem e :: Element
e s :: String
s = case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
isMWnode String
s) Element
e of
  Nothing -> MWProvingProblem
UnknownProvingProblem
  Just po :: Element
po -> Element -> MWProvingProblem
getProblemAttr Element
po

getProblemAttr :: Element -> MWProvingProblem
getProblemAttr :: Element -> MWProvingProblem
getProblemAttr e :: Element
e = let str :: String
str = Element -> String
getRdfResource Element
e in
  if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "generated_tstp_fof_problem" String
str then MWProvingProblem
TstpFOFProblem
  else if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "TstpProblem" String
str then MWProvingProblem
TstpProblem
  else MWProvingProblem
UnknownProvingProblem

parseStatus :: Element -> Either String MWStatus
parseStatus :: Element -> Either String MWStatus
parseStatus e :: Element
e = case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
isMWnode "status") Element
e of
  Nothing -> String -> Either String MWStatus
forall a b. a -> Either a b
Left "no status found"
  Just s :: Element
s -> let str :: String
str = Element -> String
getRdfResource Element
s in case String -> Maybe SolvedStatus
forall a. Read a => String -> Maybe a
readMaybe String
str of
       Just sol :: SolvedStatus
sol -> MWStatus -> Either String MWStatus
forall a b. b -> Either a b
Right (MWStatus -> Either String MWStatus)
-> MWStatus -> Either String MWStatus
forall a b. (a -> b) -> a -> b
$ Bool -> FoAtpStatus -> MWStatus
MWStatus Bool
True (FoAtpStatus -> MWStatus) -> FoAtpStatus -> MWStatus
forall a b. (a -> b) -> a -> b
$ SolvedStatus -> FoAtpStatus
Solved SolvedStatus
sol
       Nothing -> case String -> Maybe UnsolvedStatus
forall a. Read a => String -> Maybe a
readMaybe String
str of
         Just usol :: UnsolvedStatus
usol -> MWStatus -> Either String MWStatus
forall a b. b -> Either a b
Right (MWStatus -> Either String MWStatus)
-> MWStatus -> Either String MWStatus
forall a b. (a -> b) -> a -> b
$ Bool -> FoAtpStatus -> MWStatus
MWStatus Bool
False (FoAtpStatus -> MWStatus) -> FoAtpStatus -> MWStatus
forall a b. (a -> b) -> a -> b
$ UnsolvedStatus -> FoAtpStatus
Unsolved UnsolvedStatus
usol
         Nothing -> String -> Either String MWStatus
forall a b. a -> Either a b
Left (String -> Either String MWStatus)
-> String -> Either String MWStatus
forall a b. (a -> b) -> a -> b
$ "Could not classify status of proof: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str

elem2Time :: Element -> Either String TimeOfDay
elem2Time :: Element -> Either String TimeOfDay
elem2Time e :: Element
e = let s :: String
s = Element -> String
strContent Element
e in
  case String -> Maybe Double
forall a. Read a => String -> Maybe a
readMaybe String
s of
    Just x :: Double
x -> TimeOfDay -> Either String TimeOfDay
forall a b. b -> Either a b
Right (TimeOfDay -> Either String TimeOfDay)
-> TimeOfDay -> Either String TimeOfDay
forall a b. (a -> b) -> a -> b
$ DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Double -> DiffTime
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Double -> DiffTime) -> Double -> DiffTime
forall a b. (a -> b) -> a -> b
$ (Double
x :: Double) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ 1000
    Nothing -> String -> Either String TimeOfDay
forall a b. a -> Either a b
Left (String -> Either String TimeOfDay)
-> String -> Either String TimeOfDay
forall a b. (a -> b) -> a -> b
$ "cannot read time string: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s

parseTimeResource :: Element -> Either String MWTimeResource
parseTimeResource :: Element -> Either String MWTimeResource
parseTimeResource e :: Element
e = case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
isMWnode "TimeResource") Element
e of
  Nothing -> String -> Either String MWTimeResource
forall a b. a -> Either a b
Left "no time resource found"
  Just tr :: Element
tr -> do
    TimeOfDay
ct <- case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
isMWnode "cpuTime") Element
tr of
            Nothing -> String -> Either String TimeOfDay
forall a b. a -> Either a b
Left "no cpu time found"
            Just t :: Element
t -> Element -> Either String TimeOfDay
elem2Time Element
t
    TimeOfDay
wt <- case (QName -> Bool) -> Element -> Maybe Element
filterElementName (String -> QName -> Bool
isMWnode "wallClockTime") Element
tr of
            Nothing -> String -> Either String TimeOfDay
forall a b. a -> Either a b
Left "no wall clock time found"
            Just t :: Element
t -> Element -> Either String TimeOfDay
elem2Time Element
t
    MWTimeResource -> Either String MWTimeResource
forall (m :: * -> *) a. Monad m => a -> m a
return MWTimeResource :: TimeOfDay -> TimeOfDay -> MWTimeResource
MWTimeResource
      { cpuTime :: TimeOfDay
cpuTime = TimeOfDay
ct
      , wallClockTime :: TimeOfDay
wallClockTime = TimeOfDay
wt }

{- |
  Filters @_@ out of a String and upcases each letter after a @_@.
-}
filterUnderline :: Bool  -- ^ upcase next letter
                -> String -- ^ input String
                -> String -- ^ un-dashed output String
filterUnderline :: Bool -> ShowS
filterUnderline b :: Bool
b st :: String
st = case String
st of
    [] -> []
    h :: Char
h : r :: String
r -> case Char
h of
             '_' -> Bool -> ShowS
filterUnderline Bool
True String
r
             _ -> (if Bool
b then Char -> Char
toUpper Char
h else Char
h) Char -> ShowS
forall a. a -> [a] -> [a]
: Bool -> ShowS
filterUnderline Bool
False String
r

getCalcAttr :: Element -> MWCalculus
getCalcAttr :: Element -> MWCalculus
getCalcAttr =
  MWCalculus -> Maybe MWCalculus -> MWCalculus
forall a. a -> Maybe a -> a
fromMaybe MWCalculus
UnknownCalc (Maybe MWCalculus -> MWCalculus)
-> (Element -> Maybe MWCalculus) -> Element -> MWCalculus
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe MWCalculus
forall a. Read a => String -> Maybe a
readMaybe (String -> Maybe MWCalculus)
-> (Element -> String) -> Element -> Maybe MWCalculus
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ShowS
filterUnderline Bool
True ShowS -> (Element -> String) -> Element -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Element -> String
getRdfResource