{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE ScopedTypeVariables        #-}

module Persistence.Reasoning ( setupReasoning
                             , preprocessReasoning
                             , postprocessReasoning
                             ) where

import Persistence.Database
import Persistence.LogicGraph
import Persistence.Schema as DatabaseSchema
import qualified Persistence.Schema.Enums as Enums
import qualified Persistence.Schema.ConsistencyStatusType as ConsistencyStatusType
import qualified Persistence.Schema.EvaluationStateType as EvaluationStateType
import Persistence.Utils

import Persistence.Reasoning.PremiseSelectionSInE as SInE
import PGIP.ReasoningParameters as ReasoningParameters
import PGIP.Shared

import Driver.Options
import qualified Logic.Prover as LP
import Proofs.AbstractState (G_proof_tree)
import Static.DevGraph
import Static.GTheory

import Control.Exception (catch)
import Control.Exception.Base (SomeException)
import Control.Monad.IO.Class (MonadIO (..))
import qualified Control.Monad.Fail as Fail
import Data.Char (toLower)
import Data.Maybe as Maybe (fromJust, fromMaybe, isNothing)
import Data.List (elemIndex, isPrefixOf, isInfixOf, maximumBy)
import qualified Data.Text as Text
import Data.Time.LocalTime
import Database.Persist hiding ((==.))
import Database.Persist.Sql hiding ((==.))
import Database.Esqueleto hiding ((=.), update)
import qualified Database.Esqueleto as E ((=.), update)

setupReasoning :: HetcatsOpts
               -> ReasoningCacheGoal
               -> IO (Maybe ReasonerConfigurationId)
setupReasoning :: HetcatsOpts
-> ReasoningCacheGoal -> IO (Maybe ReasonerConfigurationId)
setupReasoning opts :: HetcatsOpts
opts reasoningCacheGoal :: ReasoningCacheGoal
reasoningCacheGoal
  | ReasoningCacheGoal -> Bool
rceUseDatabase ReasoningCacheGoal
reasoningCacheGoal = DBConfig
-> DBMonad (NoLoggingT IO) (Maybe ReasonerConfigurationId)
-> IO (Maybe ReasonerConfigurationId)
forall (m :: * -> *) a.
(MonadIO m, MonadBaseControl IO m, MonadUnliftIO m, MonadFail m) =>
DBConfig -> DBMonad (NoLoggingT m) a -> m a
onDatabase (HetcatsOpts -> DBConfig
databaseConfig HetcatsOpts
opts) (DBMonad (NoLoggingT IO) (Maybe ReasonerConfigurationId)
 -> IO (Maybe ReasonerConfigurationId))
-> DBMonad (NoLoggingT IO) (Maybe ReasonerConfigurationId)
-> IO (Maybe ReasonerConfigurationId)
forall a b. (a -> b) -> a -> b
$
      (ReasonerConfigurationId -> Maybe ReasonerConfigurationId)
-> ReaderT SqlBackend (NoLoggingT IO) ReasonerConfigurationId
-> DBMonad (NoLoggingT IO) (Maybe ReasonerConfigurationId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ReasonerConfigurationId -> Maybe ReasonerConfigurationId
forall a. a -> Maybe a
Just (ReaderT SqlBackend (NoLoggingT IO) ReasonerConfigurationId
 -> DBMonad (NoLoggingT IO) (Maybe ReasonerConfigurationId))
-> ReaderT SqlBackend (NoLoggingT IO) ReasonerConfigurationId
-> DBMonad (NoLoggingT IO) (Maybe ReasonerConfigurationId)
forall a b. (a -> b) -> a -> b
$ ReasoningCacheGoal
-> ReaderT SqlBackend (NoLoggingT IO) ReasonerConfigurationId
forall (m :: * -> *).
MonadIO m =>
ReasoningCacheGoal -> DBMonad m ReasonerConfigurationId
createReasonerConfiguration ReasoningCacheGoal
reasoningCacheGoal
  | Bool
otherwise = Maybe ReasonerConfigurationId -> IO (Maybe ReasonerConfigurationId)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ReasonerConfigurationId
forall a. Maybe a
Nothing

createReasonerConfiguration :: MonadIO m
                            => ReasoningCacheGoal
                            -> DBMonad m ReasonerConfigurationId
createReasonerConfiguration :: ReasoningCacheGoal -> DBMonad m ReasonerConfigurationId
createReasonerConfiguration reasoningCacheGoal :: ReasoningCacheGoal
reasoningCacheGoal = do
  Maybe (Entity Reasoner)
reasonerEntityM <-
    case ReasonerConfiguration -> Maybe String
reasoner (ReasonerConfiguration -> Maybe String)
-> ReasonerConfiguration -> Maybe String
forall a b. (a -> b) -> a -> b
$ GoalConfig -> ReasonerConfiguration
reasonerConfiguration (GoalConfig -> ReasonerConfiguration)
-> GoalConfig -> ReasonerConfiguration
forall a b. (a -> b) -> a -> b
$ ReasoningCacheGoal -> GoalConfig
rceGoalConfig ReasoningCacheGoal
reasoningCacheGoal of
      Nothing -> Maybe (Entity Reasoner)
-> ReaderT SqlBackend m (Maybe (Entity Reasoner))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Entity Reasoner)
forall a. Maybe a
Nothing
      Just reasonerName :: String
reasonerName -> String
-> ReasonerKindType
-> ReaderT SqlBackend m (Maybe (Entity Reasoner))
forall (m :: * -> *).
MonadIO m =>
String -> ReasonerKindType -> DBMonad m (Maybe (Entity Reasoner))
findReasoner String
reasonerName ReasonerKindType
Enums.Prover
  let reasonerKeyM :: Maybe (Key Reasoner)
reasonerKeyM = (Entity Reasoner -> Key Reasoner)
-> Maybe (Entity Reasoner) -> Maybe (Key Reasoner)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Entity key :: Key Reasoner
key _) -> Key Reasoner
key) Maybe (Entity Reasoner)
reasonerEntityM
  ReasonerConfiguration -> DBMonad m ReasonerConfigurationId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WReasonerConfiguration :: Maybe (Key Reasoner) -> Maybe Int -> ReasonerConfiguration
DatabaseSchema.ReasonerConfiguration
    { reasonerConfigurationConfiguredReasonerId :: Maybe (Key Reasoner)
reasonerConfigurationConfiguredReasonerId = Maybe (Key Reasoner)
reasonerKeyM
    , reasonerConfigurationTimeLimit :: Maybe Int
reasonerConfigurationTimeLimit = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$
        ReasonerConfiguration -> Int
timeLimit (ReasonerConfiguration -> Int) -> ReasonerConfiguration -> Int
forall a b. (a -> b) -> a -> b
$ GoalConfig -> ReasonerConfiguration
reasonerConfiguration (GoalConfig -> ReasonerConfiguration)
-> GoalConfig -> ReasonerConfiguration
forall a b. (a -> b) -> a -> b
$ ReasoningCacheGoal -> GoalConfig
rceGoalConfig ReasoningCacheGoal
reasoningCacheGoal
    }

preprocessReasoning :: HetcatsOpts
                    -> String
                    -> ReasoningCacheGoal
                    -> IO (Maybe [String], ReasoningCacheGoal)
preprocessReasoning :: HetcatsOpts
-> String
-> ReasoningCacheGoal
-> IO (Maybe [String], ReasoningCacheGoal)
preprocessReasoning opts :: HetcatsOpts
opts location :: String
location reasoningCacheGoal :: ReasoningCacheGoal
reasoningCacheGoal = do
  premiseSelectionResultData :: (Maybe [String], Int, PremiseSelectionResultForDatabase)
premiseSelectionResultData@(premisesM :: Maybe [String]
premisesM, _, _) <-
    case ReasoningCacheGoal -> ProverMode
rceProverMode ReasoningCacheGoal
reasoningCacheGoal of
      GlConsistency -> (Maybe [String], Int, PremiseSelectionResultForDatabase)
-> IO (Maybe [String], Int, PremiseSelectionResultForDatabase)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [String]
forall a. Maybe a
Nothing, 0, PremiseSelectionResultForDatabase
NoResult)
      GlProofs ->
        case GoalConfig -> Maybe PremiseSelection
premiseSelection (GoalConfig -> Maybe PremiseSelection)
-> GoalConfig -> Maybe PremiseSelection
forall a b. (a -> b) -> a -> b
$ ReasoningCacheGoal -> GoalConfig
rceGoalConfig ReasoningCacheGoal
reasoningCacheGoal of
          Nothing -> (Maybe [String], Int, PremiseSelectionResultForDatabase)
-> IO (Maybe [String], Int, PremiseSelectionResultForDatabase)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [String]
forall a. Maybe a
Nothing, 0, PremiseSelectionResultForDatabase
NoResult)
          Just premiseSelectionParameters :: PremiseSelection
premiseSelectionParameters -> do
            let premiseSelectionKindV :: PremiseSelectionKindType
premiseSelectionKindV =
                  PremiseSelection -> PremiseSelectionKindType
getPremiseSelectionKind PremiseSelection
premiseSelectionParameters
            let gTheory :: G_theory
gTheory = ReasoningCacheGoal -> G_theory
rceGTheory ReasoningCacheGoal
reasoningCacheGoal
            let goalName :: String
goalName = Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ ReasoningCacheGoal -> Maybe String
rceGoalNameM ReasoningCacheGoal
reasoningCacheGoal
            HetcatsOpts
-> G_theory
-> String
-> PremiseSelection
-> PremiseSelectionKindType
-> IO (Maybe [String], Int, PremiseSelectionResultForDatabase)
performPremiseSelection HetcatsOpts
opts G_theory
gTheory String
goalName
              PremiseSelection
premiseSelectionParameters PremiseSelectionKindType
premiseSelectionKindV

  ReasoningCacheGoal
reasoningCacheGoal' <- case ReasoningCacheGoal -> Maybe ReasonerConfigurationId
rceReasonerConfigurationKeyM ReasoningCacheGoal
reasoningCacheGoal of
    Nothing -> ReasoningCacheGoal -> IO ReasoningCacheGoal
forall (m :: * -> *) a. Monad m => a -> m a
return ReasoningCacheGoal
reasoningCacheGoal
    Just _ -> do
      Entity reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey _ <-
        DBConfig
-> DBMonad (NoLoggingT IO) (Entity ReasoningAttempt)
-> IO (Entity ReasoningAttempt)
forall (m :: * -> *) a.
(MonadIO m, MonadBaseControl IO m, MonadUnliftIO m, MonadFail m) =>
DBConfig -> DBMonad (NoLoggingT m) a -> m a
onDatabase (HetcatsOpts -> DBConfig
databaseConfig HetcatsOpts
opts) (DBMonad (NoLoggingT IO) (Entity ReasoningAttempt)
 -> IO (Entity ReasoningAttempt))
-> DBMonad (NoLoggingT IO) (Entity ReasoningAttempt)
-> IO (Entity ReasoningAttempt)
forall a b. (a -> b) -> a -> b
$ do
          (reasoningAttemptEntity :: Entity ReasoningAttempt
reasoningAttemptEntity, omsEntity :: Entity LocIdBase
omsEntity) <-
            HetcatsOpts
