{- |
Module      :  ./Proofs/QualifyNames.hs
Description :  qualify all names in the nodes of development graphs
Copyright   :  (c) Igor Stassiy, C.Maeder DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

qualify and disambiguate all names in the nodes of a development graph for
OMDoc output or for writing out multiple theories for Isabelle or VSE.  Note
however that signature will be always be complete, i.e. imported entities
will be repeated.
-}

module Proofs.QualifyNames (qualifyLibEnv) where

import Logic.Coerce
import Logic.Comorphism
import Logic.ExtSign
import Logic.Grothendieck
import Logic.Logic
import Logic.Prover

import Static.DevGraph
import Static.DgUtils
import Static.GTheory
import Static.History
import Static.ComputeTheory

import Common.DocUtils
import Common.ExtSign
import Common.Id
import Common.LibName
import Common.Result

import Data.Graph.Inductive.Graph
import Data.List
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set
import Control.Monad
import qualified Control.Monad.Fail as Fail

qualifyLibEnv :: LibEnv -> Result LibEnv
qualifyLibEnv :: LibEnv -> Result LibEnv
qualifyLibEnv libEnv :: LibEnv
libEnv = ((LibEnv, Map LibName RenameMap) -> LibEnv)
-> Result (LibEnv, Map LibName RenameMap) -> Result LibEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (LibEnv, Map LibName RenameMap) -> LibEnv
forall a b. (a, b) -> a
fst
  (Result (LibEnv, Map LibName RenameMap) -> Result LibEnv)
-> Result (LibEnv, Map LibName RenameMap) -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ ((LibEnv, Map LibName RenameMap)
 -> LibName -> Result (LibEnv, Map LibName RenameMap))
-> (LibEnv, Map LibName RenameMap)
-> [LibName]
-> Result (LibEnv, Map LibName RenameMap)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (le :: LibEnv
le, m :: Map LibName RenameMap
m) ln :: LibName
ln -> do
    DGraph
dg0 <- (LibEnv, Map LibName RenameMap) -> DGraph -> Result DGraph
updateRefNodes (LibEnv
le, Map LibName RenameMap
m) (DGraph -> Result DGraph) -> DGraph -> Result DGraph
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
    (dg :: DGraph
dg, trm :: RenameMap
trm) <- LibName -> DGraph -> Result (DGraph, RenameMap)
qualifyDGraph LibName
ln DGraph
dg0
    (LibEnv, Map LibName RenameMap)
-> Result (LibEnv, Map LibName RenameMap)
forall (m :: * -> *) a. Monad m => a -> m a
return ( LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln (LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
le LibName
ln DGraph
dg) LibEnv
le
           , LibName
-> RenameMap -> Map LibName RenameMap -> Map LibName RenameMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln RenameMap
trm Map LibName RenameMap
m))
    (LibEnv
libEnv, Map LibName RenameMap
forall k a. Map k a
Map.empty) ([LibName] -> Result (LibEnv, Map LibName RenameMap))
-> [LibName] -> Result (LibEnv, Map LibName RenameMap)
forall a b. (a -> b) -> a -> b
$ LibEnv -> [LibName]
getTopsortedLibs LibEnv
libEnv

type RenameMap = Map.Map Int (GMorphism, GMorphism)

qualifyDGraph :: LibName -> DGraph -> Result (DGraph, RenameMap)
qualifyDGraph :: LibName -> DGraph -> Result (DGraph, RenameMap)
qualifyDGraph ln :: LibName
ln dg :: DGraph
dg =
  String
-> LibName
-> Result (DGraph, RenameMap)
-> Result (DGraph, RenameMap)
forall a b.
(GetRange a, Pretty a) =>
String -> a -> Result b -> Result b
addErrorDiag "qualification failed for" LibName
ln
  (Result (DGraph, RenameMap) -> Result (DGraph, RenameMap))
-> Result (DGraph, RenameMap) -> Result (DGraph, RenameMap)
forall a b. (a -> b) -> a -> b
$ do
  let es :: [EdgeId]
