LogicGraph.hs

{-# LANGUAGE ExistentialQuantification  #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}
module Persistence.LogicGraph ( migrateLogicGraphKey
                              , exportLogicGraph
                              , findOrCreateLogic
                              , findOrCreateLanguageMappingAndLogicMapping
                              , findReasoner
                              , findOrCreateProver
                              , findOrCreateConsistencyChecker
                              , findLogicMappingByComorphism
                              , findOrCreateLogicTranslation
                              , findReasonerByProverOrConsChecker
                              , findReasonerByGConsChecker
                              , findReasonerByGProver
                              ) where

import Persistence.Database
import Persistence.Schema as DatabaseSchema
import Persistence.Utils
import qualified Persistence.Schema.Enums as Enums

import qualified Comorphisms.LogicGraph as LogicGraph (logicGraph)
import Common.Utils (splitByList)
import Driver.Options
import Driver.Version
import Logic.Grothendieck
import Logic.Logic as Logic
import Logic.Comorphism as Comorphism
import Proofs.AbstractState (ProverOrConsChecker (..), G_prover (..), G_cons_checker (..), getProverName, getCcName)

import Control.Monad (unless)
import Control.Monad.IO.Class (MonadIO (..))
import qualified Control.Monad.Fail as Fail
import Data.List (isPrefixOf)
import Database.Persist hiding ((==.))
import Database.Esqueleto hiding (Entity, insert, EntityField)

migrateLogicGraphKey :: String
migrateLogicGraphKey = "migrateLogicGraph"

exportLogicGraph :: HetcatsOpts -> IO ()
exportLogicGraph opts =
  onDatabase (databaseConfig opts) $
    advisoryLocked opts migrateLogicGraphKey $ migrateLogicGraph opts

migrateLogicGraph :: (MonadIO m, Fail.MonadFail m) => HetcatsOpts -> DBMonad m ()
migrateLogicGraph opts = do
  let versionKeyName = "lastMigratedVersion"
  do
    lastMigratedVersionL <- select $ from $ \hets -> do
      where_ (hets ^. HetsKey ==. val versionKeyName)
      return hets
    case lastMigratedVersionL of
      [] ->
        insert (Hets versionKeyName hetsVersionNumeric) >> migrateLogicGraph' opts
      Entity _ value : _ ->
        unless (hetsValue value == hetsVersionNumeric) $ migrateLogicGraph' opts

migrateLogicGraph' :: (MonadIO m, Fail.MonadFail m) => HetcatsOpts -> DBMonad m ()
migrateLogicGraph' opts = do
  exportLanguagesAndLogics opts LogicGraph.logicGraph
  exportLanguageMappingsAndLogicMappings opts LogicGraph.logicGraph
  exportReasoners opts LogicGraph.logicGraph

-- Export all Languages and Logics. Add those that have been added since a
-- previous version of Hets. This does not delete Languages or Logics.
exportLanguagesAndLogics :: MonadIO m
                         => HetcatsOpts -> LogicGraph -> DBMonad m ()
exportLanguagesAndLogics opts logicGraph =
  mapM_ (\ (Logic.Logic lid) -> do
          languageKey <- findOrCreateLanguage lid
          mapM_ (findOrCreateLogic opts languageKey lid) $ all_sublogics lid
        ) $ logics logicGraph

findOrCreateLanguage :: ( MonadIO m
                        , Logic.Logic lid sublogics basic_spec sentence
                            symb_items symb_map_items sign morphism symbol
                            raw_symbol proof_tree
                        )
                     => lid -> DBMonad m LanguageId
findOrCreateLanguage lid = do
  let languageSlugS = slugOfLanguageByName $ language_name lid
  languageM <- findLanguage languageSlugS
  case languageM of
    Nothing -> insert Language
        { languageSlug = languageSlugS
        , languageName = show lid
        , languageDescription = description lid
        , languageStandardizationStatus = "TODO" -- TODO: add to class Logic
        , languageDefinedBy = "registry" -- TODO: add to class Logic (URL)
        }
    Just (Entity key _) -> return key

findLanguage :: MonadIO m
             => String -> DBMonad m (Maybe (Entity DatabaseSchema.Language))
findLanguage languageSlugS = do
  languageL <- select $ from $ \languages -> do
    where_ (languages ^. LanguageSlug ==. val languageSlugS)
    return languages
  case languageL of
    [] -> return Nothing
    entity : _ -> return $ Just entity


findOrCreateLogic :: ( MonadIO m
                     , Logic.Logic lid sublogics basic_spec sentence
                         symb_items symb_map_items sign morphism symbol
                         raw_symbol proof_tree
                     )
                  => HetcatsOpts -> LanguageId -> lid -> sublogics
                  -> DBMonad m LogicId
findOrCreateLogic opts languageKey lid sublogic = do
  let logicNameS = logicNameForDB lid sublogic
  let logicSlugS = slugOfLogicByName logicNameS
  logicM <- findLogic logicSlugS
  case logicM of
    Nothing ->
      -- This is a two-staged process to save some performance:
      -- Case 1: If the logic existed beforehand, then we don't lock the
      -- database and return the logic ID. This is expected to happen very
      -- frequently.
      -- Case 2: If the logic did not exist at this point, we need to create
      -- it atomically. To do this, we do a find-or-create pattern inside a
      -- mutex. This is expected to happen only a few times.
      advisoryLocked opts migrateLogicGraphKey $ do
        logicM' <- findLogic logicSlugS
        case logicM' of
          Nothing -> insert DatabaseSchema.Logic
            { logicLanguageId = languageKey
            , logicSlug = logicSlugS
            , logicName = logicNameS
            }
          Just (Entity key _) -> return key
    Just (Entity key _) -> return key

findLogic :: MonadIO m
          => String -> DBMonad m (Maybe (Entity DatabaseSchema.Logic))
findLogic logicSlugS = do
  logicL <- select $ from $ \logicsSql -> do
    where_ (logicsSql ^. LogicSlug ==. val logicSlugS)
    return logicsSql
  case logicL of
    [] -> return Nothing
    entity : _ -> return $ Just entity

-- Export all LanguageMappings and LogicMappings. Add those that have been added
-- since a previous version of Hets. This does not delete any of the old
-- mappings.
exportLanguageMappingsAndLogicMappings :: (MonadIO m, Fail.MonadFail m)
                                       => HetcatsOpts
                                       -> LogicGraph -> DBMonad m ()
exportLanguageMappingsAndLogicMappings opts logicGraph =
  mapM_ (findOrCreateLanguageMappingAndLogicMapping opts) $
    comorphisms logicGraph

findOrCreateLanguageMappingAndLogicMapping :: (MonadIO m, Fail.MonadFail m)
                                           => HetcatsOpts -> AnyComorphism
                                           -> DBMonad m ( LanguageMappingId
                                                        , LogicMappingId
                                                        )
findOrCreateLanguageMappingAndLogicMapping opts (Comorphism.Comorphism cid) =
  let sourceLanguageSlugS = slugOfLanguageByName $ language_name $ sourceLogic cid
      targetLanguageSlugS = slugOfLanguageByName $ language_name $ targetLogic cid
  in do
    -- Find the IDs in the databases:
    Entity sourceLanguageKey _ : _ <- select $ from $ \languages -> do
      where_ (languages ^. LanguageSlug ==. val sourceLanguageSlugS)
      return languages

    Entity targetLanguageKey _ : _ <- select $ from $ \languages -> do
      where_ (languages ^. LanguageSlug ==. val targetLanguageSlugS)
      return languages

    sourceLogicKey <-
      findOrCreateLogic opts sourceLanguageKey (sourceLogic cid) $ sourceSublogic cid
    targetLogicKey <-
      findOrCreateLogic opts targetLanguageKey (targetLogic cid) $ targetSublogic cid

    languageMappingKey <-
      findOrCreateLanguageMapping sourceLanguageKey targetLanguageKey
    logicMappingKey <-
      findOrCreateLogicMapping sourceLogicKey targetLogicKey languageMappingKey $ Comorphism.Comorphism cid

    return (languageMappingKey, logicMappingKey)

findOrCreateLanguageMapping :: MonadIO m
                            => LanguageId -> LanguageId
                            -> DBMonad m LanguageMappingId
findOrCreateLanguageMapping sourceLanguageKey targetLanguageKey = do
  languageMappingL <- select $ from $ \language_mappings -> do
    where_ (language_mappings ^. LanguageMappingSourceId ==. val sourceLanguageKey
            &&. language_mappings ^. LanguageMappingTargetId ==. val targetLanguageKey)
    return language_mappings
  case languageMappingL of
    [] -> insert LanguageMapping
      { languageMappingSourceId = sourceLanguageKey
      , languageMappingTargetId = targetLanguageKey
      }
    Entity key _ : _ -> return key

findOrCreateLogicMapping :: MonadIO m
                         => LogicId -> LogicId -> LanguageMappingId -> AnyComorphism
                         -> DBMonad m LogicMappingId
findOrCreateLogicMapping sourceLogicKey targetLogicKey languageMappingKey (Comorphism.Comorphism cid) = do
  let name = language_name cid
  let logicMappingSlugS = slugOfLogicMapping (Comorphism.Comorphism cid)
  logicMappingL <- select $ from $ \logic_mappings -> do
    where_ (logic_mappings ^. LogicMappingLanguageMappingId ==. val languageMappingKey
            &&. logic_mappings ^. LogicMappingSlug ==. val logicMappingSlugS)
    return logic_mappings
  case logicMappingL of
    [] -> insert LogicMapping
      { logicMappingLanguageMappingId = languageMappingKey
      , logicMappingSourceId = sourceLogicKey
      , logicMappingTargetId = targetLogicKey
      , logicMappingSlug = logicMappingSlugS
      , logicMappingName = name
      , logicMappingIsInclusion = isInclusionComorphism cid
      , logicMappingHasModelExpansion = has_model_expansion cid
      , logicMappingIsWeaklyAmalgamable = is_weakly_amalgamable cid
      }
    Entity key _ : _ -> return key

findLogicMappingByComorphism :: (MonadIO m, Fail.MonadFail m)
                             => AnyComorphism
                             -> DBMonad m (Maybe (Entity LogicMapping))
findLogicMappingByComorphism comorphism =
  if isIdComorphism comorphism then return Nothing else do
    let logicMappingSlugS = slugOfLogicMapping comorphism
    findLogicMappingBySlug logicMappingSlugS

findLogicMappingBySlug :: (MonadIO m, Fail.MonadFail m)
                       => String
                       -> DBMonad m (Maybe (Entity LogicMapping))
findLogicMappingBySlug logicMappingSlugS = do
  logicMappingL <- select $ from $ \ logic_mappings -> do
    where_ (logic_mappings ^. LogicMappingSlug ==. val logicMappingSlugS)
    return logic_mappings
  case logicMappingL of
    [] -> Fail.fail ("Persistence.LogicGraph.findLogicMappingBySlug: Could not find LogicMapping " ++ logicMappingSlugS)
    logicMappingEntity : _ -> return $ Just logicMappingEntity

exportReasoners :: MonadIO m => HetcatsOpts -> LogicGraph -> DBMonad m ()
exportReasoners _ logicGraph =
  mapM_ (\ (Logic.Logic lid) -> do
          let proversL = provers lid
          let consistencyCheckersL = cons_checkers lid
          mapM_ (findOrCreateProver . G_prover lid) proversL
          mapM_ (findOrCreateConsistencyChecker . G_cons_checker lid) consistencyCheckersL
        ) $ logics logicGraph

findOrCreateProver :: MonadIO m => G_prover -> DBMonad m ReasonerId
findOrCreateProver gProver = do
  let reasonerSlugS = slugOfProver gProver
  let name = getProverName gProver
  findOrCreateReasoner reasonerSlugS name Enums.Prover

findOrCreateConsistencyChecker :: MonadIO m => G_cons_checker -> DBMonad m ReasonerId
findOrCreateConsistencyChecker gConsistencyChecker = do
  let reasonerSlugS = slugOfConsistencyChecker gConsistencyChecker
  let name = getCcName gConsistencyChecker
  findOrCreateReasoner reasonerSlugS name Enums.ConsistencyChecker

findReasoner :: MonadIO m
             => String -> Enums.ReasonerKindType
             -> DBMonad m (Maybe (Entity Reasoner))
findReasoner reasonerSlugS reasonerKindValue = do
  reasonerL <-
    select $ from $ \ reasoners -> do
      where_ (reasoners ^. ReasonerSlug ==. val reasonerSlugS
              &&. reasoners ^. ReasonerKind ==. val reasonerKindValue)
      return reasoners
  case reasonerL of
    reasoner : _ -> return $ Just reasoner
    [] -> return Nothing

findOrCreateReasoner :: MonadIO m
                     => String -> String -> Enums.ReasonerKindType
                     -> DBMonad m ReasonerId
findOrCreateReasoner reasonerSlugS name reasonerKindValue = do
  reasonerM <- findReasoner reasonerSlugS reasonerKindValue
  case reasonerM of
    Just (Entity reasonerKey _) -> return reasonerKey
    Nothing -> insert Reasoner
      { reasonerSlug = reasonerSlugS
      , reasonerDisplayName = name
      , reasonerKind = reasonerKindValue
      }

findReasonerByGConsChecker :: (MonadIO m, Fail.MonadFail m)
                           => G_cons_checker
                           -> DBMonad m (Entity Reasoner)
findReasonerByGConsChecker gConsChecker = do
  let reasonerSlugS = slugOfConsistencyChecker gConsChecker
  reasonerM <- findReasoner reasonerSlugS Enums.ConsistencyChecker
  case reasonerM of
    Nothing -> Fail.fail ("Persistence.LogicGraph.findReasonerByGConsChecker: Could not find Consistency Checker " ++ reasonerSlugS)
    Just reasonerEntity -> return reasonerEntity

findReasonerByGProver :: (MonadIO m, Fail.MonadFail m)
                      => G_prover
                      -> DBMonad m (Entity Reasoner)
findReasonerByGProver gProver = do
  let reasonerSlugS = slugOfProver gProver
  reasonerM <- findReasoner reasonerSlugS Enums.Prover
  case reasonerM of
    Nothing -> Fail.fail ("Persistence.LogicGraph.findReasonerByGProver: Could not find Prover " ++ reasonerSlugS)
    Just reasonerEntity -> return reasonerEntity

findReasonerByProverOrConsChecker :: (MonadIO m, Fail.MonadFail m)
                                  => ProverOrConsChecker
                                  -> DBMonad m (Entity Reasoner)
findReasonerByProverOrConsChecker reasoner = case reasoner of
  Prover gProver -> findReasonerByGProver gProver
  ConsChecker gConsChecker -> findReasonerByGConsChecker gConsChecker

findOrCreateLogicTranslation :: (MonadIO m, Fail.MonadFail m)
                             => HetcatsOpts
                             -> AnyComorphism
                             -> DBMonad m (Maybe (Entity LogicTranslation))
findOrCreateLogicTranslation _ comorphism@(Comorphism.Comorphism cid) =
  if isIdComorphism comorphism
  then return Nothing
  else do
    let logicTranslationSlugS = slugOfTranslation comorphism
    let logicTranslationNameS = language_name cid
    translationL <- select $ from $ \ translations -> do
      where_ (translations ^. LogicTranslationSlug ==. val logicTranslationSlugS)
      return translations
    case translationL of
      translationEntity : _ -> return $ Just translationEntity
      [] -> do
        let logicTranslationValue = LogicTranslation
              { logicTranslationSlug = logicTranslationSlugS
              , logicTranslationName = logicTranslationNameS
              }
        logicTranslationKey <- insert logicTranslationValue
        mapM_ (\ (number, name) ->
                createLogicTranslationStep logicTranslationKey (number, name)
              ) $ zip [1..] $ constituents cid
        return $ Just $ Entity logicTranslationKey logicTranslationValue

createLogicTranslationStep :: (MonadIO m, Fail.MonadFail m)
                           => LogicTranslationId
                           -> (Int, String)
                           -> DBMonad m (Entity LogicTranslationStep)
createLogicTranslationStep logicTranslationKey (number, name)
  | isInclusion_ name = do
      Entity logicInclusionKey _ <- findOrCreateLogicInclusion name
      let translationStepValue = LogicTranslationStep
            { logicTranslationStepLogicTranslationId = logicTranslationKey
            , logicTranslationStepNumber = number
            , logicTranslationStepLogicMappingId = Nothing
            , logicTranslationStepLogicInclusionId = Just logicInclusionKey
            }
      translationStepKey <- insert translationStepValue
      return $ Entity translationStepKey translationStepValue
  | otherwise = do
      Just (Entity logicMappingKey _) <-
        findLogicMappingBySlug $ slugOfLogicMappingByName name
      let translationStepValue = LogicTranslationStep
            { logicTranslationStepLogicTranslationId = logicTranslationKey
            , logicTranslationStepNumber = number
            , logicTranslationStepLogicMappingId = Just logicMappingKey
            , logicTranslationStepLogicInclusionId = Nothing
            }
      translationStepKey <- insert translationStepValue
      return $ Entity translationStepKey translationStepValue
  where
    isInclusion_ :: String -> Bool
    isInclusion_ name_ = "id_" `isPrefixOf` name_ || "incl_" `isPrefixOf` name_

findOrCreateLogicInclusion :: (MonadIO m, Fail.MonadFail m)
                           => String
                           -> DBMonad m (Entity LogicInclusion)
findOrCreateLogicInclusion name = do
  let logicInclusionSlugS = slugOfLogicInclusionByName name
  logicInclusionL <- select $ from $ \ logic_inclusions -> do
    where_ (logic_inclusions ^. LogicInclusionSlug ==. val logicInclusionSlugS)
    return logic_inclusions
  case logicInclusionL of
    logicInclusionEntity : _ -> return logicInclusionEntity
    [] -> do
      let (languageSlugS, sourceSlugS, targetSlugM) = slugsFromName

      languageM <- findLanguage languageSlugS
      languageKey <- case languageM of
        Nothing -> Fail.fail ("Persistence.LogicGraph.findOrCreateLogicInclusion: "
          ++ "Could not find the language " ++ languageSlugS)
        Just (Entity key _) -> return key

      sourceM <- findLogic sourceSlugS
      sourceKey <- case sourceM of
        Nothing -> Fail.fail ("Persistence.LogicGraph.findOrCreateLogicInclusion: "
          ++ "Could not find the source logic " ++ sourceSlugS)
        Just (Entity key _) -> return key

      targetKeyM <- case targetSlugM of
        Nothing -> return Nothing
        Just targetSlugS -> do
          targetM <- findLogic targetSlugS
          case targetM of
            Nothing -> Fail.fail ("Persistence.LogicGraph.findOrCreateLogicInclusion: "
              ++ "Could not find the target logic " ++ targetSlugS)
            Just (Entity key _) -> return $ Just key

      let logicInclusionValue = LogicInclusion
            { logicInclusionName = name
            , logicInclusionSlug = logicInclusionSlugS
            , logicInclusionLanguageId = languageKey
            , logicInclusionSourceId = sourceKey
            , logicInclusionTargetId = targetKeyM
            }
      logicInclusionKey <- insert logicInclusionValue
      return $ Entity logicInclusionKey logicInclusionValue
  where
    slugsFromName :: (String, String, Maybe String)
    slugsFromName
      | "id_" `isPrefixOf` name =
          let languageName_ = takeWhile (/= '.') $ drop 3 name
              logicName_ = tail $ dropWhile (/= '.') name
              logicSlugS =
                slugOfLogicByName $ logicNameForDBByName languageName_ logicName_
          in  ( slugOfLanguageByName languageName_
              , logicSlugS
              , Nothing
              )
      | "incl_" `isPrefixOf` name =
          let languageName_ = takeWhile (/= ':') $ drop 5 name
              logicNames = tail $ dropWhile (/= ':') name
              [sourceName, targetName] = splitByList "->" logicNames
              sourceSlugS =
                slugOfLogicByName $ logicNameForDBByName languageName_ sourceName
              targetSlugS =
                slugOfLogicByName $ logicNameForDBByName languageName_ targetName
          in  ( slugOfLanguageByName languageName_
              , sourceSlugS
              , Just targetSlugS
              )
      | otherwise = error ("Persistence.LogicGraph.findOrCreateLogicInclusion.slugsFromName "
                           ++ "encountered a bad comorphism name: " ++ name)