-> String
-> ReasoningCacheGoal
-> DBMonad
     (NoLoggingT IO) (Entity ReasoningAttempt, Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> String
-> ReasoningCacheGoal
-> DBMonad m (Entity ReasoningAttempt, Entity LocIdBase)
createReasoningAttempt HetcatsOpts
opts String
location ReasoningCacheGoal
reasoningCacheGoal
          case ReasoningCacheGoal -> ProverMode
rceProverMode ReasoningCacheGoal
reasoningCacheGoal of
            GlConsistency -> () -> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            GlProofs -> case GoalConfig -> Maybe PremiseSelection
premiseSelection (GoalConfig -> Maybe PremiseSelection)
-> GoalConfig -> Maybe PremiseSelection
forall a b. (a -> b) -> a -> b
$ ReasoningCacheGoal -> GoalConfig
rceGoalConfig ReasoningCacheGoal
reasoningCacheGoal of
              Nothing -> () -> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just premiseSelectionParameters :: PremiseSelection
premiseSelectionParameters -> do
                let premiseSelectionKindV :: PremiseSelectionKindType
premiseSelectionKindV =
                      PremiseSelection -> PremiseSelectionKindType
getPremiseSelectionKind PremiseSelection
premiseSelectionParameters
                HetcatsOpts
-> Entity ReasoningAttempt
-> PremiseSelection
-> PremiseSelectionKindType
-> (Maybe [String], Int, PremiseSelectionResultForDatabase)
-> Entity LocIdBase
-> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> Entity ReasoningAttempt
-> PremiseSelection
-> PremiseSelectionKindType
-> (Maybe [String], Int, PremiseSelectionResultForDatabase)
-> Entity LocIdBase
-> DBMonad m ()
createPremiseSelection HetcatsOpts
opts
                  Entity ReasoningAttempt
reasoningAttemptEntity PremiseSelection
premiseSelectionParameters
                  PremiseSelectionKindType
premiseSelectionKindV (Maybe [String], Int, PremiseSelectionResultForDatabase)
premiseSelectionResultData Entity LocIdBase
omsEntity
          Entity ReasoningAttempt
-> DBMonad (NoLoggingT IO) (Entity ReasoningAttempt)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity ReasoningAttempt
reasoningAttemptEntity
      ReasoningCacheGoal -> IO ReasoningCacheGoal
forall (m :: * -> *) a. Monad m => a -> m a
return ReasoningCacheGoal
reasoningCacheGoal { rceReasoningAttemptKeyM :: Maybe (Key ReasoningAttempt)
rceReasoningAttemptKeyM = Key ReasoningAttempt -> Maybe (Key ReasoningAttempt)
forall a. a -> Maybe a
Just Key ReasoningAttempt
reasoningAttemptKey }
  (Maybe [String], ReasoningCacheGoal)
-> IO (Maybe [String], ReasoningCacheGoal)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [String]
premisesM, ReasoningCacheGoal
reasoningCacheGoal')

getPremiseSelectionKind :: ReasoningParameters.PremiseSelection
                        -> Enums.PremiseSelectionKindType
getPremiseSelectionKind :: PremiseSelection -> PremiseSelectionKindType
getPremiseSelectionKind premiseSelectionParameters :: PremiseSelection
premiseSelectionParameters =
  case (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ PremiseSelection -> String
kind PremiseSelection
premiseSelectionParameters of
    "sine" -> PremiseSelectionKindType
Enums.SinePremiseSelection
    _ -> PremiseSelectionKindType
Enums.ManualPremiseSelection

data PremiseSelectionResultForDatabase = NoResult
                                       | SineResult SInE.G_SInEResult

performPremiseSelection :: HetcatsOpts
                        -> G_theory
                        -> String
                        -> ReasoningParameters.PremiseSelection
                        -> Enums.PremiseSelectionKindType
                        -> IO (Maybe [String], Int, PremiseSelectionResultForDatabase)
performPremiseSelection :: HetcatsOpts
-> G_theory
-> String
-> PremiseSelection
-> PremiseSelectionKindType
-> IO (Maybe [String], Int, PremiseSelectionResultForDatabase)
performPremiseSelection opts :: HetcatsOpts
opts gTheory :: G_theory
gTheory
  goalName :: String
goalName premiseSelectionParameters :: PremiseSelection
premiseSelectionParameters premiseSelectionKindV :: PremiseSelectionKindType
premiseSelectionKindV =
  case PremiseSelectionKindType
premiseSelectionKindV of
    Enums.ManualPremiseSelection ->
      (Maybe [String], Int, PremiseSelectionResultForDatabase)
-> IO (Maybe [String], Int, PremiseSelectionResultForDatabase)
forall (m :: * -> *) a. Monad m => a -> m a
return (PremiseSelection -> Maybe [String]
manualPremises PremiseSelection
premiseSelectionParameters, 0, PremiseSelectionResultForDatabase
NoResult)
    Enums.SinePremiseSelection -> do
      (premisesM :: Maybe [String]
premisesM, timeTaken :: Int
timeTaken, sineResult :: G_SInEResult
sineResult) <-
        HetcatsOpts
-> G_theory
-> PremiseSelection
-> String
-> IO (Maybe [String], Int, G_SInEResult)
SInE.perform HetcatsOpts
opts G_theory
gTheory PremiseSelection
premiseSelectionParameters String
goalName
      (Maybe [String], Int, PremiseSelectionResultForDatabase)
-> IO (Maybe [String], Int, PremiseSelectionResultForDatabase)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [String]
premisesM, Int
timeTaken, G_SInEResult -> PremiseSelectionResultForDatabase
SineResult G_SInEResult
sineResult)

createReasoningAttempt :: forall m . (MonadIO m, Fail.MonadFail m)
                       => HetcatsOpts
                       -> String
                       -> ReasoningCacheGoal
                       -> DBMonad m (Entity ReasoningAttempt, Entity LocIdBase)
createReasoningAttempt :: HetcatsOpts
-> String
-> ReasoningCacheGoal
-> DBMonad m (Entity ReasoningAttempt, Entity LocIdBase)
createReasoningAttempt opts :: HetcatsOpts
opts location :: String
location reasoningCacheGoal :: ReasoningCacheGoal
reasoningCacheGoal = do
  let nodeLabel :: DGNodeLab
nodeLabel = (Int, DGNodeLab) -> DGNodeLab
forall a b. (a, b) -> b
snd ((Int, DGNodeLab) -> DGNodeLab) -> (Int, DGNodeLab) -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ ReasoningCacheGoal -> (Int, DGNodeLab)
rceNode ReasoningCacheGoal
reasoningCacheGoal
  let reasoner_ :: ProverOrConsChecker
reasoner_ = ReasoningCacheGoal -> ProverOrConsChecker
rceReasoner ReasoningCacheGoal
reasoningCacheGoal
  let comorphism :: AnyComorphism
comorphism = ReasoningCacheGoal -> AnyComorphism
rceComorphism ReasoningCacheGoal
reasoningCacheGoal
  Entity LocIdBase
documentEntity <- HetcatsOpts -> String -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts -> String -> DBMonad m (Entity LocIdBase)
findDocument HetcatsOpts
opts String
location
  Entity LocIdBase
omsEntity <- Entity LocIdBase -> DGNodeLab -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Entity LocIdBase -> DGNodeLab -> DBMonad m (Entity LocIdBase)
findOMS Entity LocIdBase
documentEntity DGNodeLab
nodeLabel
  Entity reasonerKey :: Key Reasoner
reasonerKey _ <- ProverOrConsChecker -> DBMonad m (Entity Reasoner)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
ProverOrConsChecker -> DBMonad m (Entity Reasoner)
findReasonerByProverOrConsChecker ProverOrConsChecker
reasoner_
  Maybe (Entity LogicTranslation)
logicTranslationEntityM <- HetcatsOpts
-> AnyComorphism -> DBMonad m (Maybe (Entity LogicTranslation))
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> AnyComorphism -> DBMonad m (Maybe (Entity LogicTranslation))
findOrCreateLogicTranslation HetcatsOpts
opts AnyComorphism
comorphism
  Entity ReasoningAttempt
reasoningAttemptEntity <- case ReasoningCacheGoal -> ProverMode
rceProverMode ReasoningCacheGoal
reasoningCacheGoal of
    GlConsistency ->
      HetcatsOpts
-> String
-> DBMonad m (Entity ReasoningAttempt)
-> DBMonad m (Entity ReasoningAttempt)
forall (m :: * -> *) a.
MonadIO m =>
HetcatsOpts -> String -> DBMonad m a -> DBMonad m a
advisoryLocked HetcatsOpts
opts (LocIdBaseId -> String
omsLockKey (LocIdBaseId -> String) -> LocIdBaseId -> String
forall a b. (a -> b) -> a -> b
$ Entity LocIdBase -> LocIdBaseId
forall record. Entity record -> Key record
entityKey Entity LocIdBase
omsEntity) (DBMonad m (Entity ReasoningAttempt)
 -> DBMonad m (Entity ReasoningAttempt))
-> DBMonad m (Entity ReasoningAttempt)
-> DBMonad m (Entity ReasoningAttempt)
forall a b. (a -> b) -> a -> b
$ do
        Entity LocIdBase -> EvaluationStateType -> DBMonad m ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Entity LocIdBase -> EvaluationStateType -> DBMonad m ()
setOmsEvaluationState Entity LocIdBase
omsEntity EvaluationStateType
EvaluationStateType.Processing
        reasoningAttemptEntity :: Entity ReasoningAttempt
reasoningAttemptEntity@(Entity reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey _) <- MonadIO m =>
ReasoningAttemptKindType
-> EvaluationStateType
-> Maybe String
-> Maybe (Key Reasoner)
-> Maybe LogicTranslationId
-> DBMonad m (Entity ReasoningAttempt)
ReasoningAttemptKindType
-> EvaluationStateType
-> Maybe String
-> Maybe (Key Reasoner)
-> Maybe LogicTranslationId
-> DBMonad m (Entity ReasoningAttempt)
insertReasoningAttempt
          ReasoningAttemptKindType
Enums.ConsistencyCheckAttempt
          EvaluationStateType
EvaluationStateType.Processing
          Maybe String
forall a. Maybe a
Nothing
          (Key Reasoner -> Maybe (Key Reasoner)
forall a. a -> Maybe a
Just Key Reasoner
reasonerKey)
          ((Entity LogicTranslation -> LogicTranslationId)
-> Maybe (Entity LogicTranslation) -> Maybe LogicTranslationId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Entity LogicTranslation -> LogicTranslationId
forall record. Entity record -> Key record
entityKey Maybe (Entity LogicTranslation)
logicTranslationEntityM)
        let consistencyCheckAttemptKey :: Key ConsistencyCheckAttempt
consistencyCheckAttemptKey = Int64 -> Key ConsistencyCheckAttempt
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key ConsistencyCheckAttempt)
-> Int64 -> Key ConsistencyCheckAttempt
forall a b. (a -> b) -> a -> b
$ Key ReasoningAttempt -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey Key ReasoningAttempt
reasoningAttemptKey
        let consistencyCheckAttemptValue :: ConsistencyCheckAttempt
consistencyCheckAttemptValue = $WConsistencyCheckAttempt :: Maybe LocIdBaseId
-> ConsistencyStatusType -> ConsistencyCheckAttempt
DatabaseSchema.ConsistencyCheckAttempt
              { consistencyCheckAttemptOmsId :: Maybe LocIdBaseId
consistencyCheckAttemptOmsId = LocIdBaseId -> Maybe LocIdBaseId
forall a. a -> Maybe a
Just (LocIdBaseId -> Maybe LocIdBaseId)
-> LocIdBaseId -> Maybe LocIdBaseId
forall a b. (a -> b) -> a -> b
$ Entity LocIdBase -> LocIdBaseId
forall record. Entity record -> Key record
entityKey Entity LocIdBase
omsEntity
              , consistencyCheckAttemptConsistencyStatus :: ConsistencyStatusType
consistencyCheckAttemptConsistencyStatus =
                  ConsistencyStatusType
ConsistencyStatusType.Open
              }
        [Entity ConsistencyCheckAttempt] -> DBMonad m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany
          [Key ConsistencyCheckAttempt
-> ConsistencyCheckAttempt -> Entity ConsistencyCheckAttempt
forall record. Key record -> record -> Entity record
Entity Key ConsistencyCheckAttempt
consistencyCheckAttemptKey ConsistencyCheckAttempt
consistencyCheckAttemptValue]
        Entity ReasoningAttempt -> DBMonad m (Entity ReasoningAttempt)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity ReasoningAttempt
reasoningAttemptEntity
    GlProofs -> do
      let goalName :: String
goalName = Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ ReasoningCacheGoal -> Maybe String
rceGoalNameM ReasoningCacheGoal
reasoningCacheGoal
      Either String LocIdBaseId
conjectureKeyOrError <- IO (Either String LocIdBaseId)
-> ReaderT SqlBackend m (Either String LocIdBaseId)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either String LocIdBaseId)
 -> ReaderT SqlBackend m (Either String LocIdBaseId))
-> IO (Either String LocIdBaseId)
-> ReaderT SqlBackend m (Either String LocIdBaseId)
forall a b. (a -> b) -> a -> b
$ IO (Either String LocIdBaseId)
-> (SomeException -> IO (Either String LocIdBaseId))
-> IO (Either String LocIdBaseId)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
Control.Exception.catch
        (do
          Entity conjectureKey :: LocIdBaseId
conjectureKey _ <- DBConfig
-> DBMonad (NoLoggingT IO) (Entity LocIdBase)
-> IO (Entity LocIdBase)
forall (m :: * -> *) a.
(MonadIO m, MonadBaseControl IO m, MonadUnliftIO m, MonadFail m) =>
DBConfig -> DBMonad (NoLoggingT m) a -> m a
onDatabase (HetcatsOpts -> DBConfig
databaseConfig HetcatsOpts
opts) (DBMonad (NoLoggingT IO) (Entity LocIdBase)
 -> IO (Entity LocIdBase))
-> DBMonad (NoLoggingT IO) (Entity LocIdBase)
-> IO (Entity LocIdBase)
forall a b. (a -> b) -> a -> b
$
            Entity LocIdBase
-> String -> DBMonad (NoLoggingT IO) (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Entity LocIdBase -> String -> DBMonad m (Entity LocIdBase)
findConjecture Entity LocIdBase
omsEntity String
goalName
          Either String LocIdBaseId -> IO (Either String LocIdBaseId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String LocIdBaseId -> IO (Either String LocIdBaseId))
-> Either String LocIdBaseId -> IO (Either String LocIdBaseId)
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Either String LocIdBaseId
forall a b. b -> Either a b
Right LocIdBaseId
conjectureKey
        )
        (\ exception :: SomeException
exception ->
          Either String LocIdBaseId -> IO (Either String LocIdBaseId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String LocIdBaseId -> IO (Either String LocIdBaseId))
-> Either String LocIdBaseId -> IO (Either String LocIdBaseId)
forall a b. (a -> b) -> a -> b
$ String -> Either String LocIdBaseId
forall a b. a -> Either a b
Left ("Persistence.Reasoning.createReasoningAttempt: "
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ "Could not find conjecture \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
goalName
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\" - " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SomeException -> String
forall a. Show a => a -> String
show (SomeException
exception :: SomeException))
        )
      (reasoningAttemptEntity :: Entity ReasoningAttempt
reasoningAttemptEntity@(Entity reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey _), conjectureKeyM :: Maybe LocIdBaseId
conjectureKeyM, status :: ProofStatusType
status) <-
        case Either String LocIdBaseId
conjectureKeyOrError of
          Right conjectureKey :: LocIdBaseId
conjectureKey -> do
            Just conjectureValue :: LocIdBase
conjectureValue <- LocIdBaseId -> ReaderT SqlBackend m (Maybe LocIdBase)
forall backend (m :: * -> *) record.
(PersistStoreRead backend, MonadIO m,
 PersistRecordBackend record backend) =>
Key record -> ReaderT backend m (Maybe record)
get LocIdBaseId
conjectureKey
            let conjectureEntity :: Entity LocIdBase
conjectureEntity = LocIdBaseId -> LocIdBase -> Entity LocIdBase
forall record. Key record -> record -> Entity record
Entity LocIdBaseId
conjectureKey LocIdBase
conjectureValue
            HetcatsOpts
-> String
-> DBMonad
     m (Entity ReasoningAttempt, Maybe LocIdBaseId, ProofStatusType)
-> DBMonad
     m (Entity ReasoningAttempt, Maybe LocIdBaseId, ProofStatusType)
forall (m :: * -> *) a.
MonadIO m =>
HetcatsOpts -> String -> DBMonad m a -> DBMonad m a
advisoryLocked HetcatsOpts
opts (LocIdBaseId -> String
conjectureLockKey LocIdBaseId
conjectureKey) (DBMonad
   m (Entity ReasoningAttempt, Maybe LocIdBaseId, ProofStatusType)
 -> DBMonad
      m (Entity ReasoningAttempt, Maybe LocIdBaseId, ProofStatusType))
-> DBMonad
     m (Entity ReasoningAttempt, Maybe LocIdBaseId, ProofStatusType)
-> DBMonad
     m (Entity ReasoningAttempt, Maybe LocIdBaseId, ProofStatusType)
forall a b. (a -> b) -> a -> b
$ do
              Entity LocIdBase -> EvaluationStateType -> DBMonad m ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Entity LocIdBase -> EvaluationStateType -> DBMonad m ()
setConjectureEvaluationState
                Entity LocIdBase
conjectureEntity EvaluationStateType
EvaluationStateType.Processing
              Entity ReasoningAttempt
reasoningAttemptEntity <- MonadIO m =>
ReasoningAttemptKindType
-> EvaluationStateType
-> Maybe String
-> Maybe (Key Reasoner)
-> Maybe LogicTranslationId
-> DBMonad m (Entity ReasoningAttempt)
ReasoningAttemptKindType
-> EvaluationStateType
-> Maybe String
-> Maybe (Key Reasoner)
-> Maybe LogicTranslationId
-> DBMonad m (Entity ReasoningAttempt)
insertReasoningAttempt
                ReasoningAttemptKindType
Enums.ProofAttempt
                EvaluationStateType
EvaluationStateType.Processing
                Maybe String
forall a. Maybe a
Nothing
                (Key Reasoner -> Maybe (Key Reasoner)
forall a. a -> Maybe a
Just Key Reasoner
reasonerKey)
                ((Entity LogicTranslation -> LogicTranslationId)
-> Maybe (Entity LogicTranslation) -> Maybe LogicTranslationId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Entity LogicTranslation -> LogicTranslationId
forall record. Entity record -> Key record
entityKey Maybe (Entity LogicTranslation)
logicTranslationEntityM)
              (Entity ReasoningAttempt, Maybe LocIdBaseId, ProofStatusType)
-> DBMonad
     m (Entity ReasoningAttempt, Maybe LocIdBaseId, ProofStatusType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Entity ReasoningAttempt
reasoningAttemptEntity, LocIdBaseId -> Maybe LocIdBaseId
forall a. a -> Maybe a
Just LocIdBaseId
conjectureKey, ProofStatusType
Enums.OPN)
          Left message :: String
message -> do
            Entity ReasoningAttempt
reasoningAttemptEntity <- MonadIO m =>
ReasoningAttemptKindType
-> EvaluationStateType
-> Maybe String
-> Maybe (Key Reasoner)
-> Maybe LogicTranslationId
-> DBMonad m (Entity ReasoningAttempt)
ReasoningAttemptKindType
-> EvaluationStateType
-> Maybe String
-> Maybe (Key Reasoner)
-> Maybe LogicTranslationId
-> DBMonad m (Entity ReasoningAttempt)
insertReasoningAttempt
              ReasoningAttemptKindType
Enums.ProofAttempt
              EvaluationStateType
EvaluationStateType.FinishedUnsuccessfully
              (String -> Maybe String
forall a. a -> Maybe a
Just String
message)
              (Key Reasoner -> Maybe (Key Reasoner)
forall a. a -> Maybe a
Just Key Reasoner
reasonerKey)
              ((Entity LogicTranslation -> LogicTranslationId)
-> Maybe (Entity LogicTranslation) -> Maybe LogicTranslationId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Entity LogicTranslation -> LogicTranslationId
forall record. Entity record -> Key record
entityKey Maybe (Entity LogicTranslation)
logicTranslationEntityM)
            (Entity ReasoningAttempt, Maybe LocIdBaseId, ProofStatusType)
-> DBMonad
     m (Entity ReasoningAttempt, Maybe LocIdBaseId, ProofStatusType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Entity ReasoningAttempt
reasoningAttemptEntity, Maybe LocIdBaseId
forall a. Maybe a
Nothing, ProofStatusType
Enums.ERR)
      let proofAttemptKey :: Key ProofAttempt
proofAttemptKey = Int64 -> Key ProofAttempt
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key ProofAttempt) -> Int64 -> Key ProofAttempt
forall a b. (a -> b) -> a -> b
$ Key ReasoningAttempt -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey Key ReasoningAttempt
reasoningAttemptKey
      let proofAttemptValue :: ProofAttempt
