{-# 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 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
  { documentMap :: Map LibName LocIdBaseId -- Here, LocIdBaseId is DocumentId
  , documentByLibNameIRIMap :: Map IRI LocIdBaseId -- Here, LocIdBaseId is DocumentId
  , nodeMap :: Map (LibName, Node) (LocIdBaseId, SignatureId) -- Here, LocIdBaseId is OMSId
  , signatureMap :: Map (LibName, SigId) SignatureId
  , signatureMorphismMap :: Map (LibName, MorId)
                             (SignatureMorphismId, [SymbolMappingId], GMorphism)
  , symbolKeyMap :: Map (LibName, Int, SymbolMapIndex) LocIdBaseId -- Here, LocIdBaseId is SymbolId
  } deriving Show

emptyDBCache :: DBCache
emptyDBCache = DBCache { documentMap = Map.empty
                       , documentByLibNameIRIMap = Map.empty
                       , nodeMap = Map.empty
                       , signatureMap = Map.empty
                       , signatureMorphismMap = Map.empty
                       , symbolKeyMap = Map.empty
                       }

exportLibEnv :: HetcatsOpts -> LibEnv -> IO ()
exportLibEnv opts libEnv = do
  onDatabase dbConfig $
    setFileVersionState dbContext EvaluationStateType.Processing
  Control.Exception.catch export saveErrorAndRethrow
  where
    dbConfig = databaseConfig opts
    dbContext = databaseContext opts

    export :: IO ()
    export = onDatabase dbConfig $ do
      let dependencyLibNameRel = getLibDepRel libEnv
      let dependencyOrderedLibsSetL = Rel.depSort dependencyLibNameRel
      dbCache1 <-
        createDocuments opts libEnv emptyDBCache dependencyOrderedLibsSetL
      createDocumentLinks dbCache1 dependencyLibNameRel
      setFileVersionState dbContext EvaluationStateType.FinishedSuccessfully
      return ()

    saveErrorAndRethrow :: SomeException -> IO ()
    saveErrorAndRethrow exception = do
      let message = show exception
      saveDiagnoses dbConfig dbContext 5 [Diag { diagKind = Error
                                               , diagString = message
                                               , diagPos = nullRange
                                               }]
      fail message

createDocuments :: MonadIO m
                => HetcatsOpts -> LibEnv -> DBCache -> [Set LibName]
                -> DBMonad m DBCache
createDocuments opts libEnv dbCache0 dependencyOrderedLibsSetL = do
  fileVersion <- getFileVersion $ databaseContext opts
  dbCache1 <-
    createDocumentsInDependencyRelation opts libEnv fileVersion dbCache0 $
      reverse dependencyOrderedLibsSetL
  createDocumentsThatAreIndependent opts libEnv fileVersion dbCache1

createDocumentsInDependencyRelation :: MonadIO m
                                    => HetcatsOpts -> LibEnv
                                    -> Entity FileVersion -> DBCache -> [Set LibName]
                                    -> DBMonad m DBCache
createDocumentsInDependencyRelation opts libEnv fileVersion =
  foldM
    (\ outerAcc libNameSet ->
       foldM
         (\ dbCacheAcc libName ->
            createDocument opts libEnv fileVersion dbCacheAcc libName
         ) outerAcc libNameSet
    )

createDocumentsThatAreIndependent :: MonadIO m
                                  => HetcatsOpts -> LibEnv
                                  -> Entity FileVersion -> DBCache
                                  -> DBMonad m DBCache
createDocumentsThatAreIndependent opts libEnv fileVersion dbCache =
  foldM
    (\ dbCacheAcc libName ->
      let alreadyInserted = isJust $ Map.lookup libName $ documentMap dbCacheAcc
      in  if alreadyInserted
          then return dbCacheAcc
          else createDocument opts libEnv fileVersion dbCacheAcc libName
    ) dbCache $ Map.keys libEnv

createDocument :: MonadIO m
               => HetcatsOpts -> LibEnv -> Entity FileVersion -> DBCache
               -> LibName -> DBMonad m DBCache
createDocument opts libEnv parentFileVersion dbCache0 libName =
  let dGraph = fromJust $ Map.lookup libName libEnv
      globalAnnotations = globalAnnos dGraph
      name = show $ pretty $ getLibId libName
      displayName = show $ setAngles False $ getLibId libName
      location = fmap show $ locIRI libName
      version = fmap (intercalate "." . (\ (VersionNumber v _) -> v)) $
                  libVersion libName
      locId = locIdOfDocument opts location displayName
  in  do
        -- We need to find the FileVersion of the corresponding document
        -- if it is located inside the libdir.
        fileVersionKey <- findFileVersionByPath opts parentFileVersion location
        kind <- kindOfDocument opts location
        let fileVersionKeyS =
              show $ unSqlBackendKey $ unFileVersionKey fileVersionKey
        advisoryLocked opts (fileVersionKeyS ++ "-" ++ show kind ++ "-" ++ locId) $ do
          documentL <- select $ from $ \loc_id_bases -> do
            where_ (loc_id_bases ^. LocIdBaseLocId ==. val locId
                      &&. loc_id_bases ^. LocIdBaseFileVersionId ==. val fileVersionKey
                      &&. loc_id_bases ^. LocIdBaseKind ==. val kind)
            return loc_id_bases
          case documentL of
            [] -> return ()
            document : _ -> when (databaseReanalyze opts) $
              Persistence.DevGraph.Cleaning.clean document
          (doSave, documentKey, documentLocIdBaseValue) <-
            case (databaseReanalyze opts, documentL) of
              (False, Entity documentKey documentLocIdBaseValue : _) ->
                return (False, documentKey, documentLocIdBaseValue)
              _ -> do
                let documentLocIdBaseValue = LocIdBase
                      { locIdBaseFileVersionId = fileVersionKey
                      , locIdBaseKind = kind
                      , locIdBaseLocId = locId
                      }
                documentKey <- insert documentLocIdBaseValue
                let document = Document
                      { documentDisplayName = displayName
                      , documentName = name
                      , documentLocation = location
                      , documentVersion = version
                      }
                insertEntityMany [Entity (toSqlKey $ fromSqlKey documentKey) document]
                return (True, documentKey, documentLocIdBaseValue)
          let dbCache1 = addDocumentToCache libName documentKey dbCache0
          createAllOmsOfDocument opts libEnv fileVersionKey dbCache1 doSave dGraph
            globalAnnotations libName (Entity documentKey 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 opts (Entity fileVersionKey _) location =
  let isInLibdir = not (null $ libdirs opts)
                     && isJust location
                     && head (libdirs opts) `isPrefixOf` fromJust location
      path = fromJust $ stripPrefix (firstLibdir opts) $ fromJust location
      queryString = Text.pack (
        "SELECT file_versions.id "
        ++ "FROM file_versions "
        ++ "INNER JOIN file_version_parents "
        ++ "  ON file_version_parents.last_changed_file_version_id = file_versions.id "
        ++ "INNER JOIN file_versions AS backreference "
        ++ "  ON file_version_parents.queried_sha = backreference.commit_sha "
        ++ "WHERE (file_versions.path = ? "
        ++ "       AND backreference.id = ?);")
  in  if isInLibdir
      then do
            results <-
              rawSql queryString [ toPersistValue path
                                 , toPersistValue fileVersionKey
                                 ]
            if null results
            then return fileVersionKey
            else return $ head results
      else return 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 opts filepathM = case filepathM of
  Nothing -> return Enums.Library
  Just filepath -> case guess filepath (intype opts) of
    GuessIn -> do
      mimeR <-
        liftIO $ runResultT $ getMagicFileType (Just "--mime-type") filepath
      case maybeResult mimeR of
        Just mime -> return $ determineTypeByMime mime
        Nothing -> return Enums.Library
    t -> return $ determineType t
  where
    determineType :: InType -> Enums.LocIdBaseKindType
    determineType t = if show t `elem` ["casl", "het", "dol"]
                      then Enums.Library
                      else Enums.NativeDocument

    determineTypeByMime :: String -> Enums.LocIdBaseKindType
    determineTypeByMime t = if t `elem` ["text/casl", "text/het", "text/dol"]
                            then Enums.Library
                            else Enums.NativeDocument

createAllOmsOfDocument :: MonadIO m
                       => HetcatsOpts -> LibEnv -> FileVersionId -> DBCache
                       -> Bool -> DGraph -> GlobalAnnos -> LibName
                       -> Entity LocIdBase -> DBMonad m DBCache
createAllOmsOfDocument opts libEnv fileVersionKey dbCache0 doSave dGraph
  globalAnnotations libName documentLocIdBase =
  let labeledNodes = labNodes $ dgBody dGraph
      labeledEdges = labEdges $ dgBody dGraph
  in  do
        dbCache1 <- foldM
          (\ dbCacheAcc labeledNode ->
            fmap (\ (_, _, dbCache) -> dbCache) $
              findOrCreateOMS opts libEnv fileVersionKey dbCacheAcc doSave
                globalAnnotations libName documentLocIdBase labeledNode
          ) dbCache0 labeledNodes
        foldM
          (\ dbCacheAcc labeledEdge ->
            createMapping opts libEnv fileVersionKey dbCacheAcc doSave
              globalAnnotations libName documentLocIdBase labeledEdge
          ) dbCache1 labeledEdges

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

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

createOMS :: MonadIO m
          => HetcatsOpts -> LibEnv -> FileVersionId -> DBCache -> Bool
          -> GlobalAnnos -> LibName -> Entity LocIdBase -> (Int, DGNodeLab)
          -> ConsStatus -> DBMonad m (LocIdBaseId, SignatureId, DBCache)
createOMS opts libEnv fileVersionKey dbCache0 doSave globalAnnotations libName
  documentLocIdBase@(Entity documentKey _) (nodeId, nodeLabel) consStatus =
  let gTheory = fromJust $ computeTheory libEnv libName nodeId
      internalNodeName = dgn_name nodeLabel
      name = show $ getName internalNodeName
      nameExtension = extString internalNodeName
      nameExtensionIndex = extIndex internalNodeName
      displayName = showName internalNodeName
      locId = locIdOfOMS documentLocIdBase nodeLabel
  in  do
        languageKey <- case gTheory of
          G_theory { gTheoryLogic = lid } -> findLanguage lid

        (signatureKey, signatureIsNew, dbCache1) <- case gTheory of
          G_theory { gTheoryLogic = lid
                   , gTheorySignIdx = sigId
                   , gTheorySign = extSign
                   } -> do
           omsKeyM <-
             findOMSAndSignature fileVersionKey documentLocIdBase nodeLabel
           case omsKeyM of
             Just (_, signatureKey) ->
               return ( signatureKey
                      , False
                      , addSignatureToCache libName sigId signatureKey dbCache0
                      )
             Nothing ->
               findOrCreateSignature dbCache0 libName lid extSign sigId
                 languageKey

        (normalFormKeyM, normalFormSignatureKeyM, dbCache2) <-
          findOrCreateOMSM opts libEnv fileVersionKey dbCache1 doSave
            globalAnnotations libName documentLocIdBase $ dgn_nf nodeLabel

        (freeNormalFormKeyM, freeNormalFormSignatureKeyM, dbCache3) <-
          findOrCreateOMSM opts libEnv fileVersionKey dbCache2 doSave
            globalAnnotations libName documentLocIdBase $ dgn_freenf nodeLabel

        (normalFormSignatureMorphismKeyM, _, dbCache4) <-
          findOrCreateSignatureMorphismM opts libEnv dbCache3 doSave libName
            (nodeId, dgn_nf nodeLabel) globalAnnotations
            (signatureKey, normalFormSignatureKeyM) $
            dgn_sigma nodeLabel

        (freeNormalFormSignatureMorphismKeyM, _, dbCache5) <-
          findOrCreateSignatureMorphismM opts libEnv dbCache4 doSave libName
            (nodeId, dgn_freenf nodeLabel) globalAnnotations
            (signatureKey, freeNormalFormSignatureKeyM) $
            dgn_sigma nodeLabel

        omsLocIdBaseEntity@(Entity omsKey _) <-
          if not doSave
          then do
            omsL <- select $ from $ \loc_id_bases -> do
              where_ (loc_id_bases ^. LocIdBaseLocId ==. val locId
                        &&. loc_id_bases ^. LocIdBaseFileVersionId ==. val fileVersionKey
                        &&. loc_id_bases ^. LocIdBaseKind ==. val Enums.OMS)
              return loc_id_bases

            case omsL of
              [] -> fail ("Persistence.DevGraph.createOMS: OMS not found"
                          ++ locId)
              entity : _ -> return entity
          else do
            conservativityStatusKey <- createConservativityStatus consStatus
            nodeNameRangeKey <- createRange $ srcRange internalNodeName

            serializationKey <- case gTheory of
              G_theory { gTheorySyntax = syntaxM } ->
                findOrCreateSerializationM languageKey syntaxM

            logicKey <- case sublogicOfTh gTheory of
              G_sublogics lid sublogics -> findOrCreateLogic' opts lid sublogics

            actionKey <- insert Action
              { actionEvaluationState = EvaluationStateType.FinishedSuccessfully
              , actionMessage = Nothing
              }
            let omsLocIdBaseValue = LocIdBase
                  { locIdBaseFileVersionId = fileVersionKey
                  , locIdBaseKind = Enums.OMS
                  , locIdBaseLocId = locId
                  }
            omsKey <- insert omsLocIdBaseValue
            let oms = OMS
                  { oMSDocumentId = documentKey
                  , oMSLanguageId = languageKey
                  , oMSLogicId = logicKey
                  , oMSSerializationId = serializationKey
                  , oMSSignatureId = signatureKey
                  , oMSNormalFormId = normalFormKeyM
                  , oMSNormalFormSignatureMorphismId = normalFormSignatureMorphismKeyM
                  , oMSFreeNormalFormId = freeNormalFormKeyM
                  , oMSFreeNormalFormSignatureMorphismId = freeNormalFormSignatureMorphismKeyM
                  , oMSOrigin = omsOrigin
                  , oMSConservativityStatusId = conservativityStatusKey
                  , oMSNameFileRangeId = nodeNameRangeKey
                  , oMSDisplayName = displayName
                  , oMSName = name
                  , oMSNameExtension = nameExtension
                  , oMSNameExtensionIndex = nameExtensionIndex
                  , oMSLabelHasHiding = labelHasHiding nodeLabel
                  , oMSLabelHasFree = labelHasFree nodeLabel
                  , oMSActionId = actionKey
                  , oMSConsistencyStatus = ConsistencyStatusType.Open
                  }
            insertEntityMany [Entity (toSqlKey $ fromSqlKey omsKey) oms]
            return $ Entity omsKey omsLocIdBaseValue

        dbCache6 <- case gTheory of
          G_theory { gTheoryLogic = lid
                   , gTheorySign = extSign
                   } ->
            createSymbols libEnv fileVersionKey dbCache5 doSave libName nodeId
              omsLocIdBaseEntity lid extSign

        dbCache7 <- case gTheory of
          G_theory { gTheoryLogic = lid
                   , gTheorySign = ExtSign { plainSign = sign }
                   , gTheorySens = sentences
                   } ->
            createSentences libEnv fileVersionKey dbCache6 doSave
              globalAnnotations libName nodeId omsLocIdBaseEntity lid sign
              sentences

        dbCache8 <- case gTheory of
          G_theory { gTheoryLogic = lid
                   , gTheorySign = extSign
                   } ->
            if doSave && signatureIsNew
            then associateSymbolsOfSignature libEnv dbCache7 libName nodeId
                   lid extSign signatureKey
            else return dbCache7

        return ( omsKey
               , signatureKey
               , addNodeToCache libName nodeId omsKey signatureKey dbCache8
               )
  where
    omsOrigin :: OMSOrigin
    omsOrigin = case node_origin $ nodeInfo nodeLabel of
      DGEmpty -> OMSOrigin.DGEmpty
      DGBasic -> OMSOrigin.DGBasic
      DGBasicSpec{} -> OMSOrigin.DGBasicSpec
      DGExtension -> OMSOrigin.DGExtension
      DGLogicCoercion -> OMSOrigin.DGLogicCoercion
      DGTranslation _ -> OMSOrigin.DGTranslation
      DGUnion -> OMSOrigin.DGUnion
      DGIntersect -> OMSOrigin.DGIntersect
      DGExtract -> OMSOrigin.DGExtract
      DGRestriction _ _ -> OMSOrigin.DGRestriction
      DGRevealTranslation -> OMSOrigin.DGRevealTranslation
      DGFreeOrCofree Free -> OMSOrigin.Free
      DGFreeOrCofree Cofree -> OMSOrigin.Cofree
      DGFreeOrCofree NPFree -> OMSOrigin.NPFree
      DGFreeOrCofree Minimize -> OMSOrigin.Minimize
      DGLocal -> OMSOrigin.DGLocal
      DGClosed -> OMSOrigin.DGClosed
      DGLogicQual -> OMSOrigin.DGLogicQual
      DGData -> OMSOrigin.DGData
      DGFormalParams -> OMSOrigin.DGFormalParams
      DGVerificationGeneric -> OMSOrigin.DGVerificationGeneric
      DGImports -> OMSOrigin.DGImports
      DGInst _ -> OMSOrigin.DGInst
      DGFitSpec -> OMSOrigin.DGFitSpec
      DGFitView _ -> OMSOrigin.DGFitView
      DGProof -> OMSOrigin.DGProof
      DGNormalForm _ -> OMSOrigin.DGNormalForm
      DGintegratedSCC -> OMSOrigin.DGintegratedSCC
      DGFlattening -> OMSOrigin.DGFlattening
      DGAlignment -> OMSOrigin.DGAlignment
      DGTest -> OMSOrigin.DGTest


createConservativityStatus :: MonadIO m
                           => ConsStatus -> DBMonad m ConservativityStatusId
createConservativityStatus (ConsStatus r p _) =
  insert SchemaClass.ConservativityStatus
    { conservativityStatusRequired = toString r
    , conservativityStatusProved = toString p
    }
  where
    toString :: Conservativity -> String
    toString c = case c of
      Unknown s -> s
      _ -> map toLower $ show c

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

findOrCreateSignatureMorphism :: MonadIO m
                              => HetcatsOpts -> LibEnv -> DBCache -> Bool
                              -> LibName -> (Int, Int) -> GlobalAnnos
                              -> (SignatureId, SignatureId)
                              -> GMorphism
                              -> DBMonad m ( SignatureMorphismId
                                           , [SymbolMappingId]
                                           , DBCache
                                           )
findOrCreateSignatureMorphism opts libEnv dbCache doSave libName edge
  globalAnnotations (sourceSignatureKey, targetSignatureKey) gMorphism =
    case gMorphism of
      GMorphism { gMorphismComor = cid
                , gMorphismMorIdx = morphismId
                } ->
        case Map.lookup (libName, morphismId) $ signatureMorphismMap dbCache of
          Just (signatureMorphismKey, symbolMappingKeys, _) ->
            return (signatureMorphismKey, symbolMappingKeys, dbCache)
          Nothing ->
            let json = ppJson $ ToJson.gmorph opts globalAnnotations gMorphism
            in do
                (_, logicMappingKey) <-
                  findOrCreateLanguageMappingAndLogicMapping opts $ Comorphism cid
                signatureMorphismKey <-
                  if doSave
                  then insert SignatureMorphism
                        { signatureMorphismLogicMappingId = logicMappingKey
                        , signatureMorphismAsJson = json
                        , signatureMorphismSourceId = sourceSignatureKey
                        , signatureMorphismTargetId = targetSignatureKey
                        }
                  else do
                    signatureMorphismL <- select $ from $ \signature_morphisms -> do
                      where_ (signature_morphisms ^. SignatureMorphismLogicMappingId ==. val logicMappingKey
                                &&. signature_morphisms ^. SignatureMorphismSourceId ==. val sourceSignatureKey
                                &&. signature_morphisms ^. SignatureMorphismTargetId ==. val targetSignatureKey
                                &&. signature_morphisms ^. SignatureMorphismAsJson ==. val json)
                      return signature_morphisms
                    case signatureMorphismL of
                      [] -> fail "Persistence.DevGraph.findOrCreateSignatureMorphism: not found "
                      Entity key _ : _ -> return key

                (symbolMappingKeys, dbCache1) <-
                  findOrCreateSymbolMappings libEnv dbCache doSave libName edge
                    signatureMorphismKey gMorphism

                let signatureMorphismMap' =
                      Map.insert (libName, morphismId)
                        (signatureMorphismKey, symbolMappingKeys, gMorphism) $
                        signatureMorphismMap dbCache1
                let dbCache2 =
                      dbCache1 { signatureMorphismMap = signatureMorphismMap' }
                return ( signatureMorphismKey
                       , symbolMappingKeys
                       , dbCache2
                       )

findOrCreateSymbolMappings :: MonadIO m
                           => LibEnv -> DBCache -> Bool -> LibName -> (Int, Int)
                           -> SignatureMorphismId -> GMorphism
                           -> DBMonad m ([SymbolMappingId], DBCache)
findOrCreateSymbolMappings libEnv dbCache doSave libName edge
  signatureMorphismKey gMorphism = case gMorphism of
    GMorphism { gMorphismComor = cid
              , gMorphismMor = morphism
              , gMorphismSign = extSign@ExtSign { plainSign = sign }
              } ->
      let sourceLid = sourceLogic cid
          targetLid = targetLogic cid
          symbolMap = symmap_of targetLid morphism
      in  do
            symbolMappingKeys <-
              concatMapM
                (\ sourceSymbol ->
                  concatMapM
                    (\ translatedSymbol ->
                      case Map.lookup translatedSymbol symbolMap of
                        Nothing -> return []
                        Just targetSymbol -> do
                            symbolMappingKey <-
                              findOrCreateSymbolMapping libEnv dbCache doSave
                                libName edge signatureMorphismKey sourceLid
                                targetLid sourceSymbol targetSymbol
                            return [symbolMappingKey]
                    ) $ Set.toList $ map_symbol cid sign sourceSymbol
                ) $ Set.toList $ symset_of sourceLid $ plainSign extSign
            return (symbolMappingKeys, dbCache)

findOrCreateSymbolMapping :: ( MonadIO 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 doSave libName (sourceId, targetId)
  signatureMorphismKey sourceLid targetLid sourceSymbol targetSymbol = do
  sourceKey <-
    fromJustFail (symbolErrorMessage libEnv libName sourceId sourceSymbol sourceLid "source") $
      findSymbolInCache libEnv libName sourceId sourceLid sourceSymbol dbCache

  targetKey <-
    fromJustFail (symbolErrorMessage libEnv libName targetId targetSymbol targetLid "target") $
      findSymbolInCache libEnv libName targetId targetLid targetSymbol dbCache

  symbolMappingL <- select $ from $ \symbol_mappings -> do
    where_ (symbol_mappings ^. SymbolMappingSignatureMorphismId ==. val signatureMorphismKey
              &&. symbol_mappings ^. SymbolMappingSourceId ==. val sourceKey
              &&. symbol_mappings ^. SymbolMappingTargetId ==. val targetKey)
    return symbol_mappings
  case symbolMappingL of
    Entity symbolMappingKey _ : _ -> return symbolMappingKey
    [] ->
      if doSave
      then insert SymbolMapping
            { symbolMappingSignatureMorphismId = signatureMorphismKey
            , symbolMappingSourceId = sourceKey
            , symbolMappingTargetId = targetKey
            }
      else fail "Persistence.DevGraph.findOrCreateSymbolMapping: not found"

symbolErrorMessage :: Sentences lid sentence sign morphism symbol
                   => LibEnv -> LibName -> Node -> symbol -> lid -> String
                   -> String
symbolErrorMessage libEnv libName nodeId symbol lid end =
  let (libNameDereferenced, nodeIdDereferenced) = dereferenceNodeId libEnv libName nodeId
      fullName = show $ fullSymName lid symbol
      symbolKind = symKind lid symbol
      nodeName = show $ getName $ dgn_name $ getNodeLabel libEnv libName nodeId
  in  "Could not find " ++ end ++ " symbol for SymbolMapping:"
      ++ "\nsymbol name: " ++ fullName
      ++ "\nsymbol kind: " ++ symbolKind
      ++ "\nnode name: " ++ nodeName
      ++ "\nnode ID: " ++ show nodeIdDereferenced
      ++ "\nlibrary name: " ++ show libNameDereferenced
      ++ "\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 languageKey syntaxM =
  case syntaxM of
    Nothing -> return Nothing
    Just syntaxIRI -> do
      let syntaxIRIString = show $ setAngles False syntaxIRI
      serializationL <- select $ from $ \serializations -> do
        where_ (serializations ^. SerializationName ==. val syntaxIRIString)
        return serializations
      case serializationL of
        Entity serializationKey _ : _ -> return $ Just serializationKey
        [] -> do
          serializationKey <- insert Serialization
            { serializationLanguageId = languageKey
            , serializationSlug = parameterize syntaxIRIString
            , serializationName = syntaxIRIString
            }
          return $ Just serializationKey

findLanguage :: ( MonadIO m
                , Logic.Logic lid sublogics
                    basic_spec sentence symb_items symb_map_items
                    sign morphism symbol raw_symbol proof_tree
                )
             => lid -> DBMonad m LanguageId
findLanguage lid = do
  languageL <- select $ from $ \languages -> do
    where_ (languages ^. LanguageSlug ==. val (parameterize $ show lid))
    return languages
  case languageL of
    Entity key _ : _ -> return key
    [] -> fail ("Language not found in the database: " ++ show lid)

findOrCreateLogic' :: ( MonadIO 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' opts lid sublogic = do
  languageKey <- findLanguage lid
  findOrCreateLogic opts languageKey lid 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 sigId languageKey =
  case Map.lookup (libName, sigId) $ signatureMap dbCache of
    Just signatureKey -> return (signatureKey, False, dbCache)
    Nothing -> do
      signatureKey <- insert Signature
        { signatureLanguageId = languageKey
        , signatureAsJson = ppJson $ ToJson.symbols lid extSign
        }
      return ( signatureKey
             , True
             , addSignatureToCache libName sigId signatureKey dbCache
             )

createSymbols :: ( MonadIO 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 fileVersionKey dbCache doSave libName nodeId omsLocIdBase
  lid ExtSign { plainSign = sign } =
  foldM (\ dbCacheAcc symbol ->
          findOrCreateSymbol libEnv fileVersionKey dbCacheAcc doSave libName
            nodeId omsLocIdBase lid symbol
        ) dbCache $ symlist_of lid sign

findOrCreateSymbol :: ( MonadIO 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 fileVersionKey dbCache doSave libName nodeId
  omsLocIdBase@(Entity omsKey _) lid symbol =
    let (locId, name, fullName, symbolKind) =
          symbolDetails omsLocIdBase lid symbol
    in  if symbolIsCached libEnv libName nodeId lid symbol dbCache
        then return dbCache
        else do
          symbolKey <-
            if doSave
            then do
              symbolKey <- insert LocIdBase
                { locIdBaseFileVersionId = fileVersionKey
                , locIdBaseKind = Enums.Symbol
                , locIdBaseLocId = locId
                }
              let symbolValue = Symbol
                    { symbolOmsId = omsKey
                    , symbolFileRangeId = Nothing
                    , symbolSymbolKind = symbolKind
                    , symbolName = name
                    , symbolFullName = Text.pack fullName
                    }
              insertEntityMany [Entity (toSqlKey $ fromSqlKey symbolKey) symbolValue]
              return symbolKey
            else do
              symbolL <- select $ from $ \loc_id_bases -> do
                where_ (loc_id_bases ^. LocIdBaseLocId ==. val locId
                          &&. loc_id_bases ^. LocIdBaseFileVersionId ==. val fileVersionKey
                          &&. loc_id_bases ^. LocIdBaseKind ==. val Enums.Symbol)
                return loc_id_bases
              case symbolL of
                [] -> fail ("Persistence.DevGraph.findOrCreateSymbol: "
                                 ++ "Symbol not found: " ++ locId)
                Entity symbolKey _ : _ -> return symbolKey
          return $ addSymbolToCache libEnv libName nodeId lid symbol symbolKey dbCache

createSentences :: ( MonadIO 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 fileVersionKey dbCache0 doSave globalAnnotations libName
  nodeId omsLocId lid sign sentences =
  let (axioms, conjectures) = OMap.partition isAxiom sentences
      namedAxioms = toNamedList axioms
      orderedConjectures = OMap.toList conjectures
  in do
    dbCache1 <- createAxioms libEnv fileVersionKey dbCache0 doSave
      globalAnnotations libName nodeId omsLocId lid sign namedAxioms
    createConjectures libEnv fileVersionKey dbCache1 doSave
      globalAnnotations libName nodeId omsLocId lid sign orderedConjectures

createAxioms :: ( MonadIO 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 fileVersionKey dbCache doSave globalAnnotations libName
  nodeId omsLocId lid sign =
  foldM (\ dbCacheAcc namedAxiom -> do
          (axiomKey, dbCacheAcc1) <-
            createSentence libEnv fileVersionKey dbCacheAcc doSave globalAnnotations
              omsLocId lid sign False False namedAxiom
          associateSymbolsOfSentence libEnv fileVersionKey dbCacheAcc1 doSave
            libName nodeId omsLocId axiomKey lid sign namedAxiom
        ) dbCache

createConjectures :: ( MonadIO 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 fileVersionKey dbCache doSave globalAnnotations libName
  nodeId omsLocId lid sign =
  foldM (\ dbCacheAcc (name, senStatus) ->
          let namedConjecture = toNamed name senStatus
              isProved = isProvenSenStatus senStatus
          in do
            (conjectureKey, dbCacheAcc1) <-
              createSentence libEnv fileVersionKey dbCacheAcc doSave globalAnnotations
                omsLocId lid sign True isProved namedConjecture
            associateSymbolsOfSentence libEnv fileVersionKey dbCacheAcc1 doSave
              libName nodeId omsLocId conjectureKey lid sign namedConjecture
        ) dbCache

createSentence :: ( MonadIO 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 fileVersionKey dbCache doSave globalAnnotations
  omsLocIdBase@(Entity omsKey _) lid sign isConjecture isProved namedSentence =
  let name = senAttr namedSentence
      range = getRangeSpan $ sentence namedSentence
      locId = locIdOfSentence omsLocIdBase name
      text = show $ useGlobalAnnos globalAnnotations $
               print_named lid $ makeNamed "" $
               simplify_sen lid sign $ sentence namedSentence
      kind =
        if isConjecture
        then if isProved
             then Enums.Theorem
             else Enums.OpenConjecture
        else Enums.Axiom
      evaluationState =
        if isProved
        then EvaluationStateType.FinishedSuccessfully
        else EvaluationStateType.NotYetEnqueued
      proofStatus =
        if isProved
        then Enums.THM
        else Enums.OPN
  in  do
        sentenceKey <-
          if doSave
          then do
               originalSentenceKeyM <-
                 findOriginalSentence libEnv fileVersionKey dbCache lid namedSentence
               rangeKeyM <- createRange range
               sentenceKey <- insert LocIdBase
                 { locIdBaseFileVersionId = fileVersionKey
                 , locIdBaseKind = kind
                 , locIdBaseLocId = locId
                 }
               let sentenceValue = Sentence
                     { sentenceOmsId = omsKey
                     , sentenceFileRangeId = rangeKeyM
                     , sentenceName = name
                     , sentenceText = Text.pack text
                     , sentenceOriginalSentenceId = originalSentenceKeyM
                     }
               insertEntityMany [Entity (toSqlKey $ fromSqlKey sentenceKey) sentenceValue]
               if isConjecture
               then do
                      actionKey <- insert Action
                        { actionEvaluationState = evaluationState
                        , actionMessage = Nothing
                        }
                      let conjecture = Conjecture
                            { conjectureActionId = actionKey
                            , conjectureProofStatus = proofStatus
                            }
                      insertEntityMany [Entity (toSqlKey $ fromSqlKey sentenceKey) conjecture]
               else let axiom = Axiom { }
                    in insertEntityMany [Entity (toSqlKey $ fromSqlKey sentenceKey) axiom]
               return sentenceKey
            else do
              sentenceL <- select $ from $ \loc_id_bases -> do
                where_ (loc_id_bases ^. LocIdBaseLocId ==. val locId
                          &&. loc_id_bases ^. LocIdBaseFileVersionId ==. val fileVersionKey
                          &&. loc_id_bases ^. LocIdBaseKind ==. val kind)
                return loc_id_bases
              case sentenceL of
                [] -> fail ("Persistence.DevGraph.createSentence: Sentence not found"
                            ++ locId)
                Entity sentenceKey _ : _-> return sentenceKey
        return (sentenceKey, dbCache)

findOriginalSentence :: ( MonadIO 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 fileVersionKey dbCache _ namedSentence =
  case senOrigin namedSentence of
    Nothing -> return Nothing
    Just origin -> do
      let originLibNameIRI = dGraphName origin
      let originNodeId_ = originNodeId origin
      let originSentenceName = senName origin

      let filterPredicate libName _ = originLibNameIRI == iriOfLibName libName
      originDGraph <- case Map.toList $ Map.filterWithKey filterPredicate libEnv of
        [] -> fail ("Persistence.DevGraph.findOriginalSentence: Could not find dGraph named " ++ show originLibNameIRI)
        (_, dg) : _ -> return dg
      let nodeLabel = Graph.nodeLabel $ fromJust $ IntMap.lookup originNodeId_ $ convertToMap $ dgBody originDGraph

      let documentKey = fromJust $ Map.lookup originLibNameIRI $ documentByLibNameIRIMap dbCache
      documentLocIdBase <- fmap fromJust $ get documentKey
      let documentEntity = Entity documentKey documentLocIdBase
      let omsLocId = locIdOfOMS documentEntity nodeLabel
      omsLocIdBaseM <- findOMS fileVersionKey documentEntity nodeLabel
      omsLocIdBase <- case omsLocIdBaseM of
        Nothing -> fail ("Persistence.DevGraph.findOriginalSentence: Could not find OMS " ++ omsLocId)
        Just x -> return x
      let locIdOfOriginalSentence = locIdOfSentence omsLocIdBase originSentenceName
      sentenceM <- findSentence fileVersionKey locIdOfOriginalSentence
      (Entity sentenceKey _) <- case sentenceM of
        Nothing -> fail ("Persistence.DevGraph.findOriginalSentence: Could not find Sentence " ++ locIdOfOriginalSentence)
        Just x -> return x
      return $ Just sentenceKey

associateSymbolsOfSentence :: ( MonadIO 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 fileVersionKey dbCache doSave libName nodeId
  omsLocIdBase sentenceKey lid sign namedSentence =
  let symbolsOfSentence = symsOfSen lid sign $ sentence namedSentence
  in  do
        (dbCache', _) <-
          foldM (\ (dbCacheAcc, associatedSymbols) symbol ->
                  let mapIndex = symbolMapIndex lid symbol
                  in  if Set.member mapIndex associatedSymbols
                      then return (dbCacheAcc, associatedSymbols)
                      else case findSymbolInCache libEnv libName nodeId lid symbol dbCacheAcc of
                             Just symbolKey -> do
                               when doSave $
                                 insert SentenceSymbol
                                   { sentenceSymbolSentenceId = sentenceKey
                                   , sentenceSymbolSymbolId = symbolKey
                                   } >> return ()
                               return ( dbCacheAcc
                                      , Set.insert mapIndex associatedSymbols
                                      )
                             Nothing -> do
                               dbCacheAcc' <-
                                 findOrCreateSymbol libEnv fileVersionKey
                                   dbCacheAcc doSave libName nodeId omsLocIdBase
                                   lid symbol
                               return ( dbCacheAcc'
                                      , Set.insert mapIndex associatedSymbols
                                      )
                ) (dbCache, Set.empty) symbolsOfSentence
        return 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 nodeId lid extSign signatureKey =
  let ownSymbols = nonImportedSymbols extSign
      allSymbols = symset_of lid $ plainSign extSign
  in do
       foldM_
         (\ associatedSymbols symbol ->
           let mapIndex = symbolMapIndex lid symbol
               symbolKey =
                 fromJust $ findSymbolInCache libEnv libName nodeId lid symbol
                   dbCache
               imported = Set.member symbol ownSymbols
           in  if Set.member mapIndex associatedSymbols
               then return associatedSymbols
               else do
                 insert SignatureSymbol
                   { signatureSymbolSignatureId = signatureKey
                   , signatureSymbolSymbolId = symbolKey
                   , signatureSymbolImported = imported
                   }
                 return $ Set.insert mapIndex associatedSymbols
         ) Set.empty allSymbols
       return dbCache

createMapping :: MonadIO m
              => HetcatsOpts -> LibEnv -> FileVersionId -> DBCache -> Bool
              -> GlobalAnnos -> LibName -> Entity LocIdBase
              -> (Int, Int, DGLinkLab) -> DBMonad m DBCache
createMapping opts libEnv fileVersionKey dbCache doSave globalAnnotations
  libName documentLocIdBase (sourceId, targetId, linkLabel) = do
  (sourceOMSKey, sourceSignatureKey) <-
    case Map.lookup (libName, sourceId) $ nodeMap dbCache of
      Just (omsKey, signatureKey) -> return (omsKey, signatureKey)
      Nothing -> fail ("Persistence.DevGraph.createMapping: Could not find source node with ID " ++ show (libName, sourceId))

  (targetOMSKey, targetSignatureKey) <-
    case Map.lookup (libName, targetId) $ nodeMap dbCache of
      Just (omsKey, signatureKey) -> return (omsKey, signatureKey)
      Nothing -> fail ("Persistence.DevGraph.createMapping: Could not find target node with ID " ++ show (libName, targetId))

  (signatureMorphismKey, _, dbCache1) <-
    findOrCreateSignatureMorphism opts libEnv dbCache True libName
      (sourceId, targetId) globalAnnotations
      (sourceSignatureKey, targetSignatureKey) $ dgl_morphism linkLabel

  let displayName = if null $ dglName linkLabel
                    then show (dgl_id linkLabel)
                    else dglName linkLabel
  let locId = locIdOfMapping documentLocIdBase displayName
  mappingL <- select $ from $ \loc_id_bases -> do
    where_ (loc_id_bases ^. LocIdBaseFileVersionId ==. val fileVersionKey
              &&. loc_id_bases ^. LocIdBaseKind ==. val Enums.Mapping
              &&. loc_id_bases ^. LocIdBaseLocId ==. val locId)
    return loc_id_bases
  if null mappingL
  then do
    conservativityStatusKeyM <- case dgl_type linkLabel of
      ScopedLink _ _ consStatus ->
        fmap Just $ createConservativityStatus consStatus
      _ -> return Nothing

    (freenessParameterOMSKeyM, dbCache2) <- case dgl_type linkLabel of
      FreeOrCofreeDefLink _ (JustNode NodeSig { getNode = nodeId }) -> do
        let nodeLabel = getNodeLabel libEnv libName nodeId
        (freenessParameterOMSKey, _, dbCache') <-
          findOrCreateOMS opts libEnv fileVersionKey dbCache1 doSave
            globalAnnotations libName documentLocIdBase (nodeId, nodeLabel)
        return (Just freenessParameterOMSKey, dbCache')
      _ -> return (Nothing, dbCache)

    freenessParameterLanguageKeyM <- case dgl_type linkLabel of
      FreeOrCofreeDefLink _ (EmptyNode (Logic.Logic lid)) ->
        fmap Just $ findLanguage lid
      _ -> return Nothing

    mappingKey <- insert LocIdBase
      { locIdBaseFileVersionId = fileVersionKey
      , locIdBaseKind = Enums.Mapping
      , locIdBaseLocId = locId
      }
    let mapping = Mapping
          { mappingSourceId = sourceOMSKey
          , mappingTargetId = targetOMSKey
          , mappingSignatureMorphismId = signatureMorphismKey
          , mappingConservativityStatusId = conservativityStatusKeyM
          , mappingFreenessParameterOMSId = freenessParameterOMSKeyM
          , mappingFreenessParameterLanguageId = freenessParameterLanguageKeyM
          , mappingDisplayName = displayName
          , mappingName = dglName linkLabel
          , mappingType = mappingTypeOfLinkLabel
          , mappingOrigin = mappingOriginOfLinkLabel
          , mappingPending = dglPending linkLabel
          }
    insertEntityMany [Entity (toSqlKey $ fromSqlKey mappingKey) mapping]
    return dbCache2
  else return dbCache1
  where
    mappingOriginOfLinkLabel :: MappingOrigin
    mappingOriginOfLinkLabel = case dgl_origin linkLabel of
      SeeTarget -> MappingOrigin.SeeTarget
      SeeSource -> MappingOrigin.SeeSource
      TEST -> MappingOrigin.TEST
      DGLinkVerif -> MappingOrigin.DGLinkVerif
      DGImpliesLink -> MappingOrigin.DGImpliesLink
      DGLinkExtension -> MappingOrigin.DGLinkExtension
      DGLinkTranslation -> MappingOrigin.DGLinkTranslation
      DGLinkClosedLenv -> MappingOrigin.DGLinkClosedLenv
      DGLinkImports -> MappingOrigin.DGLinkImports
      DGLinkIntersect -> MappingOrigin.DGLinkIntersect
      DGLinkMorph _ -> MappingOrigin.DGLinkMorph
      DGLinkInst _ _ -> MappingOrigin.DGLinkInst
      DGLinkInstArg _ -> MappingOrigin.DGLinkInstArg
      DGLinkView _ _ -> MappingOrigin.DGLinkView
      DGLinkAlign _ -> MappingOrigin.DGLinkAlign
      DGLinkFitView _ -> MappingOrigin.DGLinkFitView
      DGLinkFitViewImp _ -> MappingOrigin.DGLinkFitViewImp
      DGLinkProof -> MappingOrigin.DGLinkProof
      DGLinkFlatteningUnion -> MappingOrigin.DGLinkFlatteningUnion
      DGLinkFlatteningRename -> MappingOrigin.DGLinkFlatteningRename
      DGLinkRefinement _ -> MappingOrigin.DGLinkRefinement

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


cachedOMSKey :: LibName -> Int -> DBCache -> Maybe (LocIdBaseId, SignatureId)
cachedOMSKey libName nodeId = Map.lookup (libName, nodeId) . nodeMap

symbolIsCached :: Sentences lid sentence sign morphism symbol
               => LibEnv -> LibName -> Int -> lid -> symbol -> DBCache -> Bool
symbolIsCached libEnv libName nodeId lid symbol =
  isJust . findSymbolInCache libEnv libName nodeId lid symbol

-- Gives the node label to an id. Use only if the combination exists.
getNodeLabel :: LibEnv -> LibName -> Int -> DGNodeLab
getNodeLabel libEnv libName nodeId =
  fromJust $ fmap Graph.nodeLabel $ IntMap.lookup nodeId $ convertToMap $
    dgBody $ fromJust $ Map.lookup libName libEnv

dereferenceNodeId :: LibEnv -> LibName -> Int -> (LibName, Int)
dereferenceNodeId libEnv libName nodeId =
  case nodeInfo $ getNodeLabel libEnv libName nodeId of
    DGNode {} -> (libName, nodeId)
    DGRef { ref_node = refNodeId
          , ref_libname = refLibName
          } -> dereferenceNodeId libEnv refLibName refNodeId

addDocumentToCache :: LibName -> LocIdBaseId -> DBCache -> DBCache
addDocumentToCache libName documentKey dbCache =
  dbCache { documentMap = Map.insert libName documentKey $ documentMap dbCache
          , documentByLibNameIRIMap = Map.insert (iriOfLibName libName) documentKey $ documentByLibNameIRIMap dbCache
          }

iriOfLibName :: LibName -> IRI
iriOfLibName = filePathToLibId . libToFileName

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

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

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

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

findOMS :: MonadIO m
        => FileVersionId -> Entity LocIdBase -> DGNodeLab
        -> DBMonad m (Maybe (Entity LocIdBase))
findOMS fileVersionKey documentLocIdBase nodeLabel = do
  omsLocIdL <- select $ from $ \loc_id_bases -> do
    where_ (loc_id_bases ^. LocIdBaseFileVersionId ==. val fileVersionKey
              &&. loc_id_bases ^. LocIdBaseKind ==. val Enums.OMS
              &&. loc_id_bases ^. LocIdBaseLocId ==. val (locIdOfOMS documentLocIdBase nodeLabel))
    return loc_id_bases
  case omsLocIdL of
    [] -> return Nothing
    entity : _ -> return $ Just entity

findOMSAndSignature :: MonadIO m
                    => FileVersionId -> Entity LocIdBase -> DGNodeLab
                    -> DBMonad m (Maybe (LocIdBaseId, SignatureId))
findOMSAndSignature fileVersionKey documentLocIdBase nodeLabel = do
  omsLocIdBaseM <- findOMS fileVersionKey documentLocIdBase nodeLabel
  case omsLocIdBaseM of
    Nothing -> return Nothing
    Just (Entity omsKey _) -> do
      omsValueL <- select $ from $ \omsSql -> do
        where_ (omsSql ^. OMSId ==. val (toSqlKey $ fromSqlKey omsKey))
        return omsSql
      omsValue <- case omsValueL of
        [] ->
          fail ("Persistence.DevGraph.findOMSAndSignature could not find OMS with ID "
                ++ show (unSqlBackendKey $ unLocIdBaseKey omsKey))
        Entity _ omsValue : _ -> return omsValue
      return $ Just (omsKey, oMSSignatureId omsValue)

findSentence :: MonadIO m
             => FileVersionId -> String
             -> DBMonad m (Maybe (Entity LocIdBase))
findSentence fileVersionKey locId = do
  sentenceL <- select $ from $ \loc_id_bases -> do
    where_ (loc_id_bases ^. LocIdBaseFileVersionId ==. val fileVersionKey
              &&. loc_id_bases ^. LocIdBaseKind `in_` valList [ Enums.OpenConjecture
                                                              , Enums.Theorem
                                                              , Enums.CounterTheorem
                                                              , Enums.Axiom
                                                              ]
              &&. loc_id_bases ^. LocIdBaseLocId ==. val locId)
    return loc_id_bases
  case sentenceL of
    [] -> return Nothing
    entity : _ -> return $ Just entity


symbolMapIndex :: Sentences lid sentence sign morphism symbol
               => lid -> symbol -> SymbolMapIndex
symbolMapIndex lid symbol =
  let fullName = show $ fullSymName lid symbol
      symbolKind = symKind lid symbol
  in (symbolKind, fullName)




createDocumentLinks :: MonadIO m
                    => DBCache -> Rel LibName
                    -> DBMonad m ()
createDocumentLinks dbCache dependencyLibNameRel =
  mapM_ (\ (targetLibName, sourceLibNamesSet) ->
          mapM_ (createDocumentLink targetLibName) $
            Set.toList sourceLibNamesSet
        ) $ Map.toList $ Rel.toMap dependencyLibNameRel
  where
    createDocumentLink :: MonadIO m
                       => LibName -> LibName -> DBMonad m ()
    createDocumentLink sourceLibName targetLibName = do
      -- These libNames must be in the documentMap by construction
      let sourceKey = fromJust $ Map.lookup sourceLibName $ documentMap dbCache
      let targetKey = fromJust $ Map.lookup targetLibName $ documentMap dbCache
      insert DocumentLink { documentLinkSourceId = sourceKey
                          , documentLinkTargetId = targetKey
                          }
      return ()


fromJustFail :: MonadIO m => String -> Maybe a -> m a
fromJustFail message maybeValue = case maybeValue of
  Just value -> return value
  Nothing -> fail message
