{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE TypeFamilies               #-}
{- |
Module      :  ./Persistence.DevGraph.hs
Copyright   :  (c) Uni Magdeburg 2017
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Eugen Kuksa <kuksa@iks.cs.ovgu.de>
Stability   :  provisional
Portability :  portable
-}

module Persistence.DevGraph (exportLibEnv) where

import Persistence.Database
import Persistence.DevGraph.Cleaning
import Persistence.Diagnosis
import Persistence.FileVersion
import Persistence.LogicGraph
import Persistence.Schema as SchemaClass
import Persistence.Schema.MappingOrigin (MappingOrigin)
import qualified Persistence.Schema.MappingOrigin as MappingOrigin
import Persistence.Range
import Persistence.Schema.MappingType (MappingType)
import qualified Persistence.Schema.ConsistencyStatusType as ConsistencyStatusType
import qualified Persistence.Schema.Enums as Enums
import qualified Persistence.Schema.EvaluationStateType as EvaluationStateType
import qualified Persistence.Schema.MappingType as MappingType
import Persistence.Schema.OMSOrigin (OMSOrigin)
import qualified Persistence.Schema.OMSOrigin as OMSOrigin
import Persistence.Utils

import Common.AS_Annotation
import Common.Consistency
import Common.DocUtils
import Common.ExtSign
import Common.FileType
import Common.GlobalAnnotations
import Common.Id
import Common.IRI (IRI (..), setAngles)
import Common.Json (ppJson)
import Common.Lib.Graph as Graph hiding (nodeLabel)
import qualified Common.Lib.Graph as Graph (nodeLabel)
import Common.Lib.Rel (Rel)
import qualified Common.Lib.Rel as Rel
import Common.LibName
import Common.Result (maybeResult, Diagnosis(..), DiagKind(..))
import Common.ResultT (runResultT)
import Common.Utils
import Driver.Options
import qualified Common.OrderedMap as OMap
import Logic.Comorphism
import Logic.Grothendieck hiding (gMorphism)
import Logic.Logic as Logic
import Logic.Prover
import Static.ComputeTheory (computeTheory)
import Static.DevGraph hiding (getLogic)
import Static.DgUtils
import Static.GTheory
import qualified Static.ToJson as ToJson

import Control.Exception
import Control.Monad (foldM, foldM_, when)
import Control.Monad.IO.Class (MonadIO (..))
import qualified Control.Monad.Fail as Fail
import Data.Char (toLower)
import qualified Data.IntMap as IntMap
import Data.Graph.Inductive.Graph as Graph
import Data.List (intercalate, isPrefixOf, stripPrefix)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Text as Text
import Database.Persist hiding ((==.))
import Database.Persist.Sql hiding ((==.))
import Database.Esqueleto

-- TODO: replace this by the `symbol` type variable and find a string representation that is unique such that there can be a unique index in the database
type SymbolMapIndex = (String, String) -- (SymbolKind, FullSymbolName)

data DBCache = DBCache
  { DBCache -> Map LibName LocIdBaseId
documentMap :: Map LibName LocIdBaseId -- Here, LocIdBaseId is DocumentId
  , DBCache -> Map IRI LocIdBaseId
documentByLibNameIRIMap :: Map IRI LocIdBaseId -- Here, LocIdBaseId is DocumentId
  , DBCache -> Map (LibName, Node) (LocIdBaseId, SignatureId)
nodeMap :: Map (LibName, Node) (LocIdBaseId, SignatureId) -- Here, LocIdBaseId is OMSId
  , DBCache -> Map (LibName, SigId) SignatureId
signatureMap :: Map (LibName, SigId) SignatureId
  , DBCache
-> Map
     (LibName, MorId)
     (SignatureMorphismId, [SymbolMappingId], GMorphism)
signatureMorphismMap :: Map (LibName, MorId)
                             (SignatureMorphismId, [SymbolMappingId], GMorphism)
  , DBCache -> Map (LibName, Node, SymbolMapIndex) LocIdBaseId
symbolKeyMap :: Map (LibName, Int, SymbolMapIndex) LocIdBaseId -- Here, LocIdBaseId is SymbolId
  } deriving Node -> DBCache -> ShowS
[DBCache] -> ShowS
DBCache -> String
(Node -> DBCache -> ShowS)
-> (DBCache -> String) -> ([DBCache] -> ShowS) -> Show DBCache
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DBCache] -> ShowS
$cshowList :: [DBCache] -> ShowS
show :: DBCache -> String
$cshow :: DBCache -> String
showsPrec :: Node -> DBCache -> ShowS
$cshowsPrec :: Node -> DBCache -> ShowS
Show

emptyDBCache :: DBCache
emptyDBCache :: DBCache
emptyDBCache = DBCache :: Map LibName LocIdBaseId
-> Map IRI LocIdBaseId
-> Map (LibName, Node) (LocIdBaseId, SignatureId)
-> Map (LibName, SigId) SignatureId
-> Map
     (LibName, MorId)
     (SignatureMorphismId, [SymbolMappingId], GMorphism)
-> Map (LibName, Node, SymbolMapIndex) LocIdBaseId
-> DBCache
DBCache { documentMap :: Map LibName LocIdBaseId
documentMap = Map LibName LocIdBaseId
forall k a. Map k a
Map.empty
                       , documentByLibNameIRIMap :: Map IRI LocIdBaseId
documentByLibNameIRIMap = Map IRI LocIdBaseId
forall k a. Map k a
Map.empty
                       , nodeMap :: Map (LibName, Node) (LocIdBaseId, SignatureId)
nodeMap = Map (LibName, Node) (LocIdBaseId, SignatureId)
forall k a. Map k a
Map.empty
                       , signatureMap :: Map (LibName, SigId) SignatureId
signatureMap = Map (LibName, SigId) SignatureId
forall k a. Map k a
Map.empty
                       , signatureMorphismMap :: Map
  (LibName, MorId)
  (SignatureMorphismId, [SymbolMappingId], GMorphism)
signatureMorphismMap = Map
  (LibName, MorId)
  (SignatureMorphismId, [SymbolMappingId], GMorphism)
forall k a. Map k a
Map.empty
                       , symbolKeyMap :: Map (LibName, Node, SymbolMapIndex) LocIdBaseId
symbolKeyMap = Map (LibName, Node, SymbolMapIndex) LocIdBaseId
forall k a. Map k a
Map.empty
                       }

exportLibEnv :: HetcatsOpts -> LibEnv -> IO ()
exportLibEnv :: HetcatsOpts -> LibEnv -> IO ()
exportLibEnv opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv = do
  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 DBConfig
dbConfig (DBMonad (NoLoggingT IO) () -> IO ())
-> DBMonad (NoLoggingT IO) () -> IO ()
forall a b. (a -> b) -> a -> b
$
    DBContext -> EvaluationStateType -> DBMonad (NoLoggingT IO) ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
DBContext -> EvaluationStateType -> DBMonad m ()
setFileVersionState DBContext
dbContext EvaluationStateType
EvaluationStateType.Processing
  IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
Control.Exception.catch IO ()
export SomeException -> IO ()
saveErrorAndRethrow
  where
    dbConfig :: DBConfig
dbConfig = HetcatsOpts -> DBConfig
databaseConfig HetcatsOpts
opts
    dbContext :: DBContext
dbContext = HetcatsOpts -> DBContext
databaseContext HetcatsOpts
opts

    export :: IO ()
    export :: IO ()
export = 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 DBConfig
dbConfig (DBMonad (NoLoggingT IO) () -> IO ())
-> DBMonad (NoLoggingT IO) () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      let dependencyLibNameRel :: Rel LibName
dependencyLibNameRel = LibEnv -> Rel LibName
getLibDepRel LibEnv
libEnv
      let dependencyOrderedLibsSetL :: [Set LibName]
dependencyOrderedLibsSetL = Rel LibName -> [Set LibName]
forall a. Ord a => Rel a -> [Set a]
Rel.depSort Rel LibName
dependencyLibNameRel
      DBCache
dbCache1 <-
        HetcatsOpts
-> LibEnv
-> DBCache
-> [Set LibName]
-> DBMonad (NoLoggingT IO) DBCache
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv -> DBCache -> [Set LibName] -> DBMonad m DBCache
createDocuments HetcatsOpts
opts LibEnv
libEnv DBCache
emptyDBCache [Set LibName]
dependencyOrderedLibsSetL
      DBCache -> Rel LibName -> DBMonad (NoLoggingT IO) ()
forall (m :: * -> *).
MonadIO m =>
DBCache -> Rel LibName -> DBMonad m ()
createDocumentLinks DBCache
dbCache1 Rel LibName
dependencyLibNameRel
      DBContext -> EvaluationStateType -> DBMonad (NoLoggingT IO) ()
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
DBContext -> EvaluationStateType -> DBMonad m ()
setFileVersionState DBContext
dbContext EvaluationStateType
EvaluationStateType.FinishedSuccessfully
      () -> DBMonad (NoLoggingT IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    saveErrorAndRethrow :: SomeException -> IO ()
    saveErrorAndRethrow :: SomeException -> IO ()
saveErrorAndRethrow exception :: SomeException
exception = do
      let message :: String
message = SomeException -> String
forall a. Show a => a -> String
show SomeException
exception
      DBConfig -> DBContext -> Node -> [Diagnosis] -> IO ()
saveDiagnoses DBConfig
dbConfig DBContext
dbContext 5 [Diag :: DiagKind -> String -> Range -> Diagnosis
Diag { diagKind :: DiagKind
diagKind = DiagKind
Error
                                               , diagString :: String
diagString = String
message
                                               , diagPos :: Range
diagPos = Range
nullRange
                                               }]
      String -> IO ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
message

createDocuments :: (MonadIO m, Fail.MonadFail m)
                => HetcatsOpts -> LibEnv -> DBCache -> [Set LibName]
                -> DBMonad m DBCache
createDocuments :: HetcatsOpts
-> LibEnv -> DBCache -> [Set LibName] -> DBMonad m DBCache
createDocuments opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv dbCache0 :: DBCache
dbCache0 dependencyOrderedLibsSetL :: [Set LibName]
dependencyOrderedLibsSetL = do
  Entity FileVersion
fileVersion <- DBContext -> DBMonad m (Entity FileVersion)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
DBContext -> DBMonad m (Entity FileVersion)
getFileVersion (DBContext -> DBMonad m (Entity FileVersion))
-> DBContext -> DBMonad m (Entity FileVersion)
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> DBContext
databaseContext HetcatsOpts
opts
  DBCache
dbCache1 <-
    HetcatsOpts
-> LibEnv
-> Entity FileVersion
-> DBCache
-> [Set LibName]
-> DBMonad m DBCache
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> Entity FileVersion
-> DBCache
-> [Set LibName]
-> DBMonad m DBCache
createDocumentsInDependencyRelation HetcatsOpts
opts LibEnv
libEnv Entity FileVersion
fileVersion DBCache
dbCache0 ([Set LibName] -> DBMonad m DBCache)
-> [Set LibName] -> DBMonad m DBCache
forall a b. (a -> b) -> a -> b
$
      [Set LibName] -> [Set LibName]
forall a. [a] -> [a]
reverse [Set LibName]
dependencyOrderedLibsSetL
  HetcatsOpts
-> LibEnv -> Entity FileVersion -> DBCache -> DBMonad m DBCache
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv -> Entity FileVersion -> DBCache -> DBMonad m DBCache
createDocumentsThatAreIndependent HetcatsOpts
opts LibEnv
libEnv Entity FileVersion
fileVersion DBCache
dbCache1

createDocumentsInDependencyRelation :: (MonadIO m, Fail.MonadFail m)
                                    => HetcatsOpts -> LibEnv
                                    -> Entity FileVersion -> DBCache -> [Set LibName]
                                    -> DBMonad m DBCache
createDocumentsInDependencyRelation :: HetcatsOpts
-> LibEnv
-> Entity FileVersion
-> DBCache
-> [Set LibName]
-> DBMonad m DBCache
createDocumentsInDependencyRelation opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv fileVersion :: Entity FileVersion
fileVersion =
  (DBCache -> Set LibName -> DBMonad m DBCache)
-> DBCache -> [Set LibName] -> DBMonad m DBCache
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
    (\ outerAcc :: DBCache
outerAcc libNameSet :: Set LibName
libNameSet ->
       (DBCache -> LibName -> DBMonad m DBCache)
-> DBCache -> Set LibName -> DBMonad m DBCache
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
         (\ dbCacheAcc :: DBCache
dbCacheAcc libName :: LibName
libName ->
            HetcatsOpts
-> LibEnv
-> Entity FileVersion
-> DBCache
-> LibName
-> DBMonad m DBCache
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> Entity FileVersion
-> DBCache
-> LibName
-> DBMonad m DBCache
createDocument HetcatsOpts
opts LibEnv
libEnv Entity FileVersion
fileVersion DBCache
dbCacheAcc LibName
libName
         ) DBCache
outerAcc Set LibName
libNameSet
    )

createDocumentsThatAreIndependent :: (MonadIO m, Fail.MonadFail m)
                                  => HetcatsOpts -> LibEnv
                                  -> Entity FileVersion -> DBCache
                                  -> DBMonad m DBCache
createDocumentsThatAreIndependent :: HetcatsOpts
-> LibEnv -> Entity FileVersion -> DBCache -> DBMonad m DBCache
createDocumentsThatAreIndependent opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv fileVersion :: Entity FileVersion
fileVersion dbCache :: DBCache
dbCache =
  (DBCache -> LibName -> DBMonad m DBCache)
-> DBCache -> [LibName] -> DBMonad m DBCache
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
    (\ dbCacheAcc :: DBCache
dbCacheAcc libName :: LibName
libName ->
      let alreadyInserted :: Bool
alreadyInserted = Maybe LocIdBaseId -> Bool
forall a. Maybe a -> Bool
isJust (Maybe LocIdBaseId -> Bool) -> Maybe LocIdBaseId -> Bool
forall a b. (a -> b) -> a -> b
$ LibName -> Map LibName LocIdBaseId -> Maybe LocIdBaseId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
libName (Map LibName LocIdBaseId -> Maybe LocIdBaseId)
-> Map LibName LocIdBaseId -> Maybe LocIdBaseId
forall a b. (a -> b) -> a -> b
$ DBCache -> Map LibName LocIdBaseId
documentMap DBCache
dbCacheAcc
      in  if Bool
alreadyInserted
          then DBCache -> DBMonad m DBCache
forall (m :: * -> *) a. Monad m => a -> m a
return DBCache
dbCacheAcc
          else HetcatsOpts
-> LibEnv
-> Entity FileVersion
-> DBCache
-> LibName
-> DBMonad m DBCache
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> Entity FileVersion
-> DBCache
-> LibName
-> DBMonad m DBCache
createDocument HetcatsOpts
opts LibEnv
libEnv Entity FileVersion
fileVersion DBCache
dbCacheAcc LibName
libName
    ) DBCache
dbCache ([LibName] -> DBMonad m DBCache) -> [LibName] -> DBMonad m DBCache
forall a b. (a -> b) -> a -> b
$ LibEnv -> [LibName]
forall k a. Map k a -> [k]
Map.keys LibEnv
libEnv

createDocument :: (MonadIO m, Fail.MonadFail m)
               => HetcatsOpts -> LibEnv -> Entity FileVersion -> DBCache
               -> LibName -> DBMonad m DBCache
createDocument :: HetcatsOpts
-> LibEnv
-> Entity FileVersion
-> DBCache
-> LibName
-> DBMonad m DBCache
createDocument opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv parentFileVersion :: Entity FileVersion
parentFileVersion dbCache0 :: DBCache
dbCache0 libName :: LibName
libName =
  let dGraph :: DGraph
dGraph = Maybe DGraph -> DGraph
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DGraph -> DGraph) -> Maybe DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> Maybe DGraph
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
libName LibEnv
libEnv
      globalAnnotations :: GlobalAnnos
globalAnnotations = DGraph -> GlobalAnnos
globalAnnos DGraph
dGraph
      name :: String
name = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ IRI -> Doc
forall a. Pretty a => a -> Doc
pretty (IRI -> Doc) -> IRI -> Doc
forall a b. (a -> b) -> a -> b
$ LibName -> IRI
getLibId LibName
libName
      displayName :: String
displayName = IRI -> String
forall a. Show a => a -> String
show (IRI -> String) -> IRI -> String
forall a b. (a -> b) -> a -> b
$ Bool -> IRI -> IRI
setAngles Bool
False (IRI -> IRI) -> IRI -> IRI
forall a b. (a -> b) -> a -> b
$ LibName -> IRI
getLibId LibName
libName
      location :: Maybe String
location = (IRI -> String) -> Maybe IRI -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IRI -> String
forall a. Show a => a -> String
show (Maybe IRI -> Maybe String) -> Maybe IRI -> Maybe String
forall a b. (a -> b) -> a -> b
$ LibName -> Maybe IRI
locIRI LibName
libName
      version :: Maybe String
version = (VersionNumber -> String) -> Maybe VersionNumber -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "." ([String] -> String)
-> (VersionNumber -> [String]) -> VersionNumber -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ (VersionNumber v :: [String]
v _) -> [String]
v)) (Maybe VersionNumber -> Maybe String)
-> Maybe VersionNumber -> Maybe String
forall a b. (a -> b) -> a -> b
$
                  LibName -> Maybe VersionNumber
libVersion LibName
libName
      locId :: String
locId = HetcatsOpts -> Maybe String -> ShowS
locIdOfDocument HetcatsOpts
opts Maybe String
location String
displayName
  in  do
        -- We need to find the FileVersion of the corresponding document
        -- if it is located inside the libdir.
        FileVersionId
fileVersionKey <- HetcatsOpts
-> Entity FileVersion -> Maybe String -> DBMonad m FileVersionId
forall (m :: * -> *).
MonadIO m =>
HetcatsOpts
-> Entity FileVersion -> Maybe String -> DBMonad m FileVersionId
findFileVersionByPath HetcatsOpts
opts Entity FileVersion
parentFileVersion Maybe String
location
        LocIdBaseKindType
kind <- HetcatsOpts
-> Maybe String -> ReaderT SqlBackend m LocIdBaseKindType
forall (m :: * -> *).
MonadIO m =>
HetcatsOpts -> Maybe String -> m LocIdBaseKindType
kindOfDocument HetcatsOpts
opts Maybe String
location
        let fileVersionKeyS :: String
fileVersionKeyS =
              Int64 -> String
forall a. Show a => a -> String
show (Int64 -> String) -> Int64 -> String
forall a b. (a -> b) -> a -> b
$ BackendKey SqlBackend -> Int64
unSqlBackendKey (BackendKey SqlBackend -> Int64) -> BackendKey SqlBackend -> Int64
forall a b. (a -> b) -> a -> b
$ FileVersionId -> BackendKey SqlBackend
unFileVersionKey FileVersionId
fileVersionKey
        HetcatsOpts -> String -> DBMonad m DBCache -> DBMonad m DBCache
forall (m :: * -> *) a.
MonadIO m =>
HetcatsOpts -> String -> DBMonad m a -> DBMonad m a
advisoryLocked HetcatsOpts
opts (String
fileVersionKeyS String -> ShowS
forall a. [a] -> [a] -> [a]
++ "-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ LocIdBaseKindType -> String
forall a. Show a => a -> String
show LocIdBaseKindType
kind String -> ShowS
forall a. [a] -> [a] -> [a]
++ "-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
locId) (DBMonad m DBCache -> DBMonad m DBCache)
-> DBMonad m DBCache -> DBMonad m DBCache
forall a b. (a -> b) -> a -> b
$ do
          [Entity LocIdBase]
documentL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LocIdBase)
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LocIdBase)
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (SqlExpr (Entity LocIdBase)
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ \loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases -> do
            SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase String
forall typ. (typ ~ String) => EntityField LocIdBase typ
LocIdBaseLocId 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
locId
                      SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase FileVersionId
-> SqlExpr (Value FileVersionId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase FileVersionId
forall typ. (typ ~ FileVersionId) => EntityField LocIdBase typ
LocIdBaseFileVersionId SqlExpr (Value FileVersionId)
-> SqlExpr (Value FileVersionId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. FileVersionId -> SqlExpr (Value FileVersionId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val FileVersionId
fileVersionKey
                      SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseKindType
-> SqlExpr (Value LocIdBaseKindType)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseKindType
forall typ. (typ ~ LocIdBaseKindType) => EntityField LocIdBase typ
LocIdBaseKind SqlExpr (Value LocIdBaseKindType)
-> SqlExpr (Value LocIdBaseKindType) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseKindType -> SqlExpr (Value LocIdBaseKindType)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseKindType
kind)
            SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
          case [Entity LocIdBase]
documentL of
            [] -> () -> ReaderT SqlBackend m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            document :: Entity LocIdBase
document : _ -> Bool -> ReaderT SqlBackend m () -> ReaderT SqlBackend m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HetcatsOpts -> Bool
databaseReanalyze HetcatsOpts
opts) (ReaderT SqlBackend m () -> ReaderT SqlBackend m ())
-> ReaderT SqlBackend m () -> ReaderT SqlBackend m ()
forall a b. (a -> b) -> a -> b
$
              Entity LocIdBase -> ReaderT SqlBackend m ()
forall (m :: * -> *). MonadIO m => Entity LocIdBase -> DBMonad m ()
Persistence.DevGraph.Cleaning.clean Entity LocIdBase
document
          (doSave :: Bool
doSave, documentKey :: LocIdBaseId
documentKey, documentLocIdBaseValue :: LocIdBase
documentLocIdBaseValue) <-
            case (HetcatsOpts -> Bool
databaseReanalyze HetcatsOpts
opts, [Entity LocIdBase]
documentL) of
              (False, Entity documentKey :: LocIdBaseId
documentKey documentLocIdBaseValue :: LocIdBase
documentLocIdBaseValue : _) ->
                (Bool, LocIdBaseId, LocIdBase)
-> ReaderT SqlBackend m (Bool, LocIdBaseId, LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, LocIdBaseId
documentKey, LocIdBase
documentLocIdBaseValue)
              _ -> do
                let documentLocIdBaseValue :: LocIdBase
documentLocIdBaseValue = $WLocIdBase :: FileVersionId -> LocIdBaseKindType -> String -> LocIdBase
LocIdBase
                      { locIdBaseFileVersionId :: FileVersionId
locIdBaseFileVersionId = FileVersionId
fileVersionKey
                      , locIdBaseKind :: LocIdBaseKindType
locIdBaseKind = LocIdBaseKindType
kind
                      , locIdBaseLocId :: String
locIdBaseLocId = String
locId
                      }
                LocIdBaseId
documentKey <- LocIdBase -> ReaderT SqlBackend m LocIdBaseId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert LocIdBase
documentLocIdBaseValue
                let document :: Document
document = $WDocument :: String -> String -> Maybe String -> Maybe String -> Document
Document
                      { documentDisplayName :: String
documentDisplayName = String
displayName
                      , documentName :: String
documentName = String
name
                      , documentLocation :: Maybe String
documentLocation = Maybe String
location
                      , documentVersion :: Maybe String
documentVersion = Maybe String
version
                      }
                [Entity Document] -> ReaderT SqlBackend m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany [Key Document -> Document -> Entity Document
forall record. Key record -> record -> Entity record
Entity (Int64 -> Key Document
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key Document) -> Int64 -> Key Document
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
documentKey) Document
document]
                (Bool, LocIdBaseId, LocIdBase)
-> ReaderT SqlBackend m (Bool, LocIdBaseId, LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, LocIdBaseId
documentKey, LocIdBase
documentLocIdBaseValue)
          let dbCache1 :: DBCache
dbCache1 = LibName -> LocIdBaseId -> DBCache -> DBCache
addDocumentToCache LibName
libName LocIdBaseId
documentKey DBCache
dbCache0
          HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> DGraph
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> DBMonad m DBCache
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> DGraph
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> DBMonad m DBCache
createAllOmsOfDocument HetcatsOpts
opts LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache1 Bool
doSave DGraph
dGraph
            GlobalAnnos
globalAnnotations LibName
libName (LocIdBaseId -> LocIdBase -> Entity LocIdBase
forall record. Key record -> record -> Entity record
Entity LocIdBaseId
documentKey LocIdBase
documentLocIdBaseValue)

-- A FileVersion only exists for the commit that actually changed the file, but
-- the file itself also exists in future commits that changed other files.
-- This function finds the FileVersion of the file at `location` (i.e. the
-- commit that last changed that file).
findFileVersionByPath :: MonadIO m
                      => HetcatsOpts -> Entity FileVersion -> Maybe String
                      -> DBMonad m FileVersionId
findFileVersionByPath :: HetcatsOpts
-> Entity FileVersion -> Maybe String -> DBMonad m FileVersionId
findFileVersionByPath opts :: HetcatsOpts
opts (Entity fileVersionKey :: FileVersionId
fileVersionKey _) location :: Maybe String
location =
  let isInLibdir :: Bool
isInLibdir = Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [String]
libdirs HetcatsOpts
opts)
                     Bool -> Bool -> Bool
&& Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
location
                     Bool -> Bool -> Bool
&& [String] -> String
forall a. [a] -> a
head (HetcatsOpts -> [String]
libdirs HetcatsOpts
opts) String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
location
      path :: String
path = Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix (HetcatsOpts -> String
firstLibdir HetcatsOpts
opts) (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
location
      queryString :: Text
queryString = String -> Text
Text.pack (
        "SELECT file_versions.id "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "FROM file_versions "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "INNER JOIN file_version_parents "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "  ON file_version_parents.last_changed_file_version_id = file_versions.id "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "INNER JOIN file_versions AS backreference "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "  ON file_version_parents.queried_sha = backreference.commit_sha "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "WHERE (file_versions.path = ? "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "       AND backreference.id = ?);")
  in  if Bool
isInLibdir
      then do
            [FileVersionId]
results <-
              Text -> [PersistValue] -> ReaderT SqlBackend m [FileVersionId]
forall a (m :: * -> *) backend.
(RawSql a, MonadIO m, BackendCompatible SqlBackend backend) =>
Text -> [PersistValue] -> ReaderT backend m [a]
rawSql Text
queryString [ String -> PersistValue
forall a. PersistField a => a -> PersistValue
toPersistValue String
path
                                 , FileVersionId -> PersistValue
forall a. PersistField a => a -> PersistValue
toPersistValue FileVersionId
fileVersionKey
                                 ]
            if [FileVersionId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FileVersionId]
results
            then FileVersionId -> DBMonad m FileVersionId
forall (m :: * -> *) a. Monad m => a -> m a
return FileVersionId
fileVersionKey
            else FileVersionId -> DBMonad m FileVersionId
forall (m :: * -> *) a. Monad m => a -> m a
return (FileVersionId -> DBMonad m FileVersionId)
-> FileVersionId -> DBMonad m FileVersionId
forall a b. (a -> b) -> a -> b
$ [FileVersionId] -> FileVersionId
forall a. [a] -> a
head [FileVersionId]
results
      else FileVersionId -> DBMonad m FileVersionId
forall (m :: * -> *) a. Monad m => a -> m a
return FileVersionId
fileVersionKey

-- Guess the kind of the Document. First, by the filepath only and then, by
-- searching for keywords in the content. If the type cannot be guessed,
-- default to Library.
kindOfDocument :: MonadIO m
               => HetcatsOpts -> Maybe FilePath -> m Enums.LocIdBaseKindType
kindOfDocument :: HetcatsOpts -> Maybe String -> m LocIdBaseKindType
kindOfDocument opts :: HetcatsOpts
opts filepathM :: Maybe String
filepathM = case Maybe String
filepathM of
  Nothing -> LocIdBaseKindType -> m LocIdBaseKindType
forall (m :: * -> *) a. Monad m => a -> m a
return LocIdBaseKindType
Enums.Library
  Just filepath :: String
filepath -> case String -> InType -> InType
guess String
filepath (HetcatsOpts -> InType
intype HetcatsOpts
opts) of
    GuessIn -> do
      Result String
mimeR <-
        IO (Result String) -> m (Result String)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Result String) -> m (Result String))
-> IO (Result String) -> m (Result String)
forall a b. (a -> b) -> a -> b
$ ResultT IO String -> IO (Result String)
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO String -> IO (Result String))
-> ResultT IO String -> IO (Result String)
forall a b. (a -> b) -> a -> b
$ Maybe String -> String -> ResultT IO String
getMagicFileType (String -> Maybe String
forall a. a -> Maybe a
Just "--mime-type") String
filepath
      case Result String -> Maybe String
forall a. Result a -> Maybe a
maybeResult Result String
mimeR of
        Just mime :: String
mime -> LocIdBaseKindType -> m LocIdBaseKindType
forall (m :: * -> *) a. Monad m => a -> m a
return (LocIdBaseKindType -> m LocIdBaseKindType)
-> LocIdBaseKindType -> m LocIdBaseKindType
forall a b. (a -> b) -> a -> b
$ String -> LocIdBaseKindType
determineTypeByMime String
mime
        Nothing -> LocIdBaseKindType -> m LocIdBaseKindType
forall (m :: * -> *) a. Monad m => a -> m a
return LocIdBaseKindType
Enums.Library
    t :: InType
t -> LocIdBaseKindType -> m LocIdBaseKindType
forall (m :: * -> *) a. Monad m => a -> m a
return (LocIdBaseKindType -> m LocIdBaseKindType)
-> LocIdBaseKindType -> m LocIdBaseKindType
forall a b. (a -> b) -> a -> b
$ InType -> LocIdBaseKindType
determineType InType
t
  where
    determineType :: InType -> Enums.LocIdBaseKindType
    determineType :: InType -> LocIdBaseKindType
determineType t :: InType
t = if InType -> String
forall a. Show a => a -> String
show InType
t String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ["casl", "het", "dol"]
                      then LocIdBaseKindType
Enums.Library
                      else LocIdBaseKindType
Enums.NativeDocument

    determineTypeByMime :: String -> Enums.LocIdBaseKindType
    determineTypeByMime :: String -> LocIdBaseKindType
determineTypeByMime t :: String
t = if String
t String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ["text/casl", "text/het", "text/dol"]
                            then LocIdBaseKindType
Enums.Library
                            else LocIdBaseKindType
Enums.NativeDocument

createAllOmsOfDocument :: (MonadIO m, Fail.MonadFail m)
                       => HetcatsOpts -> LibEnv -> FileVersionId -> DBCache
                       -> Bool -> DGraph -> GlobalAnnos -> LibName
                       -> Entity LocIdBase -> DBMonad m DBCache
createAllOmsOfDocument :: HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> DGraph
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> DBMonad m DBCache
createAllOmsOfDocument opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache0 :: DBCache
dbCache0 doSave :: Bool
doSave dGraph :: DGraph
dGraph
  globalAnnotations :: GlobalAnnos
globalAnnotations libName :: LibName
libName documentLocIdBase :: Entity LocIdBase
documentLocIdBase =
  let labeledNodes :: [LNode DGNodeLab]
labeledNodes = Gr DGNodeLab DGLinkLab -> [LNode DGNodeLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes (Gr DGNodeLab DGLinkLab -> [LNode DGNodeLab])
-> Gr DGNodeLab DGLinkLab -> [LNode DGNodeLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dGraph
      labeledEdges :: [LEdge DGLinkLab]
labeledEdges = Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab])
-> Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dGraph
  in  do
        DBCache
dbCache1 <- (DBCache -> LNode DGNodeLab -> DBMonad m DBCache)
-> DBCache -> [LNode DGNodeLab] -> DBMonad m DBCache
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
          (\ dbCacheAcc :: DBCache
dbCacheAcc labeledNode :: LNode DGNodeLab
labeledNode ->
            ((LocIdBaseId, SignatureId, DBCache) -> DBCache)
-> ReaderT SqlBackend m (LocIdBaseId, SignatureId, DBCache)
-> DBMonad m DBCache
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (_, _, dbCache :: DBCache
dbCache) -> DBCache
dbCache) (ReaderT SqlBackend m (LocIdBaseId, SignatureId, DBCache)
 -> DBMonad m DBCache)
-> ReaderT SqlBackend m (LocIdBaseId, SignatureId, DBCache)
-> DBMonad m DBCache
forall a b. (a -> b) -> a -> b
$
              HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> ReaderT SqlBackend m (LocIdBaseId, SignatureId, DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
findOrCreateOMS HetcatsOpts
opts LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCacheAcc Bool
doSave
                GlobalAnnos
globalAnnotations LibName
libName Entity LocIdBase
documentLocIdBase LNode DGNodeLab
labeledNode
          ) DBCache
dbCache0 [LNode DGNodeLab]
labeledNodes
        (DBCache -> LEdge DGLinkLab -> DBMonad m DBCache)
-> DBCache -> [LEdge DGLinkLab] -> DBMonad m DBCache
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
          (\ dbCacheAcc :: DBCache
dbCacheAcc labeledEdge :: LEdge DGLinkLab
labeledEdge ->
            HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LEdge DGLinkLab
-> DBMonad m DBCache
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LEdge DGLinkLab
-> DBMonad m DBCache
createMapping HetcatsOpts
opts LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCacheAcc Bool
doSave
              GlobalAnnos
globalAnnotations LibName
libName Entity LocIdBase
documentLocIdBase LEdge DGLinkLab
labeledEdge
          ) DBCache
dbCache1 [LEdge DGLinkLab]
labeledEdges

findOrCreateOMSM :: (MonadIO m, Fail.MonadFail m)
                 => HetcatsOpts -> LibEnv -> FileVersionId -> DBCache -> Bool
                 -> GlobalAnnos -> LibName -> Entity LocIdBase -> Maybe Int
                 -> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
findOrCreateOMSM :: HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> Maybe Node
-> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
findOrCreateOMSM opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache0 :: DBCache
dbCache0 doSave :: Bool
doSave globalAnnotations :: GlobalAnnos
globalAnnotations
  libName :: LibName
libName documentLocIdBase :: Entity LocIdBase
documentLocIdBase nodeIdM :: Maybe Node
nodeIdM =
  case Maybe Node
nodeIdM of
    Nothing -> (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
-> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LocIdBaseId
forall a. Maybe a
Nothing, Maybe SignatureId
forall a. Maybe a
Nothing, DBCache
dbCache0)
    Just nodeId :: Node
nodeId ->
      let nodeLabel :: DGNodeLab
nodeLabel = LibEnv -> LibName -> Node -> DGNodeLab
getNodeLabel LibEnv
libEnv LibName
libName Node
nodeId
      in  do
            (omsKey :: LocIdBaseId
omsKey, signatureKey :: SignatureId
signatureKey, dbCache1 :: DBCache
dbCache1) <-
              HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
findOrCreateOMS HetcatsOpts
opts LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache0 Bool
doSave
                GlobalAnnos
globalAnnotations LibName
libName Entity LocIdBase
documentLocIdBase (Node
nodeId, DGNodeLab
nodeLabel)
            (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
-> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (LocIdBaseId -> Maybe LocIdBaseId
forall a. a -> Maybe a
Just LocIdBaseId
omsKey, SignatureId -> Maybe SignatureId
forall a. a -> Maybe a
Just SignatureId
signatureKey, DBCache
dbCache1)

findOrCreateOMS :: (MonadIO m, Fail.MonadFail m)
                => HetcatsOpts -> LibEnv -> FileVersionId -> DBCache -> Bool
                -> GlobalAnnos -> LibName -> Entity LocIdBase
                -> (Int, DGNodeLab)
                -> DBMonad m (LocIdBaseId, SignatureId, DBCache)
findOrCreateOMS :: HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
findOrCreateOMS opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache0 :: DBCache
dbCache0 doSave :: Bool
doSave globalAnnotations :: GlobalAnnos
globalAnnotations
  libName :: LibName
libName documentLocIdBase :: Entity LocIdBase
documentLocIdBase (nodeId :: Node
nodeId, nodeLabel :: DGNodeLab
nodeLabel) =
  case LibName -> Node -> DBCache -> Maybe (LocIdBaseId, SignatureId)
cachedOMSKey LibName
libName Node
nodeId DBCache
dbCache0 of
    Just (omsKey :: LocIdBaseId
omsKey, signatureKey :: SignatureId
signatureKey) -> (LocIdBaseId, SignatureId, DBCache)
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (LocIdBaseId
omsKey, SignatureId
signatureKey, DBCache
dbCache0)
    Nothing -> case DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
nodeLabel of
      DGRef { ref_node :: DGNodeInfo -> Node
ref_node = Node
refNodeId
            , ref_libname :: DGNodeInfo -> LibName
ref_libname = LibName
refLibName
            } -> do
        let refNodeLabel :: DGNodeLab
refNodeLabel = LibEnv -> LibName -> Node -> DGNodeLab
getNodeLabel LibEnv
libEnv LibName
refLibName Node
refNodeId
        (omsKey :: LocIdBaseId
omsKey, signatureKey :: SignatureId
signatureKey, dbCache1 :: DBCache
dbCache1) <-
          HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
findOrCreateOMS HetcatsOpts
opts LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache0 Bool
doSave
            GlobalAnnos
globalAnnotations LibName
refLibName Entity LocIdBase
documentLocIdBase (Node
refNodeId, DGNodeLab
refNodeLabel)
        (LocIdBaseId, SignatureId, DBCache)
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return ( LocIdBaseId
omsKey
               , SignatureId
signatureKey
               , LibName -> Node -> LocIdBaseId -> SignatureId -> DBCache -> DBCache
addNodeToCache LibName
libName Node
nodeId LocIdBaseId
omsKey SignatureId
signatureKey DBCache
dbCache1
               )
      DGNode _ consStatus :: ConsStatus
consStatus -> do
        Maybe (LocIdBaseId, SignatureId)
omsKeyM <- FileVersionId
-> Entity LocIdBase
-> DGNodeLab
-> DBMonad m (Maybe (LocIdBaseId, SignatureId))
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
FileVersionId
-> Entity LocIdBase
-> DGNodeLab
-> DBMonad m (Maybe (LocIdBaseId, SignatureId))
findOMSAndSignature FileVersionId
fileVersionKey Entity LocIdBase
documentLocIdBase DGNodeLab
nodeLabel
        case (Bool
doSave, Maybe (LocIdBaseId, SignatureId)
omsKeyM) of
          (True, Just (omsKey :: LocIdBaseId
omsKey, signatureKey :: SignatureId
signatureKey)) ->
            (LocIdBaseId, SignatureId, DBCache)
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return ( LocIdBaseId
omsKey
                   , SignatureId
signatureKey
                   , LibName -> Node -> LocIdBaseId -> SignatureId -> DBCache -> DBCache
addNodeToCache LibName
libName Node
nodeId LocIdBaseId
omsKey SignatureId
signatureKey DBCache
dbCache0
                   )
          _ ->
            HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> ConsStatus
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> ConsStatus
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
createOMS HetcatsOpts
opts LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache0 Bool
doSave
              GlobalAnnos
globalAnnotations LibName
libName Entity LocIdBase
documentLocIdBase (Node
nodeId, DGNodeLab
nodeLabel)
              ConsStatus
consStatus

createOMS :: (MonadIO m, Fail.MonadFail m)
          => HetcatsOpts -> LibEnv -> FileVersionId -> DBCache -> Bool
          -> GlobalAnnos -> LibName -> Entity LocIdBase -> (Int, DGNodeLab)
          -> ConsStatus -> DBMonad m (LocIdBaseId, SignatureId, DBCache)
createOMS :: HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> ConsStatus
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
createOMS opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache0 :: DBCache
dbCache0 doSave :: Bool
doSave globalAnnotations :: GlobalAnnos
globalAnnotations libName :: LibName
libName
  documentLocIdBase :: Entity LocIdBase
documentLocIdBase@(Entity documentKey :: LocIdBaseId
documentKey _) (nodeId :: Node
nodeId, nodeLabel :: DGNodeLab
nodeLabel) consStatus :: ConsStatus
consStatus =
  let gTheory :: G_theory
gTheory = Maybe G_theory -> G_theory
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe G_theory -> G_theory) -> Maybe G_theory -> G_theory
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> Node -> Maybe G_theory
computeTheory LibEnv
libEnv LibName
libName Node
nodeId
      internalNodeName :: NodeName
internalNodeName = DGNodeLab -> NodeName
dgn_name DGNodeLab
nodeLabel
      name :: String
name = IRI -> String
forall a. Show a => a -> String
show (IRI -> String) -> IRI -> String
forall a b. (a -> b) -> a -> b
$ NodeName -> IRI
getName NodeName
internalNodeName
      nameExtension :: String
nameExtension = NodeName -> String
extString NodeName
internalNodeName
      nameExtensionIndex :: Node
nameExtensionIndex = NodeName -> Node
extIndex NodeName
internalNodeName
      displayName :: String
displayName = NodeName -> String
showName NodeName
internalNodeName
      locId :: String
locId = Entity LocIdBase -> DGNodeLab -> String
locIdOfOMS Entity LocIdBase
documentLocIdBase DGNodeLab
nodeLabel
  in  do
        Key Language
languageKey <- case G_theory
gTheory of
          G_theory { gTheoryLogic :: ()
gTheoryLogic = lid
lid } -> lid -> DBMonad m (Key Language)
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
lid -> DBMonad m (Key Language)
findLanguage lid
lid

        (signatureKey :: SignatureId
signatureKey, signatureIsNew :: Bool
signatureIsNew, dbCache1 :: DBCache
dbCache1) <- case G_theory
gTheory of
          G_theory { gTheoryLogic :: ()
gTheoryLogic = lid
lid
                   , gTheorySignIdx :: G_theory -> SigId
gTheorySignIdx = SigId
sigId
                   , gTheorySign :: ()
gTheorySign = ExtSign sign symbol
extSign
                   } -> do
           Maybe (LocIdBaseId, SignatureId)
omsKeyM <-
             FileVersionId
-> Entity LocIdBase
-> DGNodeLab
-> DBMonad m (Maybe (LocIdBaseId, SignatureId))
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
FileVersionId
-> Entity LocIdBase
-> DGNodeLab
-> DBMonad m (Maybe (LocIdBaseId, SignatureId))
findOMSAndSignature FileVersionId
fileVersionKey Entity LocIdBase
documentLocIdBase DGNodeLab
nodeLabel
           case Maybe (LocIdBaseId, SignatureId)
omsKeyM of
             Just (_, signatureKey :: SignatureId
signatureKey) ->
               (SignatureId, Bool, DBCache)
-> ReaderT SqlBackend m (SignatureId, Bool, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return ( SignatureId
signatureKey
                      , Bool
False
                      , LibName -> SigId -> SignatureId -> DBCache -> DBCache
addSignatureToCache LibName
libName SigId
sigId SignatureId
signatureKey DBCache
dbCache0
                      )
             Nothing ->
               DBCache
-> LibName
-> lid
-> ExtSign sign symbol
-> SigId
-> Key Language
-> ReaderT SqlBackend m (SignatureId, Bool, DBCache)
forall (m :: * -> *) lid sentence sign morphism symbol.
(MonadIO m, Sentences lid sentence sign morphism symbol) =>
DBCache
-> LibName
-> lid
-> ExtSign sign symbol
-> SigId
-> Key Language
-> DBMonad m (SignatureId, Bool, DBCache)
findOrCreateSignature DBCache
dbCache0 LibName
libName lid
lid ExtSign sign symbol
extSign SigId
sigId
                 Key Language
languageKey

        (normalFormKeyM :: Maybe LocIdBaseId
normalFormKeyM, normalFormSignatureKeyM :: Maybe SignatureId
normalFormSignatureKeyM, dbCache2 :: DBCache
dbCache2) <-
          HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> Maybe Node
-> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> Maybe Node
-> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
findOrCreateOMSM HetcatsOpts
opts LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache1 Bool
doSave
            GlobalAnnos
globalAnnotations LibName
libName Entity LocIdBase
documentLocIdBase (Maybe Node
 -> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache))
-> Maybe Node
-> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Maybe Node
dgn_nf DGNodeLab
nodeLabel

        (freeNormalFormKeyM :: Maybe LocIdBaseId
freeNormalFormKeyM, freeNormalFormSignatureKeyM :: Maybe SignatureId
freeNormalFormSignatureKeyM, dbCache3 :: DBCache
dbCache3) <-
          HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> Maybe Node
-> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> Maybe Node
-> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
findOrCreateOMSM HetcatsOpts
opts LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache2 Bool
doSave
            GlobalAnnos
globalAnnotations LibName
libName Entity LocIdBase
documentLocIdBase (Maybe Node
 -> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache))
-> Maybe Node
-> DBMonad m (Maybe LocIdBaseId, Maybe SignatureId, DBCache)
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Maybe Node
dgn_freenf DGNodeLab
nodeLabel

        (normalFormSignatureMorphismKeyM :: Maybe SignatureMorphismId
normalFormSignatureMorphismKeyM, _, dbCache4 :: DBCache
dbCache4) <-
          HetcatsOpts
-> LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Maybe Node)
-> GlobalAnnos
-> (SignatureId, Maybe SignatureId)
-> Maybe GMorphism
-> DBMonad
     m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Maybe Node)
-> GlobalAnnos
-> (SignatureId, Maybe SignatureId)
-> Maybe GMorphism
-> DBMonad
     m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
findOrCreateSignatureMorphismM HetcatsOpts
opts LibEnv
libEnv DBCache
dbCache3 Bool
doSave LibName
libName
            (Node
nodeId, DGNodeLab -> Maybe Node
dgn_nf DGNodeLab
nodeLabel) GlobalAnnos
globalAnnotations
            (SignatureId
signatureKey, Maybe SignatureId
normalFormSignatureKeyM) (Maybe GMorphism
 -> DBMonad
      m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache))
-> Maybe GMorphism
-> DBMonad
     m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
forall a b. (a -> b) -> a -> b
$
            DGNodeLab -> Maybe GMorphism
dgn_sigma DGNodeLab
nodeLabel

        (freeNormalFormSignatureMorphismKeyM :: Maybe SignatureMorphismId
freeNormalFormSignatureMorphismKeyM, _, dbCache5 :: DBCache
dbCache5) <-
          HetcatsOpts
-> LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Maybe Node)
-> GlobalAnnos
-> (SignatureId, Maybe SignatureId)
-> Maybe GMorphism
-> DBMonad
     m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Maybe Node)