proofAttemptValue = $WProofAttempt :: Maybe LocIdBaseId -> ProofStatusType -> ProofAttempt
DatabaseSchema.ProofAttempt
            { proofAttemptConjectureId :: Maybe LocIdBaseId
proofAttemptConjectureId = Maybe LocIdBaseId
conjectureKeyM
            , proofAttemptProofStatus :: ProofStatusType
proofAttemptProofStatus = ProofStatusType
status
            }
      [Entity ProofAttempt] -> DBMonad m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany [Key ProofAttempt -> ProofAttempt -> Entity ProofAttempt
forall record. Key record -> record -> Entity record
Entity Key ProofAttempt
proofAttemptKey ProofAttempt
proofAttemptValue]
      Entity ReasoningAttempt -> DBMonad m (Entity ReasoningAttempt)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity ReasoningAttempt
reasoningAttemptEntity
  (Entity ReasoningAttempt, Entity LocIdBase)
-> DBMonad m (Entity ReasoningAttempt, Entity LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return (Entity ReasoningAttempt
reasoningAttemptEntity, Entity LocIdBase
omsEntity)
  where
    insertReasoningAttempt :: MonadIO m
                           => Enums.ReasoningAttemptKindType
                           -> EvaluationStateType.EvaluationStateType
                           -> Maybe String
                           -> Maybe DatabaseSchema.ReasonerId
                           -> Maybe DatabaseSchema.LogicTranslationId
                           -> DBMonad m (Entity ReasoningAttempt)
    insertReasoningAttempt :: ReasoningAttemptKindType
-> EvaluationStateType
-> Maybe String
-> Maybe (Key Reasoner)
-> Maybe LogicTranslationId
-> DBMonad m (Entity ReasoningAttempt)
insertReasoningAttempt kind_ :: ReasoningAttemptKindType
kind_ evaluationState :: EvaluationStateType
evaluationState messageM :: Maybe String
messageM reasonerKey :: Maybe (Key Reasoner)
reasonerKey
      logicTranslationKey :: Maybe LogicTranslationId
logicTranslationKey = do
      Key Action
actionKey <- Action -> ReaderT SqlBackend m (Key Action)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WAction :: EvaluationStateType -> Maybe Text -> Action
DatabaseSchema.Action
        { actionEvaluationState :: EvaluationStateType
actionEvaluationState = EvaluationStateType
evaluationState
        , actionMessage :: Maybe Text
actionMessage = (String -> Text) -> Maybe String -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Text
Text.pack Maybe String
messageM
        }
      let reasoningAttemptValue :: ReasoningAttempt
reasoningAttemptValue = $WReasoningAttempt :: ReasoningAttemptKindType
-> Key Action
-> ReasonerConfigurationId
-> Maybe (Key Reasoner)
-> Maybe LogicTranslationId
-> Maybe Int
-> ReasoningAttempt
DatabaseSchema.ReasoningAttempt
            { reasoningAttemptKind :: ReasoningAttemptKindType
reasoningAttemptKind = ReasoningAttemptKindType
kind_
            , reasoningAttemptActionId :: Key Action
reasoningAttemptActionId = Key Action
actionKey
            , reasoningAttemptReasonerConfigurationId :: ReasonerConfigurationId
reasoningAttemptReasonerConfigurationId =
                Maybe ReasonerConfigurationId -> ReasonerConfigurationId
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe ReasonerConfigurationId -> ReasonerConfigurationId)
-> Maybe ReasonerConfigurationId -> ReasonerConfigurationId
forall a b. (a -> b) -> a -> b
$ ReasoningCacheGoal -> Maybe ReasonerConfigurationId
rceReasonerConfigurationKeyM ReasoningCacheGoal
reasoningCacheGoal
            , reasoningAttemptUsedReasonerId :: Maybe (Key Reasoner)
reasoningAttemptUsedReasonerId = Maybe (Key Reasoner)
reasonerKey
            , reasoningAttemptUsedLogicTranslationId :: Maybe LogicTranslationId
reasoningAttemptUsedLogicTranslationId = Maybe LogicTranslationId
logicTranslationKey
            , reasoningAttemptTimeTaken :: Maybe Int
reasoningAttemptTimeTaken = Maybe Int
forall a. Maybe a
Nothing
            }
      Key ReasoningAttempt
reasoningAttemptKey <- ReasoningAttempt -> ReaderT SqlBackend m (Key ReasoningAttempt)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert ReasoningAttempt
reasoningAttemptValue
      Entity ReasoningAttempt -> DBMonad m (Entity ReasoningAttempt)
forall (m :: * -> *) a. Monad m => a -> m a
return (Key ReasoningAttempt -> ReasoningAttempt -> Entity ReasoningAttempt
forall record. Key record -> record -> Entity record
Entity Key ReasoningAttempt
reasoningAttemptKey ReasoningAttempt
reasoningAttemptValue)

createPremiseSelection :: (MonadIO m, Fail.MonadFail m)
                       => HetcatsOpts
                       -> Entity ReasoningAttempt
                       -> ReasoningParameters.PremiseSelection
                       -> Enums.PremiseSelectionKindType
                       -> (Maybe [String], Int, PremiseSelectionResultForDatabase)
                       -> Entity LocIdBase
                       -> DBMonad m ()
createPremiseSelection :: HetcatsOpts
-> Entity ReasoningAttempt
-> PremiseSelection
-> PremiseSelectionKindType
-> (Maybe [String], Int, PremiseSelectionResultForDatabase)
-> Entity LocIdBase
-> DBMonad m ()
createPremiseSelection opts :: HetcatsOpts
opts
  (Entity reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey reasoningAttemptValue :: ReasoningAttempt
reasoningAttemptValue)
  premiseSelectionParameters :: PremiseSelection
premiseSelectionParameters premiseSelectionKindV :: PremiseSelectionKindType
premiseSelectionKindV
  (premisesM :: Maybe [String]
premisesM, timeTaken :: Int
timeTaken, premiseSelectionResult :: PremiseSelectionResultForDatabase
premiseSelectionResult) omsEntity :: Entity LocIdBase
omsEntity = do
  let premises :: [String]
premises = [String] -> Maybe [String] -> [String]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [String]
premisesM
  let proofAttemptKey :: Key ProofAttempt
proofAttemptKey = Int64 -> Key ProofAttempt
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key ProofAttempt) -> Int64 -> Key ProofAttempt
forall a b. (a -> b) -> a -> b
$ Key ReasoningAttempt -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey Key ReasoningAttempt
reasoningAttemptKey
  let premiseSelectionValue :: PremiseSelection
premiseSelectionValue = $WPremiseSelection :: ReasonerConfigurationId
-> Key ProofAttempt
-> PremiseSelectionKindType
-> Maybe Int
-> PremiseSelection
DatabaseSchema.PremiseSelection
        { premiseSelectionReasonerConfigurationId :: ReasonerConfigurationId
premiseSelectionReasonerConfigurationId =
            ReasoningAttempt -> ReasonerConfigurationId
reasoningAttemptReasonerConfigurationId ReasoningAttempt
reasoningAttemptValue
        , premiseSelectionProofAttemptId :: Key ProofAttempt
premiseSelectionProofAttemptId = Key ProofAttempt
proofAttemptKey
        , premiseSelectionKind :: PremiseSelectionKindType
premiseSelectionKind = PremiseSelectionKindType
premiseSelectionKindV
        , premiseSelectionTimeTaken :: Maybe Int
premiseSelectionTimeTaken = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
timeTaken
        }
  Key PremiseSelection
premiseSelectionKey <- PremiseSelection -> ReaderT SqlBackend m (Key PremiseSelection)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert PremiseSelection
premiseSelectionValue
  Key PremiseSelection -> DBMonad m ()
createSpecificPremiseSelection Key PremiseSelection
premiseSelectionKey
  (String -> DBMonad m ()) -> [String] -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ premiseName :: String
premiseName -> do
          Maybe (Entity LocIdBase)
premiseKeyM <- IO (Maybe (Entity LocIdBase))
-> ReaderT SqlBackend m (Maybe (Entity LocIdBase))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (Entity LocIdBase))
 -> ReaderT SqlBackend m (Maybe (Entity LocIdBase)))
-> IO (Maybe (Entity LocIdBase))
-> ReaderT SqlBackend m (Maybe (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ IO (Maybe (Entity LocIdBase))
-> (SomeException -> IO (Maybe (Entity LocIdBase)))
-> IO (Maybe (Entity LocIdBase))
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
Control.Exception.catch
            (do
              Entity LocIdBase
premiseKey <- DBConfig
-> DBMonad (NoLoggingT IO) (Entity LocIdBase)
-> IO (Entity LocIdBase)
forall (m :: * -> *) a.
(MonadIO m, MonadBaseControl IO m, MonadUnliftIO m, MonadFail m) =>
DBConfig -> DBMonad (NoLoggingT m) a -> m a
onDatabase (HetcatsOpts -> DBConfig
databaseConfig HetcatsOpts
opts) (DBMonad (NoLoggingT IO) (Entity LocIdBase)
 -> IO (Entity LocIdBase))
-> DBMonad (NoLoggingT IO) (Entity LocIdBase)
-> IO (Entity LocIdBase)
forall a b. (a -> b) -> a -> b
$
                Entity LocIdBase
-> String -> DBMonad (NoLoggingT IO) (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Entity LocIdBase -> String -> DBMonad m (Entity LocIdBase)
findPremise Entity LocIdBase
omsEntity String
premiseName
              Maybe (Entity LocIdBase) -> IO (Maybe (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Entity LocIdBase) -> IO (Maybe (Entity LocIdBase)))
-> Maybe (Entity LocIdBase) -> IO (Maybe (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ Entity LocIdBase -> Maybe (Entity LocIdBase)
forall a. a -> Maybe a
Just Entity LocIdBase
premiseKey
            )
            (\ exception :: SomeException
exception -> do
              SomeException -> IO SomeException
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeException
exception :: SomeException) -- GHC needs this line
              Maybe (Entity LocIdBase) -> IO (Maybe (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Entity LocIdBase)
forall a. Maybe a
Nothing
            )
          case Maybe (Entity LocIdBase)
premiseKeyM of
            Just (Entity premiseKey :: LocIdBaseId
premiseKey _) -> do
              PremiseSelectedSentence
-> ReaderT SqlBackend m (Key PremiseSelectedSentence)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WPremiseSelectedSentence :: LocIdBaseId -> Key PremiseSelection -> PremiseSelectedSentence
DatabaseSchema.PremiseSelectedSentence
                { premiseSelectedSentencePremiseId :: LocIdBaseId
premiseSelectedSentencePremiseId = LocIdBaseId
premiseKey
                , premiseSelectedSentencePremiseSelectionId :: Key PremiseSelection
premiseSelectedSentencePremiseSelectionId = Key PremiseSelection
premiseSelectionKey
                }
              () -> DBMonad m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Nothing -> () -> DBMonad m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        ) [String]
premises
  where
    createSpecificPremiseSelection :: Key PremiseSelection -> DBMonad m ()
createSpecificPremiseSelection premiseSelectionKey :: Key PremiseSelection
premiseSelectionKey = case PremiseSelectionKindType
premiseSelectionKindV of
      Enums.ManualPremiseSelection ->
        [Entity ManualPremiseSelection] -> DBMonad m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany [Key ManualPremiseSelection
-> ManualPremiseSelection -> Entity ManualPremiseSelection
forall record. Key record -> record -> Entity record
Entity (Int64 -> Key ManualPremiseSelection
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key ManualPremiseSelection)
-> Int64 -> Key ManualPremiseSelection
forall a b. (a -> b) -> a -> b
$ Key PremiseSelection -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey Key PremiseSelection
premiseSelectionKey)
                                 ManualPremiseSelection
DatabaseSchema.ManualPremiseSelection]
      Enums.SinePremiseSelection -> do
        let sinePremiseSelectionKey :: Key SinePremiseSelection
sinePremiseSelectionKey = Int64 -> Key SinePremiseSelection
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key SinePremiseSelection)
-> Int64 -> Key SinePremiseSelection
forall a b. (a -> b) -> a -> b
$ Key PremiseSelection -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey Key PremiseSelection
premiseSelectionKey
        [Entity SinePremiseSelection] -> DBMonad m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany
          [Key SinePremiseSelection
-> SinePremiseSelection -> Entity SinePremiseSelection
forall record. Key record -> record -> Entity record
Entity Key SinePremiseSelection
sinePremiseSelectionKey
                  $WSinePremiseSelection :: Maybe Int -> Maybe Double -> Maybe Int -> SinePremiseSelection
DatabaseSchema.SinePremiseSelection
                    { sinePremiseSelectionDepthLimit :: Maybe Int
sinePremiseSelectionDepthLimit =
                        PremiseSelection -> Maybe Int
sineDepthLimit PremiseSelection
premiseSelectionParameters
                    , sinePremiseSelectionTolerance :: Maybe Double
sinePremiseSelectionTolerance =
                        PremiseSelection -> Maybe Double
sineTolerance PremiseSelection
premiseSelectionParameters
                    , sinePremiseSelectionAxiomNumberLimit :: Maybe Int
sinePremiseSelectionAxiomNumberLimit =
                        PremiseSelection -> Maybe Int
sinePremiseNumberLimit PremiseSelection
premiseSelectionParameters
                    }]
        case PremiseSelectionResultForDatabase
premiseSelectionResult of
          SineResult sineResult :: G_SInEResult
sineResult ->
            HetcatsOpts
-> G_SInEResult
-> Entity LocIdBase
-> Key SinePremiseSelection
-> DBMonad m ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> G_SInEResult
-> Entity LocIdBase
-> Key SinePremiseSelection
-> DBMonad m ()
SInE.saveToDatabase HetcatsOpts
opts G_SInEResult
sineResult Entity LocIdBase
omsEntity Key SinePremiseSelection
sinePremiseSelectionKey
          _ -> () -> DBMonad m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

postprocessReasoning :: HetcatsOpts
                     -> ReasoningCacheGoal
                     -> Maybe [String]
                     -> ProofResult
                     -> IO ()
postprocessReasoning :: HetcatsOpts
-> ReasoningCacheGoal -> Maybe [String] -> ProofResult -> IO ()
postprocessReasoning opts :: HetcatsOpts
opts reasoningCacheGoal :: ReasoningCacheGoal
reasoningCacheGoal premisesM :: Maybe [String]
premisesM
  (_, goalResult :: String
goalResult, _, _, _, proofStatusM :: Maybe (ProofStatus G_proof_tree)
proofStatusM, consCheckerOutputM :: Maybe String
consCheckerOutputM) =
  case ReasoningCacheGoal -> Maybe (Key ReasoningAttempt)
rceReasoningAttemptKeyM ReasoningCacheGoal
reasoningCacheGoal of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey -> DBConfig -> ReaderT SqlBackend (NoLoggingT IO) () -> IO ()
forall (m :: * -> *) a.
(MonadIO m, MonadBaseControl IO m, MonadUnliftIO m, MonadFail m) =>
DBConfig -> DBMonad (NoLoggingT m) a -> m a
onDatabase (HetcatsOpts -> DBConfig
databaseConfig HetcatsOpts
opts) (ReaderT SqlBackend (NoLoggingT IO) () -> IO ())
-> ReaderT SqlBackend (NoLoggingT IO) () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      Just reasoningAttemptValue :: ReasoningAttempt
reasoningAttemptValue <- Key ReasoningAttempt
-> ReaderT SqlBackend (NoLoggingT IO) (Maybe ReasoningAttempt)
forall backend (m :: * -> *) record.
(PersistStoreRead backend, MonadIO m,
 PersistRecordBackend record backend) =>
Key record -> ReaderT backend m (Maybe record)
get Key ReasoningAttempt
reasoningAttemptKey
      let reasoningAttemptEntity :: Entity ReasoningAttempt
reasoningAttemptEntity = Key ReasoningAttempt -> ReasoningAttempt -> Entity ReasoningAttempt
forall record. Key record -> record -> Entity record
Entity Key ReasoningAttempt
reasoningAttemptKey ReasoningAttempt
reasoningAttemptValue
      let reasonerKey :: Key Reasoner
reasonerKey = Maybe (Key Reasoner) -> Key Reasoner
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Key Reasoner) -> Key Reasoner)
-> Maybe (Key Reasoner) -> Key Reasoner
forall a b. (a -> b) -> a -> b
$ ReasoningAttempt -> Maybe (Key Reasoner)
reasoningAttemptUsedReasonerId ReasoningAttempt
reasoningAttemptValue
      case ReasoningCacheGoal -> ProverMode