es = ((Node, Node, DGLinkLab) -> EdgeId)
-> [(Node, Node, DGLinkLab)] -> [EdgeId]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, lb :: DGLinkLab
lb) -> DGLinkLab -> EdgeId
dgl_id DGLinkLab
lb) ([(Node, Node, DGLinkLab)] -> [EdgeId])
-> [(Node, Node, DGLinkLab)] -> [EdgeId]
forall a b. (a -> b) -> a -> b
$ DGraph -> [(Node, Node, DGLinkLab)]
labEdgesDG DGraph
dg
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set EdgeId -> Node
forall a. Set a -> Node
Set.size ([EdgeId] -> Set EdgeId
forall a. Ord a => [a] -> Set a
Set.fromList [EdgeId]
es) Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== [EdgeId] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [EdgeId]
es) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$
    String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "inkonsistent graph for library " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LibName -> String -> String
forall a. Pretty a => a -> String -> String
showDoc LibName
ln ""
  (dg1 :: DGraph
dg1, trm :: RenameMap
trm) <- ((DGraph, RenameMap)
 -> LNode DGNodeLab -> Result (DGraph, RenameMap))
-> (DGraph, RenameMap)
-> [LNode DGNodeLab]
-> Result (DGraph, RenameMap)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LibName
-> (DGraph, RenameMap)
-> LNode DGNodeLab
-> Result (DGraph, RenameMap)
qualifyLabNode LibName
ln) (DGraph
dg, RenameMap
forall k a. Map k a
Map.empty) ([LNode DGNodeLab] -> Result (DGraph, RenameMap))
-> [LNode DGNodeLab] -> Result (DGraph, RenameMap)
forall a b. (a -> b) -> a -> b
$ DGraph -> [LNode DGNodeLab]
topsortedNodes DGraph
dg
  (DGraph, RenameMap) -> Result (DGraph, RenameMap)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg (String -> DGRule
DGRule "Qualified-Names") DGraph
dg1, RenameMap
trm)

{- consider that loops are part of innDG and outDG that should not be handled
   twice -}
properEdge :: LEdge a -> Bool
properEdge :: LEdge a -> Bool
properEdge (x :: Node
x, y :: Node
y, _) = Node
x Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
y

properInEdges :: DGraph -> Node -> [LEdge DGLinkLab]
properInEdges :: DGraph -> Node -> [(Node, Node, DGLinkLab)]
properInEdges dg :: DGraph
dg n :: Node
n =
  let pes :: [(Node, Node, DGLinkLab)]
