{-# LANGUAGE CPP, TypeFamilies, DeriveDataTypeable #-}

module PGIP.Output.Proof
  ( ProofFormatterOptions
  , proofFormatterOptions
  , pfoIncludeProof
  , pfoIncludeDetails

  , ProofResult
  , formatProofs
  ) where

import PGIP.Output.Formatting
import PGIP.Output.Mime ()
import PGIP.Output.Provers (Prover, prepareFormatProver)
import PGIP.Shared

import Interfaces.GenericATPState (tsTimeLimit, tsExtraOpts)
import Logic.Comorphism ()

import qualified Logic.Prover as LP

import Proofs.AbstractState (G_proof_tree)

import Common.Json (asJson)
import Common.JSONOrXML
import Common.ToXml (asXml)
import Common.Utils (readMaybe)

import Data.Data
import Data.Time.LocalTime

import Numeric

import Text.XML.Light ()
import Text.Printf (printf)

type ProofFormatter =
    ProofFormatterOptions -> [(String, [ProofResult])] -> JSONOrXML
                          -- [(dgNodeName, result)]  -> (responseType, response)

data ProofFormatterOptions = ProofFormatterOptions
  { ProofFormatterOptions -> Bool
pfoIncludeProof :: Bool
  , ProofFormatterOptions -> Bool
pfoIncludeDetails :: Bool
  } deriving (Int -> ProofFormatterOptions -> ShowS
[ProofFormatterOptions] -> ShowS
ProofFormatterOptions -> String
(Int -> ProofFormatterOptions -> ShowS)
-> (ProofFormatterOptions -> String)
-> ([ProofFormatterOptions] -> ShowS)
-> Show ProofFormatterOptions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProofFormatterOptions] -> ShowS
$cshowList :: [ProofFormatterOptions] -> ShowS
show :: ProofFormatterOptions -> String
$cshow :: ProofFormatterOptions -> String
showsPrec :: Int -> ProofFormatterOptions -> ShowS
$cshowsPrec :: Int -> ProofFormatterOptions -> ShowS
Show, ProofFormatterOptions -> ProofFormatterOptions -> Bool
(ProofFormatterOptions -> ProofFormatterOptions -> Bool)
-> (ProofFormatterOptions -> ProofFormatterOptions -> Bool)
-> Eq ProofFormatterOptions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProofFormatterOptions -> ProofFormatterOptions -> Bool
$c/= :: ProofFormatterOptions -> ProofFormatterOptions -> Bool
== :: ProofFormatterOptions -> ProofFormatterOptions -> Bool
$c== :: ProofFormatterOptions -> ProofFormatterOptions -> Bool
Eq)

proofFormatterOptions :: ProofFormatterOptions
proofFormatterOptions :: ProofFormatterOptions
proofFormatterOptions = ProofFormatterOptions :: Bool -> Bool -> ProofFormatterOptions
ProofFormatterOptions
  { pfoIncludeProof :: Bool
pfoIncludeProof = Bool
True
  , pfoIncludeDetails :: Bool
pfoIncludeDetails = Bool
True
  }

formatProofs :: Maybe String -> ProofFormatter
formatProofs :: Maybe String -> ProofFormatter
formatProofs format :: Maybe String
format options :: ProofFormatterOptions
options proofs :: [(String, [ProofResult])]
proofs = case Maybe String
format of
  Just "json" -> JSONOrXML
formatAsJSON
  _ -> JSONOrXML
formatAsXML
  where
  proof :: [Proof]
  proof :: [Proof]
proof = ((String, [ProofResult]) -> Proof)
-> [(String, [ProofResult])] -> [Proof]
forall a b. (a -> b) -> [a] -> [b]
map (String, [ProofResult]) -> Proof
convertProof [(String, [ProofResult])]
proofs

  formatAsJSON :: JSONOrXML
  formatAsJSON :: JSONOrXML