rceProverMode ReasoningCacheGoal
reasoningCacheGoal of
        GlConsistency -> do
          let consistencyStatus_ :: ConsistencyStatusType
consistencyStatus_ = String -> ConsistencyStatusType
convertGoalResultConsistencyStatus String
goalResult
          Entity LocIdBase
omsEntity <- Key ReasoningAttempt -> DBMonad (NoLoggingT IO) (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Key ReasoningAttempt -> DBMonad m (Entity LocIdBase)
getOmsFromConsistencyCheckAttempt Key ReasoningAttempt
reasoningAttemptKey
          Key ReasoningAttempt
-> Key Reasoner
-> String
-> DBMonad (NoLoggingT IO) ReasonerOutputId
forall (m :: * -> *).
MonadIO m =>
Key ReasoningAttempt
-> Key Reasoner -> String -> DBMonad m ReasonerOutputId
createReasonerOutput Key ReasoningAttempt
reasoningAttemptKey Key Reasoner
reasonerKey (String -> DBMonad (NoLoggingT IO) ReasonerOutputId)
-> String -> DBMonad (NoLoggingT IO) ReasonerOutputId
forall a b. (a -> b) -> a -> b
$
            Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
consCheckerOutputM
          HetcatsOpts
-> String
-> ReaderT SqlBackend (NoLoggingT IO) ()
-> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *) a.
MonadIO m =>
HetcatsOpts -> String -> DBMonad m a -> DBMonad m a
advisoryLocked HetcatsOpts
opts (LocIdBaseId -> String
omsLockKey (LocIdBaseId -> String) -> LocIdBaseId -> String
forall a b. (a -> b) -> a -> b
$ Entity LocIdBase -> LocIdBaseId
forall record. Entity record -> Key record
entityKey Entity LocIdBase
omsEntity) (ReaderT SqlBackend (NoLoggingT IO) ()
 -> ReaderT SqlBackend (NoLoggingT IO) ())
-> ReaderT SqlBackend (NoLoggingT IO) ()
-> ReaderT SqlBackend (NoLoggingT IO) ()
forall a b. (a -> b) -> a -> b
$ do
            Entity ReasoningAttempt
-> Maybe Int -> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *).
MonadIO m =>
Entity ReasoningAttempt -> Maybe Int -> DBMonad m ()
finishReasoningAttempt Entity ReasoningAttempt
reasoningAttemptEntity Maybe Int
forall a. Maybe a
Nothing
            Key ReasoningAttempt
-> ConsistencyStatusType -> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *).
MonadIO m =>
Key ReasoningAttempt -> ConsistencyStatusType -> DBMonad m ()
updateConsistencyCheckAttempt Key ReasoningAttempt
reasoningAttemptKey ConsistencyStatusType
consistencyStatus_
            [EvaluationStateType]
evaluationStates <- Entity LocIdBase -> DBMonad (NoLoggingT IO) [EvaluationStateType]
forall (m :: * -> *).
MonadIO m =>
Entity LocIdBase -> DBMonad m [EvaluationStateType]
fetchOmsEvaluationStates Entity LocIdBase
omsEntity
            [ConsistencyStatusType]
consistencyStatuses <- Entity LocIdBase -> DBMonad (NoLoggingT IO) [ConsistencyStatusType]
forall (m :: * -> *).
MonadIO m =>
Entity LocIdBase -> DBMonad m [ConsistencyStatusType]
fetchConsistencyStatuses Entity LocIdBase
omsEntity
            Entity LocIdBase
-> EvaluationStateType -> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Entity LocIdBase -> EvaluationStateType -> DBMonad m ()
setOmsEvaluationState Entity LocIdBase
omsEntity (EvaluationStateType -> ReaderT SqlBackend (NoLoggingT IO) ())
-> EvaluationStateType -> ReaderT SqlBackend (NoLoggingT IO) ()
forall a b. (a -> b) -> a -> b
$
              [EvaluationStateType] -> EvaluationStateType
chooseEvaluationState [EvaluationStateType]
evaluationStates
            Entity LocIdBase
-> ConsistencyStatusType -> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *).
MonadIO m =>
Entity LocIdBase -> ConsistencyStatusType -> DBMonad m ()
setOmsConsistencyCheckStatus Entity LocIdBase
omsEntity (ConsistencyStatusType -> ReaderT SqlBackend (NoLoggingT IO) ())
-> ConsistencyStatusType -> ReaderT SqlBackend (NoLoggingT IO) ()
forall a b. (a -> b) -> a -> b
$
              [ConsistencyStatusType] -> ConsistencyStatusType
chooseConsistencyStatus [ConsistencyStatusType]
consistencyStatuses
        GlProofs -> do
          let proofStatus :: ProofStatus G_proof_tree
proofStatus = Maybe (ProofStatus G_proof_tree) -> ProofStatus G_proof_tree
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (ProofStatus G_proof_tree)
proofStatusM
          let timeTakenM :: Maybe Int
timeTakenM = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ TimeOfDay -> Int
convertTime (TimeOfDay -> Int) -> TimeOfDay -> Int
forall a b. (a -> b) -> a -> b
$ ProofStatus G_proof_tree -> TimeOfDay
forall proof_tree. ProofStatus proof_tree -> TimeOfDay
LP.usedTime ProofStatus G_proof_tree
proofStatus
          Key ReasoningAttempt
-> ProofStatus G_proof_tree
-> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *).
MonadIO m =>
Key ReasoningAttempt -> ProofStatus G_proof_tree -> DBMonad m ()
createGeneratedAxioms Key ReasoningAttempt
reasoningAttemptKey ProofStatus G_proof_tree
proofStatus
          Key ReasoningAttempt
-> Key Reasoner
-> String
-> DBMonad (NoLoggingT IO) ReasonerOutputId
forall (m :: * -> *).
MonadIO m =>
Key ReasoningAttempt
-> Key Reasoner -> String -> DBMonad m ReasonerOutputId
createReasonerOutput Key ReasoningAttempt
reasoningAttemptKey Key Reasoner
reasonerKey (String -> DBMonad (NoLoggingT IO) ReasonerOutputId)
-> String -> DBMonad (NoLoggingT IO) ReasonerOutputId
forall a b. (a -> b) -> a -> b
$
            [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ProofStatus G_proof_tree -> [String]
forall proof_tree. ProofStatus proof_tree -> [String]
LP.proofLines ProofStatus G_proof_tree
proofStatus
          let proofStatusSZS :: ProofStatusType
proofStatusSZS = String -> Maybe [String] -> ProofStatusType
convertGoalResultProofStatus String
goalResult Maybe [String]
premisesM
          Entity LocIdBase
omsEntity <- Key ReasoningAttempt -> DBMonad (NoLoggingT IO) (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Key ReasoningAttempt -> DBMonad m (Entity LocIdBase)
getOmsFromProofAttempt Key ReasoningAttempt
reasoningAttemptKey
          [LocIdBaseId]
usedSentencesIds <- Entity LocIdBase
-> Maybe [String] -> DBMonad (NoLoggingT IO) [LocIdBaseId]
forall (m :: * -> *).
MonadIO m =>
Entity LocIdBase -> Maybe [String] -> DBMonad m [LocIdBaseId]
getUsedSentencesIds Entity LocIdBase
omsEntity (Maybe [String] -> DBMonad (NoLoggingT IO) [LocIdBaseId])
-> Maybe [String] -> DBMonad (NoLoggingT IO) [LocIdBaseId]
forall a b. (a -> b) -> a -> b
$
            (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
          Entity LocIdBase
conjectureEntity <- Key ReasoningAttempt -> DBMonad (NoLoggingT IO) (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Key ReasoningAttempt -> DBMonad m (Entity LocIdBase)
getConjectureFromReasoningAttempt Key ReasoningAttempt
reasoningAttemptKey
          HetcatsOpts
-> String
-> ReaderT SqlBackend (NoLoggingT IO) ()
-> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *) a.
MonadIO m =>
HetcatsOpts -> String -> DBMonad m a -> DBMonad m a
advisoryLocked HetcatsOpts
opts (LocIdBaseId -> String
conjectureLockKey (LocIdBaseId -> String) -> LocIdBaseId -> String
forall a b. (a -> b) -> a -> b
$ Entity LocIdBase -> LocIdBaseId
forall record. Entity record -> Key record
entityKey Entity LocIdBase
conjectureEntity) (ReaderT SqlBackend (NoLoggingT IO) ()
 -> ReaderT SqlBackend (NoLoggingT IO) ())
-> ReaderT SqlBackend (NoLoggingT IO) ()
-> ReaderT SqlBackend (NoLoggingT IO) ()
forall a b. (a -> b) -> a -> b
$ do
            Entity ReasoningAttempt
-> Maybe Int -> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *).
MonadIO m =>
Entity ReasoningAttempt -> Maybe Int -> DBMonad m ()
finishReasoningAttempt Entity ReasoningAttempt
reasoningAttemptEntity Maybe Int
timeTakenM
            Key ReasoningAttempt
-> ProofStatusType
-> [LocIdBaseId]
-> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *).
MonadIO m =>
Key ReasoningAttempt
-> ProofStatusType -> [LocIdBaseId] -> DBMonad m ()
updateProofAttempt Key ReasoningAttempt
reasoningAttemptKey ProofStatusType
proofStatusSZS [LocIdBaseId]
usedSentencesIds
            [EvaluationStateType]
evaluationStates <- Entity LocIdBase -> DBMonad (NoLoggingT IO) [EvaluationStateType]
forall (m :: * -> *).
MonadIO m =>
Entity LocIdBase -> DBMonad m [EvaluationStateType]
fetchConjectureEvaluationStates Entity LocIdBase
conjectureEntity
            [ProofStatusType]
proofStatusesSZS <- Entity LocIdBase -> DBMonad (NoLoggingT IO) [ProofStatusType]
forall (m :: * -> *).
MonadIO m =>
Entity LocIdBase -> DBMonad m [ProofStatusType]
fetchProofStatuses Entity LocIdBase
conjectureEntity
            Entity LocIdBase
-> EvaluationStateType -> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Entity LocIdBase -> EvaluationStateType -> DBMonad m ()
setConjectureEvaluationState Entity LocIdBase
conjectureEntity (EvaluationStateType -> ReaderT SqlBackend (NoLoggingT IO) ())
-> EvaluationStateType -> ReaderT SqlBackend (NoLoggingT IO) ()
forall a b. (a -> b) -> a -> b
$
              [EvaluationStateType] -> EvaluationStateType
chooseEvaluationState [EvaluationStateType]
evaluationStates
            Entity LocIdBase
-> ProofStatusType -> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *).
MonadIO m =>
Entity LocIdBase -> ProofStatusType -> DBMonad m ()
setConjectureProofStatus Entity LocIdBase
conjectureEntity (ProofStatusType -> ReaderT SqlBackend (NoLoggingT IO) ())
-> ProofStatusType -> ReaderT SqlBackend (NoLoggingT IO) ()
forall a b. (a -> b) -> a -> b
$
              [ProofStatusType] -> ProofStatusType
