{-# 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 :: String
migrateLogicGraphKey = "migrateLogicGraph"

exportLogicGraph :: HetcatsOpts -> IO ()
exportLogicGraph :: HetcatsOpts -> IO ()
exportLogicGraph opts :: HetcatsOpts
opts =
  DBConfig -> DBMonad (NoLoggingT IO) () -> IO ()
forall (m :: * -> *) a.
(MonadIO m, MonadBaseControl IO m, MonadUnliftIO m, MonadFail m) =>
DBConfig -> DBMonad (NoLoggingT m) a -> m a
onDatabase (HetcatsOpts -> DBConfig
databaseConfig HetcatsOpts
opts) (DBMonad (NoLoggingT IO) () -> IO ())
-> DBMonad (NoLoggingT IO) () -> IO ()
forall a b. (a -> b) -> a -> b
$
    HetcatsOpts
-> String
-> DBMonad (NoLoggingT IO) ()
-> DBMonad (NoLoggingT IO) ()
forall (m :: * -> *) a.
MonadIO m =>
HetcatsOpts -> String -> DBMonad m a -> DBMonad m a
advisoryLocked HetcatsOpts
opts String
migrateLogicGraphKey (DBMonad (NoLoggingT IO) () -> DBMonad (NoLoggingT IO) ())
-> DBMonad (NoLoggingT IO) () -> DBMonad (NoLoggingT IO) ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> DBMonad (NoLoggingT IO) ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts -> DBMonad m ()
migrateLogicGraph HetcatsOpts
opts

migrateLogicGraph :: (MonadIO m, Fail.MonadFail m) => HetcatsOpts -> DBMonad m ()
migrateLogicGraph :: HetcatsOpts -> DBMonad m ()
migrateLogicGraph opts :: HetcatsOpts
opts = do
  let versionKeyName :: String
versionKeyName = "lastMigratedVersion"
  do
    [Entity Hets]
lastMigratedVersionL <- SqlQuery (SqlExpr (Entity Hets))
-> ReaderT SqlBackend m [Entity Hets]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Hets))
 -> ReaderT SqlBackend m [Entity Hets])
-> SqlQuery (SqlExpr (Entity Hets))
-> ReaderT SqlBackend m [Entity Hets]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity Hets) -> SqlQuery (SqlExpr (Entity Hets)))
-> SqlQuery (SqlExpr (Entity Hets))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity Hets) -> SqlQuery (SqlExpr (Entity Hets)))
 -> SqlQuery (SqlExpr (Entity Hets)))
-> (SqlExpr (Entity Hets) -> SqlQuery (SqlExpr (Entity Hets)))
-> SqlQuery (SqlExpr (Entity Hets))
forall a b. (a -> b) -> a -> b
$ \hets :: SqlExpr (Entity Hets)
hets -> do
      SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity Hets)
hets SqlExpr (Entity Hets)
-> EntityField Hets String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Hets String
forall typ. (typ ~ String) => EntityField Hets typ
HetsKey SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
versionKeyName)
      SqlExpr (Entity Hets) -> SqlQuery (SqlExpr (Entity Hets))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Hets)
hets
    case [Entity Hets]
lastMigratedVersionL of
      [] ->
        Hets -> ReaderT SqlBackend m (Key Hets)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert (String -> String -> Hets
Hets String
versionKeyName String
hetsVersionNumeric) ReaderT SqlBackend m (Key Hets) -> DBMonad m () -> DBMonad m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> HetcatsOpts -> DBMonad m ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts -> DBMonad m ()
migrateLogicGraph' HetcatsOpts
opts
      Entity _ value :: Hets
value : _ ->
        Bool -> DBMonad m () -> DBMonad m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Hets -> String
hetsValue Hets
value String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
hetsVersionNumeric) (DBMonad m () -> DBMonad m ()) -> DBMonad m () -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> DBMonad m ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts -> DBMonad m ()
migrateLogicGraph' HetcatsOpts
opts

migrateLogicGraph' :: (MonadIO m, Fail.MonadFail m) => HetcatsOpts -> DBMonad m ()
migrateLogicGraph' :: HetcatsOpts -> DBMonad m ()
migrateLogicGraph' opts :: HetcatsOpts
opts = do
  HetcatsOpts -> LogicGraph -> DBMonad m ()
forall (m :: * -> *).
MonadIO m =>
HetcatsOpts -> LogicGraph -> DBMonad m ()
exportLanguagesAndLogics HetcatsOpts
opts LogicGraph
LogicGraph.logicGraph
  HetcatsOpts -> LogicGraph -> DBMonad m ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts -> LogicGraph -> DBMonad m ()
exportLanguageMappingsAndLogicMappings HetcatsOpts
opts LogicGraph
LogicGraph.logicGraph
  HetcatsOpts -> LogicGraph -> DBMonad m ()
forall (m :: * -> *).
MonadIO m =>
HetcatsOpts -> LogicGraph -> DBMonad m ()
exportReasoners HetcatsOpts
opts LogicGraph
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 :: HetcatsOpts -> LogicGraph -> DBMonad m ()
exportLanguagesAndLogics opts :: HetcatsOpts
opts logicGraph :: LogicGraph
logicGraph =
  (AnyLogic -> DBMonad m ()) -> Map String AnyLogic -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Logic.Logic lid :: lid
lid) -> do
          LanguageId
languageKey <- lid -> DBMonad m LanguageId
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
lid -> DBMonad m LanguageId
findOrCreateLanguage lid
lid
          (sublogics -> ReaderT SqlBackend m LogicId)
-> [sublogics] -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HetcatsOpts
-> LanguageId -> lid -> sublogics -> ReaderT SqlBackend m LogicId
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m,
 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 HetcatsOpts
opts LanguageId
languageKey lid
lid) ([sublogics] -> DBMonad m ()) -> [sublogics] -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$ lid -> [sublogics]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [sublogics]
all_sublogics lid
lid
        ) (Map String AnyLogic -> DBMonad m ())
-> Map String AnyLogic -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
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 -> DBMonad m LanguageId
findOrCreateLanguage lid :: lid
lid = do
  let languageSlugS :: String
languageSlugS = String -> String
slugOfLanguageByName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid
  Maybe (Entity Language)
languageM <- String -> DBMonad m (Maybe (Entity Language))
forall (m :: * -> *).
MonadIO m =>
String -> DBMonad m (Maybe (Entity Language))
findLanguage String
languageSlugS
  case Maybe (Entity Language)
languageM of
    Nothing -> Language -> DBMonad m LanguageId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WLanguage :: String -> String -> String -> String -> String -> Language
Language
        { languageSlug :: String
languageSlug = String
languageSlugS
        , languageName :: String
languageName = lid -> String
forall a. Show a => a -> String
show lid
lid
        , languageDescription :: String
languageDescription = lid -> String
forall lid. Language lid => lid -> String
description lid
lid
        , languageStandardizationStatus :: String
languageStandardizationStatus = "TODO" -- TODO: add to class Logic
        , languageDefinedBy :: String
languageDefinedBy = "registry" -- TODO: add to class Logic (URL)
        }
    Just (Entity key :: LanguageId
key _) -> LanguageId -> DBMonad m LanguageId
forall (m :: * -> *) a. Monad m => a -> m a
return LanguageId
key