-> GlobalAnnos
-> (SignatureId, Maybe SignatureId)
-> Maybe GMorphism
-> DBMonad
     m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
findOrCreateSignatureMorphismM HetcatsOpts
opts LibEnv
libEnv DBCache
dbCache4 Bool
doSave LibName
libName
            (Node
nodeId, DGNodeLab -> Maybe Node
dgn_freenf DGNodeLab
nodeLabel) GlobalAnnos
globalAnnotations
            (SignatureId
signatureKey, Maybe SignatureId
freeNormalFormSignatureKeyM) (Maybe GMorphism
 -> DBMonad
      m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache))
-> Maybe GMorphism
-> DBMonad
     m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
forall a b. (a -> b) -> a -> b
$
            DGNodeLab -> Maybe GMorphism
dgn_sigma DGNodeLab
nodeLabel

        omsLocIdBaseEntity :: Entity LocIdBase
omsLocIdBaseEntity@(Entity omsKey :: LocIdBaseId
omsKey _) <-
          if Bool -> Bool
not Bool
doSave
          then do
            [Entity LocIdBase]
omsL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LocIdBase)
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LocIdBase)
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (SqlExpr (Entity LocIdBase)
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ \loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases -> do
              SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase String
forall typ. (typ ~ String) => EntityField LocIdBase typ
LocIdBaseLocId 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
locId
                        SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase FileVersionId
-> SqlExpr (Value FileVersionId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase FileVersionId
forall typ. (typ ~ FileVersionId) => EntityField LocIdBase typ
LocIdBaseFileVersionId SqlExpr (Value FileVersionId)
-> SqlExpr (Value FileVersionId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. FileVersionId -> SqlExpr (Value FileVersionId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val FileVersionId
fileVersionKey
                        SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseKindType
-> SqlExpr (Value LocIdBaseKindType)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseKindType
forall typ. (typ ~ LocIdBaseKindType) => EntityField LocIdBase typ
LocIdBaseKind SqlExpr (Value LocIdBaseKindType)
-> SqlExpr (Value LocIdBaseKindType) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseKindType -> SqlExpr (Value LocIdBaseKindType)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseKindType
Enums.OMS)
              SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases

            case [Entity LocIdBase]
omsL of
              [] -> String -> ReaderT SqlBackend m (Entity LocIdBase)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.DevGraph.createOMS: OMS not found"
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
locId)
              entity :: Entity LocIdBase
entity : _ -> Entity LocIdBase -> ReaderT SqlBackend m (Entity LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity LocIdBase
entity
          else do
            ConservativityStatusId
conservativityStatusKey <- ConsStatus -> DBMonad m ConservativityStatusId
forall (m :: * -> *).
MonadIO m =>
ConsStatus -> DBMonad m ConservativityStatusId
createConservativityStatus ConsStatus
consStatus
            Maybe FileRangeId
nodeNameRangeKey <- Range -> DBMonad m (Maybe FileRangeId)
forall (m :: * -> *).
MonadIO m =>
Range -> DBMonad m (Maybe FileRangeId)
createRange (Range -> DBMonad m (Maybe FileRangeId))
-> Range -> DBMonad m (Maybe FileRangeId)
forall a b. (a -> b) -> a -> b
$ NodeName -> Range
srcRange NodeName
internalNodeName

            Maybe (Key Serialization)
serializationKey <- case G_theory
gTheory of
              G_theory { gTheorySyntax :: G_theory -> Maybe IRI
gTheorySyntax = Maybe IRI
syntaxM } ->
                Key Language -> Maybe IRI -> DBMonad m (Maybe (Key Serialization))
forall (m :: * -> *).
MonadIO m =>
Key Language -> Maybe IRI -> DBMonad m (Maybe (Key Serialization))
findOrCreateSerializationM Key Language
languageKey Maybe IRI
syntaxM

            Key Logic
logicKey <- case G_theory -> G_sublogics
sublogicOfTh G_theory
gTheory of
              G_sublogics lid :: lid
lid sublogics :: sublogics
sublogics -> HetcatsOpts -> lid -> sublogics -> DBMonad m (Key Logic)
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
HetcatsOpts -> lid -> sublogics -> DBMonad m (Key Logic)
findOrCreateLogic' HetcatsOpts
opts lid
lid sublogics
sublogics

            Key Action
actionKey <- Action -> ReaderT SqlBackend m (Key Action)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WAction :: EvaluationStateType -> Maybe Text -> Action
Action
              { actionEvaluationState :: EvaluationStateType
actionEvaluationState = EvaluationStateType
EvaluationStateType.FinishedSuccessfully
              , actionMessage :: Maybe Text
actionMessage = Maybe Text
forall a. Maybe a
Nothing
              }
            let omsLocIdBaseValue :: LocIdBase
omsLocIdBaseValue = $WLocIdBase :: FileVersionId -> LocIdBaseKindType -> String -> LocIdBase
LocIdBase
                  { locIdBaseFileVersionId :: FileVersionId
locIdBaseFileVersionId = FileVersionId
fileVersionKey
                  , locIdBaseKind :: LocIdBaseKindType
locIdBaseKind = LocIdBaseKindType
Enums.OMS
                  , locIdBaseLocId :: String
locIdBaseLocId = String
locId
                  }
            LocIdBaseId
omsKey <- LocIdBase -> ReaderT SqlBackend m LocIdBaseId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert LocIdBase
omsLocIdBaseValue
            let oms :: OMS
oms = $WOMS :: LocIdBaseId
-> Key Action
-> Key Logic
-> Key Language
-> Maybe (Key Serialization)
-> SignatureId
-> Maybe LocIdBaseId
-> Maybe SignatureMorphismId
-> Maybe LocIdBaseId
-> Maybe SignatureMorphismId
-> OMSOrigin
-> ConservativityStatusId
-> Maybe FileRangeId
-> String
-> String
-> String
-> Node
-> Bool
-> Bool
-> ConsistencyStatusType
-> OMS
OMS
                  { oMSDocumentId :: LocIdBaseId
oMSDocumentId = LocIdBaseId
documentKey
                  , oMSLanguageId :: Key Language
oMSLanguageId = Key Language
languageKey
                  , oMSLogicId :: Key Logic
oMSLogicId = Key Logic
logicKey
                  , oMSSerializationId :: Maybe (Key Serialization)
oMSSerializationId = Maybe (Key Serialization)
serializationKey
                  , oMSSignatureId :: SignatureId
oMSSignatureId = SignatureId
signatureKey
                  , oMSNormalFormId :: Maybe LocIdBaseId
oMSNormalFormId = Maybe LocIdBaseId
normalFormKeyM
                  , oMSNormalFormSignatureMorphismId :: Maybe SignatureMorphismId
oMSNormalFormSignatureMorphismId = Maybe SignatureMorphismId
normalFormSignatureMorphismKeyM
                  , oMSFreeNormalFormId :: Maybe LocIdBaseId
oMSFreeNormalFormId = Maybe LocIdBaseId
freeNormalFormKeyM
                  , oMSFreeNormalFormSignatureMorphismId :: Maybe SignatureMorphismId
oMSFreeNormalFormSignatureMorphismId = Maybe SignatureMorphismId
freeNormalFormSignatureMorphismKeyM
                  , oMSOrigin :: OMSOrigin
oMSOrigin = OMSOrigin
omsOrigin
                  , oMSConservativityStatusId :: ConservativityStatusId
oMSConservativityStatusId = ConservativityStatusId
conservativityStatusKey
                  , oMSNameFileRangeId :: Maybe FileRangeId
oMSNameFileRangeId = Maybe FileRangeId
nodeNameRangeKey
                  , oMSDisplayName :: String
oMSDisplayName = String
displayName
                  , oMSName :: String
oMSName = String
name
                  , oMSNameExtension :: String
oMSNameExtension = String
nameExtension
                  , oMSNameExtensionIndex :: Node
oMSNameExtensionIndex = Node
nameExtensionIndex
                  , oMSLabelHasHiding :: Bool
oMSLabelHasHiding = DGNodeLab -> Bool
labelHasHiding DGNodeLab
nodeLabel
                  , oMSLabelHasFree :: Bool
oMSLabelHasFree = DGNodeLab -> Bool
labelHasFree DGNodeLab
nodeLabel
                  , oMSActionId :: Key Action
oMSActionId = Key Action
actionKey
                  , oMSConsistencyStatus :: ConsistencyStatusType
oMSConsistencyStatus = ConsistencyStatusType
ConsistencyStatusType.Open
                  }
            [Entity OMS] -> ReaderT SqlBackend m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany [Key OMS -> OMS -> Entity OMS
forall record. Key record -> record -> Entity record
Entity (Int64 -> Key OMS
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key OMS) -> Int64 -> Key OMS
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
omsKey) OMS
oms]
            Entity LocIdBase -> ReaderT SqlBackend m (Entity LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return (Entity LocIdBase -> ReaderT SqlBackend m (Entity LocIdBase))
-> Entity LocIdBase -> ReaderT SqlBackend m (Entity LocIdBase)
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> LocIdBase -> Entity LocIdBase
forall record. Key record -> record -> Entity record
Entity LocIdBaseId
omsKey LocIdBase
omsLocIdBaseValue

        DBCache
dbCache6 <- case G_theory
gTheory of
          G_theory { gTheoryLogic :: ()
gTheoryLogic = lid
lid
                   , gTheorySign :: ()
gTheorySign = ExtSign sign symbol
extSign
                   } ->
            LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> ExtSign sign symbol
-> DBMonad m DBCache
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> ExtSign sign symbol
-> DBMonad m DBCache
createSymbols LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache5 Bool
doSave LibName
libName Node
nodeId
              Entity LocIdBase
omsLocIdBaseEntity lid
lid ExtSign sign symbol
extSign

        DBCache
dbCache7 <- case G_theory
gTheory of
          G_theory { gTheoryLogic :: ()
gTheoryLogic = lid
lid
                   , gTheorySign :: ()
gTheorySign = ExtSign { plainSign :: forall sign symbol. ExtSign sign symbol -> sign
plainSign = sign
sign }
                   , gTheorySens :: ()
gTheorySens = ThSens sentence (AnyComorphism, BasicProof)
sentences
                   } ->
            LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> sign
-> ThSens sentence (AnyComorphism, BasicProof)
-> DBMonad m DBCache
forall (m :: * -> *) sentence lid sublogics basic_spec symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m, GetRange sentence, Pretty sentence,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> sign
-> ThSens sentence (AnyComorphism, BasicProof)
-> DBMonad m DBCache
createSentences LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache6 Bool
doSave
              GlobalAnnos
globalAnnotations LibName
libName Node
nodeId Entity LocIdBase
omsLocIdBaseEntity lid
lid sign
sign
              ThSens sentence (AnyComorphism, BasicProof)
sentences

        DBCache
dbCache8 <- case G_theory
gTheory of
          G_theory { gTheoryLogic :: ()
gTheoryLogic = lid
lid
                   , gTheorySign :: ()
gTheorySign = ExtSign sign symbol
extSign
                   } ->
            if Bool
doSave Bool -> Bool -> Bool
&& Bool
signatureIsNew
            then LibEnv
-> DBCache
-> LibName
-> Node
-> lid
-> ExtSign sign symbol
-> SignatureId
-> DBMonad m DBCache
forall (m :: * -> *) lid sentence sign morphism symbol.
(MonadIO m, Sentences lid sentence sign morphism symbol) =>
LibEnv
-> DBCache
-> LibName
-> Node
-> lid
-> ExtSign sign symbol
-> SignatureId
-> DBMonad m DBCache
associateSymbolsOfSignature LibEnv
libEnv DBCache
dbCache7 LibName
libName Node
nodeId
                   lid
lid ExtSign sign symbol
extSign SignatureId
signatureKey
            else DBCache -> DBMonad m DBCache
forall (m :: * -> *) a. Monad m => a -> m a
return DBCache
dbCache7

        (LocIdBaseId, SignatureId, DBCache)
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return ( LocIdBaseId
omsKey
               , SignatureId
signatureKey
               , LibName -> Node -> LocIdBaseId -> SignatureId -> DBCache -> DBCache
addNodeToCache LibName
libName Node
nodeId LocIdBaseId
omsKey SignatureId
signatureKey DBCache
dbCache8
               )
  where
    omsOrigin :: OMSOrigin
    omsOrigin :: OMSOrigin
omsOrigin = case DGNodeInfo -> DGOrigin
node_origin (DGNodeInfo -> DGOrigin) -> DGNodeInfo -> DGOrigin
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
nodeLabel of
      DGEmpty -> OMSOrigin
OMSOrigin.DGEmpty
      DGBasic -> OMSOrigin
OMSOrigin.DGBasic
      DGBasicSpec{} -> OMSOrigin
OMSOrigin.DGBasicSpec
      DGExtension -> OMSOrigin
OMSOrigin.DGExtension
      DGLogicCoercion -> OMSOrigin
OMSOrigin.DGLogicCoercion
      DGTranslation _ -> OMSOrigin
OMSOrigin.DGTranslation
      DGUnion -> OMSOrigin
OMSOrigin.DGUnion
      DGIntersect -> OMSOrigin
OMSOrigin.DGIntersect
      DGExtract -> OMSOrigin
OMSOrigin.DGExtract
      DGRestriction _ _ -> OMSOrigin
OMSOrigin.DGRestriction
      DGRevealTranslation -> OMSOrigin
OMSOrigin.DGRevealTranslation
      DGFreeOrCofree Free -> OMSOrigin
OMSOrigin.Free
      DGFreeOrCofree Cofree -> OMSOrigin
OMSOrigin.Cofree
      DGFreeOrCofree NPFree -> OMSOrigin
OMSOrigin.NPFree
      DGFreeOrCofree Minimize -> OMSOrigin
OMSOrigin.Minimize
      DGLocal -> OMSOrigin
OMSOrigin.DGLocal
      DGClosed -> OMSOrigin
OMSOrigin.DGClosed
      DGLogicQual -> OMSOrigin
OMSOrigin.DGLogicQual
      DGData -> OMSOrigin
OMSOrigin.DGData
      DGFormalParams -> OMSOrigin
OMSOrigin.DGFormalParams
      DGVerificationGeneric -> OMSOrigin
OMSOrigin.DGVerificationGeneric
      DGImports -> OMSOrigin
OMSOrigin.DGImports
      DGInst _ -> OMSOrigin
OMSOrigin.DGInst
      DGFitSpec -> OMSOrigin
OMSOrigin.DGFitSpec
      DGFitView _ -> OMSOrigin
OMSOrigin.DGFitView
      DGProof -> OMSOrigin
OMSOrigin.DGProof
      DGNormalForm _ -> OMSOrigin
OMSOrigin.DGNormalForm
      DGintegratedSCC -> OMSOrigin
OMSOrigin.DGintegratedSCC
      DGFlattening -> OMSOrigin
OMSOrigin.DGFlattening
      DGAlignment -> OMSOrigin
OMSOrigin.DGAlignment
      DGTest -> OMSOrigin
OMSOrigin.DGTest


createConservativityStatus :: MonadIO m
                           => ConsStatus -> DBMonad m ConservativityStatusId
createConservativityStatus :: ConsStatus -> DBMonad m ConservativityStatusId
createConservativityStatus (ConsStatus r :: Conservativity
r p :: Conservativity
p _) =
  ConservativityStatus -> DBMonad m ConservativityStatusId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WConservativityStatus :: String -> String -> ConservativityStatus
SchemaClass.ConservativityStatus
    { conservativityStatusRequired :: String
conservativityStatusRequired = Conservativity -> String
toString Conservativity
r
    , conservativityStatusProved :: String
conservativityStatusProved = Conservativity -> String
toString Conservativity
p
    }
  where
    toString :: Conservativity -> String
    toString :: Conservativity -> String
toString c :: Conservativity
c = case Conservativity
c of
      Unknown s :: String
s -> String
s
      _ -> (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Conservativity -> String
forall a. Show a => a -> String
show Conservativity
c

findOrCreateSignatureMorphismM :: (MonadIO m, Fail.MonadFail m)
                               => HetcatsOpts -> LibEnv -> DBCache -> Bool
                               -> LibName -> (Int, Maybe Int) -> GlobalAnnos
                               -> (SignatureId, Maybe SignatureId)
                               -> Maybe GMorphism
                               -> DBMonad m ( Maybe SignatureMorphismId
                                            , [SymbolMappingId]
                                            , DBCache
                                            )
findOrCreateSignatureMorphismM :: HetcatsOpts
-> LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Maybe Node)
-> GlobalAnnos
-> (SignatureId, Maybe SignatureId)
-> Maybe GMorphism
-> DBMonad
     m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
findOrCreateSignatureMorphismM opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv dbCache :: DBCache
dbCache doSave :: Bool
doSave libName :: LibName
libName
  (sourceId :: Node
sourceId, targetIdM :: Maybe Node
targetIdM) globalAnnotations :: GlobalAnnos
globalAnnotations
  (sourceSignatureKey :: SignatureId
sourceSignatureKey, targetSignatureKeyM :: Maybe SignatureId
targetSignatureKeyM) gMorphismM :: Maybe GMorphism
gMorphismM =
    case Maybe GMorphism
gMorphismM of
      Nothing -> (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
-> DBMonad
     m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe SignatureMorphismId
forall a. Maybe a
Nothing, [], DBCache
dbCache)
      Just gMorphism :: GMorphism
gMorphism -> do
        (signatureMorphismKey :: SignatureMorphismId
signatureMorphismKey, symbolMappingKeys :: [SymbolMappingId]
symbolMappingKeys, dbCache1 :: DBCache
dbCache1) <-
          HetcatsOpts
-> LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> GlobalAnnos
-> (SignatureId, SignatureId)
-> GMorphism
-> DBMonad m (SignatureMorphismId, [SymbolMappingId], DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> GlobalAnnos
-> (SignatureId, SignatureId)
-> GMorphism
-> DBMonad m (SignatureMorphismId, [SymbolMappingId], DBCache)
findOrCreateSignatureMorphism HetcatsOpts
opts LibEnv
libEnv DBCache
dbCache Bool
doSave LibName
libName
            (Node
sourceId, Maybe Node -> Node
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Node
targetIdM) GlobalAnnos
globalAnnotations
            (SignatureId
sourceSignatureKey, Maybe SignatureId -> SignatureId
forall a. HasCallStack => Maybe a -> a
fromJust Maybe SignatureId
targetSignatureKeyM) GMorphism
gMorphism
        (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
-> DBMonad
     m (Maybe SignatureMorphismId, [SymbolMappingId], DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (SignatureMorphismId -> Maybe SignatureMorphismId
forall a. a -> Maybe a
Just SignatureMorphismId
signatureMorphismKey, [SymbolMappingId]
symbolMappingKeys, DBCache
dbCache1)

findOrCreateSignatureMorphism :: (MonadIO m, Fail.MonadFail m)
                              => HetcatsOpts -> LibEnv -> DBCache -> Bool
                              -> LibName -> (Int, Int) -> GlobalAnnos
                              -> (SignatureId, SignatureId)
                              -> GMorphism
                              -> DBMonad m ( SignatureMorphismId
                                           , [SymbolMappingId]
                                           , DBCache
                                           )
findOrCreateSignatureMorphism :: HetcatsOpts
-> LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> GlobalAnnos
-> (SignatureId, SignatureId)
-> GMorphism
-> DBMonad m (SignatureMorphismId, [SymbolMappingId], DBCache)
findOrCreateSignatureMorphism opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv dbCache :: DBCache
dbCache doSave :: Bool
doSave libName :: LibName
libName edge :: (Node, Node)
edge
  globalAnnotations :: GlobalAnnos
globalAnnotations (sourceSignatureKey :: SignatureId
sourceSignatureKey, targetSignatureKey :: SignatureId
targetSignatureKey) gMorphism :: GMorphism
gMorphism =
    case GMorphism
gMorphism of
      GMorphism { gMorphismComor :: ()
gMorphismComor = cid
cid
                , gMorphismMorIdx :: GMorphism -> MorId
gMorphismMorIdx = MorId
morphismId
                } ->
        case (LibName, MorId)
-> Map
     (LibName, MorId)
     (SignatureMorphismId, [SymbolMappingId], GMorphism)
-> Maybe (SignatureMorphismId, [SymbolMappingId], GMorphism)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LibName
libName, MorId
morphismId) (Map
   (LibName, MorId)
   (SignatureMorphismId, [SymbolMappingId], GMorphism)
 -> Maybe (SignatureMorphismId, [SymbolMappingId], GMorphism))
-> Map
     (LibName, MorId)
     (SignatureMorphismId, [SymbolMappingId], GMorphism)
-> Maybe (SignatureMorphismId, [SymbolMappingId], GMorphism)
forall a b. (a -> b) -> a -> b
$ DBCache
-> Map
     (LibName, MorId)
     (SignatureMorphismId, [SymbolMappingId], GMorphism)
signatureMorphismMap DBCache
dbCache of
          Just (signatureMorphismKey :: SignatureMorphismId
signatureMorphismKey, symbolMappingKeys :: [SymbolMappingId]
symbolMappingKeys, _) ->
            (SignatureMorphismId, [SymbolMappingId], DBCache)
-> DBMonad m (SignatureMorphismId, [SymbolMappingId], DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (SignatureMorphismId
signatureMorphismKey, [SymbolMappingId]
symbolMappingKeys, DBCache
dbCache)
          Nothing ->
            let json :: String
json = Json -> String
ppJson (Json -> String) -> Json -> String
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> GlobalAnnos -> GMorphism -> Json
ToJson.gmorph HetcatsOpts
opts GlobalAnnos
globalAnnotations GMorphism
gMorphism
            in do
                (_, logicMappingKey :: LogicMappingId
logicMappingKey) <-
                  HetcatsOpts
-> AnyComorphism -> DBMonad m (LanguageMappingId, LogicMappingId)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> AnyComorphism -> DBMonad m (LanguageMappingId, LogicMappingId)
findOrCreateLanguageMappingAndLogicMapping HetcatsOpts
opts (AnyComorphism -> DBMonad m (LanguageMappingId, LogicMappingId))
-> AnyComorphism -> DBMonad m (LanguageMappingId, 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 cid
cid
                SignatureMorphismId
signatureMorphismKey <-
                  if Bool
doSave
                  then SignatureMorphism -> ReaderT SqlBackend m SignatureMorphismId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WSignatureMorphism :: LogicMappingId
-> String -> SignatureId -> SignatureId -> SignatureMorphism
SignatureMorphism
                        { signatureMorphismLogicMappingId :: LogicMappingId
signatureMorphismLogicMappingId = LogicMappingId
logicMappingKey
                        , signatureMorphismAsJson :: String
signatureMorphismAsJson = String
json
                        , signatureMorphismSourceId :: SignatureId
signatureMorphismSourceId = SignatureId
sourceSignatureKey
                        , signatureMorphismTargetId :: SignatureId
signatureMorphismTargetId = SignatureId
targetSignatureKey
                        }
                  else do
                    [Entity SignatureMorphism]
signatureMorphismL <- SqlQuery (SqlExpr (Entity SignatureMorphism))
-> ReaderT SqlBackend m [Entity SignatureMorphism]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity SignatureMorphism))
 -> ReaderT SqlBackend m [Entity SignatureMorphism])
-> SqlQuery (SqlExpr (Entity SignatureMorphism))
-> ReaderT SqlBackend m [Entity SignatureMorphism]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity SignatureMorphism)
 -> SqlQuery (SqlExpr (Entity SignatureMorphism)))
-> SqlQuery (SqlExpr (Entity SignatureMorphism))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity SignatureMorphism)
  -> SqlQuery (SqlExpr (Entity SignatureMorphism)))
 -> SqlQuery (SqlExpr (Entity SignatureMorphism)))