chooseProofStatus [ProofStatusType]
proofStatusesSZS
      () -> ReaderT SqlBackend (NoLoggingT IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    getOmsFromConsistencyCheckAttempt :: (MonadIO m, Fail.MonadFail m)
                                      => DatabaseSchema.ReasoningAttemptId
                                      -> DBMonad m (Entity LocIdBase)
    getOmsFromConsistencyCheckAttempt :: Key ReasoningAttempt -> DBMonad m (Entity LocIdBase)
getOmsFromConsistencyCheckAttempt reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey = do
      [Entity LocIdBase]
omsL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (InnerJoin
   (InnerJoin
      (SqlExpr (Entity ReasoningAttempt))
      (SqlExpr (Entity ConsistencyCheckAttempt)))
   (SqlExpr (Entity LocIdBase))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((InnerJoin
    (InnerJoin
       (SqlExpr (Entity ReasoningAttempt))
       (SqlExpr (Entity ConsistencyCheckAttempt)))
    (SqlExpr (Entity LocIdBase))
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (InnerJoin
      (InnerJoin
         (SqlExpr (Entity ReasoningAttempt))
         (SqlExpr (Entity ConsistencyCheckAttempt)))
      (SqlExpr (Entity LocIdBase))
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$
        \ (reasoning_attempts :: SqlExpr (Entity ReasoningAttempt)
reasoning_attempts `InnerJoin` consistency_check_attempts :: SqlExpr (Entity ConsistencyCheckAttempt)
consistency_check_attempts
                              `InnerJoin` loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases) -> do
          SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Value LocIdBaseId) -> SqlExpr (Value (Maybe LocIdBaseId))
forall typ. SqlExpr (Value typ) -> SqlExpr (Value (Maybe typ))
just (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseId
forall typ. (typ ~ LocIdBaseId) => EntityField LocIdBase typ
LocIdBaseId) SqlExpr (Value (Maybe LocIdBaseId))
-> SqlExpr (Value (Maybe LocIdBaseId)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
                 SqlExpr (Entity ConsistencyCheckAttempt)
consistency_check_attempts SqlExpr (Entity ConsistencyCheckAttempt)
-> EntityField ConsistencyCheckAttempt (Maybe LocIdBaseId)
-> SqlExpr (Value (Maybe LocIdBaseId))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ConsistencyCheckAttempt (Maybe LocIdBaseId)
forall typ.
(typ ~ Maybe LocIdBaseId) =>
EntityField ConsistencyCheckAttempt typ
ConsistencyCheckAttemptOmsId
          SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity ConsistencyCheckAttempt)
consistency_check_attempts SqlExpr (Entity ConsistencyCheckAttempt)
-> EntityField
     ConsistencyCheckAttempt (Key ConsistencyCheckAttempt)
-> SqlExpr (Value (Key ConsistencyCheckAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ConsistencyCheckAttempt (Key ConsistencyCheckAttempt)
forall typ.
(typ ~ Key ConsistencyCheckAttempt) =>
EntityField ConsistencyCheckAttempt typ
ConsistencyCheckAttemptId SqlExpr (Value (Key ConsistencyCheckAttempt))
-> SqlExpr (Value (Key ConsistencyCheckAttempt))
-> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
                 SqlExpr (Value (Key ReasoningAttempt))
-> SqlExpr (Value (Key ConsistencyCheckAttempt))
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
coerceId (SqlExpr (Entity ReasoningAttempt)
reasoning_attempts SqlExpr (Entity ReasoningAttempt)
-> EntityField ReasoningAttempt (Key ReasoningAttempt)
-> SqlExpr (Value (Key ReasoningAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ReasoningAttempt (Key ReasoningAttempt)
forall typ.
(typ ~ Key ReasoningAttempt) =>
EntityField ReasoningAttempt typ
ReasoningAttemptId)
          SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity ReasoningAttempt)
reasoning_attempts SqlExpr (Entity ReasoningAttempt)
-> EntityField ReasoningAttempt (Key ReasoningAttempt)
-> SqlExpr (Value (Key ReasoningAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ReasoningAttempt (Key ReasoningAttempt)
forall typ.
(typ ~ Key ReasoningAttempt) =>
EntityField ReasoningAttempt typ
ReasoningAttemptId SqlExpr (Value (Key ReasoningAttempt))
-> SqlExpr (Value (Key ReasoningAttempt)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
                     Key ReasoningAttempt -> SqlExpr (Value (Key ReasoningAttempt))
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val Key ReasoningAttempt
reasoningAttemptKey
          Int64 -> SqlQuery ()
limit 1
          SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
      case [Entity LocIdBase]
omsL of
        [] -> String -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Persistence.Reasoning.postprocessReasoning: could not find OMS"
        omsEntity :: Entity LocIdBase
omsEntity : _ -> Entity LocIdBase -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity LocIdBase
omsEntity

    getOmsFromProofAttempt :: (MonadIO m, Fail.MonadFail m)
                           => DatabaseSchema.ReasoningAttemptId
                           -> DBMonad m (Entity LocIdBase)
    getOmsFromProofAttempt :: Key ReasoningAttempt -> DBMonad m (Entity LocIdBase)
getOmsFromProofAttempt reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey = do
      [Entity LocIdBase]
omsL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (InnerJoin
   (InnerJoin
      (InnerJoin
         (SqlExpr (Entity ReasoningAttempt))
         (SqlExpr (Entity ProofAttempt)))
      (SqlExpr (Entity Sentence)))
   (SqlExpr (Entity LocIdBase))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((InnerJoin
    (InnerJoin
       (InnerJoin
          (SqlExpr (Entity ReasoningAttempt))
          (SqlExpr (Entity ProofAttempt)))
       (SqlExpr (Entity Sentence)))
    (SqlExpr (Entity LocIdBase))
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (InnerJoin
      (InnerJoin
         (InnerJoin
            (SqlExpr (Entity ReasoningAttempt))
            (SqlExpr (Entity ProofAttempt)))
         (SqlExpr (Entity Sentence)))
      (SqlExpr (Entity LocIdBase))
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$
        \ (reasoning_attempts :: SqlExpr (Entity ReasoningAttempt)
reasoning_attempts `InnerJoin` proof_attempts :: SqlExpr (Entity ProofAttempt)
proof_attempts
                              `InnerJoin` sentences :: SqlExpr (Entity Sentence)
sentences
                              `InnerJoin` loc_id_bases_oms :: SqlExpr (Entity LocIdBase)
loc_id_bases_oms) -> do
          SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity LocIdBase)
loc_id_bases_oms SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseId
forall typ. (typ ~ LocIdBaseId) => EntityField LocIdBase typ
LocIdBaseId SqlExpr (Value LocIdBaseId)
-> SqlExpr (Value LocIdBaseId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
                 (SqlExpr (Entity Sentence)
sentences SqlExpr (Entity Sentence)
-> EntityField Sentence LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Sentence LocIdBaseId
forall typ. (typ ~ LocIdBaseId) => EntityField Sentence typ
SentenceOmsId)
          SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Value LocIdBaseId) -> SqlExpr (Value (Maybe LocIdBaseId))
forall typ. SqlExpr (Value typ) -> SqlExpr (Value (Maybe typ))
just (SqlExpr (Value (Key Sentence)) -> SqlExpr (Value LocIdBaseId)
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
coerceId (SqlExpr (Entity Sentence)
sentences SqlExpr (Entity Sentence)
-> EntityField Sentence (Key Sentence)
-> SqlExpr (Value (Key Sentence))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Sentence (Key Sentence)
forall typ. (typ ~ Key Sentence) => EntityField Sentence typ
SentenceId)) SqlExpr (Value (Maybe LocIdBaseId))
-> SqlExpr (Value (Maybe LocIdBaseId)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
                 SqlExpr (Entity ProofAttempt)
proof_attempts SqlExpr (Entity ProofAttempt)
-> EntityField ProofAttempt (Maybe LocIdBaseId)
-> SqlExpr (Value (Maybe LocIdBaseId))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ProofAttempt (Maybe LocIdBaseId)
forall typ.
(typ ~ Maybe LocIdBaseId) =>
EntityField ProofAttempt typ
ProofAttemptConjectureId
          SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity ProofAttempt)
proof_attempts SqlExpr (Entity ProofAttempt)
-> EntityField ProofAttempt (Key ProofAttempt)
-> SqlExpr (Value (Key ProofAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ProofAttempt (Key ProofAttempt)
forall typ.
(typ ~ Key ProofAttempt) =>
EntityField ProofAttempt typ
ProofAttemptId SqlExpr (Value (Key ProofAttempt))
-> SqlExpr (Value (Key ProofAttempt)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
                 SqlExpr (Value (Key ReasoningAttempt))
-> SqlExpr (Value (Key ProofAttempt))
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
coerceId (SqlExpr (Entity ReasoningAttempt)
reasoning_attempts SqlExpr (Entity ReasoningAttempt)
-> EntityField ReasoningAttempt (Key ReasoningAttempt)
-> SqlExpr (Value (Key ReasoningAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ReasoningAttempt (Key ReasoningAttempt)
forall typ.
(typ ~ Key ReasoningAttempt) =>
EntityField ReasoningAttempt typ
ReasoningAttemptId)
          SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity ReasoningAttempt)
reasoning_attempts SqlExpr (Entity ReasoningAttempt)
-> EntityField ReasoningAttempt (Key ReasoningAttempt)
-> SqlExpr (Value (Key ReasoningAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ReasoningAttempt (Key ReasoningAttempt)
forall typ.
(typ ~ Key ReasoningAttempt) =>
EntityField ReasoningAttempt typ
ReasoningAttemptId SqlExpr (Value (Key ReasoningAttempt))
-> SqlExpr (Value (Key ReasoningAttempt)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
                     Key ReasoningAttempt -> SqlExpr (Value (Key ReasoningAttempt))
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val Key ReasoningAttempt
reasoningAttemptKey
          Int64 -> SqlQuery ()
limit 1
          SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases_oms
      case [Entity LocIdBase]
omsL of
        [] -> String -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Persistence.Reasoning.postprocessReasoning: could not find OMS"
        omsEntity :: Entity LocIdBase
omsEntity : _ -> Entity LocIdBase -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity LocIdBase
omsEntity

    getConjectureFromReasoningAttempt :: (MonadIO m, Fail.MonadFail m)
                                      => DatabaseSchema.ReasoningAttemptId
                                      -> DBMonad m (Entity LocIdBase)
    getConjectureFromReasoningAttempt :: Key ReasoningAttempt -> DBMonad m (Entity LocIdBase)
getConjectureFromReasoningAttempt reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey = do
      [Entity LocIdBase]
conjectureL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (InnerJoin
   (InnerJoin
      (SqlExpr (Entity ReasoningAttempt))
      (SqlExpr (Entity ProofAttempt)))
   (SqlExpr (Entity LocIdBase))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((InnerJoin
    (InnerJoin
       (SqlExpr (Entity ReasoningAttempt))
       (SqlExpr (Entity ProofAttempt)))
    (SqlExpr (Entity LocIdBase))
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (InnerJoin
      (InnerJoin
         (SqlExpr (Entity ReasoningAttempt))
         (SqlExpr (Entity ProofAttempt)))
      (SqlExpr (Entity LocIdBase))
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$
        \ (reasoning_attempts :: SqlExpr (Entity ReasoningAttempt)
reasoning_attempts `InnerJoin` proof_attempts :: SqlExpr (Entity ProofAttempt)
proof_attempts
                              `InnerJoin` loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases) -> do
          SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Value LocIdBaseId) -> SqlExpr (Value (Maybe LocIdBaseId))
forall typ. SqlExpr (Value typ) -> SqlExpr (Value (Maybe typ))
just (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseId
forall typ. (typ ~ LocIdBaseId) => EntityField LocIdBase typ
LocIdBaseId) SqlExpr (Value (Maybe LocIdBaseId))
-> SqlExpr (Value (Maybe LocIdBaseId)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
                 SqlExpr (Entity ProofAttempt)
proof_attempts SqlExpr (Entity ProofAttempt)
-> EntityField ProofAttempt (Maybe LocIdBaseId)
-> SqlExpr (Value (Maybe LocIdBaseId))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ProofAttempt (Maybe LocIdBaseId)
forall typ.
(typ ~ Maybe LocIdBaseId) =>
EntityField ProofAttempt typ
ProofAttemptConjectureId
          SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity ProofAttempt)
proof_attempts SqlExpr (Entity ProofAttempt)
-> EntityField ProofAttempt (Key ProofAttempt)
-> SqlExpr (Value (Key ProofAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ProofAttempt (Key ProofAttempt)
forall typ.
(typ ~ Key ProofAttempt) =>
EntityField ProofAttempt typ
ProofAttemptId SqlExpr (Value (Key ProofAttempt))
-> SqlExpr (Value (Key ProofAttempt)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
                 SqlExpr (Value (Key ReasoningAttempt))
-> SqlExpr (Value (Key ProofAttempt))
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
coerceId (SqlExpr (Entity ReasoningAttempt)
reasoning_attempts SqlExpr (Entity ReasoningAttempt)
-> EntityField ReasoningAttempt (Key ReasoningAttempt)
-> SqlExpr (Value (Key ReasoningAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ReasoningAttempt (Key ReasoningAttempt)
forall typ.
(typ ~ Key ReasoningAttempt) =>
EntityField ReasoningAttempt typ
ReasoningAttemptId)
          SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity ReasoningAttempt)
reasoning_attempts SqlExpr (Entity ReasoningAttempt)
-> EntityField ReasoningAttempt (Key ReasoningAttempt)
-> SqlExpr (Value (Key ReasoningAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ReasoningAttempt (Key ReasoningAttempt)
forall typ.
(typ ~ Key ReasoningAttempt) =>
EntityField ReasoningAttempt typ
ReasoningAttemptId SqlExpr (Value (Key ReasoningAttempt))
-> SqlExpr (Value (Key ReasoningAttempt)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
                     Key ReasoningAttempt -> SqlExpr (Value (Key ReasoningAttempt))
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val Key ReasoningAttempt
reasoningAttemptKey
          Int64 -> SqlQuery ()
limit 1
          SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
      case [Entity LocIdBase]
conjectureL of
        [] -> String -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Persistence.Reasoning.postprocessReasoning: could not find Conjecture"
        conjectureEntity :: Entity LocIdBase
conjectureEntity : _ -> Entity LocIdBase -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity LocIdBase
conjectureEntity

    getUsedSentencesIds :: MonadIO m
                        => Entity LocIdBase
                        -> Maybe [String]
                        -> DBMonad m [LocIdBaseId] -- Sentence IDs
    getUsedSentencesIds :: Entity LocIdBase -> Maybe [String] -> DBMonad m [LocIdBaseId]
getUsedSentencesIds omsEntity :: Entity LocIdBase
omsEntity sentenceNamesM :: Maybe [String]
sentenceNamesM =
      case Maybe [String]
sentenceNamesM of
        Nothing -> [LocIdBaseId] -> DBMonad m [LocIdBaseId]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Just sentenceNames :: [String]
sentenceNames ->
          let sentenceLocIds :: [String]
sentenceLocIds = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Entity LocIdBase -> String -> String
locIdOfSentence Entity LocIdBase
omsEntity) [String]
sentenceNames
          in  do
                [Entity LocIdBase]
sentences <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LocIdBase)
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LocIdBase)
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (SqlExpr (Entity LocIdBase)
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ \ loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases -> do
                  SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase String
forall typ. (typ ~ String) => EntityField LocIdBase typ
LocIdBaseLocId SqlExpr (Value String)
-> SqlExpr (ValueList String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ)
-> SqlExpr (ValueList typ) -> SqlExpr (Value Bool)
`in_` [String] -> SqlExpr (ValueList String)
forall typ. PersistField typ => [typ] -> SqlExpr (ValueList typ)
valList [String]
sentenceLocIds
                  SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
                [LocIdBaseId] -> DBMonad m [LocIdBaseId]
forall (m :: * -> *) a. Monad m => a -> m a
return ([LocIdBaseId] -> DBMonad m [LocIdBaseId])
-> [LocIdBaseId] -> DBMonad m [LocIdBaseId]
forall a b. (a -> b) -> a -> b
$ (Entity LocIdBase -> LocIdBaseId)
-> [Entity LocIdBase] -> [LocIdBaseId]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Entity sentenceKey :: LocIdBaseId
sentenceKey _) -> LocIdBaseId
sentenceKey) [Entity LocIdBase]
sentences

    finishReasoningAttempt :: MonadIO m
                           => Entity DatabaseSchema.ReasoningAttempt
                           -> Maybe Int
                           -> DBMonad m ()
    finishReasoningAttempt :: Entity ReasoningAttempt -> Maybe Int -> DBMonad m ()
finishReasoningAttempt (Entity reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey reasoningAttemptValue :: ReasoningAttempt
reasoningAttemptValue) timeTakenM :: Maybe Int
timeTakenM = do
        Key Action -> [Update Action] -> DBMonad m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
Key record -> [Update record] -> ReaderT backend m ()
update (ReasoningAttempt -> Key Action
reasoningAttemptActionId ReasoningAttempt
reasoningAttemptValue)
               [ EntityField Action EvaluationStateType
forall typ. (typ ~ EvaluationStateType) => EntityField Action typ
ActionEvaluationState EntityField Action EvaluationStateType
-> EvaluationStateType -> Update Action
forall v typ.
PersistField typ =>
EntityField v typ -> typ -> Update v
=. EvaluationStateType
EvaluationStateType.FinishedSuccessfully
               , EntityField Action (Maybe Text)
forall typ. (typ ~ Maybe Text) => EntityField Action typ
ActionMessage EntityField Action (Maybe Text) -> Maybe Text -> Update Action
forall v typ.
PersistField typ =>
EntityField v typ -> typ -> Update v
=. Maybe Text
forall a. Maybe a
Nothing
               ]
        Key ReasoningAttempt -> [Update ReasoningAttempt] -> DBMonad m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
Key record -> [Update record] -> ReaderT backend m ()
update Key ReasoningAttempt
reasoningAttemptKey [EntityField ReasoningAttempt (Maybe Int)
forall typ. (typ ~ Maybe Int) => EntityField ReasoningAttempt typ
ReasoningAttemptTimeTaken EntityField ReasoningAttempt (Maybe Int)
-> Maybe Int -> Update ReasoningAttempt
forall v typ.
PersistField typ =>
EntityField v typ -> typ -> Update v
=. Maybe Int
timeTakenM]
        () -> DBMonad m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    updateConsistencyCheckAttempt :: MonadIO m
                                  => DatabaseSchema.ReasoningAttemptId
                                  -> ConsistencyStatusType.ConsistencyStatusType
                                  -> DBMonad m ()
    updateConsistencyCheckAttempt :: Key ReasoningAttempt -> ConsistencyStatusType -> DBMonad m ()
updateConsistencyCheckAttempt reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey consistencyStatus_ :: ConsistencyStatusType
consistencyStatus_ =
      Key ConsistencyCheckAttempt
-> [Update ConsistencyCheckAttempt] -> DBMonad m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
Key record -> [Update record] -> ReaderT backend m ()
update (Int64 -> Key ConsistencyCheckAttempt
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key ConsistencyCheckAttempt)
-> Int64 -> Key ConsistencyCheckAttempt
forall a b. (a -> b) -> a -> b
$ Key ReasoningAttempt -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey Key ReasoningAttempt
reasoningAttemptKey :: DatabaseSchema.ConsistencyCheckAttemptId)
             [ EntityField ConsistencyCheckAttempt ConsistencyStatusType
forall typ.
(typ ~ ConsistencyStatusType) =>
EntityField ConsistencyCheckAttempt typ
ConsistencyCheckAttemptConsistencyStatus EntityField ConsistencyCheckAttempt ConsistencyStatusType
-> ConsistencyStatusType -> Update ConsistencyCheckAttempt
forall v typ.
PersistField typ =>
EntityField v typ -> typ -> Update v
=. ConsistencyStatusType
consistencyStatus_
             ]

    updateProofAttempt :: MonadIO m
                       => DatabaseSchema.ReasoningAttemptId
                       -> Enums.ProofStatusType
                       -> [LocIdBaseId]
                       -> DBMonad m ()
    updateProofAttempt :: Key ReasoningAttempt
-> ProofStatusType -> [LocIdBaseId] -> DBMonad m ()
updateProofAttempt reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey proofStatus :: ProofStatusType
proofStatus usedSentencesIds :: [LocIdBaseId]
usedSentencesIds = do
      Key ProofAttempt -> [Update ProofAttempt] -> DBMonad m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
Key record -> [Update record] -> ReaderT backend m ()
update (Int64 -> Key ProofAttempt
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key ProofAttempt) -> Int64 -> Key ProofAttempt
forall a b. (a -> b) -> a -> b
$ Key ReasoningAttempt -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey Key ReasoningAttempt
reasoningAttemptKey)
             [ EntityField ProofAttempt ProofStatusType
forall typ. (typ ~ ProofStatusType) => EntityField ProofAttempt typ
ProofAttemptProofStatus EntityField ProofAttempt ProofStatusType
-> ProofStatusType -> Update ProofAttempt
forall v typ.
PersistField typ =>
EntityField v typ -> typ -> Update v
=. ProofStatusType
proofStatus
             ]
      (LocIdBaseId
 -> ReaderT SqlBackend m (Key ProofAttemptUsedSentence))
-> [LocIdBaseId] -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ sentenceKey :: LocIdBaseId
sentenceKey -> ProofAttemptUsedSentence
-> ReaderT SqlBackend m (Key ProofAttemptUsedSentence)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WProofAttemptUsedSentence :: Key ProofAttempt -> LocIdBaseId -> ProofAttemptUsedSentence
ProofAttemptUsedSentence
              { proofAttemptUsedSentenceProofAttemptId :: Key ProofAttempt
proofAttemptUsedSentenceProofAttemptId =
                  Int64 -> Key ProofAttempt
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key ProofAttempt) -> Int64 -> Key ProofAttempt
forall a b. (a -> b) -> a -> b
$ Key ReasoningAttempt -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey Key ReasoningAttempt
reasoningAttemptKey
              , proofAttemptUsedSentenceSentenceId :: LocIdBaseId
proofAttemptUsedSentenceSentenceId = LocIdBaseId
sentenceKey
              }
            ) [LocIdBaseId]
usedSentencesIds

fetchOmsEvaluationStates :: MonadIO m
                         => Entity DatabaseSchema.LocIdBase
                         -> DBMonad m [EvaluationStateType.EvaluationStateType]
fetchOmsEvaluationStates :: Entity LocIdBase -> DBMonad m [EvaluationStateType]
fetchOmsEvaluationStates (Entity omsKey :: LocIdBaseId
omsKey _) = do
  [Entity Action]
actions <- SqlQuery (SqlExpr (Entity Action))
-> ReaderT SqlBackend m [Entity Action]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Action))
 -> ReaderT SqlBackend m [Entity Action])
-> SqlQuery (SqlExpr (Entity Action))
-> ReaderT SqlBackend m [Entity Action]
forall a b. (a -> b) -> a -> b
$ (InnerJoin
   (InnerJoin
      (InnerJoin
         (SqlExpr (Entity Action)) (SqlExpr (Entity ReasoningAttempt)))
      (SqlExpr (Entity ConsistencyCheckAttempt)))
   (SqlExpr (Entity LocIdBase))
 -> SqlQuery (SqlExpr (Entity Action)))
-> SqlQuery (SqlExpr (Entity Action))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((InnerJoin
    (InnerJoin
       (InnerJoin
          (SqlExpr (Entity Action)) (SqlExpr (Entity ReasoningAttempt)))
       (SqlExpr (Entity ConsistencyCheckAttempt)))
    (SqlExpr (Entity LocIdBase))
  -> SqlQuery (SqlExpr (Entity Action)))
 -> SqlQuery (SqlExpr (Entity Action)))
-> (InnerJoin
      (InnerJoin
         (InnerJoin
            (SqlExpr (Entity Action)) (SqlExpr (Entity ReasoningAttempt)))
         (SqlExpr (Entity ConsistencyCheckAttempt)))
      (SqlExpr (Entity LocIdBase))
    -> SqlQuery (SqlExpr (Entity Action)))
-> SqlQuery (SqlExpr (Entity Action))
forall a b. (a -> b) -> a -> b
$ \ (actions :: SqlExpr (Entity Action)
actions `InnerJoin` reasoning_attempts :: SqlExpr (Entity ReasoningAttempt)
reasoning_attempts
                                        `InnerJoin` consistency_check_attempts :: SqlExpr (Entity ConsistencyCheckAttempt)
consistency_check_attempts
                                        `InnerJoin` loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases) -> do
    SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Value LocIdBaseId) -> SqlExpr (Value (Maybe LocIdBaseId))
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
coerceId(SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseId
forall typ. (typ ~ LocIdBaseId) => EntityField LocIdBase typ
LocIdBaseId) SqlExpr (Value (Maybe LocIdBaseId))
-> SqlExpr (Value (Maybe LocIdBaseId)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
           SqlExpr (Entity ConsistencyCheckAttempt)
consistency_check_attempts SqlExpr (Entity ConsistencyCheckAttempt)
-> EntityField ConsistencyCheckAttempt (Maybe LocIdBaseId)
-> SqlExpr (Value (Maybe LocIdBaseId))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ConsistencyCheckAttempt (Maybe LocIdBaseId)
forall typ.
(typ ~ Maybe LocIdBaseId) =>
EntityField ConsistencyCheckAttempt typ
ConsistencyCheckAttemptOmsId
    SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Value (Key ConsistencyCheckAttempt))
-> SqlExpr (Value (Key ReasoningAttempt))
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
coerceId (SqlExpr (Entity ConsistencyCheckAttempt)
consistency_check_attempts SqlExpr (Entity ConsistencyCheckAttempt)
-> EntityField
     ConsistencyCheckAttempt (Key ConsistencyCheckAttempt)
-> SqlExpr (Value (Key ConsistencyCheckAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ConsistencyCheckAttempt (Key ConsistencyCheckAttempt)
forall typ.
(typ ~ Key ConsistencyCheckAttempt) =>
EntityField ConsistencyCheckAttempt typ
ConsistencyCheckAttemptId) SqlExpr (Value (Key ReasoningAttempt))
-> SqlExpr (Value (Key ReasoningAttempt)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
           SqlExpr (Entity ReasoningAttempt)
reasoning_attempts SqlExpr (Entity ReasoningAttempt)
-> EntityField ReasoningAttempt (Key ReasoningAttempt)
-> SqlExpr (Value (Key ReasoningAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ReasoningAttempt (Key ReasoningAttempt)
forall typ.
(typ ~ Key ReasoningAttempt) =>
EntityField ReasoningAttempt typ
ReasoningAttemptId
    SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity ReasoningAttempt)
reasoning_attempts SqlExpr (Entity ReasoningAttempt)
-> EntityField ReasoningAttempt (Key Action)
-> SqlExpr (Value (Key Action))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ReasoningAttempt (Key Action)
forall typ. (typ ~ Key Action) => EntityField ReasoningAttempt typ
ReasoningAttemptActionId SqlExpr (Value (Key Action))
-> SqlExpr (Value (Key Action)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
           SqlExpr (Entity Action)
actions SqlExpr (Entity Action)
-> EntityField Action (Key Action) -> SqlExpr (Value (Key Action))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Action (Key Action)
forall typ. (typ ~ Key Action) => EntityField Action typ
ActionId
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseId
forall typ. (typ ~ LocIdBaseId) => EntityField LocIdBase typ
LocIdBaseId SqlExpr (Value LocIdBaseId)
-> SqlExpr (Value LocIdBaseId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseId
omsKey
    SqlExpr (Entity Action) -> SqlQuery (SqlExpr (Entity Action))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Action)
actions
  [EvaluationStateType] -> DBMonad m [EvaluationStateType]
forall (m :: * -> *) a. Monad m => a -> m a
return ([EvaluationStateType] -> DBMonad m [EvaluationStateType])
-> [EvaluationStateType] -> DBMonad m [EvaluationStateType]
forall a b. (a -> b) -> a -> b
$ (Entity Action -> EvaluationStateType)
-> [Entity Action] -> [EvaluationStateType]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Entity _ actionValue :: Action
actionValue) ->
                 Action -> EvaluationStateType
actionEvaluationState Action
actionValue
               ) [Entity Action]
actions

fetchConsistencyStatuses :: MonadIO m
                         => Entity DatabaseSchema.LocIdBase
                         -> DBMonad m [ConsistencyStatusType.ConsistencyStatusType]
fetchConsistencyStatuses :: Entity LocIdBase -> DBMonad m [ConsistencyStatusType]
fetchConsistencyStatuses (Entity omsKey :: LocIdBaseId
omsKey _) = do
  [Entity ConsistencyCheckAttempt]
consistencyCheckAttempts <- SqlQuery (SqlExpr (Entity ConsistencyCheckAttempt))
-> ReaderT SqlBackend m [Entity ConsistencyCheckAttempt]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity ConsistencyCheckAttempt))
 -> ReaderT SqlBackend m [Entity ConsistencyCheckAttempt])
-> SqlQuery (SqlExpr (Entity ConsistencyCheckAttempt))
-> ReaderT SqlBackend m [Entity ConsistencyCheckAttempt]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity ConsistencyCheckAttempt)
 -> SqlQuery (SqlExpr (Entity ConsistencyCheckAttempt)))
-> SqlQuery (SqlExpr (Entity ConsistencyCheckAttempt))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity ConsistencyCheckAttempt)
  -> SqlQuery (SqlExpr (Entity ConsistencyCheckAttempt)))
 -> SqlQuery (SqlExpr (Entity ConsistencyCheckAttempt)))
-> (SqlExpr (Entity ConsistencyCheckAttempt)
    -> SqlQuery (SqlExpr (Entity ConsistencyCheckAttempt)))
-> SqlQuery (SqlExpr (Entity ConsistencyCheckAttempt))
forall a b. (a -> b) -> a -> b
$ \ consistency_check_attempts :: SqlExpr (Entity ConsistencyCheckAttempt)
consistency_check_attempts -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity ConsistencyCheckAttempt)
consistency_check_attempts SqlExpr (Entity ConsistencyCheckAttempt)
-> EntityField ConsistencyCheckAttempt (Maybe LocIdBaseId)
-> SqlExpr (Value (Maybe LocIdBaseId))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ConsistencyCheckAttempt (Maybe LocIdBaseId)
forall typ.
(typ ~ Maybe LocIdBaseId) =>
EntityField ConsistencyCheckAttempt typ
ConsistencyCheckAttemptOmsId SqlExpr (Value (Maybe LocIdBaseId))
-> SqlExpr (Value (Maybe LocIdBaseId)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
               SqlExpr (Value LocIdBaseId) -> SqlExpr (Value (Maybe LocIdBaseId))
forall typ. SqlExpr (Value typ) -> SqlExpr (Value (Maybe typ))
just (LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseId
omsKey)
    SqlExpr (Entity ConsistencyCheckAttempt)
-> SqlQuery (SqlExpr (Entity ConsistencyCheckAttempt))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity ConsistencyCheckAttempt)
consistency_check_attempts
  [ConsistencyStatusType] -> DBMonad m [ConsistencyStatusType]
forall (m :: * -> *) a. Monad m => a -> m a
return ([ConsistencyStatusType] -> DBMonad m [ConsistencyStatusType])
-> [ConsistencyStatusType] -> DBMonad m [ConsistencyStatusType]
forall a b. (a -> b) -> a -> b
$ (Entity ConsistencyCheckAttempt -> ConsistencyStatusType)
-> [Entity ConsistencyCheckAttempt] -> [ConsistencyStatusType]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Entity _ consistencyCheckAttemptValue :: ConsistencyCheckAttempt
consistencyCheckAttemptValue) ->
                 ConsistencyCheckAttempt -> ConsistencyStatusType
consistencyCheckAttemptConsistencyStatus ConsistencyCheckAttempt
consistencyCheckAttemptValue
               ) [Entity ConsistencyCheckAttempt]
consistencyCheckAttempts

fetchProofStatuses :: MonadIO m
                   => Entity DatabaseSchema.LocIdBase
                   -> DBMonad m [Enums.ProofStatusType]
fetchProofStatuses :: Entity LocIdBase -> DBMonad m [ProofStatusType]
fetchProofStatuses (Entity conjectureKey :: LocIdBaseId
conjectureKey _) = do
  [Entity ProofAttempt]
proofAttempts <- SqlQuery (SqlExpr (Entity ProofAttempt))
-> ReaderT SqlBackend m [Entity ProofAttempt]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity ProofAttempt))
 -> ReaderT SqlBackend m [Entity ProofAttempt])
-> SqlQuery (SqlExpr (Entity ProofAttempt))
-> ReaderT SqlBackend m [Entity ProofAttempt]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity ProofAttempt)
 -> SqlQuery (SqlExpr (Entity ProofAttempt)))
-> SqlQuery (SqlExpr (Entity ProofAttempt))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity ProofAttempt)
  -> SqlQuery (SqlExpr (Entity ProofAttempt)))
 -> SqlQuery (SqlExpr (Entity ProofAttempt)))
-> (SqlExpr (Entity ProofAttempt)
    -> SqlQuery (SqlExpr (Entity ProofAttempt)))
-> SqlQuery (SqlExpr (Entity ProofAttempt))
forall a b. (a -> b) -> a -> b
$ \ proof_attempts :: SqlExpr (Entity ProofAttempt)
proof_attempts -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity ProofAttempt)
proof_attempts SqlExpr (Entity ProofAttempt)
-> EntityField ProofAttempt (Maybe LocIdBaseId)
-> SqlExpr (Value (Maybe LocIdBaseId))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ProofAttempt (Maybe LocIdBaseId)
forall typ.
(typ ~ Maybe LocIdBaseId) =>
EntityField ProofAttempt typ
ProofAttemptConjectureId SqlExpr (Value (Maybe LocIdBaseId))
-> SqlExpr (Value (Maybe LocIdBaseId)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. SqlExpr (Value LocIdBaseId) -> SqlExpr (Value (Maybe LocIdBaseId))
forall typ. SqlExpr (Value typ) -> SqlExpr (Value (Maybe typ))
just (LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseId
conjectureKey)
    SqlExpr (Entity ProofAttempt)
-> SqlQuery (SqlExpr (Entity ProofAttempt))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity ProofAttempt)
proof_attempts
  [ProofStatusType] -> DBMonad m [ProofStatusType]
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProofStatusType] -> DBMonad m [ProofStatusType])
-> [ProofStatusType] -> DBMonad m [ProofStatusType]
forall a b. (a -> b) -> a -> b
$ (Entity ProofAttempt -> ProofStatusType)
-> [Entity ProofAttempt] -> [ProofStatusType]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Entity _ proofAttemptValue :: ProofAttempt
proofAttemptValue) ->
                 ProofAttempt -> ProofStatusType
