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)
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)
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 {} ->
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)