pes = ((Node, Node, DGLinkLab) -> Bool)
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Node, Node, DGLinkLab) -> Bool
forall a. LEdge a -> Bool
properEdge ([(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)])
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> [(Node, Node, DGLinkLab)]
innDG DGraph
dg Node
n
      (gs :: [(Node, Node, DGLinkLab)]
gs, rs :: [(Node, Node, DGLinkLab)]
rs) = ((Node, Node, DGLinkLab) -> Bool)
-> [(Node, Node, DGLinkLab)]
-> ([(Node, Node, DGLinkLab)], [(Node, Node, DGLinkLab)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((DGLinkType -> Bool) -> (Node, Node, DGLinkLab) -> Bool
forall a. (DGLinkType -> a) -> (Node, Node, DGLinkLab) -> a
liftE DGLinkType -> Bool
isGlobalDef) [(Node, Node, DGLinkLab)]
pes
  in [(Node, Node, DGLinkLab)]
gs [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, DGLinkLab)]
rs

constructUnion :: Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
            lid -> morphism -> [morphism] -> morphism
constructUnion :: lid -> morphism -> [morphism] -> morphism
constructUnion lid :: lid
lid hd :: morphism
hd l :: [morphism]
l = case [morphism]
l of
  [] -> morphism
hd
  sd :: morphism
sd : tl :: [morphism]
tl -> case Result morphism -> Maybe morphism
forall a. Result a -> Maybe a
maybeResult (Result morphism -> Maybe morphism)
-> Result morphism -> Maybe morphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> morphism -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> morphism -> morphism -> Result morphism
morphism_union lid
lid morphism
hd morphism
sd of
    Just m :: morphism
m -> case Result morphism -> Maybe morphism
forall a. Result a -> Maybe a
maybeResult (Result morphism -> Maybe morphism)
-> Result morphism -> Maybe morphism
forall a b. (a -> b) -> a -> b
$ morphism -> Result morphism
forall object morphism.
Category object morphism =>
morphism -> Result morphism
inverse morphism
m of
      Just _ -> lid -> morphism -> [morphism] -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> [morphism] -> morphism
constructUnion lid
lid morphism
m [morphism]
tl
      Nothing -> lid -> morphism -> [morphism] -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> [morphism] -> morphism
constructUnion lid
lid morphism
sd [morphism]
tl
    Nothing -> lid -> morphism -> [morphism] -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> [morphism] -> morphism
constructUnion lid
lid morphism
sd [morphism]
tl

updateRefNodes :: (LibEnv, Map.Map LibName RenameMap) -> DGraph
               -> Result DGraph
updateRefNodes :: (LibEnv, Map LibName RenameMap) -> DGraph -> Result DGraph
updateRefNodes (le :: LibEnv
le, trm :: Map LibName RenameMap
trm) dgraph :: DGraph
dgraph =
  (DGraph -> LNode DGNodeLab -> Result DGraph)
-> DGraph -> [LNode DGNodeLab] -> Result DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dg :: DGraph
dg (n :: Node
n, lb :: DGNodeLab
lb) ->
     if DGNodeLab -> Bool
isDGRef DGNodeLab
lb then do
     let refLn :: LibName
refLn = DGNodeLab -> LibName
dgn_libname DGNodeLab
lb
         refNode :: Node
refNode = DGNodeLab -> Node
dgn_node DGNodeLab
lb
         gp :: (GMorphism, GMorphism)
gp = (GMorphism, GMorphism)
-> Node -> RenameMap -> (GMorphism, GMorphism)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> (GMorphism, GMorphism)
forall a. HasCallStack => String -> a
error "updateRefNodes2") Node
refNode
           (RenameMap -> (GMorphism, GMorphism))
-> RenameMap -> (GMorphism, GMorphism)
forall a b. (a -> b) -> a -> b
$ RenameMap -> LibName -> Map LibName RenameMap -> RenameMap
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> RenameMap
forall a. HasCallStack => String -> a
error "updateRefNodes1") LibName
refLn Map LibName RenameMap
trm
         refGr :: DGraph
refGr = LibName -> LibEnv -> DGraph
lookupDGraph LibName
refLn LibEnv
le
         gth :: G_theory
gth = DGNodeLab -> G_theory
dgn_theory (DGNodeLab -> G_theory) -> DGNodeLab -> G_theory
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
refGr Node
refNode
         newlb :: DGNodeLab
newlb = DGNodeLab
lb { dgn_theory :: G_theory
dgn_theory = G_theory -> SigId -> ThId -> G_theory
createGThWith G_theory
gth SigId
startSigId ThId
startThId }
     (ds :: [DGChange]
ds, is :: [DGChange]
is) <- DGraph
-> Node
-> [(Node, Node, DGLinkLab)]
-> (GMorphism, GMorphism)
-> Result ([DGChange], [DGChange])
createChanges DGraph
dg Node
n (DGraph -> Node -> [(Node, Node, DGLinkLab)]
properInEdges DGraph
dg Node
n) (GMorphism, GMorphism)
gp
     DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> Result DGraph) -> DGraph -> Result DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg ([DGChange] -> DGraph) -> [DGChange] -> DGraph
forall a b. (a -> b) -> a -> b
$ [DGChange]
ds [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
lb (Node
n, DGNodeLab
newlb) DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange]
is
     else DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg) DGraph
dgraph ([LNode DGNodeLab] -> Result DGraph)
-> [LNode DGNodeLab] -> Result DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dgraph

createChanges :: DGraph -> Node -> [LEdge DGLinkLab] -> (GMorphism, GMorphism)
              -> Result ([DGChange], [DGChange])