proofAttemptProofStatus ProofAttempt
proofAttemptValue
               ) [Entity ProofAttempt]
proofAttempts

fetchConjectureEvaluationStates :: MonadIO m
                                => Entity DatabaseSchema.LocIdBase
                                -> DBMonad m [EvaluationStateType.EvaluationStateType]
fetchConjectureEvaluationStates :: Entity LocIdBase -> DBMonad m [EvaluationStateType]
fetchConjectureEvaluationStates (Entity conjectureKey :: LocIdBaseId
conjectureKey _) = do
  [Entity Action]
actions <- SqlQuery (SqlExpr (Entity Action))
-> ReaderT SqlBackend m [Entity Action]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Action))
 -> ReaderT SqlBackend m [Entity Action])
-> SqlQuery (SqlExpr (Entity Action))
-> ReaderT SqlBackend m [Entity Action]
forall a b. (a -> b) -> a -> b
$ (InnerJoin
   (InnerJoin
      (InnerJoin
         (SqlExpr (Entity Action)) (SqlExpr (Entity ReasoningAttempt)))
      (SqlExpr (Entity ProofAttempt)))
   (SqlExpr (Entity LocIdBase))
 -> SqlQuery (SqlExpr (Entity Action)))
-> SqlQuery (SqlExpr (Entity Action))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((InnerJoin
    (InnerJoin
       (InnerJoin
          (SqlExpr (Entity Action)) (SqlExpr (Entity ReasoningAttempt)))
       (SqlExpr (Entity ProofAttempt)))
    (SqlExpr (Entity LocIdBase))
  -> SqlQuery (SqlExpr (Entity Action)))
 -> SqlQuery (SqlExpr (Entity Action)))
-> (InnerJoin
      (InnerJoin
         (InnerJoin
            (SqlExpr (Entity Action)) (SqlExpr (Entity ReasoningAttempt)))
         (SqlExpr (Entity ProofAttempt)))
      (SqlExpr (Entity LocIdBase))
    -> SqlQuery (SqlExpr (Entity Action)))
