content: module PGIP.GraphQL.Resolver.OMS (resolve) where
  
  import PGIP.GraphQL.Resolver.ToResult
  
  import PGIP.GraphQL.Result as GraphQLResult
  import PGIP.GraphQL.Result.Action as GraphQLResultAction
  import PGIP.GraphQL.Result.Mapping as GraphQLResultMapping
  import PGIP.GraphQL.Result.PremiseSelection as GraphQLResultPremiseSelection
  import PGIP.GraphQL.Result.ReasonerConfiguration as GraphQLResultReasonerConfiguration
  import PGIP.GraphQL.Result.ReasoningAttempt as GraphQLResultReasoningAttempt
  import PGIP.GraphQL.Result.Sentence as GraphQLResultSentence
  import PGIP.GraphQL.Result.StringReference (StringReference (..))
  import PGIP.GraphQL.Result.Symbol as GraphQLResultSymbol
  
  import PGIP.Shared
  
  import Driver.Options
  import Persistence.Database
  import Persistence.Schema as DatabaseSchema
  import Persistence.Utils
  
  import Database.Esqueleto
  
  import Control.Monad.IO.Class (MonadIO (..))
  import Control.Monad.Fail ()
  
  resolve :: HetcatsOpts -> Cache -> String -> IO (Maybe GraphQLResult.Result)
  resolve opts _ locIdVar =
    onDatabase (databaseConfig opts) $ resolveDB locIdVar
  
  resolveDB :: (MonadIO m, MonadFail m) => String -> DBMonad m (Maybe GraphQLResult.Result)
  resolveDB locIdVar = do
    omsL <-
      select $ from $ \(oms `InnerJoin` loc_id_bases
                            `InnerJoin` conservativity_statuses
                            `LeftOuterJoin` file_ranges
                            `LeftOuterJoin` loc_id_basesFreeNormalForm
                            `LeftOuterJoin` signature_morphismsFreeNormalForm
                            `InnerJoin` languages
                            `InnerJoin` logics
                            `LeftOuterJoin` loc_id_basesNormalForm
                            `LeftOuterJoin` signature_morphismsNormalForm) -> do
        on (signature_morphismsNormalForm ?. SignatureMorphismId ==. oms ^. OMSNormalFormSignatureMorphismId)
        on (loc_id_basesNormalForm ?. LocIdBaseId ==. coerceId (oms ^. OMSNormalFormId))
        on (logics ^. LogicId ==. oms ^. OMSLogicId)
        on (languages ^. LanguageId ==. oms ^. OMSLanguageId)
        on (signature_morphismsFreeNormalForm ?. SignatureMorphismId ==. oms ^. OMSFreeNormalFormSignatureMorphismId)
        on (loc_id_basesFreeNormalForm ?. LocIdBaseId ==. coerceId (oms ^. OMSFreeNormalFormId))
        on (file_ranges ?. FileRangeId ==. oms ^. OMSNameFileRangeId)
        on (conservativity_statuses ^. ConservativityStatusId ==. oms ^. OMSConservativityStatusId)
        on (loc_id_bases ^. LocIdBaseId ==. coerceId (oms ^. OMSId))
        where_ (loc_id_bases ^. LocIdBaseLocId ==. val locIdVar)
        return (oms, loc_id_bases, conservativity_statuses, file_ranges,
                loc_id_basesFreeNormalForm, signature_morphismsFreeNormalForm,
                languages, logics,
                loc_id_basesNormalForm, signature_morphismsNormalForm)
    case omsL of
      [] -> return Nothing
      (omsEntity, locIdBaseOMS@(Entity omsKey _ ), conservativityStatusEntity, fileRangeM,
       freeNormalFormLocIdBaseM, freeNormalFormSignatureMorphismM,
       languageEntity, logicEntity,
       normalFormLocIdBaseM, normalFormSignatureMorphismM) : _ -> do
         consistencyCheckAttemptResults <- resolveConsistencyChecks omsKey
         mappingSourceResults <- resolveMappings omsKey MappingSourceId
         mappingTargetResults <- resolveMappings omsKey MappingTargetId
         sentenceResults <- resolveSentences omsKey
         serializationResult <- case oMSSerializationId $ entityVal omsEntity of
           Nothing -> return Nothing
           Just serializationKey -> resolveSerialization serializationKey
         return $ Just $ GraphQLResult.OMSResult $
           omsToResult omsEntity locIdBaseOMS conservativityStatusEntity
             fileRangeM freeNormalFormLocIdBaseM freeNormalFormSignatureMorphismM
             languageEntity logicEntity
             normalFormLocIdBaseM normalFormSignatureMorphismM
             consistencyCheckAttemptResults mappingSourceResults mappingTargetResults
             sentenceResults serializationResult
  
  resolveConsistencyChecks :: (MonadIO m, MonadFail m)
                           => LocIdBaseId -- of the OMS
                           -> DBMonad m [GraphQLResultReasoningAttempt.ReasoningAttempt]
  resolveConsistencyChecks omsKey = do
    consistencyCheckAttemptL <-
      select $ from $ \(reasoning_attempts `InnerJoin` consistency_check_attempts
                                           `InnerJoin` reasoner_configurations
                                           `LeftOuterJoin` reasoners) -> do
        on (reasoners ?. ReasonerId ==. reasoning_attempts ^. ReasoningAttemptUsedReasonerId)
        on (reasoner_configurations ^. ReasonerConfigurationId ==.
              reasoning_attempts ^. ReasoningAttemptReasonerConfigurationId)
        on (coerceId (consistency_check_attempts ^. ConsistencyCheckAttemptId) ==.
              reasoning_attempts ^. ReasoningAttemptId)
        where_ (consistency_check_attempts ^. ConsistencyCheckAttemptOmsId ==.
                  just (val omsKey))
        return (reasoning_attempts, reasoners, reasoner_configurations)
    mapM resolveReasoningAttempt consistencyCheckAttemptL
  
  resolveMappings :: MonadIO m
                  => LocIdBaseId
                  -> EntityField DatabaseSchema.Mapping LocIdBaseId
                  -> DBMonad m [GraphQLResultMapping.Mapping]
  resolveMappings omsKey column = do
    mappingData <-
      select $ from $ \(mappingsSql `InnerJoin` loc_id_bases
                                    `InnerJoin` signature_morphisms
                                    `LeftOuterJoin` conservativity_statuses
                                    `InnerJoin` loc_id_basesSource
                                    `InnerJoin` loc_id_basesTarget
                                    `LeftOuterJoin` loc_id_basesOMS
                                    `LeftOuterJoin` languages) -> do
        on (languages ?. LanguageId ==. mappingsSql ^. MappingFreenessParameterLanguageId)
        on (loc_id_basesOMS ?. LocIdBaseId ==. mappingsSql ^. MappingFreenessParameterOMSId)
        on (loc_id_basesTarget ^. LocIdBaseId ==. mappingsSql ^. MappingTargetId)
        on (loc_id_basesSource ^. LocIdBaseId ==. mappingsSql ^. MappingSourceId)
        on (conservativity_statuses ?. ConservativityStatusId ==.
              mappingsSql ^. MappingConservativityStatusId)
        on (mappingsSql ^. MappingSignatureMorphismId ==.
              signature_morphisms ^. SignatureMorphismId)
        on (loc_id_bases ^. LocIdBaseId ==. coerceId (mappingsSql ^. MappingId))
        where_ (mappingsSql ^. column ==. val omsKey)
        return (mappingsSql, loc_id_bases, signature_morphisms,
                conservativity_statuses, loc_id_basesSource, loc_id_basesTarget,
                loc_id_basesOMS, languages)
    return $
      map (\ (mapping, locIdBase, signatureMorphismEntity, conservativityStatusM,
              locIdBaseSource, locIdBaseTarget, freenesParameterOMSLocIdM,
              freenessParameterLanguageM) ->
            mappingToResult mapping locIdBase signatureMorphismEntity
              conservativityStatusM locIdBaseSource locIdBaseTarget
              freenesParameterOMSLocIdM freenessParameterLanguageM
          ) mappingData
  
  getReasonerOutput :: MonadIO m
                    => ReasoningAttemptId
                    -> DBMonad m (Maybe (Entity DatabaseSchema.ReasonerOutput))
  getReasonerOutput reasoningAttemptKey = do
    reasonerOutputL <- select $ from $ \ reasoner_outputs -> do
      where_ (reasoner_outputs ^. ReasonerOutputReasoningAttemptId ==.
                val reasoningAttemptKey)
      return reasoner_outputs
    return $ case reasonerOutputL of
      [] -> Nothing
      reasonerOutputEntity : _ -> Just reasonerOutputEntity
  
  resolveReasoningAttempt :: (MonadIO m, MonadFail m)
                          => ( Entity DatabaseSchema.ReasoningAttempt
                             , Maybe (Entity DatabaseSchema.Reasoner)
                             , Entity DatabaseSchema.ReasonerConfiguration
                             )
                          -> DBMonad m GraphQLResultReasoningAttempt.ReasoningAttempt
  resolveReasoningAttempt (reasoningAttemptEntity, reasonerEntityM, reasonerConfigurationEntity) = do
    actionResult <-
      resolveAction $ reasoningAttemptActionId $ entityVal reasoningAttemptEntity
    reasonerOutputEntityM <- getReasonerOutput $ entityKey reasoningAttemptEntity
    reasonerConfigurationResult <-
      resolveReasonerConfiguration reasonerConfigurationEntity
    return $ reasoningAttemptToResult reasoningAttemptEntity reasonerOutputEntityM
      reasonerEntityM actionResult reasonerConfigurationResult
  
  resolveAction :: (MonadIO m, MonadFail m)
                => DatabaseSchema.ActionId
                -> DBMonad m GraphQLResultAction.Action
  resolveAction actionKey = do
    Just actionValue <- get actionKey
    return $ actionToResult $ Entity actionKey actionValue
  
  resolveSentences :: (MonadIO m, MonadFail m)
                   => LocIdBaseId -> DBMonad m [GraphQLResultSentence.Sentence]
  resolveSentences omsKey = do
    sentenceL <-
      select $ from $ \(sentencesSql `InnerJoin` loc_id_bases
                                     `LeftOuterJoin` file_ranges
                                     `LeftOuterJoin` conjectures) -> do
        on (coerceId (conjectures ?. ConjectureId) ==. loc_id_bases ^. LocIdBaseId)
        on (file_ranges ?. FileRangeId ==. sentencesSql ^. SentenceFileRangeId)
        on (loc_id_bases ^. LocIdBaseId ==. coerceId (sentencesSql ^. SentenceId))
        where_ (sentencesSql ^. SentenceOmsId ==. val omsKey)
        return (sentencesSql, loc_id_bases, file_ranges, conjectures)
    mapM (\ (sentenceEntity, locIdBaseEntity, fileRangeM, conjectureM) -> do
            symbolResults <- resolveSymbols $ entityKey sentenceEntity
            case conjectureM of
              Nothing -> return $
                axiomToResult sentenceEntity locIdBaseEntity fileRangeM symbolResults
              Just conjectureEntity -> resolveConjecture sentenceEntity
                locIdBaseEntity fileRangeM conjectureEntity symbolResults
         ) sentenceL
  
  resolveConjecture :: (MonadIO m, MonadFail m)
                    => Entity DatabaseSchema.Sentence
                    -> Entity DatabaseSchema.LocIdBase
                    -> Maybe (Entity DatabaseSchema.FileRange)
                    -> Entity DatabaseSchema.Conjecture
                    -> [GraphQLResultSymbol.Symbol]
                    -> DBMonad m GraphQLResultSentence.Sentence
  resolveConjecture sentenceEntity locIdBaseEntity fileRangeM conjectureEntity symbolResults = do
    actionResult <- resolveAction $ conjectureActionId $ entityVal conjectureEntity
    proofAttemptResults <- resolveProofAttempts $ entityKey locIdBaseEntity
    return $ conjectureToResult sentenceEntity locIdBaseEntity fileRangeM
      conjectureEntity actionResult symbolResults proofAttemptResults
  
  resolveProofAttempts :: (MonadIO m, MonadFail m)
                       => LocIdBaseId
                       -> DBMonad m [GraphQLResultReasoningAttempt.ReasoningAttempt]
  resolveProofAttempts conjectureKey = do
    proofAttemptL <-
      select $ from $ \(reasoning_attempts `InnerJoin` proof_attempts
                                           `InnerJoin` reasoner_configurations
                                           `LeftOuterJoin` reasoners) -> do
        on (reasoners ?. ReasonerId ==.
              reasoning_attempts ^. ReasoningAttemptUsedReasonerId)
        on (reasoner_configurations ^. ReasonerConfigurationId ==.
              reasoning_attempts ^. ReasoningAttemptReasonerConfigurationId)
        on (coerceId (proof_attempts ^. ProofAttemptId) ==.
              reasoning_attempts ^. ReasoningAttemptId)
        where_ (proof_attempts ^. ProofAttemptConjectureId ==.
                  just (val conjectureKey))
        return (reasoning_attempts, reasoners, reasoner_configurations)
    mapM resolveReasoningAttempt proofAttemptL
  
  resolveReasonerConfiguration :: MonadIO m
                               => Entity DatabaseSchema.ReasonerConfiguration
                               -> DBMonad m GraphQLResultReasonerConfiguration.ReasonerConfiguration
  resolveReasonerConfiguration reasonerConfigurationEntity@(Entity reasonerConfigurationKey reasonerConfigurationValue) = do
    reasonerL <-
      select $ from $ \ reasoners -> do
        where_ (reasoners ?. ReasonerId ==.
                  val (reasonerConfigurationConfiguredReasonerId reasonerConfigurationValue))
        return reasoners
    let reasonerResultM = case reasonerL of
          [] -> Nothing
          reasonerEntity : _ -> reasonerEntity
  
    premiseSelectionsL <-
      select $ from $ \ premise_selections -> do
        where_ (premise_selections ^. PremiseSelectionReasonerConfigurationId ==.
                  val reasonerConfigurationKey)
        return premise_selections
  
    premiseSelectionResults <- mapM resolvePremiseSelection premiseSelectionsL
    return $ reasonerConfigurationToResult reasonerConfigurationEntity
      reasonerResultM premiseSelectionResults
  
  resolvePremiseSelection :: MonadIO m
                          => Entity DatabaseSchema.PremiseSelection
                          -> DBMonad m GraphQLResultPremiseSelection.PremiseSelection
  resolvePremiseSelection (Entity premiseSelectionKey _) = do
    premises <-
      select $ from $ \ (loc_id_bases `InnerJoin` premise_selected_sentences
                                      `InnerJoin` premise_selections) -> do
        on (loc_id_bases ^. LocIdBaseId ==.
              premise_selected_sentences ^. PremiseSelectedSentencePremiseId)
        on (premise_selected_sentences ^. PremiseSelectedSentencePremiseSelectionId ==.
              premise_selections ^. PremiseSelectionId)
        where_ (premise_selections ^. PremiseSelectionId ==. val premiseSelectionKey)
        return loc_id_bases
    return $ premiseSelectionToResult premises
  
  resolveSerialization :: MonadIO m
                       => SerializationId
                       -> DBMonad m (Maybe StringReference)
  resolveSerialization serializationKey = do
    serializationL <-
      select $ from $ \(serializations) -> do
        where_ (serializations ^. SerializationId ==. val serializationKey)
        return serializations
    case serializationL of
      [] -> return Nothing
      Entity _ serializationValue : _ ->
        return $ Just $ StringReference $ serializationSlug serializationValue
  
  resolveSymbols :: MonadIO m
                 => SentenceId -> DBMonad m [GraphQLResultSymbol.Symbol]
  resolveSymbols sentenceKey = do
    symbolL <-
      select $ from $ \(symbols `InnerJoin` sentences_symbols
                                `InnerJoin` sentencesSql
                                `InnerJoin` loc_id_bases
                                `LeftOuterJoin` file_ranges) -> do
        on (file_ranges ?. FileRangeId ==. symbols ^. SymbolFileRangeId)
        on (loc_id_bases ^. LocIdBaseId ==. coerceId (symbols ^. SymbolId))
        on (coerceId (sentencesSql ^. SentenceId) ==.
              sentences_symbols ^. SentenceSymbolSentenceId)
        on (sentences_symbols ^. SentenceSymbolSymbolId ==.
              coerceId (symbols ^. SymbolId))
        where_ (sentences_symbols ^. SentenceSymbolSentenceId ==.
                  val (toSqlKey $ fromSqlKey sentenceKey))
        return (loc_id_bases, symbols, file_ranges)
    return $ map symbolToResultUncurried symbolL
  