createChanges :: DGraph
-> Node
-> [(Node, Node, DGLinkLab)]
-> (GMorphism, GMorphism)
-> Result ([DGChange], [DGChange])
createChanges dg :: DGraph
dg n :: Node
n inss :: [(Node, Node, DGLinkLab)]
inss (gm1 :: GMorphism
gm1, grm :: GMorphism
grm) = do
  let allOuts :: [(Node, Node, DGLinkLab)]
allOuts = DGraph -> Node -> [(Node, Node, DGLinkLab)]
outDG DGraph
dg Node
n
  [(Node, Node, DGLinkLab)]
nAllouts <- ((Node, Node, DGLinkLab) -> Result (Node, Node, DGLinkLab))
-> [(Node, Node, DGLinkLab)] -> Result [(Node, Node, DGLinkLab)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool
-> GMorphism
-> GMorphism
-> (Node, Node, DGLinkLab)
-> Result (Node, Node, DGLinkLab)
composeWithMorphism Bool
False GMorphism
gm1 GMorphism
grm) [(Node, Node, DGLinkLab)]
allOuts
  let (nouts :: [(Node, Node, DGLinkLab)]
nouts, nloops :: [(Node, Node, DGLinkLab)]
nloops) = ((Node, Node, DGLinkLab) -> Bool)
-> [(Node, Node, DGLinkLab)]
-> ([(Node, Node, DGLinkLab)], [(Node, Node, DGLinkLab)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Node, Node, DGLinkLab) -> Bool
forall a. LEdge a -> Bool
properEdge [(Node, Node, DGLinkLab)]
nAllouts
  [(Node, Node, DGLinkLab)]
nAllinss <- ((Node, Node, DGLinkLab) -> Result (Node, Node, DGLinkLab))
-> [(Node, Node, DGLinkLab)] -> Result [(Node, Node, DGLinkLab)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool
-> GMorphism
-> GMorphism
-> (Node, Node, DGLinkLab)
-> Result (Node, Node, DGLinkLab)
composeWithMorphism Bool
True GMorphism
gm1 GMorphism
grm) ([(Node, Node, DGLinkLab)] -> Result [(Node, Node, DGLinkLab)])
-> [(Node, Node, DGLinkLab)] -> Result [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ [(Node, Node, DGLinkLab)]
nloops [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, DGLinkLab)]
inss
  ([DGChange], [DGChange]) -> Result ([DGChange], [DGChange])
forall (m :: * -> *) a. Monad m => a -> m a
return (((Node, Node, DGLinkLab) -> DGChange)
-> [(Node, Node, DGLinkLab)] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map (Node, Node, DGLinkLab) -> DGChange
DeleteEdge ([(Node, Node, DGLinkLab)] -> [DGChange])
-> [(Node, Node, DGLinkLab)] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ [(Node, Node, DGLinkLab)]
allOuts [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, DGLinkLab)]
inss, ((Node, Node, DGLinkLab) -> DGChange)
-> [(Node, Node, DGLinkLab)] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map (Node, Node, DGLinkLab) -> DGChange
InsertEdge ([(Node, Node, DGLinkLab)] -> [DGChange])
-> [(Node, Node, DGLinkLab)] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ [(Node, Node, DGLinkLab)]
nAllinss [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, DGLinkLab)]
nouts)

qualifyLabNode :: LibName -> (DGraph, RenameMap) -> LNode DGNodeLab
               -> Result (DGraph, RenameMap)
qualifyLabNode :: LibName
-> (DGraph, RenameMap)
-> LNode DGNodeLab
-> Result (DGraph, RenameMap)
qualifyLabNode ln :: LibName
ln (dg :: DGraph
dg, mormap :: RenameMap
mormap) (n :: Node
n, lb :: DGNodeLab
lb) =
   if DGNodeLab -> Bool
isDGRef DGNodeLab
lb then (DGraph, RenameMap) -> Result (DGraph, RenameMap)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg, RenameMap
mormap) else case DGNodeLab -> G_theory
dgn_theory DGNodeLab
lb of
    G_theory lid :: lid
lid syn :: Maybe IRI
syn (ExtSign sig :: sign
sig _) _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ -> do
        let inss :: [(Node, Node, DGLinkLab)]
inss = DGraph -> Node -> [(Node, Node, DGLinkLab)]
properInEdges DGraph
dg Node
n
        [morphism]