formatAsJSON = Json -> JSONOrXML
JSON (Json -> JSONOrXML) -> Json -> JSONOrXML
forall a b. (a -> b) -> a -> b
$ [Proof] -> Json
forall a. ToJson a => a -> Json
asJson [Proof]
proof

  formatAsXML :: JSONOrXML
  formatAsXML :: JSONOrXML
formatAsXML = Element -> JSONOrXML
XML (Element -> JSONOrXML) -> Element -> JSONOrXML
forall a b. (a -> b) -> a -> b
$ [Proof] -> Element
forall a. ToXml a => a -> Element
asXml [Proof]
proof

  convertProof :: (String, [ProofResult]) -> Proof
  convertProof :: (String, [ProofResult]) -> Proof
convertProof (nodeName :: String
nodeName, proofResults :: [ProofResult]
proofResults) = Proof :: String -> [ProofGoal] -> Proof
Proof
    { node :: String
node = String
nodeName
    , goals :: [ProofGoal]
goals = (ProofResult -> ProofGoal) -> [ProofResult] -> [ProofGoal]
forall a b. (a -> b) -> [a] -> [b]
map ProofResult -> ProofGoal
convertGoal [ProofResult]
proofResults
    }

  convertGoal :: ProofResult -> ProofGoal
  convertGoal :: ProofResult -> ProofGoal
convertGoal (goalName :: String
goalName, goalResult :: String
goalResult, goalDetails :: String
goalDetails, proverOrConsChecker :: ProverOrConsChecker
proverOrConsChecker,
               translation :: AnyComorphism
translation, proofStatusM :: Maybe (ProofStatus G_proof_tree)
proofStatusM, _) =
    ProofGoal :: String
-> String
-> Maybe String
-> Prover
-> String
-> Maybe TacticScript
-> Maybe String
-> Maybe ProofTime
-> Maybe [String]
-> Maybe String
-> ProofGoal
ProofGoal
      { name :: String
name = String
goalName
      , result :: String
result = String
goalResult
      , details :: Maybe String
details =
          if ProofFormatterOptions -> Bool
pfoIncludeDetails ProofFormatterOptions
options
          then String -> Maybe String
forall a. a -> Maybe a
Just String
goalDetails
          else Maybe String
forall a. Maybe a
Nothing
      , usedProver :: Prover
usedProver = ProverOrConsChecker -> Prover
prepareFormatProver ProverOrConsChecker
proverOrConsChecker
      , usedTranslation :: String
usedTranslation = AnyComorphism -> String
showComorph AnyComorphism
translation
      , tacticScript :: Maybe TacticScript
tacticScript = Maybe (ProofStatus G_proof_tree) -> Maybe TacticScript
convertTacticScript Maybe (ProofStatus G_proof_tree)
proofStatusM
      , proofTree :: Maybe String
proofTree = (ProofStatus G_proof_tree -> String)
-> Maybe (ProofStatus G_proof_tree) -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (G_proof_tree -> String
forall a. Show a => a -> String
show (G_proof_tree -> String)
-> (ProofStatus G_proof_tree -> G_proof_tree)
-> ProofStatus G_proof_tree
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofStatus G_proof_tree -> G_proof_tree
forall proof_tree. ProofStatus proof_tree -> proof_tree
LP.proofTree) Maybe (ProofStatus G_proof_tree)
proofStatusM
      , usedTime :: Maybe ProofTime
usedTime = (ProofStatus G_proof_tree -> ProofTime)
-> Maybe (ProofStatus G_proof_tree) -> Maybe ProofTime
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TimeOfDay -> ProofTime
convertTime (TimeOfDay -> ProofTime)
-> (ProofStatus G_proof_tree -> TimeOfDay)
-> ProofStatus G_proof_tree
-> ProofTime
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofStatus G_proof_tree -> TimeOfDay
forall proof_tree. ProofStatus proof_tree -> TimeOfDay
LP.usedTime) Maybe (ProofStatus G_proof_tree)
proofStatusM
      , usedAxioms :: Maybe [String]
