{-# 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 Data.List (isPrefixOf)

import Database.Persist hiding ((==.))

import Database.Esqueleto

migrateLogicGraphKey :: String

migrateLogicGraphKey = "migrateLogicGraph"

exportLogicGraph :: HetcatsOpts -> IO ()

exportLogicGraph opts =

onDatabase (databaseConfig opts) $

advisoryLocked opts migrateLogicGraphKey $ migrateLogicGraph opts

migrateLogicGraph :: MonadIO 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 => 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

=> HetcatsOpts

-> LogicGraph -> DBMonad m ()

exportLanguageMappingsAndLogicMappings opts logicGraph =

mapM_ (findOrCreateLanguageMappingAndLogicMapping opts) $

comorphisms logicGraph

findOrCreateLanguageMappingAndLogicMapping :: MonadIO 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

=> 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

=> 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 ("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

=> G_cons_checker

-> DBMonad m (Entity Reasoner)

findReasonerByGConsChecker gConsChecker = do

let reasonerSlugS = slugOfConsistencyChecker gConsChecker

reasonerM <- findReasoner reasonerSlugS Enums.ConsistencyChecker

case reasonerM of

Nothing -> fail ("Persistence.LogicGraph.findReasonerByGConsChecker: Could not find Consistency Checker " ++ reasonerSlugS)

Just reasonerEntity -> return reasonerEntity

findReasonerByGProver :: MonadIO m

=> G_prover

-> DBMonad m (Entity Reasoner)

findReasonerByGProver gProver = do

let reasonerSlugS = slugOfProver gProver

reasonerM <- findReasoner reasonerSlugS Enums.Prover

case reasonerM of

Nothing -> fail ("Persistence.LogicGraph.findReasonerByGProver: Could not find Prover " ++ reasonerSlugS)

Just reasonerEntity -> return reasonerEntity

findReasonerByProverOrConsChecker :: MonadIO m

=> ProverOrConsChecker

-> DBMonad m (Entity Reasoner)

findReasonerByProverOrConsChecker reasoner = case reasoner of

Prover gProver -> findReasonerByGProver gProver

ConsChecker gConsChecker -> findReasonerByGConsChecker gConsChecker

findOrCreateLogicTranslation :: MonadIO 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

=> 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

=> 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 ("Persistence.LogicGraph.findOrCreateLogicInclusion: "

++ "Could not find the language " ++ languageSlugS)

Just (Entity key _) -> return key

sourceM <- findLogic sourceSlugS

sourceKey <- case sourceM of

Nothing -> 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 ("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)