hins <- ([morphism] -> GMorphism -> Result [morphism])
-> [morphism] -> [GMorphism] -> Result [morphism]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ l :: [morphism]
l (GMorphism cid :: cid
cid _ _ mor :: morphism2
mor _) ->
            if AnyComorphism -> Bool
isIdComorphism (cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism cid
cid) Bool -> Bool -> Bool
&& lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==
               lid2 -> String
forall lid. Language lid => lid -> String
language_name (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) then do
                morphism
hmor <- lid2 -> lid -> String -> morphism2 -> Result morphism
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> String -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) lid
lid
                        "qualifyLabNode" morphism2
mor
                [morphism] -> Result [morphism]
forall (m :: * -> *) a. Monad m => a -> m a
return ([morphism] -> Result [morphism])
-> [morphism] -> Result [morphism]
forall a b. (a -> b) -> a -> b
$ morphism
hmor morphism -> [morphism] -> [morphism]
forall a. a -> [a] -> [a]
: [morphism]
l
            else [morphism] -> Result [morphism]
forall (m :: * -> *) a. Monad m => a -> m a
return [morphism]
l) [] ([GMorphism] -> Result [morphism])
-> [GMorphism] -> Result [morphism]
forall a b. (a -> b) -> a -> b
$ ((Node, Node, DGLinkLab) -> GMorphism)
-> [(Node, Node, DGLinkLab)] -> [GMorphism]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, ld :: DGLinkLab
ld) -> DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
ld) [(Node, Node, DGLinkLab)]
inss
        let revHins :: [morphism]
revHins = (morphism -> Maybe morphism) -> [morphism] -> [morphism]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Result morphism -> Maybe morphism
forall a. Result a -> Maybe a
maybeResult (Result morphism -> Maybe morphism)
-> (morphism -> Result morphism) -> morphism -> Maybe morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. morphism -> Result morphism
forall object morphism.
Category object morphism =>
morphism -> Result morphism
inverse) [morphism]
hins
            m :: morphism
m = case [morphism]
revHins of
                  [] -> sign -> morphism
forall object morphism.
Category object morphism =>
object -> morphism
ide sign
sig
                  hd :: morphism
hd : tl :: [morphism]
tl -> lid -> morphism -> [morphism] -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> [morphism] -> morphism
constructUnion lid
lid morphism
hd [morphism]
tl
        (m1 :: morphism
m1, osens :: [Named sentence]
osens) <- lid
-> SIMPLE_ID
-> LibName
-> morphism
-> sign
-> Result (morphism, [Named sentence])
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> SIMPLE_ID
-> LibName
-> morphism
-> sign
-> Result (morphism, [Named sentence])
qualify lid
lid (String -> SIMPLE_ID
mkSimpleId (String -> SIMPLE_ID) -> String -> SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> String
getDGNodeName DGNodeLab
lb)
                       LibName
ln morphism
m sign
sig
        morphism
rm <- morphism -> Result morphism
forall object morphism.
Category object morphism =>
morphism -> Result morphism
inverse morphism
m1
        ThSens sentence (AnyComorphism, BasicProof)
nThSens <- (sentence -> Result sentence)
-> ThSens sentence (AnyComorphism, BasicProof)
-> Result (ThSens sentence (AnyComorphism, BasicProof))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> ThSens a c -> m (ThSens b c)
mapThSensValueM (lid -> morphism -> sentence -> Result sentence
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> sentence -> Result sentence
map_sen lid
lid morphism
m1) (ThSens sentence (AnyComorphism, BasicProof)
 -> Result (ThSens sentence (AnyComorphism, BasicProof)))
-> ThSens sentence (AnyComorphism, BasicProof)
-> Result (ThSens sentence (AnyComorphism, BasicProof))
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b
joinSens ThSens sentence (AnyComorphism, BasicProof)
sens
          (ThSens sentence (AnyComorphism, BasicProof)
 -> ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ [Named sentence] -> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence]
osens
        let nlb :: DGNodeLab