findLanguage :: MonadIO m
             => String -> DBMonad m (Maybe (Entity DatabaseSchema.Language))
findLanguage :: String -> DBMonad m (Maybe (Entity Language))
findLanguage languageSlugS :: String
languageSlugS = do
  [Entity Language]
languageL <- SqlQuery (SqlExpr (Entity Language))
-> ReaderT SqlBackend m [Entity Language]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Language))
 -> ReaderT SqlBackend m [Entity Language])
-> SqlQuery (SqlExpr (Entity Language))
-> ReaderT SqlBackend m [Entity Language]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity Language) -> SqlQuery (SqlExpr (Entity Language)))
-> SqlQuery (SqlExpr (Entity Language))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity Language)
  -> SqlQuery (SqlExpr (Entity Language)))
 -> SqlQuery (SqlExpr (Entity Language)))
-> (SqlExpr (Entity Language)
    -> SqlQuery (SqlExpr (Entity Language)))
-> SqlQuery (SqlExpr (Entity Language))
forall a b. (a -> b) -> a -> b
$ \languages :: SqlExpr (Entity Language)
languages -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity Language)
languages SqlExpr (Entity Language)
-> EntityField Language String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Language String
forall typ. (typ ~ String) => EntityField Language typ
LanguageSlug SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
languageSlugS)
    SqlExpr (Entity Language) -> SqlQuery (SqlExpr (Entity Language))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Language)
languages
  case [Entity Language]
languageL of
    [] -> Maybe (Entity Language) -> DBMonad m (Maybe (Entity Language))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Entity Language)
forall a. Maybe a
Nothing
    entity :: Entity Language
entity : _ -> Maybe (Entity Language) -> DBMonad m (Maybe (Entity Language))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Entity Language) -> DBMonad m (Maybe (Entity Language)))
-> Maybe (Entity Language) -> DBMonad m (Maybe (Entity Language))
forall a b. (a -> b) -> a -> b
$ Entity Language -> Maybe (Entity Language)
forall a. a -> Maybe a
Just Entity Language
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 :: HetcatsOpts -> LanguageId -> lid -> sublogics -> DBMonad m LogicId
findOrCreateLogic opts :: HetcatsOpts
opts languageKey :: LanguageId
languageKey lid :: lid
lid sublogic :: sublogics
sublogic = do
  let logicNameS :: String
logicNameS = lid -> sublogics -> String
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> String
logicNameForDB lid
lid sublogics
sublogic
  let logicSlugS :: String
logicSlugS = String -> String
slugOfLogicByName String
logicNameS
  Maybe (Entity Logic)
logicM <- String -> DBMonad m (Maybe (Entity Logic))
forall (m :: * -> *).
MonadIO m =>
String -> DBMonad m (Maybe (Entity Logic))
findLogic String
logicSlugS
  case Maybe (Entity Logic)
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.
      HetcatsOpts -> String -> DBMonad m LogicId -> DBMonad m LogicId
forall (m :: * -> *) a.
MonadIO m =>
HetcatsOpts -> String -> DBMonad m a -> DBMonad m a
advisoryLocked HetcatsOpts
opts String
migrateLogicGraphKey (DBMonad m LogicId -> DBMonad m LogicId)
-> DBMonad m LogicId -> DBMonad m LogicId
forall a b. (a -> b) -> a -> b
$ do
        Maybe (Entity Logic)
logicM' <- String -> DBMonad m (Maybe (Entity Logic))
forall (m :: * -> *).
MonadIO m =>
String -> DBMonad m (Maybe (Entity Logic))
findLogic String
logicSlugS
        case Maybe (Entity Logic)
logicM' of
          Nothing -> Logic -> DBMonad m LogicId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WLogic :: LanguageId -> String -> String -> Logic
DatabaseSchema.Logic
            { logicLanguageId :: LanguageId
logicLanguageId = LanguageId
languageKey
            , logicSlug :: String
logicSlug = String
logicSlugS
            , logicName :: String
logicName = String
logicNameS
            }
          Just (Entity key :: LogicId
key _) -> LogicId -> DBMonad m LogicId
forall (m :: * -> *) a. Monad m => a -> m a
return LogicId
key
    Just (Entity key :: LogicId
key _) -> LogicId -> DBMonad m LogicId
forall (m :: * -> *) a. Monad m => a -> m a
return LogicId
key

findLogic :: MonadIO m
          => String -> DBMonad m (Maybe (Entity DatabaseSchema.Logic))
findLogic :: String -> DBMonad m (Maybe (Entity Logic))
findLogic logicSlugS :: String
logicSlugS = do
  [Entity Logic]
logicL <- SqlQuery (SqlExpr (Entity Logic))
-> ReaderT SqlBackend m [Entity Logic]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Logic))
 -> ReaderT SqlBackend m [Entity Logic])
-> SqlQuery (SqlExpr (Entity Logic))
-> ReaderT SqlBackend m [Entity Logic]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity Logic) -> SqlQuery (SqlExpr (Entity Logic)))
-> SqlQuery (SqlExpr (Entity Logic))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity Logic) -> SqlQuery (SqlExpr (Entity Logic)))
 -> SqlQuery (SqlExpr (Entity Logic)))
-> (SqlExpr (Entity Logic) -> SqlQuery (SqlExpr (Entity Logic)))
-> SqlQuery (SqlExpr (Entity Logic))
forall a b. (a -> b) -> a -> b
$ \logicsSql :: SqlExpr (Entity Logic)
logicsSql -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity Logic)
logicsSql SqlExpr (Entity Logic)
-> EntityField Logic String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Logic String
forall typ. (typ ~ String) => EntityField Logic typ
LogicSlug SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
logicSlugS)
    SqlExpr (Entity Logic) -> SqlQuery (SqlExpr (Entity Logic))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Logic)
logicsSql
  case [Entity Logic]
logicL of
    [] -> Maybe (Entity Logic) -> DBMonad m (Maybe (Entity Logic))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Entity Logic)
forall a. Maybe a
Nothing
    entity :: Entity Logic
entity : _ -> Maybe (Entity Logic) -> DBMonad m (Maybe (Entity Logic))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Entity Logic) -> DBMonad m (Maybe (Entity Logic)))
-> Maybe (Entity Logic) -> DBMonad m (Maybe (Entity Logic))
forall a b. (a -> b) -> a -> b
$ Entity Logic -> Maybe (Entity Logic)
forall a. a -> Maybe a
Just Entity Logic
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 :: HetcatsOpts -> LogicGraph -> DBMonad m ()
exportLanguageMappingsAndLogicMappings opts :: HetcatsOpts
opts logicGraph :: LogicGraph
logicGraph =
  (AnyComorphism
 -> ReaderT SqlBackend m (LanguageMappingId, LogicMappingId))
-> Map String AnyComorphism -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HetcatsOpts
-> AnyComorphism
-> ReaderT SqlBackend m (LanguageMappingId, LogicMappingId)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> AnyComorphism -> DBMonad m (LanguageMappingId, LogicMappingId)
findOrCreateLanguageMappingAndLogicMapping HetcatsOpts
opts) (Map String AnyComorphism -> DBMonad m ())
-> Map String AnyComorphism -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$
    LogicGraph -> Map String AnyComorphism
comorphisms LogicGraph
logicGraph

