f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack{-# LANGUAGE GADTs #-}

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack{-# LANGUAGE MultiParamTypeClasses #-}

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack{-# LANGUAGE OverloadedStrings #-}

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack{-# LANGUAGE TypeFamilies #-}

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackmodule Persistence.LogicGraph ( migrateLogicGraphKey

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack , exportLogicGraph

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack , findOrCreateLogic

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack , findOrCreateLanguageMappingAndLogicMapping

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack ) where

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Persistence.Database

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Persistence.Schema as SchemaClass

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Persistence.Utils

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport qualified Comorphisms.LogicGraph as LogicGraph (logicGraph)

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Driver.Options

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Driver.Version

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Logic.Grothendieck

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Logic.Logic as Logic

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Logic.Comorphism as Comorphism

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Control.Monad (unless)

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Control.Monad.IO.Class (MonadIO (..))

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mackimport Database.Persist

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel MackmigrateLogicGraphKey :: String

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel MackmigrateLogicGraphKey = "migrateLogicGraph"

1433efd219a6df414a1821b3d3d70d86201ed3e4Lennart Poettering

1433efd219a6df414a1821b3d3d70d86201ed3e4Lennart PoetteringexportLogicGraph :: HetcatsOpts -> IO ()

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel MackexportLogicGraph opts =

f3c4724635951c5b8a2b3f3c3f25798ce4d290cdDaniel Mack onDatabase (databaseConfig opts) $

5e2de0eb1dff7bb86b40c16a0a9c9c4de33e77d1Daniel Mack advisoryLocked opts migrateLogicGraphKey $ migrateLogicGraph opts

migrateLogicGraph :: MonadIO m => HetcatsOpts -> DBMonad m ()

migrateLogicGraph opts = do

let versionKeyName = "lastMigratedVersion"

do

lastMigratedVersionM <- selectFirst [HetsKey ==. versionKeyName] []

case lastMigratedVersionM of

Nothing ->

insert (Hets versionKeyName hetsVersionNumeric) >> migrateLogicGraph' opts

Just (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

-- 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 = parameterize $ show lid

languageM <- selectFirst [LanguageSlug ==. languageSlugS] []

case languageM of

Just (Entity key _) -> return key

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)

}

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 = sublogicNameForDB lid sublogic

let logicSlugS = parameterize logicNameS

logicM <- selectFirst [LogicSlug ==. logicSlugS] []

case logicM of

Just (Entity key _) -> return key

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' <- selectFirst [LogicSlug ==. logicSlugS] []

case logicM' of

Just (Entity key _) -> return key

Nothing -> insert SchemaClass.Logic

{ logicLanguageId = languageKey

, logicSlug = logicSlugS

, logicName = logicNameS

}

-- 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 = parameterize $ show $ sourceLogic cid

targetLanguageSlugS = parameterize $ show $ targetLogic cid

in do

-- Find the IDs in the databases:

Just (Entity sourceLanguageKey _) <-

selectFirst [LanguageSlug ==. sourceLanguageSlugS] []

Just (Entity targetLanguageKey _) <-

selectFirst [LanguageSlug ==. targetLanguageSlugS] []

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

languageMappingM <-

selectFirst [ LanguageMappingSourceId ==. sourceLanguageKey

, LanguageMappingTargetId ==. targetLanguageKey

] []

case languageMappingM of

Just (Entity key _) -> return key

Nothing -> insert LanguageMapping

{ languageMappingSourceId = sourceLanguageKey

, languageMappingTargetId = targetLanguageKey

}

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

logicMappingM <-

selectFirst [ LogicMappingLanguageMappingId ==. languageMappingKey

, LogicMappingSlug ==. logicMappingSlugS

] []

case logicMappingM of

Just (Entity key _) -> return key

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

}

sublogicNameForDB :: Logic.Logic lid sublogics basic_spec sentence symb_items

symb_map_items sign morphism symbol raw_symbol proof_tree

=> lid -> sublogics -> String

sublogicNameForDB lid sublogic =

let hetsName = sublogicName sublogic

in if null hetsName then show lid else hetsName