LogicGraph.hs revision 9d63e3d6c1c65ab10d1459b9f59a134161acc1d7
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa{-# LANGUAGE GADTs #-}
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa{-# LANGUAGE MultiParamTypeClasses #-}
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa{-# LANGUAGE OverloadedStrings #-}
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa{-# LANGUAGE TypeFamilies #-}
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksamodule Persistence.LogicGraph ( migrateLogicGraphKey
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , exportLogicGraph
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , findOrCreateLogic
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , findOrCreateLanguageMappingAndLogicMapping
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa ) where
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Persistence.Database
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Persistence.Schema as SchemaClass
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Persistence.Utils
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport qualified Comorphisms.LogicGraph as LogicGraph (logicGraph)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Driver.Options
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Driver.Version
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Logic.Grothendieck
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Logic.Logic as Logic
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Logic.Comorphism as Comorphism
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Control.Monad (unless)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Control.Monad.IO.Class (MonadIO (..))
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksaimport Database.Persist hiding ((==.))
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksaimport Database.Esqueleto
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksamigrateLogicGraphKey :: String
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksamigrateLogicGraphKey = "migrateLogicGraph"
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaexportLogicGraph :: HetcatsOpts -> IO ()
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaexportLogicGraph opts =
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa onDatabase (databaseConfig opts) $
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa advisoryLocked opts migrateLogicGraphKey $ migrateLogicGraph opts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksamigrateLogicGraph :: MonadIO m => HetcatsOpts -> DBMonad m ()
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksamigrateLogicGraph opts = do
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let versionKeyName = "lastMigratedVersion"
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa lastMigratedVersionL <- select $ from $ \hets -> do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa where_ (hets ^. HetsKey ==. val versionKeyName)
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa return hets
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa case lastMigratedVersionL of
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa [] ->
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa insert (Hets versionKeyName hetsVersionNumeric) >> migrateLogicGraph' opts
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa Entity _ value : _ ->
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa unless (hetsValue value == hetsVersionNumeric) $ migrateLogicGraph' opts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksamigrateLogicGraph' :: MonadIO m => HetcatsOpts -> DBMonad m ()
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksamigrateLogicGraph' opts = do
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa exportLanguagesAndLogics opts LogicGraph.logicGraph
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa exportLanguageMappingsAndLogicMappings opts LogicGraph.logicGraph
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa-- Export all Languages and Logics. Add those that have been added since a
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa-- previous version of Hets. This does not delete Languages or Logics.
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaexportLanguagesAndLogics :: MonadIO m
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa => HetcatsOpts -> LogicGraph -> DBMonad m ()
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaexportLanguagesAndLogics opts logicGraph =
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa mapM_ (\ (Logic.Logic lid) -> do
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa languageKey <- findOrCreateLanguage lid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa mapM_ (findOrCreateLogic opts languageKey lid) $ all_sublogics lid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa ) $ logics logicGraph
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksafindOrCreateLanguage :: ( MonadIO m
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , Logic.Logic lid sublogics basic_spec sentence
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa symb_items symb_map_items sign morphism symbol
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa raw_symbol proof_tree
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa )
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa => lid -> DBMonad m LanguageId
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksafindOrCreateLanguage lid = do
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let languageSlugS = parameterize $ show lid
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa languageL <- select $ from $ \languages -> do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa where_ (languages ^. LanguageSlug ==. val languageSlugS)
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa return languages
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa case languageL of
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa [] -> insert Language
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa { languageSlug = languageSlugS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , languageName = show lid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , languageDescription = description lid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , languageStandardizationStatus = "TODO" -- TODO: add to class Logic
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , languageDefinedBy = "registry" -- TODO: add to class Logic (URL)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa }
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa Entity key _ : _-> return key
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksafindOrCreateLogic :: ( MonadIO m
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , Logic.Logic lid sublogics basic_spec sentence
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa symb_items symb_map_items sign morphism symbol
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa raw_symbol proof_tree
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa )
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa => HetcatsOpts -> LanguageId -> lid -> sublogics
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -> DBMonad m LogicId
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksafindOrCreateLogic opts languageKey lid sublogic = do
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let logicNameS = sublogicNameForDB lid sublogic
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let logicSlugS = parameterize logicNameS
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa logicL <- select $ from $ \logicsSql -> do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa where_ (logicsSql ^. LogicSlug ==. val logicSlugS)
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa return logicsSql
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa case logicL of
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa [] ->
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -- This is a two-staged process to save some performance:
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -- Case 1: If the logic existed beforehand, then we don't lock the
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -- database and return the logic ID. This is expected to happen very
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -- frequently.
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -- Case 2: If the logic did not exist at this point, we need to create
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -- it atomically. To do this, we do a find-or-create pattern inside a
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -- mutex. This is expected to happen only a few times.
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa advisoryLocked opts migrateLogicGraphKey $ do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa logicL' <- select $ from $ \logicsSql -> do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa where_ (logicsSql ^. LogicSlug ==. val logicSlugS)
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa return logicsSql
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa case logicL' of
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa [] -> insert SchemaClass.Logic
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa { logicLanguageId = languageKey
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , logicSlug = logicSlugS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , logicName = logicNameS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa }
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa Entity key _ : _ -> return key
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa Entity key _ : _ -> return key
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa-- Export all LanguageMappings and LogicMappings. Add those that have been added
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa-- since a previous version of Hets. This does not delete any of the old
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa-- mappings.
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaexportLanguageMappingsAndLogicMappings :: MonadIO m
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa => HetcatsOpts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -> LogicGraph -> DBMonad m ()
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaexportLanguageMappingsAndLogicMappings opts logicGraph =
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa mapM_ (findOrCreateLanguageMappingAndLogicMapping opts) $
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa comorphisms logicGraph
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksafindOrCreateLanguageMappingAndLogicMapping :: MonadIO m
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa => HetcatsOpts -> AnyComorphism
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -> DBMonad m ( LanguageMappingId
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , LogicMappingId
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa )
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksafindOrCreateLanguageMappingAndLogicMapping opts (Comorphism.Comorphism cid) =
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let sourceLanguageSlugS = parameterize $ show $ sourceLogic cid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa targetLanguageSlugS = parameterize $ show $ targetLogic cid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa in do
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -- Find the IDs in the databases:
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa Entity sourceLanguageKey _ : _ <- select $ from $ \languages -> do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa where_ (languages ^. LanguageSlug ==. val sourceLanguageSlugS)
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa return languages
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa Entity targetLanguageKey _ : _ <- select $ from $ \languages -> do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa where_ (languages ^. LanguageSlug ==. val targetLanguageSlugS)
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa return languages
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa sourceLogicKey <-
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa findOrCreateLogic opts sourceLanguageKey (sourceLogic cid) $ sourceSublogic cid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa targetLogicKey <-
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa findOrCreateLogic opts targetLanguageKey (targetLogic cid) $ targetSublogic cid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa languageMappingKey <-
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa findOrCreateLanguageMapping sourceLanguageKey targetLanguageKey
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa logicMappingKey <-
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa findOrCreateLogicMapping sourceLogicKey targetLogicKey languageMappingKey $ Comorphism.Comorphism cid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa return (languageMappingKey, logicMappingKey)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksafindOrCreateLanguageMapping :: MonadIO m
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa => LanguageId -> LanguageId
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -> DBMonad m LanguageMappingId
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksafindOrCreateLanguageMapping sourceLanguageKey targetLanguageKey = do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa languageMappingL <- select $ from $ \language_mappings -> do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa where_ (language_mappings ^. LanguageMappingSourceId ==. val sourceLanguageKey
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa &&. language_mappings ^. LanguageMappingTargetId ==. val targetLanguageKey)
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa return language_mappings
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa case languageMappingL of
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa [] -> insert LanguageMapping
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa { languageMappingSourceId = sourceLanguageKey
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , languageMappingTargetId = targetLanguageKey
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa }
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa Entity key _ : _ -> return key
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksafindOrCreateLogicMapping :: MonadIO m
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa => LogicId -> LogicId -> LanguageMappingId -> AnyComorphism
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -> DBMonad m LogicMappingId
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksafindOrCreateLogicMapping sourceLogicKey targetLogicKey languageMappingKey (Comorphism.Comorphism cid) = do
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let name = language_name cid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let logicMappingSlugS = parameterize name
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa logicMappingL <- select $ from $ \logic_mappings -> do
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa where_ (logic_mappings ^. LogicMappingLanguageMappingId ==. val languageMappingKey
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa &&. logic_mappings ^. LogicMappingSlug ==. val logicMappingSlugS)
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa return logic_mappings
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa case logicMappingL of
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa [] -> insert LogicMapping
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa { logicMappingLanguageMappingId = languageMappingKey
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , logicMappingSourceId = sourceLogicKey
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , logicMappingTargetId = targetLogicKey
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , logicMappingSlug = logicMappingSlugS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , logicMappingName = name
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , logicMappingIsInclusion = isInclusionComorphism cid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , logicMappingHasModelExpansion = has_model_expansion cid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , logicMappingIsWeaklyAmalgamable = is_weakly_amalgamable cid
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa }
9d63e3d6c1c65ab10d1459b9f59a134161acc1d7Eugen Kuksa Entity key _ : _ -> return key
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksasublogicNameForDB :: Logic.Logic lid sublogics basic_spec sentence symb_items
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa symb_map_items sign morphism symbol raw_symbol proof_tree
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa => lid -> sublogics -> String
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksasublogicNameForDB lid sublogic =
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let hetsName = sublogicName sublogic
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa in if null hetsName then show lid else hetsName