findOrCreateLanguageMappingAndLogicMapping :: (MonadIO m, Fail.MonadFail m)
                                           => HetcatsOpts -> AnyComorphism
                                           -> DBMonad m ( LanguageMappingId
                                                        , LogicMappingId
                                                        )
findOrCreateLanguageMappingAndLogicMapping :: HetcatsOpts
-> AnyComorphism -> DBMonad m (LanguageMappingId, LogicMappingId)
findOrCreateLanguageMappingAndLogicMapping opts :: HetcatsOpts
opts (Comorphism.Comorphism cid :: cid
cid) =
  let sourceLanguageSlugS :: String
sourceLanguageSlugS = String -> String
slugOfLanguageByName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ lid1 -> String
forall lid. Language lid => lid -> String
language_name (lid1 -> String) -> lid1 -> String
forall a b. (a -> b) -> a -> b
$ cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid
      targetLanguageSlugS :: String
targetLanguageSlugS = String -> String
slugOfLanguageByName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ lid2 -> String
forall lid. Language lid => lid -> String
language_name (lid2 -> String) -> lid2 -> String
forall a b. (a -> b) -> a -> b
$ cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid
  in do
    -- Find the IDs in the databases:
    Entity sourceLanguageKey :: LanguageId
sourceLanguageKey _ : _ <- SqlQuery (SqlExpr (Entity Language))
-> ReaderT SqlBackend m [Entity Language]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Language))
 -> ReaderT SqlBackend m [Entity Language])
-> SqlQuery (SqlExpr (Entity Language))
-> ReaderT SqlBackend m [Entity Language]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity Language) -> SqlQuery (SqlExpr (Entity Language)))
-> SqlQuery (SqlExpr (Entity Language))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity Language)
  -> SqlQuery (SqlExpr (Entity Language)))
 -> SqlQuery (SqlExpr (Entity Language)))
-> (SqlExpr (Entity Language)
    -> SqlQuery (SqlExpr (Entity Language)))
-> SqlQuery (SqlExpr (Entity Language))
forall a b. (a -> b) -> a -> b
$ \languages :: SqlExpr (Entity Language)
languages -> do
      SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity Language)
languages SqlExpr (Entity Language)
-> EntityField Language String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Language String
forall typ. (typ ~ String) => EntityField Language typ
LanguageSlug SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
sourceLanguageSlugS)
      SqlExpr (Entity Language) -> SqlQuery (SqlExpr (Entity Language))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Language)
languages

    Entity targetLanguageKey :: LanguageId
targetLanguageKey _ : _ <- SqlQuery (SqlExpr (Entity Language))
-> ReaderT SqlBackend m [Entity Language]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Language))
 -> ReaderT SqlBackend m [Entity Language])
-> SqlQuery (SqlExpr (Entity Language))
-> ReaderT SqlBackend m [Entity Language]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity Language) -> SqlQuery (SqlExpr (Entity Language)))
-> SqlQuery (SqlExpr (Entity Language))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity Language)
  -> SqlQuery (SqlExpr (Entity Language)))
 -> SqlQuery (SqlExpr (Entity Language)))
-> (SqlExpr (Entity Language)
    -> SqlQuery (SqlExpr (Entity Language)))
-> SqlQuery (SqlExpr (Entity Language))
forall a b. (a -> b) -> a -> b
$ \languages :: SqlExpr (Entity Language)
languages -> do
      SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity Language)
languages SqlExpr (Entity Language)
-> EntityField Language String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Language String
forall typ. (typ ~ String) => EntityField Language typ
LanguageSlug SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
targetLanguageSlugS)
      SqlExpr (Entity Language) -> SqlQuery (SqlExpr (Entity Language))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Language)
languages

    LogicId
sourceLogicKey <-
      HetcatsOpts
-> LanguageId -> lid1 -> sublogics1 -> DBMonad m LogicId
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m,
 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 HetcatsOpts
opts LanguageId
sourceLanguageKey (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid) (sublogics1 -> DBMonad m LogicId)
-> sublogics1 -> DBMonad m LogicId
forall a b. (a -> b) -> a -> b
$ cid -> sublogics1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics1
sourceSublogic cid
cid
    LogicId
targetLogicKey <-
      HetcatsOpts
-> LanguageId -> lid2 -> sublogics2 -> DBMonad m LogicId
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m,
 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 HetcatsOpts
opts LanguageId
targetLanguageKey (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) (sublogics2 -> DBMonad m LogicId)
-> sublogics2 -> DBMonad m LogicId
forall a b. (a -> b) -> a -> b
$ cid -> sublogics2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics2
targetSublogic cid
cid

    LanguageMappingId
languageMappingKey <-
      LanguageId -> LanguageId -> DBMonad m LanguageMappingId
forall (m :: * -> *).
MonadIO m =>
LanguageId -> LanguageId -> DBMonad m LanguageMappingId
findOrCreateLanguageMapping LanguageId
sourceLanguageKey LanguageId
targetLanguageKey
    LogicMappingId
logicMappingKey <-
      LogicId
-> LogicId
-> LanguageMappingId
-> AnyComorphism
-> DBMonad m LogicMappingId
forall (m :: * -> *).
MonadIO m =>
LogicId
-> LogicId
-> LanguageMappingId
-> AnyComorphism
-> DBMonad m LogicMappingId
findOrCreateLogicMapping LogicId
sourceLogicKey LogicId
targetLogicKey LanguageMappingId
languageMappingKey (AnyComorphism -> DBMonad m LogicMappingId)
-> AnyComorphism -> DBMonad m LogicMappingId
forall a b. (a -> b) -> a -> b
$ cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism.Comorphism cid
cid

    (LanguageMappingId, LogicMappingId)
-> DBMonad m (LanguageMappingId, LogicMappingId)
forall (m :: * -> *) a. Monad m => a -> m a
return (LanguageMappingId
languageMappingKey, LogicMappingId
logicMappingKey)

findOrCreateLanguageMapping :: MonadIO m
                            => LanguageId -> LanguageId
                            -> DBMonad m LanguageMappingId
findOrCreateLanguageMapping :: LanguageId -> LanguageId -> DBMonad m LanguageMappingId
findOrCreateLanguageMapping sourceLanguageKey :: LanguageId
sourceLanguageKey targetLanguageKey :: LanguageId
targetLanguageKey = do
  [Entity LanguageMapping]
languageMappingL <- SqlQuery (SqlExpr (Entity LanguageMapping))
-> ReaderT SqlBackend m [Entity LanguageMapping]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LanguageMapping))
 -> ReaderT SqlBackend m [Entity LanguageMapping])
-> SqlQuery (SqlExpr (Entity LanguageMapping))
-> ReaderT SqlBackend m [Entity LanguageMapping]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LanguageMapping)
 -> SqlQuery (SqlExpr (Entity LanguageMapping)))
-> SqlQuery (SqlExpr (Entity LanguageMapping))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LanguageMapping)
  -> SqlQuery (SqlExpr (Entity LanguageMapping)))
 -> SqlQuery (SqlExpr (Entity LanguageMapping)))
-> (SqlExpr (Entity LanguageMapping)
    -> SqlQuery (SqlExpr (Entity LanguageMapping)))