-> SqlQuery (SqlExpr (Entity Action))
forall a b. (a -> b) -> a -> b
$ \ (actions :: SqlExpr (Entity Action)
actions `InnerJoin` reasoning_attempts :: SqlExpr (Entity ReasoningAttempt)
reasoning_attempts
                                        `InnerJoin` proof_attempts :: SqlExpr (Entity ProofAttempt)
proof_attempts
                                        `InnerJoin` loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases) -> do
    SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Value LocIdBaseId) -> SqlExpr (Value (Maybe LocIdBaseId))
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
coerceId(SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseId
forall typ. (typ ~ LocIdBaseId) => EntityField LocIdBase typ
LocIdBaseId) SqlExpr (Value (Maybe LocIdBaseId))
-> SqlExpr (Value (Maybe LocIdBaseId)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
           SqlExpr (Entity ProofAttempt)
proof_attempts SqlExpr (Entity ProofAttempt)
-> EntityField ProofAttempt (Maybe LocIdBaseId)
-> SqlExpr (Value (Maybe LocIdBaseId))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ProofAttempt (Maybe LocIdBaseId)
forall typ.
(typ ~ Maybe LocIdBaseId) =>
EntityField ProofAttempt typ
ProofAttemptConjectureId
    SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Value (Key ProofAttempt))
-> SqlExpr (Value (Key ReasoningAttempt))
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
coerceId (SqlExpr (Entity ProofAttempt)
proof_attempts SqlExpr (Entity ProofAttempt)
-> EntityField ProofAttempt (Key ProofAttempt)
-> SqlExpr (Value (Key ProofAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ProofAttempt (Key ProofAttempt)
forall typ.
(typ ~ Key ProofAttempt) =>
EntityField ProofAttempt typ
ProofAttemptId) SqlExpr (Value (Key ReasoningAttempt))
-> SqlExpr (Value (Key ReasoningAttempt)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
           SqlExpr (Entity ReasoningAttempt)
reasoning_attempts SqlExpr (Entity ReasoningAttempt)
-> EntityField ReasoningAttempt (Key ReasoningAttempt)
-> SqlExpr (Value (Key ReasoningAttempt))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ReasoningAttempt (Key ReasoningAttempt)
forall typ.
(typ ~ Key ReasoningAttempt) =>
EntityField ReasoningAttempt typ
ReasoningAttemptId
    SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity ReasoningAttempt)
reasoning_attempts SqlExpr (Entity ReasoningAttempt)
-> EntityField ReasoningAttempt (Key Action)
-> SqlExpr (Value (Key Action))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField ReasoningAttempt (Key Action)
forall typ. (typ ~ Key Action) => EntityField ReasoningAttempt typ
ReasoningAttemptActionId SqlExpr (Value (Key Action))
-> SqlExpr (Value (Key Action)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==.
           SqlExpr (Entity Action)
actions SqlExpr (Entity Action)
-> EntityField Action (Key Action) -> SqlExpr (Value (Key Action))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Action (Key Action)
forall typ. (typ ~ Key Action) => EntityField Action typ
ActionId
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseId
forall typ. (typ ~ LocIdBaseId) => EntityField LocIdBase typ
LocIdBaseId SqlExpr (Value LocIdBaseId)
-> SqlExpr (Value LocIdBaseId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseId
conjectureKey
    SqlExpr (Entity Action) -> SqlQuery (SqlExpr (Entity Action))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Action)
actions
  [EvaluationStateType] -> DBMonad m [EvaluationStateType]
forall (m :: * -> *) a. Monad m => a -> m a
return ([EvaluationStateType] -> DBMonad m [EvaluationStateType])
-> [EvaluationStateType] -> DBMonad m [EvaluationStateType]
forall a b. (a -> b) -> a -> b
$ (Entity Action -> EvaluationStateType)
-> [Entity Action] -> [EvaluationStateType]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Entity _ actionValue :: Action
actionValue) ->
                 Action -> EvaluationStateType
actionEvaluationState Action
actionValue
               ) [Entity Action]
actions

chooseEvaluationState :: [EvaluationStateType.EvaluationStateType]
                      -> EvaluationStateType.EvaluationStateType
chooseEvaluationState :: [EvaluationStateType] -> EvaluationStateType
chooseEvaluationState =
  let ordering :: [EvaluationStateType]
ordering = [ EvaluationStateType
EvaluationStateType.FinishedUnsuccessfully
                 , EvaluationStateType
EvaluationStateType.FinishedSuccessfully
                 , EvaluationStateType
EvaluationStateType.NotYetEnqueued
                 , EvaluationStateType
EvaluationStateType.Enqueued
                 , EvaluationStateType
EvaluationStateType.Processing
                 ]
  in  (EvaluationStateType -> EvaluationStateType -> Ordering)
-> [EvaluationStateType] -> EvaluationStateType
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy (\ a :: EvaluationStateType
a b :: EvaluationStateType
b -> Maybe Int -> Maybe Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (EvaluationStateType -> [EvaluationStateType] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex EvaluationStateType
a [EvaluationStateType]
ordering) (EvaluationStateType -> [EvaluationStateType] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex EvaluationStateType
b [EvaluationStateType]
ordering))

chooseConsistencyStatus :: [ConsistencyStatusType.ConsistencyStatusType]
                        -> ConsistencyStatusType.ConsistencyStatusType
chooseConsistencyStatus :: [ConsistencyStatusType] -> ConsistencyStatusType
chooseConsistencyStatus statuses :: [ConsistencyStatusType]
statuses =
  if ConsistencyStatusType
ConsistencyStatusType.Consistent ConsistencyStatusType -> [ConsistencyStatusType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ConsistencyStatusType]
statuses Bool -> Bool -> Bool
&&
       ConsistencyStatusType
ConsistencyStatusType.Inconsistent ConsistencyStatusType -> [ConsistencyStatusType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ConsistencyStatusType]
statuses
  then ConsistencyStatusType
ConsistencyStatusType.Contradictory
  else let ordering :: [ConsistencyStatusType]
ordering = [ ConsistencyStatusType
ConsistencyStatusType.Open
                      , ConsistencyStatusType
ConsistencyStatusType.Timeout
                      , ConsistencyStatusType
ConsistencyStatusType.Error
                      , ConsistencyStatusType
ConsistencyStatusType.Inconsistent
                      , ConsistencyStatusType
ConsistencyStatusType.Consistent
                      , ConsistencyStatusType
ConsistencyStatusType.Contradictory
                      ]
           fixOrdering :: ConsistencyStatusType -> ConsistencyStatusType -> Ordering
fixOrdering a :: ConsistencyStatusType
a b :: ConsistencyStatusType
b =
             Maybe Int -> Maybe Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (ConsistencyStatusType -> [ConsistencyStatusType] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex ConsistencyStatusType
a [ConsistencyStatusType]
ordering) (ConsistencyStatusType -> [ConsistencyStatusType] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex ConsistencyStatusType
b [ConsistencyStatusType]
ordering)
       in  (ConsistencyStatusType -> ConsistencyStatusType -> Ordering)
-> [ConsistencyStatusType] -> ConsistencyStatusType
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy ConsistencyStatusType -> ConsistencyStatusType -> Ordering
fixOrdering [ConsistencyStatusType]
statuses

chooseProofStatus :: [Enums.ProofStatusType] -> Enums.ProofStatusType
chooseProofStatus :: [ProofStatusType] -> ProofStatusType
chooseProofStatus statuses :: [ProofStatusType]
statuses =
  if ProofStatusType
Enums.THM ProofStatusType -> [ProofStatusType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ProofStatusType]
statuses Bool -> Bool -> Bool
&& ProofStatusType
Enums.CSA ProofStatusType -> [ProofStatusType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ProofStatusType]
statuses
  then ProofStatusType
Enums.CONTR
  else let ordering :: [ProofStatusType]
ordering = [ ProofStatusType
Enums.OPN
                      , ProofStatusType
Enums.UNK
                      , ProofStatusType
Enums.RSO
                      , ProofStatusType
Enums.ERR
                      , ProofStatusType
Enums.CSAS
                      , ProofStatusType
Enums.CSA
                      , ProofStatusType
Enums.THM
                      , ProofStatusType
Enums.CONTR
                      ]
           fixOrdering :: ProofStatusType -> ProofStatusType -> Ordering
fixOrdering a :: ProofStatusType
a b :: ProofStatusType
b =
             Maybe Int -> Maybe Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (ProofStatusType -> [ProofStatusType] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex ProofStatusType
a [ProofStatusType]
ordering) (ProofStatusType -> [ProofStatusType] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex ProofStatusType
b [ProofStatusType]
ordering)
       in  (ProofStatusType -> ProofStatusType -> Ordering)
-> [ProofStatusType] -> ProofStatusType
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy ProofStatusType -> ProofStatusType -> Ordering
fixOrdering [ProofStatusType]
statuses

setOmsEvaluationState :: (MonadIO m, Fail.MonadFail m)
                      => Entity DatabaseSchema.LocIdBase
                      -> EvaluationStateType.EvaluationStateType
                      -> DBMonad m ()
setOmsEvaluationState :: Entity LocIdBase -> EvaluationStateType -> DBMonad m ()
setOmsEvaluationState (Entity omsKey :: LocIdBaseId
omsKey _) evaluationState :: EvaluationStateType
evaluationState = do
  [Entity Action]
actionL <- SqlQuery (SqlExpr (Entity Action))
-> ReaderT SqlBackend m [Entity Action]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Action))
 -> ReaderT SqlBackend m [Entity Action])
-> SqlQuery (SqlExpr (Entity Action))
-> ReaderT SqlBackend m [Entity Action]
forall a b. (a -> b) -> a -> b
$ (InnerJoin (SqlExpr (Entity Action)) (SqlExpr (Entity OMS))
 -> SqlQuery (SqlExpr (Entity Action)))
-> SqlQuery (SqlExpr (Entity Action))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((InnerJoin (SqlExpr (Entity Action)) (SqlExpr (Entity OMS))
  -> SqlQuery (SqlExpr (Entity Action)))
 -> SqlQuery (SqlExpr (Entity Action)))
-> (InnerJoin (SqlExpr (Entity Action)) (SqlExpr (Entity OMS))
    -> SqlQuery (SqlExpr (Entity Action)))
-> SqlQuery (SqlExpr (Entity Action))
forall a b. (a -> b) -> a -> b
$ \ (actions :: SqlExpr (Entity Action)
actions `InnerJoin` oms :: SqlExpr (Entity OMS)
oms) -> do
    SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity Action)
actions SqlExpr (Entity Action)
-> EntityField Action (Key Action) -> SqlExpr (Value (Key Action))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Action (Key Action)
forall typ. (typ ~ Key Action) => EntityField Action typ
ActionId SqlExpr (Value (Key Action))
-> SqlExpr (Value (Key Action)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. SqlExpr (Entity OMS)
oms SqlExpr (Entity OMS)
-> EntityField OMS (Key Action) -> SqlExpr (Value (Key Action))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField OMS (Key Action)
forall typ. (typ ~ Key Action) => EntityField OMS typ
OMSActionId
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity OMS)
oms SqlExpr (Entity OMS)
-> EntityField OMS (Key OMS) -> SqlExpr (Value (Key OMS))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField OMS (Key OMS)
forall typ. (typ ~ Key OMS) => EntityField OMS typ
OMSId SqlExpr (Value (Key OMS))
-> SqlExpr (Value (Key OMS)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. Key OMS -> SqlExpr (Value (Key OMS))
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val (Int64 -> Key OMS
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key OMS) -> Int64 -> Key OMS
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
omsKey)
    Int64 -> SqlQuery ()
limit 1
    SqlExpr (Entity Action) -> SqlQuery (SqlExpr (Entity Action))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Action)
actions
  (Entity actionKey :: Key Action
actionKey _) <- case [Entity Action]
actionL of
    [] -> String -> ReaderT SqlBackend m (Entity Action)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Persistence.Reasoning.setOmsEvaluationState: Could not find Action"
    actionEntity :: Entity Action
actionEntity : _ -> Entity Action -> ReaderT SqlBackend m (Entity Action)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity Action
actionEntity
  Key Action -> [Update Action] -> DBMonad m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
Key record -> [Update record] -> ReaderT backend m ()
update Key Action
actionKey [EntityField Action EvaluationStateType
forall typ. (typ ~ EvaluationStateType) => EntityField Action typ
ActionEvaluationState EntityField Action EvaluationStateType
-> EvaluationStateType -> Update Action
forall v typ.
PersistField typ =>
EntityField v typ -> typ -> Update v
=. EvaluationStateType
evaluationState]
  () -> DBMonad m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

setConjectureEvaluationState :: (MonadIO m, Fail.MonadFail m)
                             => Entity DatabaseSchema.LocIdBase
                             -> EvaluationStateType.EvaluationStateType
                             -> DBMonad m ()
setConjectureEvaluationState :: Entity LocIdBase -> EvaluationStateType -> DBMonad m ()
setConjectureEvaluationState (Entity conjectureKey :: LocIdBaseId
conjectureKey _) evaluationState :: EvaluationStateType
evaluationState = do
  [Entity Action]
actionL <- SqlQuery (SqlExpr (Entity Action))
-> ReaderT SqlBackend m [Entity Action]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Action))
 -> ReaderT SqlBackend m [Entity Action])
-> SqlQuery (SqlExpr (Entity Action))
-> ReaderT SqlBackend m [Entity Action]
forall a b. (a -> b) -> a -> b
$ (InnerJoin (SqlExpr (Entity Action)) (SqlExpr (Entity Conjecture))
 -> SqlQuery (SqlExpr (Entity Action)))
-> SqlQuery (SqlExpr (Entity Action))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((InnerJoin (SqlExpr (Entity Action)) (SqlExpr (Entity Conjecture))
  -> SqlQuery (SqlExpr (Entity Action)))
 -> SqlQuery (SqlExpr (Entity Action)))
-> (InnerJoin
      (SqlExpr (Entity Action)) (SqlExpr (Entity Conjecture))
    -> SqlQuery (SqlExpr (Entity Action)))
-> SqlQuery (SqlExpr (Entity Action))
forall a b. (a -> b) -> a -> b
$ \ (actions :: SqlExpr (Entity Action)
actions `InnerJoin` conjectures :: SqlExpr (Entity Conjecture)
conjectures) -> do
    SqlExpr (Value Bool) -> SqlQuery ()
on (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity Action)
actions SqlExpr (Entity Action)
-> EntityField Action (Key Action) -> SqlExpr (Value (Key Action))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Action (Key Action)
forall typ. (typ ~ Key Action) => EntityField Action typ
ActionId SqlExpr (Value (Key Action))
-> SqlExpr (Value (Key Action)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. SqlExpr (Entity Conjecture)
conjectures SqlExpr (Entity Conjecture)
-> EntityField Conjecture (Key Action)
-> SqlExpr (Value (Key Action))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Conjecture (Key Action)
forall typ. (typ ~ Key Action) => EntityField Conjecture typ
ConjectureActionId
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Entity Conjecture)
conjectures SqlExpr (Entity Conjecture)
-> EntityField Conjecture (Key Conjecture)
-> SqlExpr (Value (Key Conjecture))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Conjecture (Key Conjecture)
forall typ. (typ ~ Key Conjecture) => EntityField Conjecture typ
ConjectureId SqlExpr (Value (Key Conjecture))
-> SqlExpr (Value (Key Conjecture)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. Key Conjecture -> SqlExpr (Value (Key Conjecture))
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val (Int64 -> Key Conjecture
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key Conjecture) -> Int64 -> Key Conjecture
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
conjectureKey)
    Int64 -> SqlQuery ()
limit 1
    SqlExpr (Entity Action) -> SqlQuery (SqlExpr (Entity Action))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Action)
actions
  (Entity actionKey :: Key Action
actionKey _) <- case [Entity Action]
actionL of
    [] -> String -> ReaderT SqlBackend m (Entity Action)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Persistence.Reasoning.setConjectureEvaluationState: Could not find Action"
    actionEntity :: Entity Action
actionEntity : _ -> Entity Action -> ReaderT SqlBackend m (Entity Action)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity Action
actionEntity
  Key Action -> [Update Action] -> DBMonad m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