-> (SqlExpr (Entity SignatureMorphism)
    -> SqlQuery (SqlExpr (Entity SignatureMorphism)))
-> SqlQuery (SqlExpr (Entity SignatureMorphism))
forall a b. (a -> b) -> a -> b
$ \signature_morphisms :: SqlExpr (Entity SignatureMorphism)
signature_morphisms -> do
                      SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity SignatureMorphism)
signature_morphisms SqlExpr (Entity SignatureMorphism)
-> EntityField SignatureMorphism LogicMappingId
-> SqlExpr (Value LogicMappingId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField SignatureMorphism LogicMappingId
forall typ.
(typ ~ LogicMappingId) =>
EntityField SignatureMorphism typ
SignatureMorphismLogicMappingId SqlExpr (Value LogicMappingId)
-> SqlExpr (Value LogicMappingId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LogicMappingId -> SqlExpr (Value LogicMappingId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LogicMappingId
logicMappingKey
                                SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity SignatureMorphism)
signature_morphisms SqlExpr (Entity SignatureMorphism)
-> EntityField SignatureMorphism SignatureId
-> SqlExpr (Value SignatureId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField SignatureMorphism SignatureId
forall typ.
(typ ~ SignatureId) =>
EntityField SignatureMorphism typ
SignatureMorphismSourceId SqlExpr (Value SignatureId)
-> SqlExpr (Value SignatureId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. SignatureId -> SqlExpr (Value SignatureId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val SignatureId
sourceSignatureKey
                                SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity SignatureMorphism)
signature_morphisms SqlExpr (Entity SignatureMorphism)
-> EntityField SignatureMorphism SignatureId
-> SqlExpr (Value SignatureId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField SignatureMorphism SignatureId
forall typ.
(typ ~ SignatureId) =>
EntityField SignatureMorphism typ
SignatureMorphismTargetId SqlExpr (Value SignatureId)
-> SqlExpr (Value SignatureId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. SignatureId -> SqlExpr (Value SignatureId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val SignatureId
targetSignatureKey
                                SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity SignatureMorphism)
signature_morphisms SqlExpr (Entity SignatureMorphism)
-> EntityField SignatureMorphism String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField SignatureMorphism String
forall typ. (typ ~ String) => EntityField SignatureMorphism typ
SignatureMorphismAsJson 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
json)
                      SqlExpr (Entity SignatureMorphism)
-> SqlQuery (SqlExpr (Entity SignatureMorphism))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity SignatureMorphism)
signature_morphisms
                    case [Entity SignatureMorphism]
signatureMorphismL of
                      [] -> String -> ReaderT SqlBackend m SignatureMorphismId
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Persistence.DevGraph.findOrCreateSignatureMorphism: not found "
                      Entity key :: SignatureMorphismId
key _ : _ -> SignatureMorphismId -> ReaderT SqlBackend m SignatureMorphismId
forall (m :: * -> *) a. Monad m => a -> m a
return SignatureMorphismId
key

                (symbolMappingKeys :: [SymbolMappingId]
symbolMappingKeys, dbCache1 :: DBCache
dbCache1) <-
                  LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> SignatureMorphismId
-> GMorphism
-> DBMonad m ([SymbolMappingId], DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> SignatureMorphismId
-> GMorphism
-> DBMonad m ([SymbolMappingId], DBCache)
findOrCreateSymbolMappings LibEnv
libEnv DBCache
dbCache Bool
doSave LibName
libName (Node, Node)
edge
                    SignatureMorphismId
signatureMorphismKey GMorphism
gMorphism

                let signatureMorphismMap' :: Map
  (LibName, MorId)
  (SignatureMorphismId, [SymbolMappingId], GMorphism)
signatureMorphismMap' =
                      (LibName, MorId)
-> (SignatureMorphismId, [SymbolMappingId], GMorphism)
-> Map
     (LibName, MorId)
     (SignatureMorphismId, [SymbolMappingId], GMorphism)
-> Map
     (LibName, MorId)
     (SignatureMorphismId, [SymbolMappingId], GMorphism)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName
libName, MorId
morphismId)
                        (SignatureMorphismId
signatureMorphismKey, [SymbolMappingId]
symbolMappingKeys, GMorphism
gMorphism) (Map
   (LibName, MorId)
   (SignatureMorphismId, [SymbolMappingId], GMorphism)
 -> Map
      (LibName, MorId)
      (SignatureMorphismId, [SymbolMappingId], GMorphism))
-> Map
     (LibName, MorId)
     (SignatureMorphismId, [SymbolMappingId], GMorphism)
-> Map
     (LibName, MorId)
     (SignatureMorphismId, [SymbolMappingId], GMorphism)
forall a b. (a -> b) -> a -> b
$
                        DBCache
-> Map
     (LibName, MorId)
     (SignatureMorphismId, [SymbolMappingId], GMorphism)
signatureMorphismMap DBCache
dbCache1
                let dbCache2 :: DBCache
dbCache2 =
                      DBCache
dbCache1 { signatureMorphismMap :: Map
  (LibName, MorId)
  (SignatureMorphismId, [SymbolMappingId], GMorphism)
signatureMorphismMap = Map
  (LibName, MorId)
  (SignatureMorphismId, [SymbolMappingId], GMorphism)
signatureMorphismMap' }
                (SignatureMorphismId, [SymbolMappingId], DBCache)
-> DBMonad m (SignatureMorphismId, [SymbolMappingId], DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return ( SignatureMorphismId
signatureMorphismKey
                       , [SymbolMappingId]
symbolMappingKeys
                       , DBCache
dbCache2
                       )

findOrCreateSymbolMappings :: (MonadIO m, Fail.MonadFail m)
                           => LibEnv -> DBCache -> Bool -> LibName -> (Int, Int)
                           -> SignatureMorphismId -> GMorphism
                           -> DBMonad m ([SymbolMappingId], DBCache)
findOrCreateSymbolMappings :: LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> SignatureMorphismId
-> GMorphism
-> DBMonad m ([SymbolMappingId], DBCache)
findOrCreateSymbolMappings libEnv :: LibEnv
libEnv dbCache :: DBCache
dbCache doSave :: Bool
doSave libName :: LibName
libName edge :: (Node, Node)
edge
  signatureMorphismKey :: SignatureMorphismId
signatureMorphismKey gMorphism :: GMorphism
gMorphism = case GMorphism
gMorphism of
    GMorphism { gMorphismComor :: ()
gMorphismComor = cid
cid
              , gMorphismMor :: ()
gMorphismMor = morphism2
morphism
              , gMorphismSign :: ()
gMorphismSign = extSign :: ExtSign sign1 symbol1
extSign@ExtSign { plainSign :: forall sign symbol. ExtSign sign symbol -> sign
plainSign = sign1
sign }
              } ->
      let sourceLid :: lid1
sourceLid = 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
          targetLid :: lid2
targetLid = 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
          symbolMap :: EndoMap symbol2
symbolMap = lid2 -> morphism2 -> EndoMap symbol2
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> EndoMap symbol
symmap_of lid2
targetLid morphism2
morphism
      in  do
            [SymbolMappingId]
symbolMappingKeys <-
              (symbol1 -> ReaderT SqlBackend m [SymbolMappingId])
-> [symbol1] -> ReaderT SqlBackend m [SymbolMappingId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m [b]) -> t a -> m [b]
concatMapM
                (\ sourceSymbol :: symbol1
sourceSymbol ->
                  (symbol2 -> ReaderT SqlBackend m [SymbolMappingId])
-> [symbol2] -> ReaderT SqlBackend m [SymbolMappingId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m [b]) -> t a -> m [b]
concatMapM
                    (\ translatedSymbol :: symbol2
translatedSymbol ->
                      case symbol2 -> EndoMap symbol2 -> Maybe symbol2
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup symbol2
translatedSymbol EndoMap symbol2
symbolMap of
                        Nothing -> [SymbolMappingId] -> ReaderT SqlBackend m [SymbolMappingId]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                        Just targetSymbol :: symbol2
targetSymbol -> do
                            SymbolMappingId
symbolMappingKey <-
                              LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> SignatureMorphismId
-> lid1
-> lid2
-> symbol1
-> symbol2
-> DBMonad m SymbolMappingId
forall (m :: * -> *) lid1 sentence1 sign1 morphism1 symbol1 lid2
       sentence2 sign2 morphism2 symbol2.
(MonadIO m, MonadFail m,
 Sentences lid1 sentence1 sign1 morphism1 symbol1,
 Sentences lid2 sentence2 sign2 morphism2 symbol2) =>
LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> SignatureMorphismId
-> lid1
-> lid2
-> symbol1
-> symbol2
-> DBMonad m SymbolMappingId
findOrCreateSymbolMapping LibEnv
libEnv DBCache
dbCache Bool
doSave
                                LibName
libName (Node, Node)
edge SignatureMorphismId
signatureMorphismKey lid1
sourceLid
                                lid2
targetLid symbol1
sourceSymbol symbol2
targetSymbol
                            [SymbolMappingId] -> ReaderT SqlBackend m [SymbolMappingId]
forall (m :: * -> *) a. Monad m => a -> m a
return [SymbolMappingId
symbolMappingKey]
                    ) ([symbol2] -> ReaderT SqlBackend m [SymbolMappingId])
-> [symbol2] -> ReaderT SqlBackend m [SymbolMappingId]
forall a b. (a -> b) -> a -> b
$ Set symbol2 -> [symbol2]
forall a. Set a -> [a]
Set.toList (Set symbol2 -> [symbol2]) -> Set symbol2 -> [symbol2]
forall a b. (a -> b) -> a -> b
$ cid -> sign1 -> symbol1 -> Set symbol2
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 -> sign1 -> symbol1 -> Set symbol2
map_symbol cid
cid sign1
sign symbol1
sourceSymbol
                ) ([symbol1] -> ReaderT SqlBackend m [SymbolMappingId])
-> [symbol1] -> ReaderT SqlBackend m [SymbolMappingId]
forall a b. (a -> b) -> a -> b
$ Set symbol1 -> [symbol1]
forall a. Set a -> [a]
Set.toList (Set symbol1 -> [symbol1]) -> Set symbol1 -> [symbol1]
forall a b. (a -> b) -> a -> b
$ lid1 -> sign1 -> Set symbol1
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid1
sourceLid (sign1 -> Set symbol1) -> sign1 -> Set symbol1
forall a b. (a -> b) -> a -> b
$ ExtSign sign1 symbol1 -> sign1
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign1 symbol1
extSign
            ([SymbolMappingId], DBCache)
-> DBMonad m ([SymbolMappingId], DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SymbolMappingId]
symbolMappingKeys, DBCache
dbCache)

findOrCreateSymbolMapping :: ( MonadIO m
                             , Fail.MonadFail m
                             , Sentences lid1 sentence1 sign1 morphism1 symbol1
                             , Sentences lid2 sentence2 sign2 morphism2 symbol2
                             )
                          => LibEnv -> DBCache -> Bool -> LibName -> (Int, Int)
                          -> SignatureMorphismId
                          -> lid1 -> lid2 -> symbol1 -> symbol2
                          -> DBMonad m SymbolMappingId
findOrCreateSymbolMapping :: LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> SignatureMorphismId
-> lid1
-> lid2
-> symbol1
-> symbol2
-> DBMonad m SymbolMappingId
findOrCreateSymbolMapping libEnv :: LibEnv
libEnv dbCache :: DBCache
dbCache doSave :: Bool
doSave libName :: LibName
libName (sourceId :: Node
sourceId, targetId :: Node
targetId)
  signatureMorphismKey :: SignatureMorphismId
signatureMorphismKey sourceLid :: lid1
sourceLid targetLid :: lid2
targetLid sourceSymbol :: symbol1
sourceSymbol targetSymbol :: symbol2
targetSymbol = do
  LocIdBaseId
sourceKey <-
    String -> Maybe LocIdBaseId -> ReaderT SqlBackend m LocIdBaseId
forall (m :: * -> *) a.
(MonadIO m, MonadFail m) =>
String -> Maybe a -> m a
fromJustFail (LibEnv -> LibName -> Node -> symbol1 -> lid1 -> ShowS
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
LibEnv -> LibName -> Node -> symbol -> lid -> ShowS
symbolErrorMessage LibEnv
libEnv LibName
libName Node
sourceId symbol1
sourceSymbol lid1
sourceLid "source") (Maybe LocIdBaseId -> ReaderT SqlBackend m LocIdBaseId)
-> Maybe LocIdBaseId -> ReaderT SqlBackend m LocIdBaseId
forall a b. (a -> b) -> a -> b
$
      LibEnv
-> LibName
-> Node
-> lid1
-> symbol1
-> DBCache
-> Maybe LocIdBaseId
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
LibEnv
-> LibName -> Node -> lid -> symbol -> DBCache -> Maybe LocIdBaseId
findSymbolInCache LibEnv
libEnv LibName
libName Node
sourceId lid1
sourceLid symbol1
sourceSymbol DBCache
dbCache

  LocIdBaseId
targetKey <-
    String -> Maybe LocIdBaseId -> ReaderT SqlBackend m LocIdBaseId
forall (m :: * -> *) a.
(MonadIO m, MonadFail m) =>
String -> Maybe a -> m a
fromJustFail (LibEnv -> LibName -> Node -> symbol2 -> lid2 -> ShowS
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
LibEnv -> LibName -> Node -> symbol -> lid -> ShowS
symbolErrorMessage LibEnv
libEnv LibName
libName Node
targetId symbol2
targetSymbol lid2
targetLid "target") (Maybe LocIdBaseId -> ReaderT SqlBackend m LocIdBaseId)
-> Maybe LocIdBaseId -> ReaderT SqlBackend m LocIdBaseId
forall a b. (a -> b) -> a -> b
$
      LibEnv
-> LibName
-> Node
-> lid2
-> symbol2
-> DBCache
-> Maybe LocIdBaseId
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
LibEnv
-> LibName -> Node -> lid -> symbol -> DBCache -> Maybe LocIdBaseId
findSymbolInCache LibEnv
libEnv LibName
libName Node
targetId lid2
targetLid symbol2
targetSymbol DBCache
dbCache

  [Entity SymbolMapping]
symbolMappingL <- SqlQuery (SqlExpr (Entity SymbolMapping))
-> ReaderT SqlBackend m [Entity SymbolMapping]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity SymbolMapping))
 -> ReaderT SqlBackend m [Entity SymbolMapping])
-> SqlQuery (SqlExpr (Entity SymbolMapping))
-> ReaderT SqlBackend m [Entity SymbolMapping]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity SymbolMapping)
 -> SqlQuery (SqlExpr (Entity SymbolMapping)))
-> SqlQuery (SqlExpr (Entity SymbolMapping))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity SymbolMapping)
  -> SqlQuery (SqlExpr (Entity SymbolMapping)))
 -> SqlQuery (SqlExpr (Entity SymbolMapping)))
-> (SqlExpr (Entity SymbolMapping)
    -> SqlQuery (SqlExpr (Entity SymbolMapping)))
-> SqlQuery (SqlExpr (Entity SymbolMapping))
forall a b. (a -> b) -> a -> b
$ \symbol_mappings :: SqlExpr (Entity SymbolMapping)
symbol_mappings -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity SymbolMapping)
symbol_mappings SqlExpr (Entity SymbolMapping)
-> EntityField SymbolMapping SignatureMorphismId
-> SqlExpr (Value SignatureMorphismId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField SymbolMapping SignatureMorphismId
forall typ.
(typ ~ SignatureMorphismId) =>
EntityField SymbolMapping typ
SymbolMappingSignatureMorphismId SqlExpr (Value SignatureMorphismId)
-> SqlExpr (Value SignatureMorphismId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. SignatureMorphismId -> SqlExpr (Value SignatureMorphismId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val SignatureMorphismId
signatureMorphismKey
              SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity SymbolMapping)
symbol_mappings SqlExpr (Entity SymbolMapping)
-> EntityField SymbolMapping LocIdBaseId
-> SqlExpr (Value LocIdBaseId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField SymbolMapping LocIdBaseId
forall typ. (typ ~ LocIdBaseId) => EntityField SymbolMapping typ
SymbolMappingSourceId SqlExpr (Value LocIdBaseId)
-> SqlExpr (Value LocIdBaseId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseId
sourceKey
              SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity SymbolMapping)
symbol_mappings SqlExpr (Entity SymbolMapping)
-> EntityField SymbolMapping LocIdBaseId
-> SqlExpr (Value LocIdBaseId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField SymbolMapping LocIdBaseId
forall typ. (typ ~ LocIdBaseId) => EntityField SymbolMapping typ
SymbolMappingTargetId SqlExpr (Value LocIdBaseId)
-> SqlExpr (Value LocIdBaseId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseId -> SqlExpr (Value LocIdBaseId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseId
targetKey)
    SqlExpr (Entity SymbolMapping)
-> SqlQuery (SqlExpr (Entity SymbolMapping))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity SymbolMapping)
symbol_mappings
  case [Entity SymbolMapping]
symbolMappingL of
    Entity symbolMappingKey :: SymbolMappingId
symbolMappingKey _ : _ -> SymbolMappingId -> DBMonad m SymbolMappingId
forall (m :: * -> *) a. Monad m => a -> m a
return SymbolMappingId
symbolMappingKey
    [] ->
      if Bool
doSave
      then SymbolMapping -> DBMonad m SymbolMappingId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WSymbolMapping :: SignatureMorphismId -> LocIdBaseId -> LocIdBaseId -> SymbolMapping
SymbolMapping
            { symbolMappingSignatureMorphismId :: SignatureMorphismId
symbolMappingSignatureMorphismId = SignatureMorphismId
signatureMorphismKey
            , symbolMappingSourceId :: LocIdBaseId
symbolMappingSourceId = LocIdBaseId
sourceKey
            , symbolMappingTargetId :: LocIdBaseId
symbolMappingTargetId = LocIdBaseId
targetKey
            }
      else String -> DBMonad m SymbolMappingId
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Persistence.DevGraph.findOrCreateSymbolMapping: not found"

symbolErrorMessage :: Sentences lid sentence sign morphism symbol
                   => LibEnv -> LibName -> Node -> symbol -> lid -> String
                   -> String
symbolErrorMessage :: LibEnv -> LibName -> Node -> symbol -> lid -> ShowS
symbolErrorMessage libEnv :: LibEnv
libEnv libName :: LibName
libName nodeId :: Node
nodeId symbol :: symbol
symbol lid :: lid
lid end :: String
end =
  let (libNameDereferenced :: LibName
libNameDereferenced, nodeIdDereferenced :: Node
nodeIdDereferenced) = LibEnv -> LibName -> Node -> (LibName, Node)
dereferenceNodeId LibEnv
libEnv LibName
libName Node
nodeId
      fullName :: String
fullName = ShowS
forall a. Show a => a -> String
show ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ lid -> symbol -> String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> String
fullSymName lid
lid symbol
symbol
      symbolKind :: String
symbolKind = lid -> symbol -> String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> String
symKind lid
lid symbol
symbol
      nodeName :: String
nodeName = IRI -> String
forall a. Show a => a -> String
show (IRI -> String) -> IRI -> String
forall a b. (a -> b) -> a -> b
$ NodeName -> IRI
getName (NodeName -> IRI) -> NodeName -> IRI
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> NodeName
dgn_name (DGNodeLab -> NodeName) -> DGNodeLab -> NodeName
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> Node -> DGNodeLab
getNodeLabel LibEnv
libEnv LibName
libName Node
nodeId
  in  "Could not find " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
end String -> ShowS
forall a. [a] -> [a] -> [a]
++ " symbol for SymbolMapping:"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nsymbol name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fullName
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nsymbol kind: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
symbolKind
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nnode name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nodeName
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nnode ID: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
nodeIdDereferenced
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nlibrary name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ LibName -> String
forall a. Show a => a -> String
show LibName
libNameDereferenced
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nThis is a system error. Please report it at https://github.com/spechub/Hets/issues"


findOrCreateSerializationM :: MonadIO m
                           => LanguageId -> Maybe IRI
                           -> DBMonad m (Maybe SerializationId)
findOrCreateSerializationM :: Key Language -> Maybe IRI -> DBMonad m (Maybe (Key Serialization))
findOrCreateSerializationM languageKey :: Key Language
languageKey syntaxM :: Maybe IRI
syntaxM =
  case Maybe IRI
syntaxM of
    Nothing -> Maybe (Key Serialization) -> DBMonad m (Maybe (Key Serialization))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Key Serialization)
forall a. Maybe a
Nothing
    Just syntaxIRI :: IRI
syntaxIRI -> do
      let syntaxIRIString :: String
syntaxIRIString = IRI -> String
forall a. Show a => a -> String
show (IRI -> String) -> IRI -> String
forall a b. (a -> b) -> a -> b
$ Bool -> IRI -> IRI
setAngles Bool
False IRI
syntaxIRI
      [Entity Serialization]
serializationL <- SqlQuery (SqlExpr (Entity Serialization))
-> ReaderT SqlBackend m [Entity Serialization]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity Serialization))
 -> ReaderT SqlBackend m [Entity Serialization])
-> SqlQuery (SqlExpr (Entity Serialization))
-> ReaderT SqlBackend m [Entity Serialization]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity Serialization)
 -> SqlQuery (SqlExpr (Entity Serialization)))
-> SqlQuery (SqlExpr (Entity Serialization))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity Serialization)
  -> SqlQuery (SqlExpr (Entity Serialization)))
 -> SqlQuery (SqlExpr (Entity Serialization)))
-> (SqlExpr (Entity Serialization)
    -> SqlQuery (SqlExpr (Entity Serialization)))
-> SqlQuery (SqlExpr (Entity Serialization))
forall a b. (a -> b) -> a -> b
$ \serializations :: SqlExpr (Entity Serialization)
serializations -> do
        SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity Serialization)
serializations SqlExpr (Entity Serialization)
-> EntityField Serialization String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField Serialization String
forall typ. (typ ~ String) => EntityField Serialization typ
SerializationName 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
syntaxIRIString)
        SqlExpr (Entity Serialization)
-> SqlQuery (SqlExpr (Entity Serialization))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity Serialization)
serializations
      case [Entity Serialization]
serializationL of
        Entity serializationKey :: Key Serialization
serializationKey _ : _ -> Maybe (Key Serialization) -> DBMonad m (Maybe (Key Serialization))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Key Serialization)
 -> DBMonad m (Maybe (Key Serialization)))
-> Maybe (Key Serialization)
-> DBMonad m (Maybe (Key Serialization))
forall a b. (a -> b) -> a -> b
$ Key Serialization -> Maybe (Key Serialization)
forall a. a -> Maybe a
Just Key Serialization
serializationKey
        [] -> do
          Key Serialization