-> SqlQuery (SqlExpr (Entity LanguageMapping))
forall a b. (a -> b) -> a -> b
$ \language_mappings :: SqlExpr (Entity LanguageMapping)
language_mappings -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LanguageMapping)
language_mappings SqlExpr (Entity LanguageMapping)
-> EntityField LanguageMapping LanguageId
-> SqlExpr (Value LanguageId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LanguageMapping LanguageId
forall typ. (typ ~ LanguageId) => EntityField LanguageMapping typ
LanguageMappingSourceId SqlExpr (Value LanguageId)
-> SqlExpr (Value LanguageId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LanguageId -> SqlExpr (Value LanguageId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LanguageId
sourceLanguageKey
            SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LanguageMapping)
language_mappings SqlExpr (Entity LanguageMapping)
-> EntityField LanguageMapping LanguageId
-> SqlExpr (Value LanguageId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LanguageMapping LanguageId
forall typ. (typ ~ LanguageId) => EntityField LanguageMapping typ
LanguageMappingTargetId SqlExpr (Value LanguageId)
-> SqlExpr (Value LanguageId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LanguageId -> SqlExpr (Value LanguageId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LanguageId
targetLanguageKey)
    SqlExpr (Entity LanguageMapping)
-> SqlQuery (SqlExpr (Entity LanguageMapping))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LanguageMapping)
language_mappings
  case [Entity LanguageMapping]
languageMappingL of
    [] -> LanguageMapping -> DBMonad m LanguageMappingId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WLanguageMapping :: LanguageId -> LanguageId -> LanguageMapping
LanguageMapping
      { languageMappingSourceId :: LanguageId
languageMappingSourceId = LanguageId
sourceLanguageKey
      , languageMappingTargetId :: LanguageId
languageMappingTargetId = LanguageId
targetLanguageKey
      }
    Entity key :: LanguageMappingId
key _ : _ -> LanguageMappingId -> DBMonad m LanguageMappingId
forall (m :: * -> *) a. Monad m => a -> m a
return LanguageMappingId
key

findOrCreateLogicMapping :: MonadIO m
                         => LogicId -> LogicId -> LanguageMappingId -> AnyComorphism
                         -> DBMonad m LogicMappingId
findOrCreateLogicMapping :: LogicId
-> LogicId
-> LanguageMappingId
-> AnyComorphism
-> DBMonad m LogicMappingId
findOrCreateLogicMapping sourceLogicKey :: LogicId
sourceLogicKey targetLogicKey :: LogicId
targetLogicKey languageMappingKey :: LanguageMappingId
languageMappingKey (Comorphism.Comorphism cid :: cid
cid) = do
  let name :: String
name = cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid
  let logicMappingSlugS :: String
logicMappingSlugS = AnyComorphism -> String
slugOfLogicMapping (cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism.Comorphism cid
cid)
  [Entity LogicMapping]
logicMappingL <- SqlQuery (SqlExpr (Entity LogicMapping))
-> ReaderT SqlBackend m [Entity LogicMapping]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LogicMapping))
 -> ReaderT SqlBackend m [Entity LogicMapping])
-> SqlQuery (SqlExpr (Entity LogicMapping))
-> ReaderT SqlBackend m [Entity LogicMapping]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LogicMapping)
 -> SqlQuery (SqlExpr (Entity LogicMapping)))
-> SqlQuery (SqlExpr (Entity LogicMapping))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LogicMapping)
  -> SqlQuery (SqlExpr (Entity LogicMapping)))
 -> SqlQuery (SqlExpr (Entity LogicMapping)))
-> (SqlExpr (Entity LogicMapping)
    -> SqlQuery (SqlExpr (Entity LogicMapping)))
-> SqlQuery (SqlExpr (Entity LogicMapping))
forall a b. (a -> b) -> a -> b
$ \logic_mappings :: SqlExpr (Entity LogicMapping)
logic_mappings -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LogicMapping)
logic_mappings SqlExpr (Entity LogicMapping)
-> EntityField LogicMapping LanguageMappingId
-> SqlExpr (Value LanguageMappingId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LogicMapping LanguageMappingId
forall typ.
(typ ~ LanguageMappingId) =>
EntityField LogicMapping typ
LogicMappingLanguageMappingId SqlExpr (Value LanguageMappingId)
-> SqlExpr (Value LanguageMappingId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LanguageMappingId -> SqlExpr (Value LanguageMappingId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LanguageMappingId
languageMappingKey
            SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LogicMapping)
logic_mappings SqlExpr (Entity LogicMapping)
-> EntityField LogicMapping String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LogicMapping String
forall typ. (typ ~ String) => EntityField LogicMapping typ
LogicMappingSlug SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
logicMappingSlugS)
    SqlExpr (Entity LogicMapping)
-> SqlQuery (SqlExpr (Entity LogicMapping))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LogicMapping)
logic_mappings
  case [Entity LogicMapping]
logicMappingL of
    [] -> LogicMapping -> DBMonad m LogicMappingId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WLogicMapping :: LanguageMappingId
-> LogicId
-> LogicId
-> String
-> String
-> Bool
-> Bool
-> Bool
-> LogicMapping
LogicMapping
      { logicMappingLanguageMappingId :: LanguageMappingId
logicMappingLanguageMappingId = LanguageMappingId
languageMappingKey
      , logicMappingSourceId :: LogicId
logicMappingSourceId = LogicId
sourceLogicKey
      , logicMappingTargetId :: LogicId
logicMappingTargetId = LogicId
targetLogicKey
      , logicMappingSlug :: String
logicMappingSlug = String
logicMappingSlugS
      , logicMappingName :: String
logicMappingName = String
name
      , logicMappingIsInclusion :: Bool
logicMappingIsInclusion = cid -> Bool
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> Bool
isInclusionComorphism cid
cid
      , logicMappingHasModelExpansion :: Bool
logicMappingHasModelExpansion = cid -> Bool
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> Bool
has_model_expansion cid
cid
      , logicMappingIsWeaklyAmalgamable :: Bool
logicMappingIsWeaklyAmalgamable = cid -> Bool
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> Bool
is_weakly_amalgamable cid
cid
      }
    Entity key :: LogicMappingId
key _ : _ -> LogicMappingId -> DBMonad m LogicMappingId
forall (m :: * -> *) a. Monad m => a -> m a
return LogicMappingId
key

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

findLogicMappingBySlug :: (MonadIO m, Fail.MonadFail m)
                       => String
                       -> DBMonad m (Maybe (Entity LogicMapping))
findLogicMappingBySlug :: String -> DBMonad m (Maybe (Entity LogicMapping))
findLogicMappingBySlug logicMappingSlugS :: String
logicMappingSlugS = do
  [Entity LogicMapping]
logicMappingL <- SqlQuery (SqlExpr (Entity LogicMapping))
-> ReaderT SqlBackend m [Entity LogicMapping]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LogicMapping))
 -> ReaderT SqlBackend m [Entity LogicMapping])
-> SqlQuery (SqlExpr (Entity LogicMapping))
-> ReaderT SqlBackend m [Entity LogicMapping]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LogicMapping)
 -> SqlQuery (SqlExpr (Entity LogicMapping)))
-> SqlQuery (SqlExpr (Entity LogicMapping))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LogicMapping)
  -> SqlQuery (SqlExpr (Entity LogicMapping)))
 -> SqlQuery (SqlExpr (Entity LogicMapping)))
-> (SqlExpr (Entity LogicMapping)
    -> SqlQuery (SqlExpr (Entity LogicMapping)))