usedAxioms = (ProofStatus G_proof_tree -> [String])
-> Maybe (ProofStatus G_proof_tree) -> Maybe [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProofStatus G_proof_tree -> [String]
forall proof_tree. ProofStatus proof_tree -> [String]
LP.usedAxioms Maybe (ProofStatus G_proof_tree)
proofStatusM
      , proverOutput :: Maybe String
proverOutput =
          if ProofFormatterOptions -> Bool
pfoIncludeProof ProofFormatterOptions
options
          then (ProofStatus G_proof_tree -> String)
-> Maybe (ProofStatus G_proof_tree) -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([String] -> String
unlines ([String] -> String)
-> (ProofStatus G_proof_tree -> [String])
-> ProofStatus G_proof_tree
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofStatus G_proof_tree -> [String]
forall proof_tree. ProofStatus proof_tree -> [String]
LP.proofLines) Maybe (ProofStatus G_proof_tree)
proofStatusM
          else Maybe String
forall a. Maybe a
Nothing
      }

  convertTime :: TimeOfDay -> ProofTime
  convertTime :: TimeOfDay -> ProofTime
convertTime tod :: TimeOfDay
tod = ProofTime :: String -> ProofTimeComponents -> ProofTime
ProofTime
    { seconds :: String
seconds = String -> Double -> String
forall r. PrintfType r => String -> r
printf "%.3f" (String -> Double
forall a. Read a => String -> a
read (String -> Double) -> String -> Double
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
init ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ DiffTime -> String
forall a. Show a => a -> String
show (DiffTime -> String) -> DiffTime -> String
forall a b. (a -> b) -> a -> b
$ TimeOfDay -> DiffTime
timeOfDayToTime TimeOfDay
tod :: Double)
    , components :: ProofTimeComponents
components = TimeOfDay -> ProofTimeComponents
convertTimeComponents TimeOfDay
tod
    }

  convertTimeComponents :: TimeOfDay -> ProofTimeComponents
  convertTimeComponents :: TimeOfDay -> ProofTimeComponents
convertTimeComponents tod :: TimeOfDay
tod = ProofTimeComponents :: Int -> Int -> Double -> ProofTimeComponents
ProofTimeComponents
    { hours :: Int
hours = TimeOfDay -> Int
todHour TimeOfDay
tod
    , mins :: Int
mins = TimeOfDay -> Int
todMin TimeOfDay
tod
    , secs :: Double
secs = case ReadS Double -> ReadS Double
forall a. Real a => ReadS a -> ReadS a
readSigned ReadS Double
forall a. RealFrac a => ReadS a
readFloat ReadS Double -> ReadS Double
forall a b. (a -> b) -> a -> b
$ Pico -> String
forall a. Show a => a -> String
show (Pico -> String) -> Pico -> String
forall a b. (a -> b) -> a -> b
$ TimeOfDay -> Pico
todSec TimeOfDay
tod of
        [(n :: Double
n, "")] -> Double
n
        _ -> String -> Double
forall a. HasCallStack => String -> a
error (String -> Double) -> String -> Double
forall a b. (a -> b) -> a -> b
$ "Failed reading the number " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pico -> String
forall a. Show a => a -> String
show (TimeOfDay -> Pico
todSec TimeOfDay
tod)
    }

  convertTacticScript :: Maybe (LP.ProofStatus G_proof_tree)
                      -> Maybe TacticScript
  convertTacticScript :: Maybe (ProofStatus G_proof_tree) -> Maybe TacticScript
convertTacticScript Nothing = Maybe TacticScript
forall a. Maybe a
Nothing
  convertTacticScript (Just ps :: ProofStatus G_proof_tree
ps) =
    case (\ (LP.TacticScript ts :: String
ts) -> String -> Maybe ATPTacticScript
forall a. Read a => String -> Maybe a
readMaybe String
ts) (TacticScript -> Maybe ATPTacticScript)
-> TacticScript -> Maybe ATPTacticScript
forall a b. (a -> b) -> a -> b
$ ProofStatus G_proof_tree -> TacticScript
forall proof_tree. ProofStatus proof_tree -> TacticScript
LP.tacticScript ProofStatus G_proof_tree
ps of
      Nothing -> Maybe TacticScript