serializationKey <- Serialization -> ReaderT SqlBackend m (Key Serialization)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WSerialization :: Key Language -> String -> String -> Serialization
Serialization
            { serializationLanguageId :: Key Language
serializationLanguageId = Key Language
languageKey
            , serializationSlug :: String
serializationSlug = ShowS
parameterize String
syntaxIRIString
            , serializationName :: String
serializationName = String
syntaxIRIString
            }
          Maybe (Key Serialization) -> DBMonad m (Maybe (Key Serialization))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Key Serialization)
 -> DBMonad m (Maybe (Key Serialization)))
-> Maybe (Key Serialization)
-> DBMonad m (Maybe (Key Serialization))
forall a b. (a -> b) -> a -> b
$ Key Serialization -> Maybe (Key Serialization)
forall a. a -> Maybe a
Just Key Serialization
serializationKey

findLanguage :: ( MonadIO m
                , Fail.MonadFail m
                , Logic.Logic lid sublogics
                    basic_spec sentence symb_items symb_map_items
                    sign morphism symbol raw_symbol proof_tree
                )
             => lid -> DBMonad m LanguageId
findLanguage :: lid -> DBMonad m (Key Language)
findLanguage lid :: lid
lid = 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 (ShowS
parameterize ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ lid -> String
forall a. Show a => a -> String
show lid
lid))
    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
    Entity key :: Key Language
key _ : _ -> Key Language -> DBMonad m (Key Language)
forall (m :: * -> *) a. Monad m => a -> m a
return Key Language
key
    [] -> String -> DBMonad m (Key Language)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Language not found in the database: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> String
forall a. Show a => a -> String
show lid
lid)

findOrCreateLogic' :: ( MonadIO m
                      , Fail.MonadFail m
                      , Logic.Logic lid sublogics
                          basic_spec sentence symb_items symb_map_items
                          sign morphism symbol raw_symbol proof_tree
                      )
                   => HetcatsOpts -> lid -> sublogics -> DBMonad m LogicId
findOrCreateLogic' :: HetcatsOpts -> lid -> sublogics -> DBMonad m (Key Logic)
findOrCreateLogic' opts :: HetcatsOpts
opts lid :: lid
lid sublogic :: sublogics
sublogic = do
  Key Language
languageKey <- lid -> DBMonad m (Key Language)
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
lid -> DBMonad m (Key Language)
findLanguage lid
lid
  HetcatsOpts
-> Key Language -> lid -> sublogics -> DBMonad m (Key Logic)
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
-> Key Language -> lid -> sublogics -> DBMonad m (Key Logic)
findOrCreateLogic HetcatsOpts
opts Key Language
languageKey lid
lid sublogics
sublogic

findOrCreateSignature :: ( MonadIO m
                         , Sentences lid sentence sign morphism symbol
                         )
                      => DBCache -> LibName -> lid -> ExtSign sign symbol
                      -> SigId -> LanguageId
                      -> DBMonad m (SignatureId, Bool, DBCache)
findOrCreateSignature :: DBCache
-> LibName
-> lid
-> ExtSign sign symbol
-> SigId
-> Key Language
-> DBMonad m (SignatureId, Bool, DBCache)
findOrCreateSignature dbCache :: DBCache
dbCache libName :: LibName
libName lid :: lid
lid extSign :: ExtSign sign symbol
extSign sigId :: SigId
sigId languageKey :: Key Language
languageKey =
  case (LibName, SigId)
-> Map (LibName, SigId) SignatureId -> Maybe SignatureId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LibName
libName, SigId
sigId) (Map (LibName, SigId) SignatureId -> Maybe SignatureId)
-> Map (LibName, SigId) SignatureId -> Maybe SignatureId
forall a b. (a -> b) -> a -> b
$ DBCache -> Map (LibName, SigId) SignatureId
signatureMap DBCache
dbCache of
    Just signatureKey :: SignatureId