-> SqlQuery (SqlExpr (Entity LogicMapping))
forall a b. (a -> b) -> a -> b
$ \ logic_mappings :: SqlExpr (Entity LogicMapping)
logic_mappings -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LogicMapping)
logic_mappings SqlExpr (Entity LogicMapping)
-> EntityField LogicMapping String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LogicMapping String
forall typ. (typ ~ String) => EntityField LogicMapping typ
LogicMappingSlug SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
logicMappingSlugS)
    SqlExpr (Entity LogicMapping)
-> SqlQuery (SqlExpr (Entity LogicMapping))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LogicMapping)
logic_mappings
  case [Entity LogicMapping]
logicMappingL of
    [] -> String -> DBMonad m (Maybe (Entity LogicMapping))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.LogicGraph.findLogicMappingBySlug: Could not find LogicMapping " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
logicMappingSlugS)
    logicMappingEntity :: Entity LogicMapping
logicMappingEntity : _ -> Maybe (Entity LogicMapping)
-> DBMonad m (Maybe (Entity LogicMapping))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Entity LogicMapping)
 -> DBMonad m (Maybe (Entity LogicMapping)))
-> Maybe (Entity LogicMapping)
-> DBMonad m (Maybe (Entity LogicMapping))
forall a b. (a -> b) -> a -> b
$ Entity LogicMapping -> Maybe (Entity LogicMapping)
forall a. a -> Maybe a
Just Entity LogicMapping
logicMappingEntity

exportReasoners :: MonadIO m => HetcatsOpts -> LogicGraph -> DBMonad m ()
exportReasoners :: HetcatsOpts -> LogicGraph -> DBMonad m ()
exportReasoners _ logicGraph :: LogicGraph
logicGraph =
  (AnyLogic -> DBMonad m ()) -> Map String AnyLogic -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Logic.Logic lid :: lid
lid) -> do
          let proversL :: [Prover sign sentence morphism sublogics proof_tree]
proversL = lid -> [Prover sign sentence morphism sublogics proof_tree]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [Prover sign sentence morphism sublogics proof_tree]
provers lid
lid
          let consistencyCheckersL :: [ConsChecker sign sentence sublogics morphism proof_tree]
consistencyCheckersL = lid -> [ConsChecker sign sentence sublogics morphism proof_tree]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [ConsChecker sign sentence sublogics morphism proof_tree]
cons_checkers lid
lid
          (Prover sign sentence morphism sublogics proof_tree
 -> ReaderT SqlBackend m ReasonerId)
-> [Prover sign sentence morphism sublogics proof_tree]
-> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (G_prover -> ReaderT SqlBackend m ReasonerId
forall (m :: * -> *). MonadIO m => G_prover -> DBMonad m ReasonerId
findOrCreateProver (G_prover -> ReaderT SqlBackend m ReasonerId)
-> (Prover sign sentence morphism sublogics proof_tree -> G_prover)
-> Prover sign sentence morphism sublogics proof_tree
-> ReaderT SqlBackend m ReasonerId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid
-> Prover sign sentence morphism sublogics proof_tree -> G_prover
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Prover sign sentence morphism sublogics proof_tree -> G_prover
G_prover lid
lid) [Prover sign sentence morphism sublogics proof_tree]
proversL
          (ConsChecker sign sentence sublogics morphism proof_tree
 -> ReaderT SqlBackend m ReasonerId)
-> [ConsChecker sign sentence sublogics morphism proof_tree]
-> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (G_cons_checker -> ReaderT SqlBackend m ReasonerId
forall (m :: * -> *).
MonadIO m =>
G_cons_checker -> DBMonad m ReasonerId
findOrCreateConsistencyChecker (G_cons_checker -> ReaderT SqlBackend m ReasonerId)
-> (ConsChecker sign sentence sublogics morphism proof_tree
    -> G_cons_checker)
-> ConsChecker sign sentence sublogics morphism proof_tree
-> ReaderT SqlBackend m ReasonerId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid
-> ConsChecker sign sentence sublogics morphism proof_tree
-> G_cons_checker
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> ConsChecker sign sentence sublogics morphism proof_tree
-> G_cons_checker
G_cons_checker lid
lid) [ConsChecker sign sentence sublogics morphism proof_tree]
consistencyCheckersL
        ) (Map String AnyLogic -> DBMonad m ())
-> Map String AnyLogic -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
logicGraph

findOrCreateProver :: MonadIO m => G_prover -> DBMonad m ReasonerId
findOrCreateProver :: G_prover -> DBMonad m ReasonerId
findOrCreateProver gProver :: G_prover
gProver = do
  let reasonerSlugS :: String
reasonerSlugS = G_prover -> String
slugOfProver G_prover
gProver
  let name :: String
name = G_prover -> String
getProverName G_prover
gProver
  String -> String -> ReasonerKindType -> DBMonad m ReasonerId
forall (m :: * -> *).
MonadIO m =>
String -> String -> ReasonerKindType -> DBMonad m ReasonerId
findOrCreateReasoner String
reasonerSlugS String
name ReasonerKindType
Enums.Prover

findOrCreateConsistencyChecker :: MonadIO m => G_cons_checker -> DBMonad m ReasonerId
findOrCreateConsistencyChecker :: G_cons_checker -> DBMonad m ReasonerId
findOrCreateConsistencyChecker gConsistencyChecker :: G_cons_checker
gConsistencyChecker = do
  let reasonerSlugS :: String
reasonerSlugS = G_cons_checker -> String
slugOfConsistencyChecker G_cons_checker
gConsistencyChecker
  let name :: String
name = G_cons_checker -> String
getCcName G_cons_checker
gConsistencyChecker
  String -> String -> ReasonerKindType -> DBMonad m ReasonerId
forall (m :: * -> *).
MonadIO m =>
String -> String -> ReasonerKindType -> DBMonad m ReasonerId
findOrCreateReasoner String
reasonerSlugS String
name ReasonerKindType
Enums.ConsistencyChecker

findReasoner :: MonadIO m
             => String -> Enums.ReasonerKindType
             -> DBMonad m (Maybe (Entity Reasoner))
findReasoner :: String -> ReasonerKindType -> DBMonad m (Maybe (Entity Reasoner))
findReasoner reasonerSlugS :: String
reasonerSlugS reasonerKindValue :: ReasonerKindType
reasonerKindValue = do
  [Entity Reasoner]
reasonerL <-
    SqlQuery (SqlExpr (Entity Reasoner))
-> ReaderT SqlBackend m [Entity Reasoner]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Reasoner))
 -> ReaderT SqlBackend m [Entity Reasoner])
-> SqlQuery (SqlExpr (Entity Reasoner))
-> ReaderT SqlBackend m [Entity Reasoner]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity Reasoner) -> SqlQuery (SqlExpr (Entity Reasoner)))
-> SqlQuery (SqlExpr (Entity Reasoner))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity Reasoner)
  -> SqlQuery (SqlExpr (Entity Reasoner)))
 -> SqlQuery (SqlExpr (Entity Reasoner)))
-> (SqlExpr (Entity Reasoner)
    -> SqlQuery (SqlExpr (Entity Reasoner)))
-> SqlQuery (SqlExpr (Entity Reasoner))
forall a b. (a -> b) -> a -> b
$ \ reasoners :: SqlExpr (Entity Reasoner)
reasoners -> do
      SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity Reasoner)