forall a. Maybe a
Nothing
      Just atp :: ATPTacticScript
atp -> TacticScript -> Maybe TacticScript
forall a. a -> Maybe a
Just TacticScript :: Int -> [String] -> TacticScript
TacticScript { timeLimit :: Int
timeLimit = ATPTacticScript -> Int
tsTimeLimit ATPTacticScript
atp
                                    , extraOptions :: [String]
extraOptions = ATPTacticScript -> [String]
tsExtraOpts ATPTacticScript
atp
                                    }

data Proof = Proof
  { Proof -> String
node :: String
  , Proof -> [ProofGoal]
goals :: [ProofGoal]
  } deriving (Int -> Proof -> ShowS
[Proof] -> ShowS
Proof -> String
(Int -> Proof -> ShowS)
-> (Proof -> String) -> ([Proof] -> ShowS) -> Show Proof
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Proof] -> ShowS
$cshowList :: [Proof] -> ShowS
show :: Proof -> String
$cshow :: Proof -> String
showsPrec :: Int -> Proof -> ShowS
$cshowsPrec :: Int -> Proof -> ShowS
Show, Typeable, Typeable Proof
Constr
DataType
Typeable Proof =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Proof -> c Proof)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Proof)
-> (Proof -> Constr)
-> (Proof -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Proof))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Proof))
-> ((forall b. Data b => b -> b) -> Proof -> Proof)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proof -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proof -> r)
-> (forall u. (forall d. Data d => d -> u) -> Proof -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Proof -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Proof -> m Proof)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Proof -> m Proof)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Proof -> m Proof)
-> Data Proof
Proof -> Constr
Proof -> DataType
(forall b. Data b => b -> b) -> Proof -> Proof
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Proof -> c Proof
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Proof
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Proof -> u
forall u. (forall d. Data d => d -> u) -> Proof -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proof -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proof -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Proof -> m Proof
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Proof -> m Proof
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Proof
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Proof -> c Proof
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Proof)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Proof)
$cProof :: Constr
$tProof :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Proof -> m Proof
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Proof -> m Proof
gmapMp :: (forall d. Data d => d -> m d) -> Proof -> m Proof
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Proof -> m Proof
gmapM :: (forall d. Data d => d -> m d) -> Proof -> m Proof
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Proof -> m Proof
gmapQi :: Int -> (forall d. Data d => d -> u) -> Proof -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Proof -> u
gmapQ :: (forall d. Data d => d -> u) -> Proof -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Proof -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proof -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proof -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proof -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proof -> r
gmapT :: (forall b. Data b => b -> b) -> Proof -> Proof
$cgmapT :: (forall b. Data b => b -> b) -> Proof -> Proof
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Proof)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Proof)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Proof)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Proof)
dataTypeOf :: Proof -> DataType
$cdataTypeOf :: Proof -> DataType
toConstr :: Proof -> Constr
$ctoConstr :: Proof -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Proof
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Proof
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Proof -> c Proof
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Proof -> c Proof
$cp1Data :: Typeable Proof
Data)

