{-# LANGUAGE TemplateHaskell #-}
module Persistence.Schema.Enums where

import Database.Persist.TH

data LocIdBaseKindType = FileVersion | NativeDocument | Library | OMS | Mapping | OpenConjecture | Theorem | CounterTheorem | Axiom | Symbol
                         deriving (Int -> LocIdBaseKindType -> ShowS
[LocIdBaseKindType] -> ShowS
LocIdBaseKindType -> String
(Int -> LocIdBaseKindType -> ShowS)
-> (LocIdBaseKindType -> String)
-> ([LocIdBaseKindType] -> ShowS)
-> Show LocIdBaseKindType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LocIdBaseKindType] -> ShowS
$cshowList :: [LocIdBaseKindType] -> ShowS
show :: LocIdBaseKindType -> String
$cshow :: LocIdBaseKindType -> String
showsPrec :: Int -> LocIdBaseKindType -> ShowS
$cshowsPrec :: Int -> LocIdBaseKindType -> ShowS
Show, ReadPrec [LocIdBaseKindType]
ReadPrec LocIdBaseKindType
Int -> ReadS LocIdBaseKindType
ReadS [LocIdBaseKindType]
(Int -> ReadS LocIdBaseKindType)
-> ReadS [LocIdBaseKindType]
-> ReadPrec LocIdBaseKindType
-> ReadPrec [LocIdBaseKindType]
-> Read LocIdBaseKindType
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [LocIdBaseKindType]
$creadListPrec :: ReadPrec [LocIdBaseKindType]
readPrec :: ReadPrec LocIdBaseKindType
$creadPrec :: ReadPrec LocIdBaseKindType
readList :: ReadS [LocIdBaseKindType]
$creadList :: ReadS [LocIdBaseKindType]
readsPrec :: Int -> ReadS LocIdBaseKindType
$creadsPrec :: Int -> ReadS LocIdBaseKindType
Read, LocIdBaseKindType -> LocIdBaseKindType -> Bool
(LocIdBaseKindType -> LocIdBaseKindType -> Bool)
-> (LocIdBaseKindType -> LocIdBaseKindType -> Bool)
-> Eq LocIdBaseKindType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LocIdBaseKindType -> LocIdBaseKindType -> Bool
$c/= :: LocIdBaseKindType -> LocIdBaseKindType -> Bool
== :: LocIdBaseKindType -> LocIdBaseKindType -> Bool
$c== :: LocIdBaseKindType -> LocIdBaseKindType -> Bool
Eq)
derivePersistField "LocIdBaseKindType"

data DiagnosisKindType = Error | Warn | Hint | Debug
                         deriving (Int -> DiagnosisKindType -> ShowS
[DiagnosisKindType] -> ShowS
DiagnosisKindType -> String
(Int -> DiagnosisKindType -> ShowS)
-> (DiagnosisKindType -> String)
-> ([DiagnosisKindType] -> ShowS)
-> Show DiagnosisKindType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiagnosisKindType] -> ShowS
$cshowList :: [DiagnosisKindType] -> ShowS
show :: DiagnosisKindType -> String
$cshow :: DiagnosisKindType -> String
showsPrec :: Int -> DiagnosisKindType -> ShowS
$cshowsPrec :: Int -> DiagnosisKindType -> ShowS
Show, ReadPrec [DiagnosisKindType]
ReadPrec DiagnosisKindType
Int -> ReadS DiagnosisKindType
ReadS [DiagnosisKindType]
(Int -> ReadS DiagnosisKindType)
-> ReadS [DiagnosisKindType]
-> ReadPrec DiagnosisKindType
-> ReadPrec [DiagnosisKindType]
-> Read DiagnosisKindType
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [DiagnosisKindType]
$creadListPrec :: ReadPrec [DiagnosisKindType]
readPrec :: ReadPrec DiagnosisKindType
$creadPrec :: ReadPrec DiagnosisKindType
readList :: ReadS [DiagnosisKindType]
$creadList :: ReadS [DiagnosisKindType]
readsPrec :: Int -> ReadS DiagnosisKindType
$creadsPrec :: Int -> ReadS DiagnosisKindType
Read, DiagnosisKindType -> DiagnosisKindType -> Bool
(DiagnosisKindType -> DiagnosisKindType -> Bool)
-> (DiagnosisKindType -> DiagnosisKindType -> Bool)
-> Eq DiagnosisKindType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DiagnosisKindType -> DiagnosisKindType -> Bool
$c/= :: DiagnosisKindType -> DiagnosisKindType -> Bool
== :: DiagnosisKindType -> DiagnosisKindType -> Bool
$c== :: DiagnosisKindType -> DiagnosisKindType -> Bool
Eq)
derivePersistField "DiagnosisKindType"