reasoners SqlExpr (Entity Reasoner)
-> EntityField Reasoner String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Reasoner String
forall typ. (typ ~ String) => EntityField Reasoner typ
ReasonerSlug SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
reasonerSlugS
              SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity Reasoner)
reasoners SqlExpr (Entity Reasoner)
-> EntityField Reasoner ReasonerKindType
-> SqlExpr (Value ReasonerKindType)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Reasoner ReasonerKindType
forall typ. (typ ~ ReasonerKindType) => EntityField Reasoner typ
ReasonerKind SqlExpr (Value ReasonerKindType)
-> SqlExpr (Value ReasonerKindType) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. ReasonerKindType -> SqlExpr (Value ReasonerKindType)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val ReasonerKindType
reasonerKindValue)
      SqlExpr (Entity Reasoner) -> SqlQuery (SqlExpr (Entity Reasoner))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Reasoner)
reasoners
  case [Entity Reasoner]
reasonerL of
    reasoner :: Entity Reasoner
reasoner : _ -> Maybe (Entity Reasoner) -> DBMonad m (Maybe (Entity Reasoner))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Entity Reasoner) -> DBMonad m (Maybe (Entity Reasoner)))
-> Maybe (Entity Reasoner) -> DBMonad m (Maybe (Entity Reasoner))
forall a b. (a -> b) -> a -> b
$ Entity Reasoner -> Maybe (Entity Reasoner)
forall a. a -> Maybe a
Just Entity Reasoner
reasoner
    [] -> Maybe (Entity Reasoner) -> DBMonad m (Maybe (Entity Reasoner))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Entity Reasoner)
forall a. Maybe a
Nothing

findOrCreateReasoner :: MonadIO m
                     => String -> String -> Enums.ReasonerKindType
                     -> DBMonad m ReasonerId
findOrCreateReasoner :: String -> String -> ReasonerKindType -> DBMonad m ReasonerId
findOrCreateReasoner reasonerSlugS :: String
reasonerSlugS name :: String
name reasonerKindValue :: ReasonerKindType
reasonerKindValue = do
  Maybe (Entity Reasoner)
reasonerM <- String -> ReasonerKindType -> DBMonad m (Maybe (Entity Reasoner))
forall (m :: * -> *).
MonadIO m =>
String -> ReasonerKindType -> DBMonad m (Maybe (Entity Reasoner))
findReasoner String
reasonerSlugS ReasonerKindType
reasonerKindValue
  case Maybe (Entity Reasoner)
reasonerM of
    Just (Entity reasonerKey :: ReasonerId
reasonerKey _) -> ReasonerId -> DBMonad m ReasonerId
forall (m :: * -> *) a. Monad m => a -> m a
return ReasonerId
reasonerKey
    Nothing -> Reasoner -> DBMonad m ReasonerId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WReasoner :: String -> ReasonerKindType -> String -> Reasoner
Reasoner
      { reasonerSlug :: String
reasonerSlug = String
reasonerSlugS
      , reasonerDisplayName :: String
reasonerDisplayName = String
name
      , reasonerKind :: ReasonerKindType
reasonerKind = ReasonerKindType
reasonerKindValue
      }

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

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

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

findOrCreateLogicTranslation :: (MonadIO m, Fail.MonadFail m)
                             => HetcatsOpts
                             -> AnyComorphism
                             -> DBMonad m (Maybe (Entity LogicTranslation))
findOrCreateLogicTranslation :: HetcatsOpts
-> AnyComorphism -> DBMonad m (Maybe (Entity LogicTranslation))
findOrCreateLogicTranslation _ comorphism :: AnyComorphism
comorphism@(Comorphism.Comorphism cid :: cid
cid) =
  if AnyComorphism -> Bool
isIdComorphism AnyComorphism
comorphism
  then Maybe (Entity LogicTranslation)
-> DBMonad m (Maybe (Entity LogicTranslation))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Entity LogicTranslation)
forall a. Maybe a
Nothing
  else do
    let logicTranslationSlugS :: String
logicTranslationSlugS = AnyComorphism -> String
slugOfTranslation AnyComorphism
comorphism
    let logicTranslationNameS :: String
logicTranslationNameS = cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid
    [Entity LogicTranslation]
translationL <- SqlQuery (SqlExpr (Entity LogicTranslation))
-> ReaderT SqlBackend m [Entity LogicTranslation]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LogicTranslation))
 -> ReaderT SqlBackend m [Entity LogicTranslation])
-> SqlQuery (SqlExpr (Entity LogicTranslation))
-> ReaderT SqlBackend m [Entity LogicTranslation]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LogicTranslation)
 -> SqlQuery (SqlExpr (Entity LogicTranslation)))
-> SqlQuery (SqlExpr (Entity LogicTranslation))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LogicTranslation)
  -> SqlQuery (SqlExpr (Entity LogicTranslation)))
 -> SqlQuery (SqlExpr (Entity LogicTranslation)))
-> (SqlExpr (Entity LogicTranslation)
    -> SqlQuery (SqlExpr (Entity LogicTranslation)))
-> SqlQuery (SqlExpr (Entity LogicTranslation))
forall a b. (a -> b) -> a -> b
$ \ translations :: SqlExpr (Entity LogicTranslation)
translations -> do
      SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LogicTranslation)
translations SqlExpr (Entity LogicTranslation)
-> EntityField LogicTranslation String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LogicTranslation String
forall typ. (typ ~ String) => EntityField LogicTranslation typ
LogicTranslationSlug SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
logicTranslationSlugS)
      SqlExpr (Entity LogicTranslation)
-> SqlQuery (SqlExpr (Entity LogicTranslation))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LogicTranslation)
translations
    case [Entity LogicTranslation]
translationL of
      translationEntity :: Entity LogicTranslation
translationEntity : _ -> Maybe (Entity LogicTranslation)
-> DBMonad m (Maybe (Entity LogicTranslation))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Entity LogicTranslation)
 -> DBMonad m (Maybe (Entity LogicTranslation)))
-> Maybe (Entity LogicTranslation)
-> DBMonad m (Maybe (Entity LogicTranslation))
forall a b. (a -> b) -> a -> b
$ Entity LogicTranslation -> Maybe (Entity LogicTranslation)
forall a. a -> Maybe a
Just Entity LogicTranslation
translationEntity
      [] -> do
        let logicTranslationValue :: LogicTranslation
logicTranslationValue = $WLogicTranslation :: String -> String -> LogicTranslation
LogicTranslation
              { logicTranslationSlug :: String
logicTranslationSlug = String
logicTranslationSlugS
              , logicTranslationName :: String
logicTranslationName = String
logicTranslationNameS
              }
        Key LogicTranslation
logicTranslationKey <- LogicTranslation -> ReaderT SqlBackend m (Key LogicTranslation)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert LogicTranslation
logicTranslationValue
        ((Int, String)
 -> ReaderT SqlBackend m (Entity LogicTranslationStep))
-> [(Int, String)] -> ReaderT SqlBackend m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (number :: Int
number, name :: String
name) ->
                Key LogicTranslation
-> (Int, String)
-> ReaderT SqlBackend m (Entity LogicTranslationStep)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
Key LogicTranslation
-> (Int, String) -> DBMonad m (Entity LogicTranslationStep)
createLogicTranslationStep Key LogicTranslation
logicTranslationKey (Int
number, String
name)
              ) ([(Int, String)] -> ReaderT SqlBackend m ())