signatureKey -> (SignatureId, Bool, DBCache)
-> DBMonad m (SignatureId, Bool, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (SignatureId
signatureKey, Bool
False, DBCache
dbCache)
    Nothing -> do
      SignatureId
signatureKey <- Signature -> ReaderT SqlBackend m SignatureId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WSignature :: Key Language -> String -> Signature
Signature
        { signatureLanguageId :: Key Language
signatureLanguageId = Key Language
languageKey
        , signatureAsJson :: String
signatureAsJson = Json -> String
ppJson (Json -> String) -> Json -> String
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> Json
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> ExtSign sign symbol -> Json
ToJson.symbols lid
lid ExtSign sign symbol
extSign
        }
      (SignatureId, Bool, DBCache)
-> DBMonad m (SignatureId, Bool, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return ( SignatureId
signatureKey
             , Bool
True
             , LibName -> SigId -> SignatureId -> DBCache -> DBCache
addSignatureToCache LibName
libName SigId
sigId SignatureId
signatureKey DBCache
dbCache
             )

createSymbols :: ( MonadIO m
                 , Fail.MonadFail m
                 , Logic.Logic lid sublogics
                     basic_spec sentence symb_items symb_map_items
                     sign morphism symbol raw_symbol proof_tree
                 )
              => LibEnv -> FileVersionId -> DBCache -> Bool -> LibName -> Int
              -> Entity LocIdBase -> lid -> ExtSign sign symbol
              -> DBMonad m DBCache
createSymbols :: LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> ExtSign sign symbol
-> DBMonad m DBCache
createSymbols libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache :: DBCache
dbCache doSave :: Bool
doSave libName :: LibName
libName nodeId :: Node
nodeId omsLocIdBase :: Entity LocIdBase
omsLocIdBase
  lid :: lid
lid ExtSign { plainSign :: forall sign symbol. ExtSign sign symbol -> sign
plainSign = sign
sign } =
  (DBCache -> symbol -> DBMonad m DBCache)
-> DBCache -> [symbol] -> DBMonad m DBCache
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dbCacheAcc :: DBCache
dbCacheAcc symbol :: symbol
symbol ->
          LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> symbol
-> DBMonad m DBCache
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> symbol
-> DBMonad m DBCache
findOrCreateSymbol LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCacheAcc Bool
doSave LibName
libName
            Node
nodeId Entity LocIdBase
omsLocIdBase lid
lid symbol
symbol
        ) DBCache
dbCache ([symbol] -> DBMonad m DBCache) -> [symbol] -> DBMonad m DBCache
forall a b. (a -> b) -> a -> b
$ lid -> sign -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [symbol]
symlist_of lid
lid sign
sign

findOrCreateSymbol :: ( MonadIO m
                      , Fail.MonadFail m
                      , Logic.Logic lid sublogics
                          basic_spec sentence symb_items symb_map_items
                          sign morphism symbol raw_symbol proof_tree
                      )
                   => LibEnv -> FileVersionId -> DBCache -> Bool -> LibName
                   -> Int -> Entity LocIdBase -> lid -> symbol
                   -> DBMonad m DBCache
findOrCreateSymbol :: LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> symbol
-> DBMonad m DBCache
findOrCreateSymbol libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache :: DBCache
dbCache doSave :: Bool
doSave libName :: LibName
libName nodeId :: Node
nodeId
  omsLocIdBase :: Entity LocIdBase
omsLocIdBase@(Entity omsKey :: LocIdBaseId
omsKey _) lid :: lid
lid symbol :: symbol
symbol =
    let (locId :: String
locId, name :: String
name, fullName :: String
fullName, symbolKind :: String
symbolKind) =
          Entity LocIdBase
-> lid -> symbol -> (String, String, String, 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 =>
Entity LocIdBase
-> lid -> symbol -> (String, String, String, String)
symbolDetails Entity LocIdBase
omsLocIdBase lid
lid symbol
symbol
    in  if LibEnv -> LibName -> Node -> lid -> symbol -> DBCache -> Bool
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
LibEnv -> LibName -> Node -> lid -> symbol -> DBCache -> Bool
symbolIsCached LibEnv
libEnv LibName
libName Node
nodeId lid
lid symbol
symbol DBCache
dbCache
        then DBCache -> DBMonad m DBCache
forall (m :: * -> *) a. Monad m => a -> m a
return DBCache
dbCache
        else do
          LocIdBaseId
symbolKey <-
            if Bool
doSave
            then do
              LocIdBaseId
symbolKey <- LocIdBase -> ReaderT SqlBackend m LocIdBaseId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WLocIdBase :: FileVersionId -> LocIdBaseKindType -> String -> LocIdBase
LocIdBase
                { locIdBaseFileVersionId :: FileVersionId
locIdBaseFileVersionId = FileVersionId
fileVersionKey
                , locIdBaseKind :: LocIdBaseKindType
locIdBaseKind = LocIdBaseKindType
Enums.Symbol
                , locIdBaseLocId :: String
locIdBaseLocId = String
locId
                }
              let symbolValue :: Symbol
symbolValue = $WSymbol :: LocIdBaseId
-> Maybe FileRangeId -> String -> String -> Text -> Symbol
Symbol
                    { symbolOmsId :: LocIdBaseId
symbolOmsId = LocIdBaseId
omsKey
                    , symbolFileRangeId :: Maybe FileRangeId
symbolFileRangeId = Maybe FileRangeId
forall a. Maybe a
Nothing
                    , symbolSymbolKind :: String
symbolSymbolKind = String
symbolKind
                    , symbolName :: String
symbolName = String
name
                    , symbolFullName :: Text
symbolFullName = String -> Text
Text.pack String
fullName
                    }
              [Entity Symbol] -> ReaderT SqlBackend m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany [Key Symbol -> Symbol -> Entity Symbol
forall record. Key record -> record -> Entity record
Entity (Int64 -> Key Symbol
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key Symbol) -> Int64 -> Key Symbol
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
symbolKey) Symbol
symbolValue]
              LocIdBaseId -> ReaderT SqlBackend m LocIdBaseId
forall (m :: * -> *) a. Monad m => a -> m a
return LocIdBaseId
symbolKey
            else do
              [Entity LocIdBase]
symbolL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LocIdBase)
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LocIdBase)
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (SqlExpr (Entity LocIdBase)
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ \loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases -> do
                SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase String
forall typ. (typ ~ String) => EntityField LocIdBase typ
LocIdBaseLocId 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
locId
                          SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase FileVersionId
-> SqlExpr (Value FileVersionId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase FileVersionId
forall typ. (typ ~ FileVersionId) => EntityField LocIdBase typ
LocIdBaseFileVersionId SqlExpr (Value FileVersionId)
-> SqlExpr (Value FileVersionId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. FileVersionId -> SqlExpr (Value FileVersionId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val FileVersionId
fileVersionKey
                          SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseKindType
-> SqlExpr (Value LocIdBaseKindType)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseKindType
forall typ. (typ ~ LocIdBaseKindType) => EntityField LocIdBase typ
LocIdBaseKind SqlExpr (Value LocIdBaseKindType)
-> SqlExpr (Value LocIdBaseKindType) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseKindType -> SqlExpr (Value LocIdBaseKindType)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseKindType
Enums.Symbol)
                SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
              case [Entity LocIdBase]
symbolL of
                [] -> String -> ReaderT SqlBackend m LocIdBaseId
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.DevGraph.findOrCreateSymbol: "
                                 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "Symbol not found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
locId)
                Entity symbolKey :: LocIdBaseId
symbolKey _ : _ -> LocIdBaseId -> ReaderT SqlBackend m LocIdBaseId
forall (m :: * -> *) a. Monad m => a -> m a
return LocIdBaseId
symbolKey
          DBCache -> DBMonad m DBCache
forall (m :: * -> *) a. Monad m => a -> m a
return (DBCache -> DBMonad m DBCache) -> DBCache -> DBMonad m DBCache
forall a b. (a -> b) -> a -> b
$ LibEnv
-> LibName
-> Node
-> lid
-> symbol
-> LocIdBaseId
-> DBCache
-> DBCache
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
LibEnv
-> LibName
-> Node
-> lid
-> symbol
-> LocIdBaseId
-> DBCache
-> DBCache
addSymbolToCache LibEnv
libEnv LibName
libName Node
nodeId lid
lid symbol
symbol LocIdBaseId
symbolKey DBCache
dbCache

createSentences :: ( MonadIO m
                   , Fail.MonadFail m
                   , GetRange sentence
                   , Pretty sentence
                   , Logic.Logic lid sublogics basic_spec sentence symb_items
                       symb_map_items sign morphism symbol
                       raw_symbol proof_tree
                   )
                => LibEnv -> FileVersionId -> DBCache -> Bool -> GlobalAnnos
                -> LibName -> Int -> Entity LocIdBase -> lid -> sign
                -> ThSens sentence (AnyComorphism, BasicProof)
                -> DBMonad m DBCache
createSentences :: LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> sign
-> ThSens sentence (AnyComorphism, BasicProof)
-> DBMonad m DBCache
createSentences libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache0 :: DBCache
dbCache0 doSave :: Bool
doSave globalAnnotations :: GlobalAnnos
globalAnnotations libName :: LibName
libName
  nodeId :: Node
nodeId omsLocId :: Entity LocIdBase
omsLocId lid :: lid
lid sign :: sign
sign sentences :: ThSens sentence (AnyComorphism, BasicProof)
sentences =
  let (axioms :: ThSens sentence (AnyComorphism, BasicProof)
axioms, conjectures :: ThSens sentence (AnyComorphism, BasicProof)
conjectures) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> (ThSens sentence (AnyComorphism, BasicProof),
    ThSens sentence (AnyComorphism, BasicProof))
forall k a.
Ord k =>
(a -> Bool) -> OMap k a -> (OMap k a, OMap k a)
OMap.partition SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (AnyComorphism, BasicProof)
sentences
      namedAxioms :: [Named sentence]
namedAxioms = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
axioms
      orderedConjectures :: [(String,
  SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
orderedConjectures = ThSens sentence (AnyComorphism, BasicProof)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList ThSens sentence (AnyComorphism, BasicProof)
conjectures
  in do
    DBCache
dbCache1 <- LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> sign
-> [Named sentence]
-> DBMonad m DBCache
forall (m :: * -> *) (t :: * -> *) lid sublogics basic_spec
       sentence symb_items symb_map_items sign morphism symbol raw_symbol
       proof_tree.
(MonadIO m, MonadFail m, Foldable t,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> sign
-> t (Named sentence)
-> DBMonad m DBCache
createAxioms LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache0 Bool
doSave
      GlobalAnnos
globalAnnotations LibName
libName Node
nodeId Entity LocIdBase
omsLocId lid
lid sign
sign [Named sentence]
namedAxioms
    LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> sign
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> DBMonad m DBCache
forall (m :: * -> *) (t :: * -> *) lid sublogics basic_spec
       sentence symb_items symb_map_items sign morphism symbol raw_symbol
       proof_tree.
(MonadIO m, MonadFail m, Foldable t,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> sign
-> t (String, SenStatus sentence (AnyComorphism, BasicProof))
-> DBMonad m DBCache
createConjectures LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache1 Bool
doSave
      GlobalAnnos
globalAnnotations LibName
libName Node
nodeId Entity LocIdBase
omsLocId lid
lid sign
sign [(String,
  SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
orderedConjectures

createAxioms :: ( MonadIO m
                , Fail.MonadFail m
                , Foldable t
                , Logic.Logic lid sublogics basic_spec sentence symb_items
                    symb_map_items sign morphism symbol
                    raw_symbol proof_tree
                )
             => LibEnv -> FileVersionId -> DBCache -> Bool -> GlobalAnnos
             -> LibName -> Int -> Entity LocIdBase -> lid -> sign
             -> t (Named sentence)
             -> DBMonad m DBCache
createAxioms :: LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> sign
-> t (Named sentence)
-> DBMonad m DBCache
createAxioms libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache :: DBCache
dbCache doSave :: Bool
doSave globalAnnotations :: GlobalAnnos
globalAnnotations libName :: LibName
libName
  nodeId :: Node
nodeId omsLocId :: Entity LocIdBase
omsLocId lid :: lid
lid sign :: sign
sign =
  (DBCache -> Named sentence -> DBMonad m DBCache)
-> DBCache -> t (Named sentence) -> DBMonad m DBCache
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dbCacheAcc :: DBCache
dbCacheAcc namedAxiom :: Named sentence
namedAxiom -> do
          (axiomKey :: LocIdBaseId
axiomKey, dbCacheAcc1 :: DBCache
dbCacheAcc1) <-
            LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> Entity LocIdBase
-> lid
-> sign
-> Bool
-> Bool
-> Named sentence
-> DBMonad m (LocIdBaseId, DBCache)
forall (m :: * -> *) sentence lid sublogics basic_spec symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m, GetRange sentence, Pretty sentence,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> Entity LocIdBase
-> lid
-> sign
-> Bool
-> Bool
-> Named sentence
-> DBMonad m (LocIdBaseId, DBCache)
createSentence LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCacheAcc Bool
doSave GlobalAnnos
globalAnnotations
              Entity LocIdBase
omsLocId lid
lid sign
sign Bool
False Bool
False Named sentence
namedAxiom
          LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> LocIdBaseId
-> lid
-> sign
-> Named sentence
-> DBMonad m DBCache
forall (m :: * -> *) sentence lid sublogics basic_spec symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m, GetRange sentence, Pretty sentence,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> LocIdBaseId
-> lid
-> sign
-> Named sentence
-> DBMonad m DBCache
associateSymbolsOfSentence LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCacheAcc1 Bool
doSave
            LibName
libName Node
nodeId Entity LocIdBase
omsLocId LocIdBaseId
axiomKey lid
lid sign
sign Named sentence
namedAxiom
        ) DBCache
dbCache

createConjectures :: ( MonadIO m
                     , Fail.MonadFail m
                     , Foldable t
                     , Logic.Logic lid sublogics basic_spec sentence symb_items
                         symb_map_items sign morphism symbol
                         raw_symbol proof_tree
                     )
                  => LibEnv -> FileVersionId -> DBCache -> Bool -> GlobalAnnos
                  -> LibName -> Int -> Entity LocIdBase -> lid -> sign
                  -> t (String, SenStatus sentence (AnyComorphism, BasicProof))
                  -> DBMonad m DBCache
createConjectures :: LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> sign
-> t (String, SenStatus sentence (AnyComorphism, BasicProof))
-> DBMonad m DBCache
createConjectures libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache :: DBCache
dbCache doSave :: Bool
doSave globalAnnotations :: GlobalAnnos
globalAnnotations libName :: LibName
libName
  nodeId :: Node
nodeId omsLocId :: Entity LocIdBase
omsLocId lid :: lid
lid sign :: sign
sign =
  (DBCache
 -> (String, SenStatus sentence (AnyComorphism, BasicProof))
 -> DBMonad m DBCache)
-> DBCache
-> t (String, SenStatus sentence (AnyComorphism, BasicProof))
-> DBMonad m DBCache
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dbCacheAcc :: DBCache
dbCacheAcc (name :: String
name, senStatus :: SenStatus sentence (AnyComorphism, BasicProof)
senStatus) ->
          let namedConjecture :: Named sentence
namedConjecture = String
-> SenStatus sentence (AnyComorphism, BasicProof) -> Named sentence
forall a b. String -> SenStatus a b -> Named a
toNamed String
name SenStatus sentence (AnyComorphism, BasicProof)
senStatus
              isProved :: Bool
isProved = SenStatus sentence (AnyComorphism, BasicProof) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenStatus sentence (AnyComorphism, BasicProof)
senStatus
          in do
            (conjectureKey :: LocIdBaseId
conjectureKey, dbCacheAcc1 :: DBCache
dbCacheAcc1) <-
              LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> Entity LocIdBase
-> lid
-> sign
-> Bool
-> Bool
-> Named sentence
-> DBMonad m (LocIdBaseId, DBCache)
forall (m :: * -> *) sentence lid sublogics basic_spec symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m, GetRange sentence, Pretty sentence,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> Entity LocIdBase
-> lid
-> sign
-> Bool
-> Bool
-> Named sentence
-> DBMonad m (LocIdBaseId, DBCache)
createSentence LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCacheAcc Bool
doSave GlobalAnnos
globalAnnotations
                Entity LocIdBase
omsLocId lid
lid sign
sign Bool
True Bool
isProved Named sentence
namedConjecture
            LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> LocIdBaseId
-> lid
-> sign
-> Named sentence
-> DBMonad m DBCache
forall (m :: * -> *) sentence lid sublogics basic_spec symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m, GetRange sentence, Pretty sentence,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> LocIdBaseId
-> lid
-> sign
-> Named sentence
-> DBMonad m DBCache
associateSymbolsOfSentence LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCacheAcc1 Bool
doSave
              LibName
libName Node
nodeId Entity LocIdBase
omsLocId LocIdBaseId
conjectureKey lid
lid sign
sign Named sentence
namedConjecture
        ) DBCache
dbCache

createSentence :: ( MonadIO m
                  , Fail.MonadFail m
                  , GetRange sentence
                  , Pretty sentence
                  , Logic.Logic lid sublogics basic_spec sentence symb_items
                      symb_map_items sign morphism symbol
                      raw_symbol proof_tree
                  )
               => LibEnv -> FileVersionId -> DBCache -> Bool -> GlobalAnnos
               -> Entity LocIdBase -> lid -> sign -> Bool -> Bool
               -> Named sentence -> DBMonad m (LocIdBaseId, DBCache)
createSentence :: LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> Entity LocIdBase
-> lid
-> sign
-> Bool
-> Bool
-> Named sentence
-> DBMonad m (LocIdBaseId, DBCache)
createSentence libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache :: DBCache
dbCache doSave :: Bool
doSave globalAnnotations :: GlobalAnnos
globalAnnotations
  omsLocIdBase :: Entity LocIdBase
omsLocIdBase@(Entity omsKey :: LocIdBaseId
omsKey _) lid :: lid
lid sign :: sign
sign isConjecture :: Bool
isConjecture isProved :: Bool
isProved namedSentence :: Named sentence
namedSentence =
  let name :: String
name = Named sentence -> String
forall s a. SenAttr s a -> a
senAttr Named sentence
namedSentence
      range :: Range
range = sentence -> Range
forall a. GetRange a => a -> Range
getRangeSpan (sentence -> Range) -> sentence -> Range
forall a b. (a -> b) -> a -> b
$ Named sentence -> sentence
forall s a. SenAttr s a -> s
sentence Named sentence
namedSentence
      locId :: String
locId = Entity LocIdBase -> ShowS
locIdOfSentence Entity LocIdBase
omsLocIdBase String
name
      text :: String
text = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Doc -> Doc
useGlobalAnnos GlobalAnnos
globalAnnotations (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
               lid -> Named sentence -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named lid
lid (Named sentence -> Doc) -> Named sentence -> Doc
forall a b. (a -> b) -> a -> b
$ String -> sentence -> Named sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (sentence -> Named sentence) -> sentence -> Named sentence
forall a b. (a -> b) -> a -> b
$
               lid -> sign -> sentence -> sentence
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> sentence
simplify_sen lid
lid sign
sign (sentence -> sentence) -> sentence -> sentence
forall a b. (a -> b) -> a -> b
$ Named sentence -> sentence
forall s a. SenAttr s a -> s
sentence Named sentence
namedSentence
      kind :: LocIdBaseKindType
kind =
        if Bool
isConjecture
        then if Bool
isProved
             then LocIdBaseKindType
Enums.Theorem
             else LocIdBaseKindType
Enums.OpenConjecture
        else LocIdBaseKindType
Enums.Axiom
      evaluationState :: EvaluationStateType
evaluationState =
        if Bool
isProved
        then EvaluationStateType
EvaluationStateType.FinishedSuccessfully
        else EvaluationStateType
EvaluationStateType.NotYetEnqueued
      proofStatus :: ProofStatusType
proofStatus =
        if Bool
isProved
        then ProofStatusType
Enums.THM
        else ProofStatusType
Enums.OPN
  in  do
        LocIdBaseId
sentenceKey <-
          if Bool
doSave
          then do
               Maybe LocIdBaseId
originalSentenceKeyM <-
                 LibEnv
-> FileVersionId
-> DBCache
-> lid
-> Named sentence
-> DBMonad m (Maybe LocIdBaseId)
forall (m :: * -> *) sentence lid sublogics basic_spec symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m, GetRange sentence, Pretty sentence,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> lid
-> Named sentence
-> DBMonad m (Maybe LocIdBaseId)
findOriginalSentence LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache lid
lid Named sentence
namedSentence
               Maybe FileRangeId
rangeKeyM <- Range -> DBMonad m (Maybe FileRangeId)
forall (m :: * -> *).
MonadIO m =>
Range -> DBMonad m (Maybe FileRangeId)
createRange Range
range
               LocIdBaseId
sentenceKey <- LocIdBase -> ReaderT SqlBackend m LocIdBaseId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WLocIdBase :: FileVersionId -> LocIdBaseKindType -> String -> LocIdBase
LocIdBase
                 { locIdBaseFileVersionId :: FileVersionId
locIdBaseFileVersionId = FileVersionId
fileVersionKey
                 , locIdBaseKind :: LocIdBaseKindType
locIdBaseKind = LocIdBaseKindType
kind
                 , locIdBaseLocId :: String
locIdBaseLocId = String
locId
                 }
               let sentenceValue :: Sentence
sentenceValue = $WSentence :: LocIdBaseId
-> Maybe FileRangeId
-> String
-> Text
-> Maybe LocIdBaseId
-> Sentence
Sentence
                     { sentenceOmsId :: LocIdBaseId
sentenceOmsId = LocIdBaseId
omsKey
                     , sentenceFileRangeId :: Maybe FileRangeId
sentenceFileRangeId = Maybe FileRangeId
rangeKeyM
                     , sentenceName :: String
sentenceName = String
name
                     , sentenceText :: Text
sentenceText = String -> Text
Text.pack String
text
                     , sentenceOriginalSentenceId :: Maybe LocIdBaseId
sentenceOriginalSentenceId = Maybe LocIdBaseId
originalSentenceKeyM
                     }
               [Entity Sentence] -> ReaderT SqlBackend m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany [Key Sentence -> Sentence -> Entity Sentence
forall record. Key record -> record -> Entity record
Entity (Int64 -> Key Sentence
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key Sentence) -> Int64 -> Key Sentence
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
sentenceKey) Sentence
sentenceValue]
               if Bool
isConjecture
               then do
                      Key Action
actionKey <- Action -> ReaderT SqlBackend m (Key Action)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WAction :: EvaluationStateType -> Maybe Text -> Action
Action
                        { actionEvaluationState :: EvaluationStateType
actionEvaluationState = EvaluationStateType
evaluationState
                        , actionMessage :: Maybe Text
actionMessage = Maybe Text
forall a. Maybe a
Nothing
                        }
                      let conjecture :: Conjecture
conjecture = $WConjecture :: Key Action -> ProofStatusType -> Conjecture
Conjecture
                            { conjectureActionId :: Key Action
conjectureActionId = Key Action
actionKey
                            , conjectureProofStatus :: ProofStatusType
conjectureProofStatus = ProofStatusType
proofStatus
                            }
                      [Entity Conjecture] -> ReaderT SqlBackend m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany [Key Conjecture -> Conjecture -> Entity Conjecture
forall record. Key record -> record -> Entity record
Entity (Int64 -> Key Conjecture
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key Conjecture) -> Int64 -> Key Conjecture
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
sentenceKey) Conjecture
conjecture]
               else let axiom :: Axiom
axiom = Axiom :: Axiom
Axiom { }
                    in [Entity Axiom] -> ReaderT SqlBackend m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany [Key Axiom -> Axiom -> Entity Axiom
forall record. Key record -> record -> Entity record
Entity (Int64 -> Key Axiom
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key Axiom) -> Int64 -> Key Axiom
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
sentenceKey) Axiom
axiom]
               LocIdBaseId -> ReaderT SqlBackend m LocIdBaseId
forall (m :: * -> *) a. Monad m => a -> m a
return LocIdBaseId
sentenceKey
            else do
              [Entity LocIdBase]
sentenceL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LocIdBase)
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LocIdBase)
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (SqlExpr (Entity LocIdBase)
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ \loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases -> do
                SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase String
forall typ. (typ ~ String) => EntityField LocIdBase typ
LocIdBaseLocId 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
locId
                          SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase FileVersionId
-> SqlExpr (Value FileVersionId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase FileVersionId
forall typ. (typ ~ FileVersionId) => EntityField LocIdBase typ
LocIdBaseFileVersionId SqlExpr (Value FileVersionId)
-> SqlExpr (Value FileVersionId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. FileVersionId -> SqlExpr (Value FileVersionId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val FileVersionId
fileVersionKey
                          SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseKindType
-> SqlExpr (Value LocIdBaseKindType)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseKindType
forall typ. (typ ~ LocIdBaseKindType) => EntityField LocIdBase typ
LocIdBaseKind SqlExpr (Value LocIdBaseKindType)
-> SqlExpr (Value LocIdBaseKindType) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseKindType -> SqlExpr (Value LocIdBaseKindType)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseKindType
kind)
                SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
              case [Entity LocIdBase]
sentenceL of
                [] -> String -> ReaderT SqlBackend m LocIdBaseId
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.DevGraph.createSentence: Sentence not found"
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
locId)
                Entity sentenceKey :: LocIdBaseId
sentenceKey _ : _-> LocIdBaseId -> ReaderT SqlBackend m LocIdBaseId
forall (m :: * -> *) a. Monad m => a -> m a
return LocIdBaseId
sentenceKey
        (LocIdBaseId, DBCache) -> DBMonad m (LocIdBaseId, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (LocIdBaseId
sentenceKey, DBCache
dbCache)

findOriginalSentence :: ( MonadIO m
                        , Fail.MonadFail m
                        , GetRange sentence
                        , Pretty sentence
                        , Logic.Logic lid sublogics basic_spec sentence symb_items
                            symb_map_items sign morphism symbol
                            raw_symbol proof_tree
                        )
                     => LibEnv -> FileVersionId -> DBCache -> lid -> Named sentence
                     -> DBMonad m (Maybe LocIdBaseId)
findOriginalSentence :: LibEnv
-> FileVersionId
-> DBCache
-> lid
-> Named sentence
-> DBMonad m (Maybe LocIdBaseId)
findOriginalSentence libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache :: DBCache
dbCache _ namedSentence :: Named sentence
namedSentence =
  case Named sentence -> Maybe SenOrigin
forall s a. SenAttr s a -> Maybe SenOrigin
senOrigin Named sentence
namedSentence of
    Nothing -> Maybe LocIdBaseId -> DBMonad m (Maybe LocIdBaseId)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LocIdBaseId
forall a. Maybe a
Nothing
    Just origin :: SenOrigin
origin -> do
      let originLibNameIRI :: IRI
originLibNameIRI = SenOrigin -> IRI
dGraphName SenOrigin
origin
      let originNodeId_ :: Node
originNodeId_ = SenOrigin -> Node
originNodeId SenOrigin
origin
      let originSentenceName :: String
originSentenceName = SenOrigin -> String
senName SenOrigin
origin

      let filterPredicate :: LibName -> DGraph -> Bool
filterPredicate libName :: LibName
libName _ = IRI
originLibNameIRI IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== LibName -> IRI
iriOfLibName LibName
libName
      DGraph
originDGraph <- case LibEnv -> [(LibName, DGraph)]
forall k a. Map k a -> [(k, a)]
Map.toList (LibEnv -> [(LibName, DGraph)]) -> LibEnv -> [(LibName, DGraph)]
forall a b. (a -> b) -> a -> b
$ (LibName -> DGraph -> Bool) -> LibEnv -> LibEnv
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey LibName -> DGraph -> Bool
filterPredicate LibEnv
libEnv of
        [] -> String -> ReaderT SqlBackend m DGraph
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.DevGraph.findOriginalSentence: Could not find dGraph named " String -> ShowS
forall a. [a] -> [a] -> [a]
++ IRI -> String
forall a. Show a => a -> String
show IRI
originLibNameIRI)
        (_, dg :: DGraph
dg) : _ -> DGraph -> ReaderT SqlBackend m DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg
      let nodeLabel :: DGNodeLab
nodeLabel = GrContext DGNodeLab DGLinkLab -> DGNodeLab
forall a b. GrContext a b -> a
Graph.nodeLabel (GrContext DGNodeLab DGLinkLab -> DGNodeLab)
-> GrContext DGNodeLab DGLinkLab -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ Maybe (GrContext DGNodeLab DGLinkLab)
-> GrContext DGNodeLab DGLinkLab
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (GrContext DGNodeLab DGLinkLab)
 -> GrContext DGNodeLab DGLinkLab)
-> Maybe (GrContext DGNodeLab DGLinkLab)
-> GrContext DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ Node
-> IntMap (GrContext DGNodeLab DGLinkLab)
-> Maybe (GrContext DGNodeLab DGLinkLab)
forall a. Node -> IntMap a -> Maybe a
IntMap.lookup Node
originNodeId_ (IntMap (GrContext DGNodeLab DGLinkLab)
 -> Maybe (GrContext DGNodeLab DGLinkLab))
-> IntMap (GrContext DGNodeLab DGLinkLab)
-> Maybe (GrContext DGNodeLab DGLinkLab)
forall a b. (a -> b) -> a -> b
$ Gr DGNodeLab DGLinkLab -> IntMap (GrContext DGNodeLab DGLinkLab)
forall a b. Gr a b -> IntMap (GrContext a b)
convertToMap (Gr DGNodeLab DGLinkLab -> IntMap (GrContext DGNodeLab DGLinkLab))
-> Gr DGNodeLab DGLinkLab -> IntMap (GrContext DGNodeLab DGLinkLab)
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
originDGraph

      let documentKey :: LocIdBaseId
documentKey = Maybe LocIdBaseId -> LocIdBaseId
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe LocIdBaseId -> LocIdBaseId)
-> Maybe LocIdBaseId -> LocIdBaseId
forall a b. (a -> b) -> a -> b
$ IRI -> Map IRI LocIdBaseId -> Maybe LocIdBaseId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IRI
originLibNameIRI (Map IRI LocIdBaseId -> Maybe LocIdBaseId)
-> Map IRI LocIdBaseId -> Maybe LocIdBaseId
forall a b. (a -> b) -> a -> b
$ DBCache -> Map IRI LocIdBaseId
documentByLibNameIRIMap DBCache
dbCache
      LocIdBase
documentLocIdBase <- (Maybe LocIdBase -> LocIdBase)
-> ReaderT SqlBackend m (Maybe LocIdBase)
-> ReaderT SqlBackend m LocIdBase
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe LocIdBase -> LocIdBase
forall a. HasCallStack => Maybe a -> a
fromJust (ReaderT SqlBackend m (Maybe LocIdBase)
 -> ReaderT SqlBackend m LocIdBase)
-> ReaderT SqlBackend m (Maybe LocIdBase)
-> ReaderT SqlBackend m LocIdBase
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> ReaderT SqlBackend m (Maybe LocIdBase)
forall backend (m :: * -> *) record.
(PersistStoreRead backend, MonadIO m,
 PersistRecordBackend record backend) =>
Key record -> ReaderT backend m (Maybe record)
get LocIdBaseId
documentKey
      let documentEntity :: Entity LocIdBase
documentEntity = LocIdBaseId -> LocIdBase -> Entity LocIdBase
forall record. Key record -> record -> Entity record
Entity LocIdBaseId
documentKey LocIdBase
documentLocIdBase
      let omsLocId :: String
omsLocId = Entity LocIdBase -> DGNodeLab -> String
locIdOfOMS Entity LocIdBase
documentEntity DGNodeLab
nodeLabel
      Maybe (Entity LocIdBase)
omsLocIdBaseM <- FileVersionId
-> Entity LocIdBase
-> DGNodeLab
-> DBMonad m (Maybe (Entity LocIdBase))
forall (m :: * -> *).
MonadIO m =>
FileVersionId
-> Entity LocIdBase
-> DGNodeLab
-> DBMonad m (Maybe (Entity LocIdBase))
findOMS FileVersionId
fileVersionKey Entity LocIdBase
documentEntity DGNodeLab
nodeLabel
      Entity LocIdBase
omsLocIdBase <- case Maybe (Entity LocIdBase)
omsLocIdBaseM of
        Nothing -> String -> ReaderT SqlBackend m (Entity LocIdBase)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.DevGraph.findOriginalSentence: Could not find OMS " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
omsLocId)
        Just x :: Entity LocIdBase
x -> Entity LocIdBase -> ReaderT SqlBackend m (Entity LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity LocIdBase
x
      let locIdOfOriginalSentence :: String
locIdOfOriginalSentence = Entity LocIdBase -> ShowS
locIdOfSentence Entity LocIdBase
omsLocIdBase String
originSentenceName
      Maybe (Entity LocIdBase)
sentenceM <- FileVersionId -> String -> DBMonad m (Maybe (Entity LocIdBase))
forall (m :: * -> *).
MonadIO m =>
FileVersionId -> String -> DBMonad m (Maybe (Entity LocIdBase))
findSentence FileVersionId
fileVersionKey String
locIdOfOriginalSentence
      (Entity sentenceKey :: LocIdBaseId
sentenceKey _) <- case Maybe (Entity LocIdBase)
sentenceM of
        Nothing -> String -> ReaderT SqlBackend m (Entity LocIdBase)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.DevGraph.findOriginalSentence: Could not find Sentence " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
locIdOfOriginalSentence)
        Just x :: Entity LocIdBase
x -> Entity LocIdBase -> ReaderT SqlBackend m (Entity LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity LocIdBase
x
      Maybe LocIdBaseId -> DBMonad m (Maybe LocIdBaseId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LocIdBaseId -> DBMonad m (Maybe LocIdBaseId))
-> Maybe LocIdBaseId -> DBMonad m (Maybe LocIdBaseId)
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Maybe LocIdBaseId
forall a. a -> Maybe a
Just LocIdBaseId
sentenceKey

associateSymbolsOfSentence :: ( MonadIO m
                              , Fail.MonadFail m
                              , GetRange sentence
                              , Pretty sentence
                              , Logic.Logic lid sublogics basic_spec sentence
                                  symb_items symb_map_items sign morphism symbol
                                  raw_symbol proof_tree
                              )
                           => LibEnv -> FileVersionId -> DBCache -> Bool
                           -> LibName -> Int -> Entity LocIdBase -> LocIdBaseId
                           -> lid -> sign -> Named sentence
                           -> DBMonad m DBCache
associateSymbolsOfSentence :: LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> LocIdBaseId
-> lid
-> sign
-> Named sentence
-> DBMonad m DBCache
associateSymbolsOfSentence libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache :: DBCache
dbCache doSave :: Bool
doSave libName :: LibName
libName nodeId :: Node
nodeId
  omsLocIdBase :: Entity LocIdBase
omsLocIdBase sentenceKey :: LocIdBaseId
sentenceKey lid :: lid
lid sign :: sign
sign namedSentence :: Named sentence
namedSentence =
  let symbolsOfSentence :: [symbol]
symbolsOfSentence = lid -> sign -> sentence -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> [symbol]
symsOfSen lid
lid sign
sign (sentence -> [symbol]) -> sentence -> [symbol]
forall a b. (a -> b) -> a -> b
$ Named sentence -> sentence
forall s a. SenAttr s a -> s
sentence Named sentence
namedSentence
  in  do
        (dbCache' :: DBCache
dbCache', _) <-
          ((DBCache, Set SymbolMapIndex)
 -> symbol -> ReaderT SqlBackend m (DBCache, Set SymbolMapIndex))
-> (DBCache, Set SymbolMapIndex)
-> [symbol]
-> ReaderT SqlBackend m (DBCache, Set SymbolMapIndex)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (dbCacheAcc :: DBCache
dbCacheAcc, associatedSymbols :: Set SymbolMapIndex
associatedSymbols) symbol :: symbol
symbol ->
                  let mapIndex :: SymbolMapIndex
mapIndex = lid -> symbol -> SymbolMapIndex
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> SymbolMapIndex
symbolMapIndex lid
lid symbol
symbol
                  in  if SymbolMapIndex -> Set SymbolMapIndex -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SymbolMapIndex
mapIndex Set SymbolMapIndex
associatedSymbols
                      then (DBCache, Set SymbolMapIndex)
-> ReaderT SqlBackend m (DBCache, Set SymbolMapIndex)
forall (m :: * -> *) a. Monad m => a -> m a
return (DBCache
dbCacheAcc, Set SymbolMapIndex
associatedSymbols)
                      else case LibEnv
-> LibName -> Node -> lid -> symbol -> DBCache -> Maybe LocIdBaseId
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
LibEnv
-> LibName -> Node -> lid -> symbol -> DBCache -> Maybe LocIdBaseId
findSymbolInCache LibEnv
libEnv LibName
libName Node
nodeId lid
lid symbol
symbol DBCache
dbCacheAcc of
                             Just symbolKey :: LocIdBaseId
symbolKey -> do
                               Bool -> ReaderT SqlBackend m () -> ReaderT SqlBackend m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
doSave (ReaderT SqlBackend m () -> ReaderT SqlBackend m ())
-> ReaderT SqlBackend m () -> ReaderT SqlBackend m ()
forall a b. (a -> b) -> a -> b
$
                                 SentenceSymbol -> ReaderT SqlBackend m (Key SentenceSymbol)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WSentenceSymbol :: LocIdBaseId -> LocIdBaseId -> SentenceSymbol
SentenceSymbol
                                   { sentenceSymbolSentenceId :: LocIdBaseId
sentenceSymbolSentenceId = LocIdBaseId
sentenceKey
                                   , sentenceSymbolSymbolId :: LocIdBaseId
sentenceSymbolSymbolId = LocIdBaseId
symbolKey
                                   } ReaderT SqlBackend m (Key SentenceSymbol)
-> ReaderT SqlBackend m () -> ReaderT SqlBackend m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> ReaderT SqlBackend m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                               (DBCache, Set SymbolMapIndex)
-> ReaderT SqlBackend m (DBCache, Set SymbolMapIndex)
forall (m :: * -> *) a. Monad m => a -> m a
return ( DBCache
dbCacheAcc
                                      , SymbolMapIndex -> Set SymbolMapIndex -> Set SymbolMapIndex
forall a. Ord a => a -> Set a -> Set a
Set.insert SymbolMapIndex
mapIndex Set SymbolMapIndex
associatedSymbols
                                      )
                             Nothing -> do
                               DBCache
dbCacheAcc' <-
                                 LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> symbol
-> DBMonad m DBCache
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> LibName
-> Node
-> Entity LocIdBase
-> lid
-> symbol
-> DBMonad m DBCache
findOrCreateSymbol LibEnv
libEnv FileVersionId
fileVersionKey
                                   DBCache
dbCacheAcc Bool
doSave LibName
libName Node
nodeId Entity LocIdBase
omsLocIdBase
                                   lid
lid symbol
symbol
                               (DBCache, Set SymbolMapIndex)
-> ReaderT SqlBackend m (DBCache, Set SymbolMapIndex)
forall (m :: * -> *) a. Monad m => a -> m a
return ( DBCache
dbCacheAcc'
                                      , SymbolMapIndex -> Set SymbolMapIndex -> Set SymbolMapIndex
forall a. Ord a => a -> Set a -> Set a
Set.insert SymbolMapIndex
mapIndex Set SymbolMapIndex
associatedSymbols
                                      )
                ) (DBCache
dbCache, Set SymbolMapIndex
forall a. Set a
Set.empty) [symbol]
symbolsOfSentence
        DBCache -> DBMonad m DBCache
forall (m :: * -> *) a. Monad m => a -> m a
return DBCache
dbCache'

associateSymbolsOfSignature :: ( MonadIO m
                               , Sentences lid sentence sign morphism symbol
                               )
                            => LibEnv -> DBCache -> LibName -> Int -> lid
                            -> ExtSign sign symbol -> SignatureId
                            -> DBMonad m DBCache
associateSymbolsOfSignature :: LibEnv
-> DBCache
-> LibName
-> Node
-> lid
-> ExtSign sign symbol
-> SignatureId
-> DBMonad m DBCache
associateSymbolsOfSignature libEnv :: LibEnv
libEnv dbCache :: DBCache
dbCache libName :: LibName
libName nodeId :: Node
nodeId lid :: lid
lid extSign :: ExtSign sign symbol
extSign signatureKey :: SignatureId
signatureKey =
  let ownSymbols :: Set symbol
ownSymbols = ExtSign sign symbol -> Set symbol
forall sign symbol. ExtSign sign symbol -> Set symbol
nonImportedSymbols ExtSign sign symbol
extSign
      allSymbols :: Set symbol
allSymbols = lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
lid (sign -> Set symbol) -> sign -> Set symbol
forall a b. (a -> b) -> a -> b
$ ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
extSign
  in do
       (Set SymbolMapIndex
 -> symbol -> ReaderT SqlBackend m (Set SymbolMapIndex))
-> Set SymbolMapIndex -> Set symbol -> ReaderT SqlBackend m ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_
         (\ associatedSymbols :: Set SymbolMapIndex
associatedSymbols symbol :: symbol
symbol ->
           let mapIndex :: SymbolMapIndex
mapIndex = lid -> symbol -> SymbolMapIndex
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> SymbolMapIndex
symbolMapIndex lid
lid symbol
symbol
               symbolKey :: LocIdBaseId
symbolKey =
                 Maybe LocIdBaseId -> LocIdBaseId
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe LocIdBaseId -> LocIdBaseId)
-> Maybe LocIdBaseId -> LocIdBaseId
forall a b. (a -> b) -> a -> b
$ LibEnv
-> LibName -> Node -> lid -> symbol -> DBCache -> Maybe LocIdBaseId
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
LibEnv
-> LibName -> Node -> lid -> symbol -> DBCache -> Maybe LocIdBaseId
findSymbolInCache LibEnv
libEnv LibName
libName Node
nodeId lid
lid symbol
symbol
                   DBCache
dbCache
               imported :: Bool
imported = symbol -> Set symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member symbol
symbol Set symbol
ownSymbols
           in  if SymbolMapIndex -> Set SymbolMapIndex -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SymbolMapIndex
mapIndex Set SymbolMapIndex
associatedSymbols
               then Set SymbolMapIndex -> ReaderT SqlBackend m (Set SymbolMapIndex)
forall (m :: * -> *) a. Monad m => a -> m a
return Set SymbolMapIndex
associatedSymbols
               else do
                 SignatureSymbol -> ReaderT SqlBackend m (Key SignatureSymbol)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WSignatureSymbol :: SignatureId -> LocIdBaseId -> Bool -> SignatureSymbol
SignatureSymbol
                   { signatureSymbolSignatureId :: SignatureId
signatureSymbolSignatureId = SignatureId
signatureKey
                   , signatureSymbolSymbolId :: LocIdBaseId
signatureSymbolSymbolId = LocIdBaseId
symbolKey
                   , signatureSymbolImported :: Bool
signatureSymbolImported = Bool
imported
                   }
                 Set SymbolMapIndex -> ReaderT SqlBackend m (Set SymbolMapIndex)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set SymbolMapIndex -> ReaderT SqlBackend m (Set SymbolMapIndex))
-> Set SymbolMapIndex -> ReaderT SqlBackend m (Set SymbolMapIndex)
forall a b. (a -> b) -> a -> b
$ SymbolMapIndex -> Set SymbolMapIndex -> Set SymbolMapIndex
forall a. Ord a => a -> Set a -> Set a
Set.insert SymbolMapIndex
mapIndex Set SymbolMapIndex
associatedSymbols
         ) Set SymbolMapIndex