data ReasoningAttemptKindType = ProofAttempt | ConsistencyCheckAttempt
                                deriving (Int -> ReasoningAttemptKindType -> ShowS
[ReasoningAttemptKindType] -> ShowS
ReasoningAttemptKindType -> String
(Int -> ReasoningAttemptKindType -> ShowS)
-> (ReasoningAttemptKindType -> String)
-> ([ReasoningAttemptKindType] -> ShowS)
-> Show ReasoningAttemptKindType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ReasoningAttemptKindType] -> ShowS
$cshowList :: [ReasoningAttemptKindType] -> ShowS
show :: ReasoningAttemptKindType -> String
$cshow :: ReasoningAttemptKindType -> String
showsPrec :: Int -> ReasoningAttemptKindType -> ShowS
$cshowsPrec :: Int -> ReasoningAttemptKindType -> ShowS
Show, ReadPrec [ReasoningAttemptKindType]
ReadPrec ReasoningAttemptKindType
Int -> ReadS ReasoningAttemptKindType
ReadS [ReasoningAttemptKindType]
(Int -> ReadS ReasoningAttemptKindType)
-> ReadS [ReasoningAttemptKindType]
-> ReadPrec ReasoningAttemptKindType
-> ReadPrec [ReasoningAttemptKindType]
-> Read ReasoningAttemptKindType
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [ReasoningAttemptKindType]
$creadListPrec :: ReadPrec [ReasoningAttemptKindType]
readPrec :: ReadPrec ReasoningAttemptKindType
$creadPrec :: ReadPrec ReasoningAttemptKindType
readList :: ReadS [ReasoningAttemptKindType]
$creadList :: ReadS [ReasoningAttemptKindType]
readsPrec :: Int -> ReadS ReasoningAttemptKindType
$creadsPrec :: Int -> ReadS ReasoningAttemptKindType
Read, ReasoningAttemptKindType -> ReasoningAttemptKindType -> Bool
(ReasoningAttemptKindType -> ReasoningAttemptKindType -> Bool)
-> (ReasoningAttemptKindType -> ReasoningAttemptKindType -> Bool)
-> Eq ReasoningAttemptKindType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ReasoningAttemptKindType -> ReasoningAttemptKindType -> Bool
$c/= :: ReasoningAttemptKindType -> ReasoningAttemptKindType -> Bool
== :: ReasoningAttemptKindType -> ReasoningAttemptKindType -> Bool
$c== :: ReasoningAttemptKindType -> ReasoningAttemptKindType -> Bool
Eq)
derivePersistField "ReasoningAttemptKindType"

-- "CONTR" is only used on Conjecture while the others can be used on
-- ProofAttempt. "CONTR" is used when there are some ProofAttempts with "THM"
-- and some with "CSA".
data ProofStatusType = OPN | ERR | UNK | RSO | THM | CSA | CSAS | CONTR
                       deriving (Int -> ProofStatusType -> ShowS
[ProofStatusType] -> ShowS
ProofStatusType -> String
(Int -> ProofStatusType -> ShowS)
-> (ProofStatusType -> String)
-> ([ProofStatusType] -> ShowS)
-> Show ProofStatusType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProofStatusType] -> ShowS
$cshowList :: [ProofStatusType] -> ShowS
show :: ProofStatusType -> String
$cshow :: ProofStatusType -> String
showsPrec :: Int -> ProofStatusType -> ShowS
$cshowsPrec :: Int -> ProofStatusType -> ShowS
Show, ReadPrec [ProofStatusType]
ReadPrec ProofStatusType
Int -> ReadS ProofStatusType
ReadS [ProofStatusType]
(Int -> ReadS ProofStatusType)
-> ReadS [ProofStatusType]
-> ReadPrec ProofStatusType
-> ReadPrec [ProofStatusType]
-> Read ProofStatusType
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [ProofStatusType]
$creadListPrec :: ReadPrec [ProofStatusType]
readPrec :: ReadPrec ProofStatusType
$creadPrec :: ReadPrec ProofStatusType
readList :: ReadS [ProofStatusType]
$creadList :: ReadS [ProofStatusType]
readsPrec :: Int -> ReadS ProofStatusType
$creadsPrec :: Int -> ReadS ProofStatusType
Read, ProofStatusType -> ProofStatusType -> Bool
(ProofStatusType -> ProofStatusType -> Bool)
-> (ProofStatusType -> ProofStatusType -> Bool)
-> Eq ProofStatusType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProofStatusType -> ProofStatusType -> Bool
$c/= :: ProofStatusType -> ProofStatusType -> Bool
== :: ProofStatusType -> ProofStatusType -> Bool
$c== :: ProofStatusType -> ProofStatusType -> Bool
Eq)
derivePersistField "ProofStatusType"