-> [(Int, String)] -> ReaderT SqlBackend m ()
forall a b. (a -> b) -> a -> b
$ [Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [1..] ([String] -> [(Int, String)]) -> [String] -> [(Int, String)]
forall a b. (a -> b) -> a -> b
$ cid -> [String]
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> [String]
constituents cid
cid
        Maybe (Entity LogicTranslation)
-> DBMonad m (Maybe (Entity LogicTranslation))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Entity LogicTranslation)
 -> DBMonad m (Maybe (Entity LogicTranslation)))
-> Maybe (Entity LogicTranslation)
-> DBMonad m (Maybe (Entity LogicTranslation))
forall a b. (a -> b) -> a -> b
$ Entity LogicTranslation -> Maybe (Entity LogicTranslation)
forall a. a -> Maybe a
Just (Entity LogicTranslation -> Maybe (Entity LogicTranslation))
-> Entity LogicTranslation -> Maybe (Entity LogicTranslation)
forall a b. (a -> b) -> a -> b
$ Key LogicTranslation -> LogicTranslation -> Entity LogicTranslation
forall record. Key record -> record -> Entity record
Entity Key LogicTranslation
logicTranslationKey LogicTranslation
logicTranslationValue

createLogicTranslationStep :: (MonadIO m, Fail.MonadFail m)
                           => LogicTranslationId
                           -> (Int, String)
                           -> DBMonad m (Entity LogicTranslationStep)
createLogicTranslationStep :: Key LogicTranslation
-> (Int, String) -> DBMonad m (Entity LogicTranslationStep)
createLogicTranslationStep logicTranslationKey :: Key LogicTranslation
logicTranslationKey (number :: Int
number, name :: String
name)
  | String -> Bool
isInclusion_ String
name = do
      Entity logicInclusionKey :: Key LogicInclusion
logicInclusionKey _ <- String -> DBMonad m (Entity LogicInclusion)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
String -> DBMonad m (Entity LogicInclusion)
findOrCreateLogicInclusion String
name
      let translationStepValue :: LogicTranslationStep
translationStepValue = $WLogicTranslationStep :: Key LogicTranslation
-> Int
-> Maybe LogicMappingId
-> Maybe (Key LogicInclusion)
-> LogicTranslationStep
LogicTranslationStep
            { logicTranslationStepLogicTranslationId :: Key LogicTranslation
logicTranslationStepLogicTranslationId = Key LogicTranslation
logicTranslationKey
            , logicTranslationStepNumber :: Int
logicTranslationStepNumber = Int
number
            , logicTranslationStepLogicMappingId :: Maybe LogicMappingId
logicTranslationStepLogicMappingId = Maybe LogicMappingId
forall a. Maybe a
Nothing
            , logicTranslationStepLogicInclusionId :: Maybe (Key LogicInclusion)
logicTranslationStepLogicInclusionId = Key LogicInclusion -> Maybe (Key LogicInclusion)
forall a. a -> Maybe a
Just Key LogicInclusion
logicInclusionKey
            }
      Key LogicTranslationStep
translationStepKey <- LogicTranslationStep
-> ReaderT SqlBackend m (Key LogicTranslationStep)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert LogicTranslationStep
translationStepValue
      Entity LogicTranslationStep
-> DBMonad m (Entity LogicTranslationStep)
forall (m :: * -> *) a. Monad m => a -> m a
return (Entity LogicTranslationStep
 -> DBMonad m (Entity LogicTranslationStep))
-> Entity LogicTranslationStep
-> DBMonad m (Entity LogicTranslationStep)
forall a b. (a -> b) -> a -> b
$ Key LogicTranslationStep
-> LogicTranslationStep -> Entity LogicTranslationStep
forall record. Key record -> record -> Entity record
Entity Key LogicTranslationStep
translationStepKey LogicTranslationStep
translationStepValue
  | Bool
otherwise = do
      Just (Entity logicMappingKey :: LogicMappingId
logicMappingKey _) <-
        String -> DBMonad m (Maybe (Entity LogicMapping))
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
String -> DBMonad m (Maybe (Entity LogicMapping))
findLogicMappingBySlug (String -> DBMonad m (Maybe (Entity LogicMapping)))
-> String -> DBMonad m (Maybe (Entity LogicMapping))
forall a b. (a -> b) -> a -> b
$ String -> String
slugOfLogicMappingByName String
name
      let translationStepValue :: LogicTranslationStep
translationStepValue = $WLogicTranslationStep :: Key LogicTranslation
-> Int
-> Maybe LogicMappingId
-> Maybe (Key LogicInclusion)
-> LogicTranslationStep
LogicTranslationStep
            { logicTranslationStepLogicTranslationId :: Key LogicTranslation
logicTranslationStepLogicTranslationId = Key LogicTranslation
logicTranslationKey
            , logicTranslationStepNumber :: Int
logicTranslationStepNumber = Int
number
            , logicTranslationStepLogicMappingId :: Maybe LogicMappingId
logicTranslationStepLogicMappingId = LogicMappingId -> Maybe LogicMappingId
forall a. a -> Maybe a
Just LogicMappingId
logicMappingKey
            , logicTranslationStepLogicInclusionId :: Maybe (Key LogicInclusion)
logicTranslationStepLogicInclusionId = Maybe (Key LogicInclusion)
forall a. Maybe a
Nothing
            }
      Key LogicTranslationStep
translationStepKey <- LogicTranslationStep
-> ReaderT SqlBackend m (Key LogicTranslationStep)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert LogicTranslationStep
translationStepValue
      Entity LogicTranslationStep
-> DBMonad m (Entity LogicTranslationStep)
forall (m :: * -> *) a. Monad m => a -> m a
return (Entity LogicTranslationStep
 -> DBMonad m (Entity LogicTranslationStep))
-> Entity LogicTranslationStep
-> DBMonad m (Entity LogicTranslationStep)
forall a b. (a -> b) -> a -> b
$ Key LogicTranslationStep
-> LogicTranslationStep -> Entity LogicTranslationStep
forall record. Key record -> record -> Entity record
Entity Key LogicTranslationStep
translationStepKey LogicTranslationStep
translationStepValue
  where
    isInclusion_ :: String -> Bool
    isInclusion_ :: String -> Bool
isInclusion_ name_ :: String
name_ = "id_" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
name_ Bool -> Bool -> Bool
|| "incl_" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
name_

findOrCreateLogicInclusion :: (MonadIO m, Fail.MonadFail m)
                           => String
                           -> DBMonad m (Entity LogicInclusion)
findOrCreateLogicInclusion :: String -> DBMonad m (Entity LogicInclusion)
findOrCreateLogicInclusion name :: String
name = do
  let logicInclusionSlugS :: String
logicInclusionSlugS = String -> String
slugOfLogicInclusionByName String
name
  [Entity LogicInclusion]
logicInclusionL <- SqlQuery (SqlExpr (Entity LogicInclusion))
-> ReaderT SqlBackend m [Entity LogicInclusion]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LogicInclusion))
 -> ReaderT SqlBackend m [Entity LogicInclusion])
-> SqlQuery (SqlExpr (Entity LogicInclusion))
-> ReaderT SqlBackend m [Entity LogicInclusion]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LogicInclusion)
 -> SqlQuery (SqlExpr (Entity LogicInclusion)))
