content: {-# 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
    { 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.fail message
  
  createDocuments :: (MonadIO m, Fail.MonadFail 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, Fail.MonadFail 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, Fail.MonadFail 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, Fail.MonadFail 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, Fail.MonadFail 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, Fail.MonadFail 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, Fail.MonadFail 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, Fail.MonadFail 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.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, Fail.MonadFail 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, Fail.MonadFail 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.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, Fail.MonadFail 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
                               , 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 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.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
                  , 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 = do
    languageL <- select $ from $ \languages -> do
      where_ (languages ^. LanguageSlug ==. val (parameterize $ show lid))
      return languages
    case languageL of
      Entity key _ : _ -> return key
      [] -> Fail.fail ("Language not found in the database: " ++ show 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' 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
                   , 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 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
                        , 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 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.fail ("Persistence.DevGraph.findOrCreateSymbol: "
                                   ++ "Symbol not found: " ++ locId)
                  Entity symbolKey _ : _ -> return symbolKey
            return $ addSymbolToCache libEnv libName nodeId lid symbol symbolKey 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 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
                  , 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 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
                       , 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 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
                    , 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 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.fail ("Persistence.DevGraph.createSentence: Sentence not found"
                              ++ locId)
                  Entity sentenceKey _ : _-> return sentenceKey
          return (sentenceKey, 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 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.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.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.fail ("Persistence.DevGraph.findOriginalSentence: Could not find Sentence " ++ locIdOfOriginalSentence)
          Just x -> return x
        return $ Just 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 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, Fail.MonadFail 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.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.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, Fail.MonadFail 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.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, Fail.MonadFail m) => String -> Maybe a -> m a
  fromJustFail message maybeValue = case maybeValue of
    Just value -> return value
    Nothing -> Fail.fail message
  