Key record -> [Update record] -> ReaderT backend m ()
update Key Action
actionKey [EntityField Action EvaluationStateType
forall typ. (typ ~ EvaluationStateType) => EntityField Action typ
ActionEvaluationState EntityField Action EvaluationStateType
-> EvaluationStateType -> Update Action
forall v typ.
PersistField typ =>
EntityField v typ -> typ -> Update v
=. EvaluationStateType
evaluationState]
  () -> DBMonad m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

setOmsConsistencyCheckStatus :: MonadIO m
                             => Entity DatabaseSchema.LocIdBase
                             -> ConsistencyStatusType.ConsistencyStatusType
                             -> DBMonad m ()
setOmsConsistencyCheckStatus :: Entity LocIdBase -> ConsistencyStatusType -> DBMonad m ()
setOmsConsistencyCheckStatus (Entity omsKey :: LocIdBaseId
omsKey _) consistencyCheckStatus :: ConsistencyStatusType
consistencyCheckStatus = do
  (SqlExpr (Entity OMS) -> SqlQuery ()) -> DBMonad m ()
forall (m :: * -> *) val.
(MonadIO m, PersistEntity val,
 BackendCompatible SqlBackend (PersistEntityBackend val)) =>
(SqlExpr (Entity val) -> SqlQuery ()) -> SqlWriteT m ()
E.update ((SqlExpr (Entity OMS) -> SqlQuery ()) -> DBMonad m ())
-> (SqlExpr (Entity OMS) -> SqlQuery ()) -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$ \ oms :: SqlExpr (Entity OMS)
oms -> do
    SqlExpr (Entity OMS) -> [SqlExpr (Update OMS)] -> SqlQuery ()
forall val.
PersistEntity val =>
SqlExpr (Entity val) -> [SqlExpr (Update val)] -> SqlQuery ()
set SqlExpr (Entity OMS)
oms [EntityField OMS ConsistencyStatusType
forall typ. (typ ~ ConsistencyStatusType) => EntityField OMS typ
OMSConsistencyStatus EntityField OMS ConsistencyStatusType
-> SqlExpr (Value ConsistencyStatusType) -> SqlExpr (Update OMS)
forall val typ.
(PersistEntity val, PersistField typ) =>
EntityField val typ -> SqlExpr (Value typ) -> SqlExpr (Update val)
E.=. ConsistencyStatusType -> SqlExpr (Value ConsistencyStatusType)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val ConsistencyStatusType
consistencyCheckStatus]
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Value (Key OMS)) -> SqlExpr (Value LocIdBaseId)
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
coerceId (SqlExpr (Entity OMS)
oms SqlExpr (Entity OMS)
-> EntityField OMS (Key OMS) -> SqlExpr (Value (Key OMS))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField OMS (Key OMS)
forall typ. (typ ~ Key OMS) => EntityField OMS typ
OMSId) SqlExpr (Value LocIdBaseId)
-> SqlExpr (Value LocIdBaseId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseId
omsKey
  () -> DBMonad m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

setConjectureProofStatus :: MonadIO m
                         => Entity DatabaseSchema.LocIdBase
                         -> Enums.ProofStatusType
                         -> DBMonad m ()
setConjectureProofStatus :: Entity LocIdBase -> ProofStatusType -> DBMonad m ()
setConjectureProofStatus (Entity conjectureKey :: LocIdBaseId
conjectureKey _) proofStatus :: ProofStatusType
proofStatus = do
  (SqlExpr (Entity Conjecture) -> SqlQuery ()) -> DBMonad m ()
forall (m :: * -> *) val.
(MonadIO m, PersistEntity val,
 BackendCompatible SqlBackend (PersistEntityBackend val)) =>
(SqlExpr (Entity val) -> SqlQuery ()) -> SqlWriteT m ()
E.update ((SqlExpr (Entity Conjecture) -> SqlQuery ()) -> DBMonad m ())
-> (SqlExpr (Entity Conjecture) -> SqlQuery ()) -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$ \ conjectures :: SqlExpr (Entity Conjecture)
conjectures -> do
    SqlExpr (Entity Conjecture)
-> [SqlExpr (Update Conjecture)] -> SqlQuery ()
forall val.
PersistEntity val =>
SqlExpr (Entity val) -> [SqlExpr (Update val)] -> SqlQuery ()
set SqlExpr (Entity Conjecture)
conjectures [ EntityField Conjecture ProofStatusType
forall typ. (typ ~ ProofStatusType) => EntityField Conjecture typ
ConjectureProofStatus EntityField Conjecture ProofStatusType
-> SqlExpr (Value ProofStatusType) -> SqlExpr (Update Conjecture)
forall val typ.
(PersistEntity val, PersistField typ) =>
EntityField val typ -> SqlExpr (Value typ) -> SqlExpr (Update val)
E.=. ProofStatusType -> SqlExpr (Value ProofStatusType)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val ProofStatusType
proofStatus]
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Value Bool) -> SqlQuery ())
-> SqlExpr (Value Bool) -> SqlQuery ()
forall a b. (a -> b) -> a -> b
$ SqlExpr (Value (Key Conjecture)) -> SqlExpr (Value LocIdBaseId)
forall a b. SqlExpr (Value a) -> SqlExpr (Value b)
coerceId (SqlExpr (Entity Conjecture)
conjectures SqlExpr (Entity Conjecture)
-> EntityField Conjecture (Key Conjecture)
-> SqlExpr (Value (Key Conjecture))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Conjecture (Key Conjecture)
forall typ. (typ ~ Key Conjecture) => EntityField Conjecture typ
ConjectureId) SqlExpr (Value LocIdBaseId)
-> SqlExpr (Value LocIdBaseId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseId
conjectureKey
  () -> DBMonad m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

findDocument :: (MonadIO m, Fail.MonadFail m)
             => HetcatsOpts -> String -> DBMonad m (Entity LocIdBase)
findDocument :: HetcatsOpts -> String -> DBMonad m (Entity LocIdBase)
findDocument opts :: HetcatsOpts
opts location :: String
location = do
  let locId :: String
locId = HetcatsOpts -> Maybe String -> String -> String
locIdOfDocument HetcatsOpts
opts (String -> Maybe String
forall a. a -> Maybe a
Just String
location) ""
  String
-> [LocIdBaseKindType] -> String -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
String
-> [LocIdBaseKindType] -> String -> DBMonad m (Entity LocIdBase)
findLocIdBase "Document" [LocIdBaseKindType
Enums.Library, LocIdBaseKindType
Enums.NativeDocument] String
locId

findOMS :: (MonadIO m, Fail.MonadFail m)
        => Entity LocIdBase
        -> DGNodeLab
        -> DBMonad m (Entity LocIdBase)
findOMS :: Entity LocIdBase -> DGNodeLab -> DBMonad m (Entity LocIdBase)
findOMS documentEntity :: Entity LocIdBase
documentEntity nodeLabel :: DGNodeLab
nodeLabel = do
  let locId :: String
locId = Entity LocIdBase -> DGNodeLab -> String
locIdOfOMS Entity LocIdBase
documentEntity DGNodeLab
nodeLabel
  String
-> [LocIdBaseKindType] -> String -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
String
-> [LocIdBaseKindType] -> String -> DBMonad m (Entity LocIdBase)
findLocIdBase "OMS" [LocIdBaseKindType
Enums.OMS] String
locId

findConjecture :: (MonadIO m, Fail.MonadFail m)
               => Entity LocIdBase
               -> String
               -> DBMonad m (Entity LocIdBase)
findConjecture :: Entity LocIdBase -> String -> DBMonad m (Entity LocIdBase)
findConjecture omsEntity :: Entity LocIdBase
omsEntity name :: String
name = do
  let locId :: String
locId = Entity LocIdBase -> String -> String
locIdOfSentence Entity LocIdBase
omsEntity String
name
  String
-> [LocIdBaseKindType] -> String -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
String
-> [LocIdBaseKindType] -> String -> DBMonad m (Entity LocIdBase)
findLocIdBase "Conjecture" [ LocIdBaseKindType
Enums.OpenConjecture
                             , LocIdBaseKindType
Enums.Theorem
                             , LocIdBaseKindType
Enums.CounterTheorem
                             ] String
locId

findPremise :: (MonadIO m, Fail.MonadFail m)
            => Entity LocIdBase
            -> String
            -> DBMonad m (Entity LocIdBase)
findPremise :: Entity LocIdBase -> String -> DBMonad m (Entity LocIdBase)
findPremise omsEntity :: Entity LocIdBase
omsEntity name :: String
name = do
  let locId :: String
locId = Entity LocIdBase -> String -> String
locIdOfSentence Entity LocIdBase
omsEntity String
name
  String
-> [LocIdBaseKindType] -> String -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
String
-> [LocIdBaseKindType] -> String -> DBMonad m (Entity LocIdBase)
findLocIdBase "Premise" [ LocIdBaseKindType
Enums.OpenConjecture
                          , LocIdBaseKindType
Enums.Theorem
                          , LocIdBaseKindType
Enums.CounterTheorem
                          , LocIdBaseKindType
Enums.Axiom
                          ] String
locId

createGeneratedAxioms :: MonadIO m
                      => ReasoningAttemptId
                      -> LP.ProofStatus G_proof_tree
                      -> DBMonad m ()
createGeneratedAxioms :: Key ReasoningAttempt -> ProofStatus G_proof_tree -> DBMonad m ()
createGeneratedAxioms reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey proofStatus :: ProofStatus G_proof_tree
proofStatus =
  (String -> ReaderT SqlBackend m (Key GeneratedAxiom))
-> [String] -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ axiomText :: String
axiomText -> GeneratedAxiom -> ReaderT SqlBackend m (Key GeneratedAxiom)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WGeneratedAxiom :: Key ReasoningAttempt -> Text -> GeneratedAxiom
GeneratedAxiom
          { generatedAxiomReasoningAttemptId :: Key ReasoningAttempt
generatedAxiomReasoningAttemptId = Key ReasoningAttempt
reasoningAttemptKey
          , generatedAxiomText :: Text
generatedAxiomText = String -> Text
Text.pack String
axiomText
          }
        ) ([String] -> DBMonad m ()) -> [String] -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$ ProofStatus G_proof_tree -> [String]
forall proof_tree. ProofStatus proof_tree -> [String]
LP.usedAxioms ProofStatus G_proof_tree
proofStatus

createReasonerOutput :: MonadIO m
                     => ReasoningAttemptId
                     -> ReasonerId
                     -> String
                     -> DBMonad m ReasonerOutputId
createReasonerOutput :: Key ReasoningAttempt
-> Key Reasoner -> String -> DBMonad m ReasonerOutputId
createReasonerOutput reasoningAttemptKey :: Key ReasoningAttempt
reasoningAttemptKey reasonerKey :: Key Reasoner
reasonerKey text :: String
text =
  ReasonerOutput -> DBMonad m ReasonerOutputId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WReasonerOutput :: Key ReasoningAttempt -> Key Reasoner -> Text -> ReasonerOutput
ReasonerOutput
    { reasonerOutputReasoningAttemptId :: Key ReasoningAttempt
reasonerOutputReasoningAttemptId = Key ReasoningAttempt
reasoningAttemptKey
    , reasonerOutputReasonerId :: Key Reasoner
reasonerOutputReasonerId = Key Reasoner
reasonerKey
    , reasonerOutputText :: Text
reasonerOutputText = String -> Text
Text.pack String
text
    }

findLocIdBase :: (MonadIO m, Fail.MonadFail m)
              => String
              -> [Enums.LocIdBaseKindType]
              -> String
              -> DBMonad m (Entity LocIdBase)
findLocIdBase :: String
-> [LocIdBaseKindType] -> String -> DBMonad m (Entity LocIdBase)
findLocIdBase entityKind :: String
entityKind kinds :: [LocIdBaseKindType]
kinds locId :: String
locId = do
  [Entity LocIdBase]
omsL <-
    SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LocIdBase)
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LocIdBase)
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (SqlExpr (Entity LocIdBase)
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ \ loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases -> do
      SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase String
forall typ. (typ ~ String) => EntityField LocIdBase typ
LocIdBaseLocId SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
locId SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases
              SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseKindType
-> SqlExpr (Value LocIdBaseKindType)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseKindType
forall typ. (typ ~ LocIdBaseKindType) => EntityField LocIdBase typ
LocIdBaseKind SqlExpr (Value LocIdBaseKindType)
-> SqlExpr (ValueList LocIdBaseKindType) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ)
-> SqlExpr (ValueList typ) -> SqlExpr (Value Bool)
`in_` [LocIdBaseKindType] -> SqlExpr (ValueList LocIdBaseKindType)
forall typ. PersistField typ => [typ] -> SqlExpr (ValueList typ)
valList [LocIdBaseKindType]
kinds)
      SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
  case [Entity LocIdBase]
omsL of
    [] -> String -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Could not save reasoning results to database: "
                     String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
entityKind String -> String -> String
forall a. [a] -> [a] -> [a]
++ " not found in database.")
    entity :: Entity LocIdBase
entity : _ -> Entity LocIdBase -> DBMonad m (Entity LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity LocIdBase
entity

convertTime :: TimeOfDay -> Int
convertTime :: TimeOfDay -> Int
convertTime tod :: TimeOfDay
tod =
  -- Sometimes, the reasoning system returns -1 seconds
  [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ Double -> Int
forall a b. (RealFrac a, Integral b) => a -> b
floor (String -> Double
forall a. Read a => String -> a
read (String -> Double) -> String -> Double
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
init (String -> String) -> String -> String
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)
          , 0
          ]

convertGoalResultConsistencyStatus :: String
                                   -> ConsistencyStatusType.ConsistencyStatusType
convertGoalResultConsistencyStatus :: String -> ConsistencyStatusType
convertGoalResultConsistencyStatus goalResult :: String
goalResult
  | "Timeout" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
goalResult = ConsistencyStatusType
ConsistencyStatusType.Timeout
  | "Error" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
goalResult = ConsistencyStatusType
ConsistencyStatusType.Timeout
  | "Consistent" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
goalResult = ConsistencyStatusType
ConsistencyStatusType.Consistent
  | "Inconsistent" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
goalResult = ConsistencyStatusType
ConsistencyStatusType.Inconsistent
  | Bool
otherwise = ConsistencyStatusType
ConsistencyStatusType.Open

convertGoalResultProofStatus :: String -> Maybe [String] -> Enums.ProofStatusType
convertGoalResultProofStatus :: String -> Maybe [String] -> ProofStatusType
convertGoalResultProofStatus goalResult :: String
goalResult premisesM :: Maybe [String]
premisesM
  | "Proved" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
goalResult = ProofStatusType
Enums.THM
  | "Disproved" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
goalResult Bool -> Bool -> Bool
&& Maybe [String] -> Bool
forall a. Maybe a -> Bool
Maybe.isNothing Maybe [String]
premisesM = ProofStatusType
Enums.CSA
  | "Disproved" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
goalResult Bool -> Bool -> Bool
&& Maybe [String]
premisesM Maybe [String] -> Maybe [String] -> Bool
forall a. Eq a => a -> a -> Bool
== [String] -> Maybe [String]
forall a. a -> Maybe a
Just [] = ProofStatusType
Enums.CSA
  | "Disproved" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
goalResult Bool -> Bool -> Bool
&& Maybe [String]
premisesM Maybe [String] -> Maybe [String] -> Bool
forall a. Eq a => a -> a -> Bool
/= [String] -> Maybe [String]
forall a. a -> Maybe a
Just [] = ProofStatusType
Enums.CSAS
  | "Timeout" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` String
goalResult = ProofStatusType
Enums.RSO
  | Bool
otherwise = ProofStatusType
Enums.UNK

conjectureLockKey :: DatabaseSchema.LocIdBaseId -> String
conjectureLockKey :: LocIdBaseId -> String
conjectureLockKey conjectureKey :: LocIdBaseId
conjectureKey =
  "conjecture-reasoning-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int64 -> String
forall a. Show a => a -> String
show (LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
conjectureKey)

omsLockKey :: DatabaseSchema.LocIdBaseId -> String
omsLockKey :: LocIdBaseId -> String
omsLockKey omsKey :: LocIdBaseId
omsKey =
  "oms-reasoning-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int64 -> String
forall a. Show a => a -> String
show (LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
omsKey)