-> SqlQuery (SqlExpr (Entity LogicInclusion))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LogicInclusion)
  -> SqlQuery (SqlExpr (Entity LogicInclusion)))
 -> SqlQuery (SqlExpr (Entity LogicInclusion)))
-> (SqlExpr (Entity LogicInclusion)
    -> SqlQuery (SqlExpr (Entity LogicInclusion)))
-> SqlQuery (SqlExpr (Entity LogicInclusion))
forall a b. (a -> b) -> a -> b
$ \ logic_inclusions :: SqlExpr (Entity LogicInclusion)
logic_inclusions -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LogicInclusion)
logic_inclusions SqlExpr (Entity LogicInclusion)
-> EntityField LogicInclusion String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LogicInclusion String
forall typ. (typ ~ String) => EntityField LogicInclusion typ
LogicInclusionSlug SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
logicInclusionSlugS)
    SqlExpr (Entity LogicInclusion)
-> SqlQuery (SqlExpr (Entity LogicInclusion))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LogicInclusion)
logic_inclusions
  case [Entity LogicInclusion]
logicInclusionL of
    logicInclusionEntity :: Entity LogicInclusion
logicInclusionEntity : _ -> Entity LogicInclusion -> DBMonad m (Entity LogicInclusion)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity LogicInclusion
logicInclusionEntity
    [] -> do
      let (languageSlugS :: String
languageSlugS, sourceSlugS :: String
sourceSlugS, targetSlugM :: Maybe String
targetSlugM) = (String, String, Maybe String)
slugsFromName

      Maybe (Entity Language)
languageM <- String -> DBMonad m (Maybe (Entity Language))
forall (m :: * -> *).
MonadIO m =>
String -> DBMonad m (Maybe (Entity Language))
findLanguage String
languageSlugS
      LanguageId
languageKey <- case Maybe (Entity Language)
languageM of
        Nothing -> String -> ReaderT SqlBackend m LanguageId
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.LogicGraph.findOrCreateLogicInclusion: "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ "Could not find the language " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
languageSlugS)
        Just (Entity key :: LanguageId
key _) -> LanguageId -> ReaderT SqlBackend m LanguageId
forall (m :: * -> *) a. Monad m => a -> m a
return LanguageId
key

      Maybe (Entity Logic)
sourceM <- String -> DBMonad m (Maybe (Entity Logic))
forall (m :: * -> *).
MonadIO m =>
String -> DBMonad m (Maybe (Entity Logic))
findLogic String
sourceSlugS
      LogicId
sourceKey <- case Maybe (Entity Logic)
sourceM of
        Nothing -> String -> ReaderT SqlBackend m LogicId
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.LogicGraph.findOrCreateLogicInclusion: "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ "Could not find the source logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sourceSlugS)
        Just (Entity key :: LogicId
key _) -> LogicId -> ReaderT SqlBackend m LogicId
forall (m :: * -> *) a. Monad m => a -> m a
return LogicId
key

      Maybe LogicId
targetKeyM <- case Maybe String
targetSlugM of
        Nothing -> Maybe LogicId -> ReaderT SqlBackend m (Maybe LogicId)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LogicId
forall a. Maybe a
Nothing
        Just targetSlugS :: String
targetSlugS -> do
          Maybe (Entity Logic)
targetM <- String -> DBMonad m (Maybe (Entity Logic))
forall (m :: * -> *).
MonadIO m =>
String -> DBMonad m (Maybe (Entity Logic))
findLogic String
targetSlugS
          case Maybe (Entity Logic)
targetM of
            Nothing -> String -> ReaderT SqlBackend m (Maybe LogicId)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.LogicGraph.findOrCreateLogicInclusion: "
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ "Could not find the target logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
targetSlugS)
            Just (Entity key :: LogicId
key _) -> Maybe LogicId -> ReaderT SqlBackend m (Maybe LogicId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LogicId -> ReaderT SqlBackend m (Maybe LogicId))
-> Maybe LogicId -> ReaderT SqlBackend m (Maybe LogicId)
forall a b. (a -> b) -> a -> b
$ LogicId -> Maybe LogicId
forall a. a -> Maybe a
Just LogicId
key

      let logicInclusionValue :: LogicInclusion
logicInclusionValue = $WLogicInclusion :: String
-> String
-> LanguageId
-> LogicId
-> Maybe LogicId
-> LogicInclusion
LogicInclusion
            { logicInclusionName :: String
logicInclusionName = String
name
            , logicInclusionSlug :: String
logicInclusionSlug = String
logicInclusionSlugS
            , logicInclusionLanguageId :: LanguageId
logicInclusionLanguageId = LanguageId
languageKey
            , logicInclusionSourceId :: LogicId
logicInclusionSourceId = LogicId
sourceKey
            , logicInclusionTargetId :: Maybe LogicId
logicInclusionTargetId = Maybe LogicId
targetKeyM
            }
      Key LogicInclusion
logicInclusionKey <- LogicInclusion -> ReaderT SqlBackend m (Key LogicInclusion)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert LogicInclusion
logicInclusionValue
      Entity LogicInclusion -> DBMonad m (Entity LogicInclusion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Entity LogicInclusion -> DBMonad m (Entity LogicInclusion))
-> Entity LogicInclusion -> DBMonad m (Entity LogicInclusion)
forall a b. (a -> b) -> a -> b
$ Key LogicInclusion -> LogicInclusion -> Entity LogicInclusion
forall record. Key record -> record -> Entity record
Entity Key LogicInclusion
logicInclusionKey LogicInclusion
logicInclusionValue
  where
    slugsFromName :: (String, String, Maybe String)
    slugsFromName :: (String, String, Maybe String)
slugsFromName
      | "id_" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
name =
          let languageName_ :: String
languageName_ = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '.') (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
drop 3 String
name
              logicName_ :: String
logicName_ = String -> String
forall a. [a] -> [a]
tail (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '.') String
name
              logicSlugS :: String
logicSlugS =
                String -> String
slugOfLogicByName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
logicNameForDBByName String
languageName_ String
logicName_
          in  ( String -> String
slugOfLanguageByName String
languageName_
              , String
logicSlugS
              , Maybe String
forall a. Maybe a
Nothing
              )
      | "incl_" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
name =
          let languageName_ :: String
languageName_ = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= ':') (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
drop 5 String
name
              logicNames :: String
logicNames = String -> String
forall a. [a] -> [a]
tail (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= ':') String
name
              [sourceName :: String
sourceName, targetName :: String
targetName] = String -> String -> [String]
forall a. Eq a => [a] -> [a] -> [[a]]
splitByList "->" String
logicNames
              sourceSlugS :: String
sourceSlugS =
                String -> String
slugOfLogicByName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
logicNameForDBByName String
languageName_ String
sourceName
              targetSlugS :: String
targetSlugS =
                String -> String
slugOfLogicByName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
logicNameForDBByName String
languageName_ String
targetName
          in  ( String -> String
slugOfLanguageByName String
languageName_
              , String
sourceSlugS
              , String -> Maybe String
forall a. a -> Maybe a
Just String
targetSlugS
              )
      | Bool
otherwise = String -> (String, String, Maybe String)
forall a. HasCallStack => String -> a
error ("Persistence.LogicGraph.findOrCreateLogicInclusion.slugsFromName "
                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ "encountered a bad comorphism name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name)