data ProofGoal = ProofGoal
  { ProofGoal -> String
name :: String
  , ProofGoal -> String
result :: String
  , ProofGoal -> Maybe String
details :: Maybe String
  , ProofGoal -> Prover
usedProver :: Prover
  , ProofGoal -> String
usedTranslation :: String
  , ProofGoal -> Maybe TacticScript
tacticScript :: Maybe TacticScript
  , ProofGoal -> Maybe String
proofTree :: Maybe String
  , ProofGoal -> Maybe ProofTime
usedTime :: Maybe ProofTime
  , ProofGoal -> Maybe [String]
usedAxioms :: Maybe [String]
  , ProofGoal -> Maybe String
proverOutput :: Maybe String
  } deriving (Int -> ProofGoal -> ShowS
[ProofGoal] -> ShowS
ProofGoal -> String
(Int -> ProofGoal -> ShowS)
-> (ProofGoal -> String)
-> ([ProofGoal] -> ShowS)
-> Show ProofGoal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProofGoal] -> ShowS
$cshowList :: [ProofGoal] -> ShowS
show :: ProofGoal -> String
$cshow :: ProofGoal -> String
showsPrec :: Int -> ProofGoal -> ShowS
$cshowsPrec :: Int -> ProofGoal -> ShowS
Show, Typeable, Typeable ProofGoal
Constr
DataType
Typeable ProofGoal =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ProofGoal -> c ProofGoal)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ProofGoal)
-> (ProofGoal -> Constr)
-> (ProofGoal -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ProofGoal))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofGoal))
-> ((forall b. Data b => b -> b) -> ProofGoal -> ProofGoal)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ProofGoal -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ProofGoal -> r)
-> (forall u. (forall d. Data d => d -> u) -> ProofGoal -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ProofGoal -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal)
-> Data ProofGoal
ProofGoal -> Constr
ProofGoal -> DataType
(forall b. Data b => b -> b) -> ProofGoal -> ProofGoal
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofGoal -> c ProofGoal
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofGoal
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ProofGoal -> u
forall u. (forall d. Data d => d -> u) -> ProofGoal -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofGoal -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofGoal -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofGoal
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofGoal -> c ProofGoal
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProofGoal)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofGoal)
$cProofGoal :: Constr
$tProofGoal :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal
gmapMp :: (forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal
gmapM :: (forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProofGoal -> m ProofGoal
gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofGoal -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ProofGoal -> u
gmapQ :: (forall d. Data d => d -> u) -> ProofGoal -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ProofGoal -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofGoal -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofGoal -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofGoal -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofGoal -> r
gmapT :: (forall b. Data b => b -> b) -> ProofGoal -> ProofGoal
$cgmapT :: (forall b. Data b => b -> b) -> ProofGoal -> ProofGoal
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofGoal)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofGoal)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ProofGoal)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProofGoal)
dataTypeOf :: ProofGoal -> DataType
$cdataTypeOf :: ProofGoal -> DataType
toConstr :: ProofGoal -> Constr
$ctoConstr :: ProofGoal -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofGoal
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofGoal
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofGoal -> c ProofGoal
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofGoal -> c ProofGoal
$cp1Data :: Typeable ProofGoal
Data)

data TacticScript = TacticScript
  { TacticScript -> Int
timeLimit :: Int
  , TacticScript -> [String]
extraOptions :: [String]
  } deriving (Int -> TacticScript -> ShowS
[TacticScript] -> ShowS
TacticScript -> String
(Int -> TacticScript -> ShowS)
-> (TacticScript -> String)
-> ([TacticScript] -> ShowS)
-> Show TacticScript
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TacticScript] -> ShowS
$cshowList :: [TacticScript] -> ShowS
show :: TacticScript -> String
$cshow :: TacticScript -> String
showsPrec :: Int -> TacticScript -> ShowS
$cshowsPrec :: Int -> TacticScript -> ShowS
Show, Typeable, Typeable TacticScript
Constr
DataType
Typeable TacticScript =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TacticScript -> c TacticScript)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TacticScript)
-> (TacticScript -> Constr)
-> (TacticScript -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TacticScript))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c TacticScript))
-> ((forall b. Data b => b -> b) -> TacticScript -> TacticScript)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TacticScript -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TacticScript -> r)
-> (forall u. (forall d. Data d => d -> u) -> TacticScript -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> TacticScript -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TacticScript -> m TacticScript)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TacticScript -> m TacticScript)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TacticScript -> m TacticScript)
-> Data TacticScript
TacticScript -> Constr
TacticScript -> DataType
(forall b. Data b => b -> b) -> TacticScript -> TacticScript
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TacticScript -> c TacticScript
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TacticScript
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TacticScript -> u
forall u. (forall d. Data d => d -> u) -> TacticScript -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TacticScript -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TacticScript -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TacticScript -> m TacticScript
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TacticScript -> m TacticScript
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TacticScript
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TacticScript -> c TacticScript
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TacticScript)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TacticScript)
$cTacticScript :: Constr
$tTacticScript :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TacticScript -> m TacticScript
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TacticScript -> m TacticScript
gmapMp :: (forall d. Data d => d -> m d) -> TacticScript -> m TacticScript
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TacticScript -> m TacticScript
gmapM :: (forall d. Data d => d -> m d) -> TacticScript -> m TacticScript
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TacticScript -> m TacticScript
gmapQi :: Int -> (forall d. Data d => d -> u) -> TacticScript -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TacticScript -> u
gmapQ :: (forall d. Data d => d -> u) -> TacticScript -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TacticScript -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TacticScript -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TacticScript -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TacticScript -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TacticScript -> r
gmapT :: (forall b. Data b => b -> b) -> TacticScript -> TacticScript
$cgmapT :: (forall b. Data b => b -> b) -> TacticScript -> TacticScript
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TacticScript)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TacticScript)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TacticScript)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TacticScript)
dataTypeOf :: TacticScript -> DataType
$cdataTypeOf :: TacticScript -> DataType
toConstr :: TacticScript -> Constr
$ctoConstr :: TacticScript -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TacticScript
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TacticScript
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TacticScript -> c TacticScript
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TacticScript -> c TacticScript
$cp1Data :: Typeable TacticScript
Data)