data ReasonerKindType = Prover | ConsistencyChecker
                         deriving (Int -> ReasonerKindType -> ShowS
[ReasonerKindType] -> ShowS
ReasonerKindType -> String
(Int -> ReasonerKindType -> ShowS)
-> (ReasonerKindType -> String)
-> ([ReasonerKindType] -> ShowS)
-> Show ReasonerKindType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ReasonerKindType] -> ShowS
$cshowList :: [ReasonerKindType] -> ShowS
show :: ReasonerKindType -> String
$cshow :: ReasonerKindType -> String
showsPrec :: Int -> ReasonerKindType -> ShowS
$cshowsPrec :: Int -> ReasonerKindType -> ShowS
Show, ReadPrec [ReasonerKindType]
ReadPrec ReasonerKindType
Int -> ReadS ReasonerKindType
ReadS [ReasonerKindType]
(Int -> ReadS ReasonerKindType)
-> ReadS [ReasonerKindType]
-> ReadPrec ReasonerKindType
-> ReadPrec [ReasonerKindType]
-> Read ReasonerKindType
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [ReasonerKindType]
$creadListPrec :: ReadPrec [ReasonerKindType]
readPrec :: ReadPrec ReasonerKindType
$creadPrec :: ReadPrec ReasonerKindType
readList :: ReadS [ReasonerKindType]
$creadList :: ReadS [ReasonerKindType]
readsPrec :: Int -> ReadS ReasonerKindType
$creadsPrec :: Int -> ReadS ReasonerKindType
Read, ReasonerKindType -> ReasonerKindType -> Bool
(ReasonerKindType -> ReasonerKindType -> Bool)
-> (ReasonerKindType -> ReasonerKindType -> Bool)
-> Eq ReasonerKindType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ReasonerKindType -> ReasonerKindType -> Bool
$c/= :: ReasonerKindType -> ReasonerKindType -> Bool
== :: ReasonerKindType -> ReasonerKindType -> Bool
$c== :: ReasonerKindType -> ReasonerKindType -> Bool
Eq)
derivePersistField "ReasonerKindType"

data PremiseSelectionKindType = ManualPremiseSelection | SinePremiseSelection
                                deriving (Int -> PremiseSelectionKindType -> ShowS
[PremiseSelectionKindType] -> ShowS
PremiseSelectionKindType -> String
(Int -> PremiseSelectionKindType -> ShowS)
-> (PremiseSelectionKindType -> String)
-> ([PremiseSelectionKindType] -> ShowS)
-> Show PremiseSelectionKindType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PremiseSelectionKindType] -> ShowS
$cshowList :: [PremiseSelectionKindType] -> ShowS
show :: PremiseSelectionKindType -> String
$cshow :: PremiseSelectionKindType -> String
showsPrec :: Int -> PremiseSelectionKindType -> ShowS
$cshowsPrec :: Int -> PremiseSelectionKindType -> ShowS
Show, ReadPrec [PremiseSelectionKindType]
ReadPrec PremiseSelectionKindType
Int -> ReadS PremiseSelectionKindType
ReadS [PremiseSelectionKindType]
(Int -> ReadS PremiseSelectionKindType)
-> ReadS [PremiseSelectionKindType]
-> ReadPrec PremiseSelectionKindType
-> ReadPrec [PremiseSelectionKindType]
-> Read PremiseSelectionKindType
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [PremiseSelectionKindType]
$creadListPrec :: ReadPrec [PremiseSelectionKindType]
readPrec :: ReadPrec PremiseSelectionKindType
$creadPrec :: ReadPrec PremiseSelectionKindType
readList :: ReadS [PremiseSelectionKindType]
$creadList :: ReadS [PremiseSelectionKindType]
readsPrec :: Int -> ReadS PremiseSelectionKindType
$creadsPrec :: Int -> ReadS PremiseSelectionKindType
Read, PremiseSelectionKindType -> PremiseSelectionKindType -> Bool
(PremiseSelectionKindType -> PremiseSelectionKindType -> Bool)
-> (PremiseSelectionKindType -> PremiseSelectionKindType -> Bool)
-> Eq PremiseSelectionKindType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PremiseSelectionKindType -> PremiseSelectionKindType -> Bool
$c/= :: PremiseSelectionKindType -> PremiseSelectionKindType -> Bool
== :: PremiseSelectionKindType -> PremiseSelectionKindType -> Bool
$c== :: PremiseSelectionKindType -> PremiseSelectionKindType -> Bool
Eq)
derivePersistField "PremiseSelectionKindType"