forall a. Set a
Set.empty Set symbol
allSymbols
       DBCache -> DBMonad m DBCache
forall (m :: * -> *) a. Monad m => a -> m a
return DBCache
dbCache

createMapping :: (MonadIO m, Fail.MonadFail m)
              => HetcatsOpts -> LibEnv -> FileVersionId -> DBCache -> Bool
              -> GlobalAnnos -> LibName -> Entity LocIdBase
              -> (Int, Int, DGLinkLab) -> DBMonad m DBCache
createMapping :: HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LEdge DGLinkLab
-> DBMonad m DBCache
createMapping opts :: HetcatsOpts
opts libEnv :: LibEnv
libEnv fileVersionKey :: FileVersionId
fileVersionKey dbCache :: DBCache
dbCache doSave :: Bool
doSave globalAnnotations :: GlobalAnnos
globalAnnotations
  libName :: LibName
libName documentLocIdBase :: Entity LocIdBase
documentLocIdBase (sourceId :: Node
sourceId, targetId :: Node
targetId, linkLabel :: DGLinkLab
linkLabel) = do
  (sourceOMSKey :: LocIdBaseId
sourceOMSKey, sourceSignatureKey :: SignatureId
sourceSignatureKey) <-
    case (LibName, Node)
-> Map (LibName, Node) (LocIdBaseId, SignatureId)
-> Maybe (LocIdBaseId, SignatureId)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LibName
libName, Node
sourceId) (Map (LibName, Node) (LocIdBaseId, SignatureId)
 -> Maybe (LocIdBaseId, SignatureId))
-> Map (LibName, Node) (LocIdBaseId, SignatureId)
-> Maybe (LocIdBaseId, SignatureId)
forall a b. (a -> b) -> a -> b
$ DBCache -> Map (LibName, Node) (LocIdBaseId, SignatureId)
nodeMap DBCache
dbCache of
      Just (omsKey :: LocIdBaseId
omsKey, signatureKey :: SignatureId
signatureKey) -> (LocIdBaseId, SignatureId)
-> ReaderT SqlBackend m (LocIdBaseId, SignatureId)
forall (m :: * -> *) a. Monad m => a -> m a
return (LocIdBaseId
omsKey, SignatureId
signatureKey)
      Nothing -> String -> ReaderT SqlBackend m (LocIdBaseId, SignatureId)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.DevGraph.createMapping: Could not find source node with ID " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LibName, Node) -> String
forall a. Show a => a -> String
show (LibName
libName, Node
sourceId))

  (targetOMSKey :: LocIdBaseId
targetOMSKey, targetSignatureKey :: SignatureId
targetSignatureKey) <-
    case (LibName, Node)
-> Map (LibName, Node) (LocIdBaseId, SignatureId)
-> Maybe (LocIdBaseId, SignatureId)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LibName
libName, Node
targetId) (Map (LibName, Node) (LocIdBaseId, SignatureId)
 -> Maybe (LocIdBaseId, SignatureId))
-> Map (LibName, Node) (LocIdBaseId, SignatureId)
-> Maybe (LocIdBaseId, SignatureId)
forall a b. (a -> b) -> a -> b
$ DBCache -> Map (LibName, Node) (LocIdBaseId, SignatureId)
nodeMap DBCache
dbCache of
      Just (omsKey :: LocIdBaseId
omsKey, signatureKey :: SignatureId
signatureKey) -> (LocIdBaseId, SignatureId)
-> ReaderT SqlBackend m (LocIdBaseId, SignatureId)
forall (m :: * -> *) a. Monad m => a -> m a
return (LocIdBaseId
omsKey, SignatureId
signatureKey)
      Nothing -> String -> ReaderT SqlBackend m (LocIdBaseId, SignatureId)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.DevGraph.createMapping: Could not find target node with ID " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LibName, Node) -> String
forall a. Show a => a -> String
show (LibName
libName, Node
targetId))

  (signatureMorphismKey :: SignatureMorphismId
signatureMorphismKey, _, dbCache1 :: DBCache
dbCache1) <-
    HetcatsOpts
-> LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> GlobalAnnos
-> (SignatureId, SignatureId)
-> GMorphism
-> DBMonad m (SignatureMorphismId, [SymbolMappingId], DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> DBCache
-> Bool
-> LibName
-> (Node, Node)
-> GlobalAnnos
-> (SignatureId, SignatureId)
-> GMorphism
-> DBMonad m (SignatureMorphismId, [SymbolMappingId], DBCache)
findOrCreateSignatureMorphism HetcatsOpts
opts LibEnv
libEnv DBCache
dbCache Bool
True LibName
libName
      (Node
sourceId, Node
targetId) GlobalAnnos
globalAnnotations
      (SignatureId
sourceSignatureKey, SignatureId
targetSignatureKey) (GMorphism
 -> DBMonad m (SignatureMorphismId, [SymbolMappingId], DBCache))
-> GMorphism
-> DBMonad m (SignatureMorphismId, [SymbolMappingId], DBCache)
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
linkLabel

  let displayName :: String
displayName = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> String
dglName DGLinkLab
linkLabel
                    then EdgeId -> String
forall a. Show a => a -> String
show (DGLinkLab -> EdgeId
dgl_id DGLinkLab
linkLabel)
                    else DGLinkLab -> String
dglName DGLinkLab
linkLabel
  let locId :: String
locId = Entity LocIdBase -> ShowS
locIdOfMapping Entity LocIdBase
documentLocIdBase String
displayName
  [Entity LocIdBase]
mappingL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LocIdBase)
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LocIdBase)
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (SqlExpr (Entity LocIdBase)
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ \loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase FileVersionId
-> SqlExpr (Value FileVersionId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase FileVersionId
forall typ. (typ ~ FileVersionId) => EntityField LocIdBase typ
LocIdBaseFileVersionId SqlExpr (Value FileVersionId)
-> SqlExpr (Value FileVersionId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. FileVersionId -> SqlExpr (Value FileVersionId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val FileVersionId
fileVersionKey
              SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseKindType
-> SqlExpr (Value LocIdBaseKindType)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseKindType
forall typ. (typ ~ LocIdBaseKindType) => EntityField LocIdBase typ
LocIdBaseKind SqlExpr (Value LocIdBaseKindType)
-> SqlExpr (Value LocIdBaseKindType) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseKindType -> SqlExpr (Value LocIdBaseKindType)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseKindType
Enums.Mapping
              SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase String
forall typ. (typ ~ String) => EntityField LocIdBase typ
LocIdBaseLocId 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
locId)
    SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
  if [Entity LocIdBase] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Entity LocIdBase]
mappingL
  then do
    Maybe ConservativityStatusId
conservativityStatusKeyM <- case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
linkLabel of
      ScopedLink _ _ consStatus :: ConsStatus
consStatus ->
        (ConservativityStatusId -> Maybe ConservativityStatusId)
-> ReaderT SqlBackend m ConservativityStatusId
-> ReaderT SqlBackend m (Maybe ConservativityStatusId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ConservativityStatusId -> Maybe ConservativityStatusId
forall a. a -> Maybe a
Just (ReaderT SqlBackend m ConservativityStatusId
 -> ReaderT SqlBackend m (Maybe ConservativityStatusId))
-> ReaderT SqlBackend m ConservativityStatusId
-> ReaderT SqlBackend m (Maybe ConservativityStatusId)
forall a b. (a -> b) -> a -> b
$ ConsStatus -> ReaderT SqlBackend m ConservativityStatusId
forall (m :: * -> *).
MonadIO m =>
ConsStatus -> DBMonad m ConservativityStatusId
createConservativityStatus ConsStatus
consStatus
      _ -> Maybe ConservativityStatusId
-> ReaderT SqlBackend m (Maybe ConservativityStatusId)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ConservativityStatusId
forall a. Maybe a
Nothing

    (freenessParameterOMSKeyM :: Maybe LocIdBaseId
freenessParameterOMSKeyM, dbCache2 :: DBCache
dbCache2) <- case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
linkLabel of
      FreeOrCofreeDefLink _ (JustNode NodeSig { getNode :: NodeSig -> Node
getNode = Node
nodeId }) -> do
        let nodeLabel :: DGNodeLab
nodeLabel = LibEnv -> LibName -> Node -> DGNodeLab
getNodeLabel LibEnv
libEnv LibName
libName Node
nodeId
        (freenessParameterOMSKey :: LocIdBaseId
freenessParameterOMSKey, _, dbCache' :: DBCache
dbCache') <-
          HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
HetcatsOpts
-> LibEnv
-> FileVersionId
-> DBCache
-> Bool
-> GlobalAnnos
-> LibName
-> Entity LocIdBase
-> LNode DGNodeLab
-> DBMonad m (LocIdBaseId, SignatureId, DBCache)
findOrCreateOMS HetcatsOpts
opts LibEnv
libEnv FileVersionId
fileVersionKey DBCache
dbCache1 Bool
doSave
            GlobalAnnos
globalAnnotations LibName
libName Entity LocIdBase
documentLocIdBase (Node
nodeId, DGNodeLab
nodeLabel)
        (Maybe LocIdBaseId, DBCache)
-> ReaderT SqlBackend m (Maybe LocIdBaseId, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (LocIdBaseId -> Maybe LocIdBaseId
forall a. a -> Maybe a
Just LocIdBaseId
freenessParameterOMSKey, DBCache
dbCache')
      _ -> (Maybe LocIdBaseId, DBCache)
-> ReaderT SqlBackend m (Maybe LocIdBaseId, DBCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LocIdBaseId
forall a. Maybe a
Nothing, DBCache
dbCache)

    Maybe (Key Language)
freenessParameterLanguageKeyM <- case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
linkLabel of
      FreeOrCofreeDefLink _ (EmptyNode (Logic.Logic lid :: lid
lid)) ->
        (Key Language -> Maybe (Key Language))
-> ReaderT SqlBackend m (Key Language)
-> ReaderT SqlBackend m (Maybe (Key Language))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Key Language -> Maybe (Key Language)
forall a. a -> Maybe a
Just (ReaderT SqlBackend m (Key Language)
 -> ReaderT SqlBackend m (Maybe (Key Language)))
-> ReaderT SqlBackend m (Key Language)
-> ReaderT SqlBackend m (Maybe (Key Language))
forall a b. (a -> b) -> a -> b
$ lid -> ReaderT SqlBackend m (Key Language)
forall (m :: * -> *) lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
(MonadIO m, MonadFail m,
 Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree) =>
lid -> DBMonad m (Key Language)
findLanguage lid
lid
      _ -> Maybe (Key Language) -> ReaderT SqlBackend m (Maybe (Key Language))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Key Language)
forall a. Maybe a
Nothing

    LocIdBaseId
mappingKey <- LocIdBase -> ReaderT SqlBackend m LocIdBaseId
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WLocIdBase :: FileVersionId -> LocIdBaseKindType -> String -> LocIdBase
LocIdBase
      { locIdBaseFileVersionId :: FileVersionId
locIdBaseFileVersionId = FileVersionId
fileVersionKey
      , locIdBaseKind :: LocIdBaseKindType
locIdBaseKind = LocIdBaseKindType
Enums.Mapping
      , locIdBaseLocId :: String
locIdBaseLocId = String
locId
      }
    let mapping :: Mapping
mapping = $WMapping :: LocIdBaseId
-> LocIdBaseId
-> SignatureMorphismId
-> Maybe ConservativityStatusId
-> Maybe LocIdBaseId
-> Maybe (Key Language)
-> String
-> String
-> MappingOrigin
-> Bool
-> MappingType
-> Mapping
Mapping
          { mappingSourceId :: LocIdBaseId
mappingSourceId = LocIdBaseId
sourceOMSKey
          , mappingTargetId :: LocIdBaseId
mappingTargetId = LocIdBaseId
targetOMSKey
          , mappingSignatureMorphismId :: SignatureMorphismId
mappingSignatureMorphismId = SignatureMorphismId
signatureMorphismKey
          , mappingConservativityStatusId :: Maybe ConservativityStatusId
mappingConservativityStatusId = Maybe ConservativityStatusId
conservativityStatusKeyM
          , mappingFreenessParameterOMSId :: Maybe LocIdBaseId
mappingFreenessParameterOMSId = Maybe LocIdBaseId
freenessParameterOMSKeyM
          , mappingFreenessParameterLanguageId :: Maybe (Key Language)
mappingFreenessParameterLanguageId = Maybe (Key Language)
freenessParameterLanguageKeyM
          , mappingDisplayName :: String
mappingDisplayName = String
displayName
          , mappingName :: String
mappingName = DGLinkLab -> String
dglName DGLinkLab
linkLabel
          , mappingType :: MappingType
mappingType = MappingType
mappingTypeOfLinkLabel
          , mappingOrigin :: MappingOrigin
mappingOrigin = MappingOrigin
mappingOriginOfLinkLabel
          , mappingPending :: Bool
mappingPending = DGLinkLab -> Bool
dglPending DGLinkLab
linkLabel
          }
    [Entity Mapping] -> ReaderT SqlBackend m ()
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
[Entity record] -> ReaderT backend m ()
insertEntityMany [Key Mapping -> Mapping -> Entity Mapping
forall record. Key record -> record -> Entity record
Entity (Int64 -> Key Mapping
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key Mapping) -> Int64 -> Key Mapping
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
mappingKey) Mapping
mapping]
    DBCache -> DBMonad m DBCache
forall (m :: * -> *) a. Monad m => a -> m a
return DBCache
dbCache2
  else DBCache -> DBMonad m DBCache
forall (m :: * -> *) a. Monad m => a -> m a
return DBCache
dbCache1
  where
    mappingOriginOfLinkLabel :: MappingOrigin
    mappingOriginOfLinkLabel :: MappingOrigin
mappingOriginOfLinkLabel = case DGLinkLab -> DGLinkOrigin
dgl_origin DGLinkLab
linkLabel of
      SeeTarget -> MappingOrigin
MappingOrigin.SeeTarget
      SeeSource -> MappingOrigin
MappingOrigin.SeeSource
      TEST -> MappingOrigin
MappingOrigin.TEST
      DGLinkVerif -> MappingOrigin
MappingOrigin.DGLinkVerif
      DGImpliesLink -> MappingOrigin
MappingOrigin.DGImpliesLink
      DGLinkExtension -> MappingOrigin
MappingOrigin.DGLinkExtension
      DGLinkTranslation -> MappingOrigin
MappingOrigin.DGLinkTranslation
      DGLinkClosedLenv -> MappingOrigin
MappingOrigin.DGLinkClosedLenv
      DGLinkImports -> MappingOrigin
MappingOrigin.DGLinkImports
      DGLinkIntersect -> MappingOrigin
MappingOrigin.DGLinkIntersect
      DGLinkMorph _ -> MappingOrigin
MappingOrigin.DGLinkMorph
      DGLinkInst _ _ -> MappingOrigin
MappingOrigin.DGLinkInst
      DGLinkInstArg _ -> MappingOrigin
MappingOrigin.DGLinkInstArg
      DGLinkView _ _ -> MappingOrigin
MappingOrigin.DGLinkView
      DGLinkAlign _ -> MappingOrigin
MappingOrigin.DGLinkAlign
      DGLinkFitView _ -> MappingOrigin
MappingOrigin.DGLinkFitView
      DGLinkFitViewImp _ -> MappingOrigin
MappingOrigin.DGLinkFitViewImp
      DGLinkProof -> MappingOrigin
MappingOrigin.DGLinkProof
      DGLinkFlatteningUnion -> MappingOrigin
MappingOrigin.DGLinkFlatteningUnion
      DGLinkFlatteningRename -> MappingOrigin
MappingOrigin.DGLinkFlatteningRename
      DGLinkRefinement _ -> MappingOrigin
MappingOrigin.DGLinkRefinement

    mappingTypeOfLinkLabel :: MappingType
    mappingTypeOfLinkLabel :: MappingType
mappingTypeOfLinkLabel = case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
linkLabel of
      ScopedLink Local DefLink _ -> MappingType
MappingType.LocalDef
      ScopedLink Local (ThmLink LeftOpen) _ -> MappingType
MappingType.LocalThmOpen
      ScopedLink Local (ThmLink (Proven _ _)) _ -> MappingType
MappingType.LocalThmProved
      ScopedLink Global DefLink _ -> MappingType
MappingType.GlobalDef
      ScopedLink Global (ThmLink LeftOpen) _ -> MappingType
MappingType.GlobalThmOpen
      ScopedLink Global (ThmLink (Proven _ _)) _ -> MappingType
MappingType.GlobalThmProved
      HidingDefLink -> MappingType
MappingType.HidingDef
      FreeOrCofreeDefLink Free _ -> MappingType
MappingType.FreeDef
      FreeOrCofreeDefLink Cofree _ -> MappingType
MappingType.CofreeDef
      FreeOrCofreeDefLink NPFree _ -> MappingType
MappingType.NPFreeDef
      FreeOrCofreeDefLink Minimize _ -> MappingType
MappingType.MinimizeDef
      HidingFreeOrCofreeThm Nothing _ _ LeftOpen -> MappingType
MappingType.HidingOpen
      HidingFreeOrCofreeThm Nothing _ _ (Proven _ _) -> MappingType
MappingType.HidingProved
      HidingFreeOrCofreeThm (Just Free) _ _ LeftOpen -> MappingType
MappingType.FreeOpen
      HidingFreeOrCofreeThm (Just Cofree) _ _ LeftOpen -> MappingType
MappingType.CofreeOpen
      HidingFreeOrCofreeThm (Just NPFree) _ _ LeftOpen -> MappingType
MappingType.NPFreeOpen
      HidingFreeOrCofreeThm (Just Minimize) _ _ LeftOpen -> MappingType
MappingType.MinimizeOpen
      HidingFreeOrCofreeThm (Just Free) _ _ (Proven _ _) -> MappingType
MappingType.FreeProved
      HidingFreeOrCofreeThm (Just Cofree) _ _ (Proven _ _) -> MappingType
MappingType.CofreeProved
      HidingFreeOrCofreeThm (Just NPFree) _ _ (Proven _ _) -> MappingType
MappingType.NPFreeProved
      HidingFreeOrCofreeThm (Just Minimize) _ _ (Proven _ _) -> MappingType
MappingType.MinimizeProved


cachedOMSKey :: LibName -> Int -> DBCache -> Maybe (LocIdBaseId, SignatureId)
cachedOMSKey :: LibName -> Node -> DBCache -> Maybe (LocIdBaseId, SignatureId)
cachedOMSKey libName :: LibName
libName nodeId :: Node
nodeId = (LibName, Node)
-> Map (LibName, Node) (LocIdBaseId, SignatureId)
-> Maybe (LocIdBaseId, SignatureId)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LibName
libName, Node
nodeId) (Map (LibName, Node) (LocIdBaseId, SignatureId)
 -> Maybe (LocIdBaseId, SignatureId))
-> (DBCache -> Map (LibName, Node) (LocIdBaseId, SignatureId))
-> DBCache
-> Maybe (LocIdBaseId, SignatureId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DBCache -> Map (LibName, Node) (LocIdBaseId, SignatureId)
nodeMap

symbolIsCached :: Sentences lid sentence sign morphism symbol
               => LibEnv -> LibName -> Int -> lid -> symbol -> DBCache -> Bool
symbolIsCached :: LibEnv -> LibName -> Node -> lid -> symbol -> DBCache -> Bool
symbolIsCached libEnv :: LibEnv
libEnv libName :: LibName
libName nodeId :: Node
nodeId lid :: lid
lid symbol :: symbol
symbol =
  Maybe LocIdBaseId -> Bool
forall a. Maybe a -> Bool
isJust (Maybe LocIdBaseId -> Bool)
-> (DBCache -> Maybe LocIdBaseId) -> DBCache -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibEnv
-> LibName -> Node -> lid -> symbol -> DBCache -> Maybe LocIdBaseId
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
LibEnv
-> LibName -> Node -> lid -> symbol -> DBCache -> Maybe LocIdBaseId
findSymbolInCache LibEnv
libEnv LibName
libName Node
nodeId lid
lid symbol
symbol

-- Gives the node label to an id. Use only if the combination exists.
getNodeLabel :: LibEnv -> LibName -> Int -> DGNodeLab
getNodeLabel :: LibEnv -> LibName -> Node -> DGNodeLab
getNodeLabel libEnv :: LibEnv
libEnv libName :: LibName
libName nodeId :: Node
nodeId =
  Maybe DGNodeLab -> DGNodeLab
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DGNodeLab -> DGNodeLab) -> Maybe DGNodeLab -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ (GrContext DGNodeLab DGLinkLab -> DGNodeLab)
-> Maybe (GrContext DGNodeLab DGLinkLab) -> Maybe DGNodeLab
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GrContext DGNodeLab DGLinkLab -> DGNodeLab
forall a b. GrContext a b -> a
Graph.nodeLabel (Maybe (GrContext DGNodeLab DGLinkLab) -> Maybe DGNodeLab)
-> Maybe (GrContext DGNodeLab DGLinkLab) -> Maybe DGNodeLab
forall a b. (a -> b) -> a -> b
$ Node
-> IntMap (GrContext DGNodeLab DGLinkLab)
-> Maybe (GrContext DGNodeLab DGLinkLab)
forall a. Node -> IntMap a -> Maybe a
IntMap.lookup Node
nodeId (IntMap (GrContext DGNodeLab DGLinkLab)
 -> Maybe (GrContext DGNodeLab DGLinkLab))
-> IntMap (GrContext DGNodeLab DGLinkLab)
-> Maybe (GrContext DGNodeLab DGLinkLab)
forall a b. (a -> b) -> a -> b
$ Gr DGNodeLab DGLinkLab -> IntMap (GrContext DGNodeLab DGLinkLab)
forall a b. Gr a b -> IntMap (GrContext a b)
convertToMap (Gr DGNodeLab DGLinkLab -> IntMap (GrContext DGNodeLab DGLinkLab))
-> Gr DGNodeLab DGLinkLab -> IntMap (GrContext DGNodeLab DGLinkLab)
forall a b. (a -> b) -> a -> b
$
    DGraph -> Gr DGNodeLab DGLinkLab
dgBody (DGraph -> Gr DGNodeLab DGLinkLab)
-> DGraph -> Gr DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ Maybe DGraph -> DGraph
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DGraph -> DGraph) -> Maybe DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> Maybe DGraph
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
libName LibEnv
libEnv

dereferenceNodeId :: LibEnv -> LibName -> Int -> (LibName, Int)
dereferenceNodeId :: LibEnv -> LibName -> Node -> (LibName, Node)
dereferenceNodeId libEnv :: LibEnv
libEnv libName :: LibName
libName nodeId :: Node
nodeId =
  case DGNodeLab -> DGNodeInfo
nodeInfo (DGNodeLab -> DGNodeInfo) -> DGNodeLab -> DGNodeInfo
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> Node -> DGNodeLab
getNodeLabel LibEnv
libEnv LibName
libName Node
nodeId of
    DGNode {} -> (LibName
libName, Node
nodeId)
    DGRef { ref_node :: DGNodeInfo -> Node
ref_node = Node
refNodeId
          , ref_libname :: DGNodeInfo -> LibName
ref_libname = LibName
refLibName
          } -> LibEnv -> LibName -> Node -> (LibName, Node)
dereferenceNodeId LibEnv
libEnv LibName
refLibName Node
refNodeId

addDocumentToCache :: LibName -> LocIdBaseId -> DBCache -> DBCache
addDocumentToCache :: LibName -> LocIdBaseId -> DBCache -> DBCache
addDocumentToCache libName :: LibName
libName documentKey :: LocIdBaseId
documentKey dbCache :: DBCache
dbCache =
  DBCache
dbCache { documentMap :: Map LibName LocIdBaseId
documentMap = LibName
-> LocIdBaseId
-> Map LibName LocIdBaseId
-> Map LibName LocIdBaseId
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
libName LocIdBaseId
documentKey (Map LibName LocIdBaseId -> Map LibName LocIdBaseId)
-> Map LibName LocIdBaseId -> Map LibName LocIdBaseId
forall a b. (a -> b) -> a -> b
$ DBCache -> Map LibName LocIdBaseId
documentMap DBCache
dbCache
          , documentByLibNameIRIMap :: Map IRI LocIdBaseId
documentByLibNameIRIMap = IRI -> LocIdBaseId -> Map IRI LocIdBaseId -> Map IRI LocIdBaseId
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName -> IRI
iriOfLibName LibName
libName) LocIdBaseId
documentKey (Map IRI LocIdBaseId -> Map IRI LocIdBaseId)
-> Map IRI LocIdBaseId -> Map IRI LocIdBaseId
forall a b. (a -> b) -> a -> b
$ DBCache -> Map IRI LocIdBaseId
documentByLibNameIRIMap DBCache
dbCache
          }

iriOfLibName :: LibName -> IRI
iriOfLibName :: LibName -> IRI
iriOfLibName = String -> IRI
filePathToLibId (String -> IRI) -> (LibName -> String) -> LibName -> IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> String
libToFileName

addNodeToCache :: LibName -> Int -> LocIdBaseId -> SignatureId -> DBCache
               -> DBCache
addNodeToCache :: LibName -> Node -> LocIdBaseId -> SignatureId -> DBCache -> DBCache
addNodeToCache libName :: LibName
libName nodeId :: Node
nodeId omsKey :: LocIdBaseId
omsKey signatureKey :: SignatureId
signatureKey dbCache :: DBCache
dbCache =
  DBCache
dbCache { nodeMap :: Map (LibName, Node) (LocIdBaseId, SignatureId)
nodeMap = (LibName, Node)
-> (LocIdBaseId, SignatureId)
-> Map (LibName, Node) (LocIdBaseId, SignatureId)
-> Map (LibName, Node) (LocIdBaseId, SignatureId)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName
libName, Node
nodeId) (LocIdBaseId
omsKey, SignatureId
signatureKey) (Map (LibName, Node) (LocIdBaseId, SignatureId)
 -> Map (LibName, Node) (LocIdBaseId, SignatureId))
-> Map (LibName, Node) (LocIdBaseId, SignatureId)
-> Map (LibName, Node) (LocIdBaseId, SignatureId)
forall a b. (a -> b) -> a -> b
$
                        DBCache -> Map (LibName, Node) (LocIdBaseId, SignatureId)
nodeMap DBCache
dbCache
          }