data ProofTime = ProofTime
  { ProofTime -> String
seconds :: String
  , ProofTime -> ProofTimeComponents
components :: ProofTimeComponents
  } deriving (Int -> ProofTime -> ShowS
[ProofTime] -> ShowS
ProofTime -> String
(Int -> ProofTime -> ShowS)
-> (ProofTime -> String)
-> ([ProofTime] -> ShowS)
-> Show ProofTime
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProofTime] -> ShowS
$cshowList :: [ProofTime] -> ShowS
show :: ProofTime -> String
$cshow :: ProofTime -> String
showsPrec :: Int -> ProofTime -> ShowS
$cshowsPrec :: Int -> ProofTime -> ShowS
Show, Typeable, Typeable ProofTime
Constr
DataType
Typeable ProofTime =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ProofTime -> c ProofTime)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ProofTime)
-> (ProofTime -> Constr)
-> (ProofTime -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ProofTime))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofTime))
-> ((forall b. Data b => b -> b) -> ProofTime -> ProofTime)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ProofTime -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ProofTime -> r)
-> (forall u. (forall d. Data d => d -> u) -> ProofTime -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ProofTime -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ProofTime -> m ProofTime)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProofTime -> m ProofTime)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProofTime -> m ProofTime)
-> Data ProofTime
ProofTime -> Constr
ProofTime -> DataType
(forall b. Data b => b -> b) -> ProofTime -> ProofTime
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofTime -> c ProofTime
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTime
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ProofTime -> u
forall u. (forall d. Data d => d -> u) -> ProofTime -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTime -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTime -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProofTime -> m ProofTime
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofTime -> m ProofTime
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTime
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofTime -> c ProofTime
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProofTime)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofTime)
$cProofTime :: Constr
$tProofTime :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ProofTime -> m ProofTime
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofTime -> m ProofTime
gmapMp :: (forall d. Data d => d -> m d) -> ProofTime -> m ProofTime
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofTime -> m ProofTime
gmapM :: (forall d. Data d => d -> m d) -> ProofTime -> m ProofTime
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProofTime -> m ProofTime
gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofTime -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ProofTime -> u
gmapQ :: (forall d. Data d => d -> u) -> ProofTime -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ProofTime -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTime -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTime -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTime -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTime -> r
gmapT :: (forall b. Data b => b -> b) -> ProofTime -> ProofTime
$cgmapT :: (forall b. Data b => b -> b) -> ProofTime -> ProofTime
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofTime)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofTime)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ProofTime)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProofTime)
dataTypeOf :: ProofTime -> DataType
$cdataTypeOf :: ProofTime -> DataType
toConstr :: ProofTime -> Constr
$ctoConstr :: ProofTime -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTime
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTime
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofTime -> c ProofTime
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofTime -> c ProofTime
$cp1Data :: Typeable ProofTime
Data)