nlb = DGNodeLab
lb { dgn_theory :: G_theory
dgn_theory = lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
syn
                       (lid -> sign -> ExtSign sign symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign lid
lid (morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
m1)) SigId
startSigId
                       ThSens sentence (AnyComorphism, BasicProof)
nThSens ThId
startThId }
            gp :: (GMorphism, GMorphism)
gp = ( G_morphism -> GMorphism
gEmbed (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> MorId -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> MorId -> G_morphism
G_morphism lid
lid morphism
m1 MorId
startMorId
                 , G_morphism -> GMorphism
gEmbed (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> MorId -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> MorId -> G_morphism
G_morphism lid
lid morphism
rm MorId
startMorId)
        (ds :: [DGChange]
ds, is :: [DGChange]
is) <- DGraph
-> Node
-> [(Node, Node, DGLinkLab)]
-> (GMorphism, GMorphism)
-> Result ([DGChange], [DGChange])
createChanges DGraph
dg Node
n [(Node, Node, DGLinkLab)]
inss (GMorphism, GMorphism)
gp
        (DGraph, RenameMap) -> Result (DGraph, RenameMap)
forall (m :: * -> *) a. Monad m => a -> m a
return ( DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg ([DGChange] -> DGraph) -> [DGChange] -> DGraph
forall a b. (a -> b) -> a -> b
$ [DGChange]
ds [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
lb (Node
n, DGNodeLab
nlb) DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange]
is
               , Node -> (GMorphism, GMorphism) -> RenameMap -> RenameMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Node
n (GMorphism, GMorphism)
gp RenameMap
mormap)

{- consider that hiding definition links have a reverse morphism
and hiding theorems are also special -}
composeWithMorphism :: Bool -> GMorphism -> GMorphism -> LEdge DGLinkLab
                    -> Result (LEdge DGLinkLab)
composeWithMorphism :: Bool
-> GMorphism
-> GMorphism
-> (Node, Node, DGLinkLab)
-> Result (Node, Node, DGLinkLab)
composeWithMorphism dir :: Bool
dir mor :: GMorphism
mor rmor :: GMorphism
rmor (s :: Node
s, t :: Node
t, lb :: DGLinkLab
lb) = do
    let lmor :: GMorphism
lmor = DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lb
        inmor :: Result GMorphism
inmor = GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp GMorphism
lmor GMorphism
mor
        outmor :: Result GMorphism
outmor = GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp GMorphism
rmor GMorphism
lmor
    DGLinkLab
nlb <- String -> () -> Result DGLinkLab -> Result DGLinkLab
forall a b.
(GetRange a, Pretty a) =>
String -> a -> Result b -> Result b
addErrorDiag
      ((if Bool
dir then "in" else "out") String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-edge " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Node, Node, EdgeId) -> String
forall a. Show a => a -> String
show (Node
s, Node
t, DGLinkLab -> EdgeId
dgl_id DGLinkLab
lb)) ()
      (Result DGLinkLab -> Result DGLinkLab)
-> Result DGLinkLab -> Result DGLinkLab
forall a b. (a -> b) -> a -> b
$ case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lb of
        HidingDefLink -> do
          GMorphism
nmor <- if Bool
dir then Result GMorphism
outmor else Result GMorphism
inmor
          DGLinkLab -> Result DGLinkLab
forall (m :: * -> *) a. Monad m => a -> m a
return DGLinkLab
lb { dgl_morphism :: GMorphism
dgl_morphism = GMorphism
nmor }
        HidingFreeOrCofreeThm {} ->
          -- adjusting the morphisms here is more tricky and omitted for now
          DGLinkLab -> Result DGLinkLab
forall (m :: * -> *) a. Monad m => a -> m a
return DGLinkLab
lb
        _ -> do
          GMorphism
nmor <- if Bool
dir then Result GMorphism
inmor else Result GMorphism
outmor
          DGLinkLab -> Result DGLinkLab
forall (m :: * -> *) a. Monad m => a -> m a
return DGLinkLab
lb { dgl_morphism :: GMorphism
dgl_morphism = GMorphism
nmor }
    (Node, Node, DGLinkLab) -> Result (Node, Node, DGLinkLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node
s, Node
t, DGLinkLab
nlb)