addSignatureToCache :: LibName -> SigId -> SignatureId -> DBCache -> DBCache
addSignatureToCache :: LibName -> SigId -> SignatureId -> DBCache -> DBCache
addSignatureToCache libName :: LibName
libName sigId :: SigId
sigId signatureKey :: SignatureId
signatureKey dbCache :: DBCache
dbCache =
  DBCache
dbCache { signatureMap :: Map (LibName, SigId) SignatureId
signatureMap = (LibName, SigId)
-> SignatureId
-> Map (LibName, SigId) SignatureId
-> Map (LibName, SigId) SignatureId
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName
libName, SigId
sigId) SignatureId
signatureKey (Map (LibName, SigId) SignatureId
 -> Map (LibName, SigId) SignatureId)
-> Map (LibName, SigId) SignatureId
-> Map (LibName, SigId) SignatureId
forall a b. (a -> b) -> a -> b
$
                             DBCache -> Map (LibName, SigId) SignatureId
signatureMap DBCache
dbCache }

addSymbolToCache :: Sentences lid sentence sign morphism symbol
                 => LibEnv -> LibName -> Int -> lid -> symbol -> LocIdBaseId
                 -> DBCache -> DBCache
addSymbolToCache :: LibEnv
-> LibName
-> Node
-> lid
-> symbol
-> LocIdBaseId
-> DBCache
-> DBCache
addSymbolToCache libEnv :: LibEnv
libEnv libName :: LibName
libName nodeId :: Node
nodeId lid :: lid
lid symbol :: symbol
symbol symbolKey :: LocIdBaseId
symbolKey dbCache :: DBCache
dbCache =
  let mapIndex :: SymbolMapIndex
mapIndex = lid -> symbol -> SymbolMapIndex
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> SymbolMapIndex
symbolMapIndex lid
lid symbol
symbol
      (libNameDereferenced :: LibName
libNameDereferenced, nodeIdDereferenced :: Node
nodeIdDereferenced) = LibEnv -> LibName -> Node -> (LibName, Node)
dereferenceNodeId LibEnv
libEnv LibName
libName Node
nodeId
  in  DBCache
dbCache { symbolKeyMap :: Map (LibName, Node, SymbolMapIndex) LocIdBaseId
symbolKeyMap =
                  (LibName, Node, SymbolMapIndex)
-> LocIdBaseId
-> Map (LibName, Node, SymbolMapIndex) LocIdBaseId
-> Map (LibName, Node, SymbolMapIndex) LocIdBaseId
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName
libNameDereferenced, Node
nodeIdDereferenced, SymbolMapIndex
mapIndex) LocIdBaseId
symbolKey (Map (LibName, Node, SymbolMapIndex) LocIdBaseId
 -> Map (LibName, Node, SymbolMapIndex) LocIdBaseId)
-> Map (LibName, Node, SymbolMapIndex) LocIdBaseId
-> Map (LibName, Node, SymbolMapIndex) LocIdBaseId
forall a b. (a -> b) -> a -> b
$
                    DBCache -> Map (LibName, Node, SymbolMapIndex) LocIdBaseId
symbolKeyMap DBCache
dbCache
              }

findSymbolInCache :: Sentences lid sentence sign morphism symbol
                  => LibEnv -> LibName -> Int -> lid -> symbol
                  -> DBCache -> Maybe LocIdBaseId
findSymbolInCache :: LibEnv
-> LibName -> Node -> lid -> symbol -> DBCache -> Maybe LocIdBaseId
findSymbolInCache libEnv :: LibEnv
libEnv libName :: LibName
libName nodeId :: Node
nodeId lid :: lid
lid symbol :: symbol
symbol dbCache :: DBCache
dbCache =
  let mapIndex :: SymbolMapIndex
mapIndex = lid -> symbol -> SymbolMapIndex
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> SymbolMapIndex
symbolMapIndex lid
lid symbol
symbol
      (libNameDereferenced :: LibName
libNameDereferenced, nodeIdDereferenced :: Node
nodeIdDereferenced) = LibEnv -> LibName -> Node -> (LibName, Node)
dereferenceNodeId LibEnv
libEnv LibName
libName Node
nodeId
  in  (LibName, Node, SymbolMapIndex)
-> Map (LibName, Node, SymbolMapIndex) LocIdBaseId
-> Maybe LocIdBaseId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LibName
libNameDereferenced, Node
nodeIdDereferenced, SymbolMapIndex
mapIndex) (Map (LibName, Node, SymbolMapIndex) LocIdBaseId
 -> Maybe LocIdBaseId)
-> Map (LibName, Node, SymbolMapIndex) LocIdBaseId
-> Maybe LocIdBaseId
forall a b. (a -> b) -> a -> b
$ DBCache -> Map (LibName, Node, SymbolMapIndex) LocIdBaseId
symbolKeyMap DBCache
dbCache

findOMS :: MonadIO m
        => FileVersionId -> Entity LocIdBase -> DGNodeLab
        -> DBMonad m (Maybe (Entity LocIdBase))
findOMS :: FileVersionId
-> Entity LocIdBase
-> DGNodeLab
-> DBMonad m (Maybe (Entity LocIdBase))
findOMS fileVersionKey :: FileVersionId
fileVersionKey documentLocIdBase :: Entity LocIdBase
documentLocIdBase nodeLabel :: DGNodeLab
nodeLabel = do
  [Entity LocIdBase]
omsLocIdL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LocIdBase)
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LocIdBase)
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (SqlExpr (Entity LocIdBase)
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ \loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase FileVersionId
-> SqlExpr (Value FileVersionId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase FileVersionId
forall typ. (typ ~ FileVersionId) => EntityField LocIdBase typ
LocIdBaseFileVersionId SqlExpr (Value FileVersionId)
-> SqlExpr (Value FileVersionId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. FileVersionId -> SqlExpr (Value FileVersionId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val FileVersionId
fileVersionKey
              SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseKindType
-> SqlExpr (Value LocIdBaseKindType)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseKindType
forall typ. (typ ~ LocIdBaseKindType) => EntityField LocIdBase typ
LocIdBaseKind SqlExpr (Value LocIdBaseKindType)
-> SqlExpr (Value LocIdBaseKindType) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. LocIdBaseKindType -> SqlExpr (Value LocIdBaseKindType)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val LocIdBaseKindType
Enums.OMS
              SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase String
forall typ. (typ ~ String) => EntityField LocIdBase typ
LocIdBaseLocId 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 (Entity LocIdBase -> DGNodeLab -> String
locIdOfOMS Entity LocIdBase
documentLocIdBase DGNodeLab
nodeLabel))
    SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
  case [Entity LocIdBase]
omsLocIdL of
    [] -> Maybe (Entity LocIdBase) -> DBMonad m (Maybe (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Entity LocIdBase)
forall a. Maybe a
Nothing
    entity :: Entity LocIdBase
entity : _ -> Maybe (Entity LocIdBase) -> DBMonad m (Maybe (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Entity LocIdBase) -> DBMonad m (Maybe (Entity LocIdBase)))
-> Maybe (Entity LocIdBase) -> DBMonad m (Maybe (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ Entity LocIdBase -> Maybe (Entity LocIdBase)
forall a. a -> Maybe a
Just Entity LocIdBase
entity

findOMSAndSignature :: (MonadIO m, Fail.MonadFail m)
                    => FileVersionId -> Entity LocIdBase -> DGNodeLab
                    -> DBMonad m (Maybe (LocIdBaseId, SignatureId))
findOMSAndSignature :: FileVersionId
-> Entity LocIdBase
-> DGNodeLab
-> DBMonad m (Maybe (LocIdBaseId, SignatureId))
findOMSAndSignature fileVersionKey :: FileVersionId
fileVersionKey documentLocIdBase :: Entity LocIdBase
documentLocIdBase nodeLabel :: DGNodeLab
nodeLabel = do
  Maybe (Entity LocIdBase)
omsLocIdBaseM <- FileVersionId
-> Entity LocIdBase
-> DGNodeLab
-> DBMonad m (Maybe (Entity LocIdBase))
forall (m :: * -> *).
MonadIO m =>
FileVersionId
-> Entity LocIdBase
-> DGNodeLab
-> DBMonad m (Maybe (Entity LocIdBase))
findOMS FileVersionId
fileVersionKey Entity LocIdBase
documentLocIdBase DGNodeLab
nodeLabel
  case Maybe (Entity LocIdBase)
omsLocIdBaseM of
    Nothing -> Maybe (LocIdBaseId, SignatureId)
-> DBMonad m (Maybe (LocIdBaseId, SignatureId))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (LocIdBaseId, SignatureId)
forall a. Maybe a
Nothing
    Just (Entity omsKey :: LocIdBaseId
omsKey _) -> do
      [Entity OMS]
omsValueL <- SqlQuery (SqlExpr (Entity OMS))
-> ReaderT SqlBackend m [Entity OMS]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity OMS))
 -> ReaderT SqlBackend m [Entity OMS])
-> SqlQuery (SqlExpr (Entity OMS))
-> ReaderT SqlBackend m [Entity OMS]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity OMS) -> SqlQuery (SqlExpr (Entity OMS)))
-> SqlQuery (SqlExpr (Entity OMS))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity OMS) -> SqlQuery (SqlExpr (Entity OMS)))
 -> SqlQuery (SqlExpr (Entity OMS)))
-> (SqlExpr (Entity OMS) -> SqlQuery (SqlExpr (Entity OMS)))
-> SqlQuery (SqlExpr (Entity OMS))
forall a b. (a -> b) -> a -> b
$ \omsSql :: SqlExpr (Entity OMS)
omsSql -> do
        SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity OMS)
omsSql SqlExpr (Entity OMS)
-> EntityField OMS (Key OMS) -> SqlExpr (Value (Key OMS))
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField OMS (Key OMS)
forall typ. (typ ~ Key OMS) => EntityField OMS typ
OMSId SqlExpr (Value (Key OMS))
-> SqlExpr (Value (Key OMS)) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. Key OMS -> SqlExpr (Value (Key OMS))
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val (Int64 -> Key OMS
forall record.
ToBackendKey SqlBackend record =>
Int64 -> Key record
toSqlKey (Int64 -> Key OMS) -> Int64 -> Key OMS
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> Int64
forall record.
ToBackendKey SqlBackend record =>
Key record -> Int64
fromSqlKey LocIdBaseId
omsKey))
        SqlExpr (Entity OMS) -> SqlQuery (SqlExpr (Entity OMS))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity OMS)
omsSql
      OMS
omsValue <- case [Entity OMS]
omsValueL of
        [] ->
          String -> ReaderT SqlBackend m OMS
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.DevGraph.findOMSAndSignature could not find OMS with ID "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int64 -> String
forall a. Show a => a -> String
show (BackendKey SqlBackend -> Int64
unSqlBackendKey (BackendKey SqlBackend -> Int64) -> BackendKey SqlBackend -> Int64
forall a b. (a -> b) -> a -> b
$ LocIdBaseId -> BackendKey SqlBackend
unLocIdBaseKey LocIdBaseId
omsKey))
        Entity _ omsValue :: OMS
omsValue : _ -> OMS -> ReaderT SqlBackend m OMS
forall (m :: * -> *) a. Monad m => a -> m a
return OMS
omsValue
      Maybe (LocIdBaseId, SignatureId)
-> DBMonad m (Maybe (LocIdBaseId, SignatureId))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (LocIdBaseId, SignatureId)
 -> DBMonad m (Maybe (LocIdBaseId, SignatureId)))
-> Maybe (LocIdBaseId, SignatureId)
-> DBMonad m (Maybe (LocIdBaseId, SignatureId))
forall a b. (a -> b) -> a -> b
$ (LocIdBaseId, SignatureId) -> Maybe (LocIdBaseId, SignatureId)
forall a. a -> Maybe a
Just (LocIdBaseId
omsKey, OMS -> SignatureId
oMSSignatureId OMS
omsValue)

findSentence :: MonadIO m
             => FileVersionId -> String
             -> DBMonad m (Maybe (Entity LocIdBase))
findSentence :: FileVersionId -> String -> DBMonad m (Maybe (Entity LocIdBase))
findSentence fileVersionKey :: FileVersionId
fileVersionKey locId :: String
locId = do
  [Entity LocIdBase]
sentenceL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT SqlBackend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT SqlBackend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LocIdBase)
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LocIdBase)
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (SqlExpr (Entity LocIdBase)
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ \loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases -> do
    SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase FileVersionId
-> SqlExpr (Value FileVersionId)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase FileVersionId
forall typ. (typ ~ FileVersionId) => EntityField LocIdBase typ
LocIdBaseFileVersionId SqlExpr (Value FileVersionId)
-> SqlExpr (Value FileVersionId) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. FileVersionId -> SqlExpr (Value FileVersionId)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val FileVersionId
fileVersionKey
              SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase LocIdBaseKindType
-> SqlExpr (Value LocIdBaseKindType)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase LocIdBaseKindType
forall typ. (typ ~ LocIdBaseKindType) => EntityField LocIdBase typ
LocIdBaseKind SqlExpr (Value LocIdBaseKindType)
-> SqlExpr (ValueList LocIdBaseKindType) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ)
-> SqlExpr (ValueList typ) -> SqlExpr (Value Bool)
`in_` [LocIdBaseKindType] -> SqlExpr (ValueList LocIdBaseKindType)
forall typ. PersistField typ => [typ] -> SqlExpr (ValueList typ)
valList [ LocIdBaseKindType
Enums.OpenConjecture
                                                              , LocIdBaseKindType
Enums.Theorem
                                                              , LocIdBaseKindType
Enums.CounterTheorem
                                                              , LocIdBaseKindType
Enums.Axiom
                                                              ]
              SqlExpr (Value Bool)
-> SqlExpr (Value Bool) -> SqlExpr (Value Bool)
&&. SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase String
forall typ. (typ ~ String) => EntityField LocIdBase typ
LocIdBaseLocId 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
locId)
    SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
  case [Entity LocIdBase]
sentenceL of
    [] -> Maybe (Entity LocIdBase) -> DBMonad m (Maybe (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Entity LocIdBase)
forall a. Maybe a
Nothing
    entity :: Entity LocIdBase
entity : _ -> Maybe (Entity LocIdBase) -> DBMonad m (Maybe (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Entity LocIdBase) -> DBMonad m (Maybe (Entity LocIdBase)))
-> Maybe (Entity LocIdBase) -> DBMonad m (Maybe (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ Entity LocIdBase -> Maybe (Entity LocIdBase)
forall a. a -> Maybe a
Just Entity LocIdBase
entity


symbolMapIndex :: Sentences lid sentence sign morphism symbol
               => lid -> symbol -> SymbolMapIndex
symbolMapIndex :: lid -> symbol -> SymbolMapIndex
symbolMapIndex lid :: lid
lid symbol :: symbol
symbol =
  let fullName :: String
fullName = ShowS
forall a. Show a => a -> String
show ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ lid -> symbol -> String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> String
fullSymName lid
lid symbol
symbol
      symbolKind :: String
symbolKind = lid -> symbol -> String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> String
symKind lid
lid symbol
symbol
  in (String
symbolKind, String
fullName)




createDocumentLinks :: MonadIO m
                    => DBCache -> Rel LibName
                    -> DBMonad m ()
createDocumentLinks :: DBCache -> Rel LibName -> DBMonad m ()
createDocumentLinks dbCache :: DBCache
dbCache dependencyLibNameRel :: Rel LibName
dependencyLibNameRel =
  ((LibName, Set LibName) -> DBMonad m ())
-> [(LibName, Set LibName)] -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (targetLibName :: LibName
targetLibName, sourceLibNamesSet :: Set LibName
sourceLibNamesSet) ->
          (LibName -> DBMonad m ()) -> [LibName] -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (LibName -> LibName -> DBMonad m ()
forall (m :: * -> *).
MonadIO m =>
LibName -> LibName -> DBMonad m ()
createDocumentLink LibName
targetLibName) ([LibName] -> DBMonad m ()) -> [LibName] -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$
            Set LibName -> [LibName]
forall a. Set a -> [a]
Set.toList Set LibName
sourceLibNamesSet
        ) ([(LibName, Set LibName)] -> DBMonad m ())
-> [(LibName, Set LibName)] -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$ Map LibName (Set LibName) -> [(LibName, Set LibName)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map LibName (Set LibName) -> [(LibName, Set LibName)])
-> Map LibName (Set LibName) -> [(LibName, Set LibName)]
forall a b. (a -> b) -> a -> b
$ Rel LibName -> Map LibName (Set LibName)
forall a. Rel a -> Map a (Set a)
Rel.toMap Rel LibName
dependencyLibNameRel
  where
    createDocumentLink :: MonadIO m
                       => LibName -> LibName -> DBMonad m ()
    createDocumentLink :: LibName -> LibName -> DBMonad m ()
createDocumentLink sourceLibName :: LibName
sourceLibName targetLibName :: LibName
targetLibName = do
      -- These libNames must be in the documentMap by construction
      let sourceKey :: LocIdBaseId
sourceKey = Maybe LocIdBaseId -> LocIdBaseId
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe LocIdBaseId -> LocIdBaseId)
-> Maybe LocIdBaseId -> LocIdBaseId
forall a b. (a -> b) -> a -> b
$ LibName -> Map LibName LocIdBaseId -> Maybe LocIdBaseId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
sourceLibName (Map LibName LocIdBaseId -> Maybe LocIdBaseId)
-> Map LibName LocIdBaseId -> Maybe LocIdBaseId
forall a b. (a -> b) -> a -> b
$ DBCache -> Map LibName LocIdBaseId
documentMap DBCache
dbCache
      let targetKey :: LocIdBaseId
targetKey = Maybe LocIdBaseId -> LocIdBaseId
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe LocIdBaseId -> LocIdBaseId)
-> Maybe LocIdBaseId -> LocIdBaseId
forall a b. (a -> b) -> a -> b
$ LibName -> Map LibName LocIdBaseId -> Maybe LocIdBaseId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
targetLibName (Map LibName LocIdBaseId -> Maybe LocIdBaseId)
-> Map LibName LocIdBaseId -> Maybe LocIdBaseId
forall a b. (a -> b) -> a -> b
$ DBCache -> Map LibName LocIdBaseId
documentMap DBCache
dbCache
      DocumentLink -> ReaderT SqlBackend m (Key DocumentLink)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WDocumentLink :: LocIdBaseId -> LocIdBaseId -> DocumentLink
DocumentLink { documentLinkSourceId :: LocIdBaseId
documentLinkSourceId = LocIdBaseId
sourceKey
                          , documentLinkTargetId :: LocIdBaseId
documentLinkTargetId = LocIdBaseId
targetKey
                          }
      () -> DBMonad m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()


fromJustFail :: (MonadIO m, Fail.MonadFail m) => String -> Maybe a -> m a
fromJustFail :: String -> Maybe a -> m a
fromJustFail message :: String
message maybeValue :: Maybe a
maybeValue = case Maybe a
maybeValue of
  Just value :: a
value -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
value
  Nothing -> String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
message