data ProofTimeComponents = ProofTimeComponents
  { ProofTimeComponents -> Int
hours :: Int
  , ProofTimeComponents -> Int
mins :: Int
  , ProofTimeComponents -> Double
secs :: Double
  } deriving (Int -> ProofTimeComponents -> ShowS
[ProofTimeComponents] -> ShowS
ProofTimeComponents -> String
(Int -> ProofTimeComponents -> ShowS)
-> (ProofTimeComponents -> String)
-> ([ProofTimeComponents] -> ShowS)
-> Show ProofTimeComponents
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProofTimeComponents] -> ShowS
$cshowList :: [ProofTimeComponents] -> ShowS
show :: ProofTimeComponents -> String
$cshow :: ProofTimeComponents -> String
showsPrec :: Int -> ProofTimeComponents -> ShowS
$cshowsPrec :: Int -> ProofTimeComponents -> ShowS
Show, Typeable, Typeable ProofTimeComponents
Constr
DataType
Typeable ProofTimeComponents =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> ProofTimeComponents
 -> c ProofTimeComponents)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ProofTimeComponents)
-> (ProofTimeComponents -> Constr)
-> (ProofTimeComponents -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ProofTimeComponents))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ProofTimeComponents))
-> ((forall b. Data b => b -> b)
    -> ProofTimeComponents -> ProofTimeComponents)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ProofTimeComponents -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ProofTimeComponents -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> ProofTimeComponents -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ProofTimeComponents -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> ProofTimeComponents -> m ProofTimeComponents)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ProofTimeComponents -> m ProofTimeComponents)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ProofTimeComponents -> m ProofTimeComponents)
-> Data ProofTimeComponents
ProofTimeComponents -> Constr
ProofTimeComponents -> DataType
(forall b. Data b => b -> b)
-> ProofTimeComponents -> ProofTimeComponents
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ProofTimeComponents
-> c ProofTimeComponents
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTimeComponents
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> ProofTimeComponents -> u
forall u.
(forall d. Data d => d -> u) -> ProofTimeComponents -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTimeComponents -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTimeComponents -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ProofTimeComponents -> m ProofTimeComponents
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ProofTimeComponents -> m ProofTimeComponents
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTimeComponents
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ProofTimeComponents
-> c ProofTimeComponents
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProofTimeComponents)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProofTimeComponents)
$cProofTimeComponents :: Constr
$tProofTimeComponents :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> ProofTimeComponents -> m ProofTimeComponents
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ProofTimeComponents -> m ProofTimeComponents
gmapMp :: (forall d. Data d => d -> m d)
-> ProofTimeComponents -> m ProofTimeComponents
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ProofTimeComponents -> m ProofTimeComponents
gmapM :: (forall d. Data d => d -> m d)
-> ProofTimeComponents -> m ProofTimeComponents
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ProofTimeComponents -> m ProofTimeComponents
gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofTimeComponents -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ProofTimeComponents -> u
gmapQ :: (forall d. Data d => d -> u) -> ProofTimeComponents -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> ProofTimeComponents -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTimeComponents -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTimeComponents -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTimeComponents -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTimeComponents -> r
gmapT :: (forall b. Data b => b -> b)
-> ProofTimeComponents -> ProofTimeComponents
$cgmapT :: (forall b. Data b => b -> b)
-> ProofTimeComponents -> ProofTimeComponents
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProofTimeComponents)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProofTimeComponents)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ProofTimeComponents)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProofTimeComponents)
dataTypeOf :: ProofTimeComponents -> DataType
$cdataTypeOf :: ProofTimeComponents -> DataType
toConstr :: ProofTimeComponents -> Constr
$ctoConstr :: ProofTimeComponents -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTimeComponents
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTimeComponents
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ProofTimeComponents
-> c ProofTimeComponents
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ProofTimeComponents
-> c ProofTimeComponents
$cp1Data :: Typeable ProofTimeComponents
Data)