{- |
Module      :  ./Proofs/NormalForm.hs
Description :  compute the normal forms of all nodes in development graphs
Copyright   :  (c) Christian Maeder, DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

compute normal forms
-}

module Proofs.NormalForm
    ( normalFormLibEnv
    , normalForm
    , normalFormRule
    ) where

import Logic.Logic
import Logic.Grothendieck

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

import Proofs.ComputeColimit

import Common.Consistency
import Common.Id
import Common.LibName
import Common.Result
import Common.Lib.Graph
import Common.Utils (nubOrd)

import Data.Graph.Inductive.Graph as Graph
import qualified Data.Map as Map
import Control.Monad
import qualified Control.Monad.Fail as Fail

normalFormRule :: DGRule
normalFormRule :: DGRule
normalFormRule = String -> DGRule
DGRule "NormalForm"

-- | compute normal form for a library and imported libs
normalForm :: LibName -> LibEnv -> Result LibEnv
normalForm :: LibName -> LibEnv -> Result LibEnv
normalForm ln :: LibName
ln le :: LibEnv
le = [LibName] -> LibEnv -> Result LibEnv
normalFormLNS (LibName -> LibEnv -> [LibName]
dependentLibs LibName
ln LibEnv
le) LibEnv
le

-- | compute norm form for all libraries
normalFormLibEnv :: LibEnv -> Result LibEnv
normalFormLibEnv :: LibEnv -> Result LibEnv
normalFormLibEnv le :: LibEnv
le = [LibName] -> LibEnv -> Result LibEnv
normalFormLNS (LibEnv -> [LibName]
getTopsortedLibs LibEnv
le) LibEnv
le

normalFormLNS :: [LibName] -> LibEnv -> Result LibEnv
normalFormLNS :: [LibName] -> LibEnv -> Result LibEnv
normalFormLNS lns :: [LibName]
lns libEnv :: LibEnv
libEnv = (LibEnv -> LibName -> Result LibEnv)
-> LibEnv -> [LibName] -> Result LibEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ le :: LibEnv
le ln :: LibName
ln -> do
  let dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
  DGraph
newDg <- LibEnv -> LibName -> DGraph -> Result DGraph
normalFormDG LibEnv
le LibName
ln DGraph
dg
  LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv) -> LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln
    (DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg DGRule
normalFormRule DGraph
newDg) LibEnv
le)
  LibEnv
libEnv [LibName]
lns

normalFormDG :: LibEnv -> LibName -> DGraph -> Result DGraph
normalFormDG :: LibEnv -> LibName -> DGraph -> Result DGraph
normalFormDG libEnv :: LibEnv
libEnv ln :: LibName
ln dgraph :: DGraph
dgraph = (DGraph -> (Node, DGNodeLab) -> Result DGraph)
-> DGraph -> [(Node, 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 (node :: Node
node, nodelab :: DGNodeLab
nodelab) ->
  if DGNodeLab -> Bool
labelHasHiding DGNodeLab
nodelab then case DGNodeLab -> Maybe Node
dgn_nf DGNodeLab
nodelab of
    Just _ -> DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg -- already computed
    Nothing -> if DGNodeLab -> Bool
isDGRef DGNodeLab
nodelab then do
        {- the normal form of the node
        is a reference to the normal form of the node it references
        careful: here not refNf, but a new Node which references refN -}
       let refLib :: LibName
refLib = DGNodeLab -> LibName
dgn_libname DGNodeLab
nodelab
           refNode :: Node
refNode = DGNodeLab -> Node
dgn_node DGNodeLab
nodelab
           refGraph' :: DGraph
refGraph' = LibName -> LibEnv -> DGraph
lookupDGraph LibName
refLib LibEnv
libEnv
           refLabel :: DGNodeLab
refLabel = DGraph -> Node -> DGNodeLab
labDG DGraph
refGraph' Node
refNode
       case DGNodeLab -> Maybe Node
dgn_nf DGNodeLab
refLabel of
         Nothing -> DGraph -> String -> Range -> Result DGraph
forall a. a -> String -> Range -> Result a
warning DGraph
dg
           (DGNodeLab -> String
getDGNodeName DGNodeLab
refLabel String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
refNode
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") from '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String
forall a. Show a => a -> String
show (LibName -> IRI
getLibId LibName
refLib)
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' without normal form") Range
nullRange
         Just refNf :: Node
refNf -> do
           let refNodelab :: DGNodeLab
refNodelab = DGraph -> Node -> DGNodeLab
labDG DGraph
refGraph' Node
refNf
               -- the label of the normal form ^
               nfNode :: Node
nfNode = DGraph -> Node
getNewNodeDG DGraph
dg
               -- the new reference node in the old graph ^
               refLab :: DGNodeLab
refLab = DGNodeLab
refNodelab
                 { dgn_name :: NodeName
dgn_name = String -> NodeName -> NodeName
extName "NormalForm" (NodeName -> NodeName) -> NodeName -> NodeName
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> NodeName
dgn_name DGNodeLab
nodelab
                 , dgn_nf :: Maybe Node
dgn_nf = Node -> Maybe Node
forall a. a -> Maybe a
Just Node
nfNode
                 , dgn_sigma :: Maybe GMorphism
dgn_sigma = GMorphism -> Maybe GMorphism
forall a. a -> Maybe a
Just (GMorphism -> Maybe GMorphism) -> GMorphism -> Maybe GMorphism
forall a b. (a -> b) -> a -> b
$ G_sign -> GMorphism
forall object morphism.
Category object morphism =>
object -> morphism
ide (G_sign -> GMorphism) -> G_sign -> GMorphism
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_sign
dgn_sign DGNodeLab
refNodelab
                 , nodeInfo :: DGNodeInfo
nodeInfo = LibName -> Node -> DGNodeInfo
newRefInfo LibName
refLib Node
refNf
                 , dgn_lock :: Maybe (MVar ())
dgn_lock = Maybe (MVar ())
forall a. Maybe a
Nothing }
               newLab :: DGNodeLab
newLab = DGNodeLab
nodelab
                 { dgn_nf :: Maybe Node
dgn_nf = Node -> Maybe Node
forall a. a -> Maybe a
Just Node
nfNode,
                   dgn_sigma :: Maybe GMorphism
dgn_sigma = DGNodeLab -> Maybe GMorphism
dgn_sigma DGNodeLab
refLabel }
               chLab :: DGChange
chLab = DGNodeLab -> (Node, DGNodeLab) -> DGChange
SetNodeLab DGNodeLab
nodelab (Node
node, DGNodeLab
newLab)
               changes :: [DGChange]
changes = [(Node, DGNodeLab) -> DGChange
InsertNode (Node
nfNode, DGNodeLab
refLab), DGChange
chLab]
               newGraph :: DGraph
newGraph = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dgraph [DGChange]
changes
           DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
newGraph
      else do
        let gd :: Gr G_theory b
gd = LNode G_theory -> Gr G_theory b -> Gr G_theory b
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Node
node, DGNodeLab -> G_theory
dgn_theory DGNodeLab
nodelab) Gr G_theory b
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
empty
            g0 :: Map Node Node
g0 = [(Node, Node)] -> Map Node Node
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Node
node, Node
node)]
            (diagram :: GDiagram
diagram, g :: Map Node Node
g) = DGraph
-> [Node] -> (GDiagram, Map Node Node) -> (GDiagram, Map Node Node)
computeDiagram DGraph
dg [Node
node] (GDiagram
forall b. Gr G_theory b
gd, Map Node Node
g0)
            fsub :: GDiagram
fsub = GDiagram -> GDiagram
finalSubcateg GDiagram
diagram
            Result ds :: [Diagnosis]
ds res :: Maybe (G_theory, Map Node GMorphism)
res = GDiagram -> Result (G_theory, Map Node GMorphism)
gWeaklyAmalgamableCocone GDiagram
fsub
            es :: [Diagnosis]
es = (Diagnosis -> Diagnosis) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ d :: Diagnosis
d -> if Diagnosis -> Bool
isErrorDiag Diagnosis
d then Diagnosis
d { diagKind :: DiagKind
diagKind = DiagKind
Warning }
                             else Diagnosis
d) [Diagnosis]
ds
        [Diagnosis] -> Result ()
appendDiags [Diagnosis]
es
        case Maybe (G_theory, Map Node GMorphism)
res of
          Nothing -> DGraph -> String -> Range -> Result DGraph
forall a. a -> String -> Range -> Result a
warning DGraph
dg
                ("cocone failure for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> String
getDGNodeName DGNodeLab
nodelab
                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> String -> String
forall a. Show a => a -> String -> String
shows Node
node ")") Range
nullRange
          Just (sign :: G_theory
sign, mmap :: Map Node GMorphism
mmap) -> do
            {- we don't know that node is in fsub
            if it's not, we have to find a tip accessible from node
            and dgn_sigma = edgeLabel(node, tip); mmap (g Map.! tip) -}
            GMorphism
morNode <- if Node
node Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` GDiagram -> [Node]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Node]
nodes GDiagram
fsub then let
                        gn :: Node
gn = Node -> Node -> Map Node Node -> Node
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Node
forall a. HasCallStack => String -> a
error "gn") Node
node Map Node Node
g
                        phi :: GMorphism
phi = GMorphism -> Node -> Map Node GMorphism -> GMorphism
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> GMorphism
forall a. HasCallStack => String -> a
error "mor") Node
gn Map Node GMorphism
mmap
                       in GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return GMorphism
phi else let
                          leaves :: [Node]
leaves = (Node -> Bool) -> [Node] -> [Node]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: Node
x -> GDiagram -> Node -> Node
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Node -> Node
outdeg GDiagram
fsub Node
x Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== 0) ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$
                                     GDiagram -> [Node]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Node]
nodes GDiagram
fsub
                          paths :: [(Node, GMorphism)]
paths = (Node -> (Node, GMorphism)) -> [Node] -> [(Node, GMorphism)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: Node
x ->
                                       (Node
x, String -> Result GMorphism -> GMorphism
forall a. String -> Result a -> a
propagateErrors "normalFormDG"
                                             (Result GMorphism -> GMorphism) -> Result GMorphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ GDiagram -> Node -> Node -> Result GMorphism
dijkstra GDiagram
diagram Node
node Node
x))
                                      ([Node] -> [(Node, GMorphism)]) -> [Node] -> [(Node, GMorphism)]
forall a b. (a -> b) -> a -> b
$ (Node -> Bool) -> [Node] -> [Node]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: Node
x -> Node
node Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` GDiagram -> Node -> [Node]
forall a b. Gr a b -> Node -> [Node]
predecs
                                                      GDiagram
diagram Node
x) [Node]
leaves
                                          in
                            case [(Node, GMorphism)]
paths of
                             [] -> String -> Result GMorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "node should reach a tip"
                             (xn :: Node
xn, xf :: GMorphism
xf) : _ -> GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp GMorphism
xf (GMorphism -> Result GMorphism) -> GMorphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ Map Node GMorphism
mmap Map Node GMorphism -> Node -> GMorphism
forall k a. Ord k => Map k a -> k -> a
Map.! Node
xn
            let nfNode :: Node
nfNode = DGraph -> Node
getNewNodeDG DGraph
dg -- new node for normal form
                info :: DGNodeInfo
info = DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
nodelab
                ConsStatus c :: Conservativity
c cp :: Conservativity
cp pr :: ThmLinkStatus
pr = DGNodeInfo -> ConsStatus
node_cons_status DGNodeInfo
info
                nfLabel :: DGNodeLab
nfLabel = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab
                  (String -> NodeName -> NodeName
extName "NormalForm" (NodeName -> NodeName) -> NodeName -> NodeName
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> NodeName
dgn_name DGNodeLab
nodelab)
                  DGNodeInfo
info
                  { node_origin :: DGOrigin
node_origin = Node -> DGOrigin
DGNormalForm Node
node
                  , node_cons_status :: ConsStatus
node_cons_status = Conservativity -> ConsStatus
mkConsStatus Conservativity
c }
                  G_theory
sign
                newLab :: DGNodeLab
newLab = DGNodeLab
nodelab -- the new label for node
                     { dgn_nf :: Maybe Node
dgn_nf = Node -> Maybe Node
forall a. a -> Maybe a
Just Node
nfNode
                     , dgn_sigma :: Maybe GMorphism
dgn_sigma = GMorphism -> Maybe GMorphism
forall a. a -> Maybe a
Just GMorphism
morNode
                     , nodeInfo :: DGNodeInfo
nodeInfo = DGNodeInfo
info
                         { node_cons_status :: ConsStatus
node_cons_status = Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus Conservativity
None Conservativity
cp ThmLinkStatus
pr }
                     }
            -- add the nf to the label of node
                chLab :: DGChange
chLab = DGNodeLab -> (Node, DGNodeLab) -> DGChange
SetNodeLab DGNodeLab
nodelab (Node
node, DGNodeLab
newLab)
            -- insert the new node and add edges from the predecessors
                insNNF :: DGChange
insNNF = (Node, DGNodeLab) -> DGChange
InsertNode (Node
nfNode, DGNodeLab
nfLabel)
                makeEdge :: a -> b -> GMorphism -> (a, b, DGLinkLab)
makeEdge src :: a
src tgt :: b
tgt m :: GMorphism
m = (a
src, b
tgt, GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
m DGLinkOrigin
DGLinkProof)
                insStrMor :: [DGChange]
insStrMor = ((Node, GMorphism) -> DGChange)
-> [(Node, GMorphism)] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Node
x, f :: GMorphism
f) -> LEdge DGLinkLab -> DGChange
InsertEdge (LEdge DGLinkLab -> DGChange) -> LEdge DGLinkLab -> DGChange
forall a b. (a -> b) -> a -> b
$ Node -> Node -> GMorphism -> LEdge DGLinkLab
forall a b. a -> b -> GMorphism -> (a, b, DGLinkLab)
makeEdge Node
x Node
nfNode GMorphism
f)
                  ([(Node, GMorphism)] -> [DGChange])
-> [(Node, GMorphism)] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ [(Node, GMorphism)] -> [(Node, GMorphism)]
forall a. Ord a => [a] -> [a]
nubOrd ([(Node, GMorphism)] -> [(Node, GMorphism)])
-> [(Node, GMorphism)] -> [(Node, GMorphism)]
forall a b. (a -> b) -> a -> b
$ ((Node, GMorphism) -> (Node, GMorphism))
-> [(Node, GMorphism)] -> [(Node, GMorphism)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Node
x, y :: GMorphism
y) -> (Map Node Node
g Map Node Node -> Node -> Node
forall k a. Ord k => Map k a -> k -> a
Map.! Node
x, GMorphism
y))
                  ([(Node, GMorphism)] -> [(Node, GMorphism)])
-> [(Node, GMorphism)] -> [(Node, GMorphism)]
forall a b. (a -> b) -> a -> b
$ (Node
node, GMorphism
morNode) (Node, GMorphism) -> [(Node, GMorphism)] -> [(Node, GMorphism)]
forall a. a -> [a] -> [a]
: Map Node GMorphism -> [(Node, GMorphism)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Node GMorphism
mmap
                allChanges :: [DGChange]
allChanges = DGChange
insNNF DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: DGChange
chLab DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange]
insStrMor
                newDG :: DGraph
newDG = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
allChanges
            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
changeDGH DGraph
newDG (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> (Node, DGNodeLab) -> DGChange
SetNodeLab DGNodeLab
nfLabel (Node
nfNode, DGNodeLab
nfLabel
              { globalTheory :: Maybe G_theory
globalTheory = LibEnv -> LibName -> DGraph -> (Node, DGNodeLab) -> Maybe G_theory
computeLabelTheory LibEnv
libEnv LibName
ln DGraph
newDG
                (Node
nfNode, DGNodeLab
nfLabel) })
  else DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg) DGraph
dgraph ([(Node, DGNodeLab)] -> Result DGraph)
-> [(Node, DGNodeLab)] -> Result DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [(Node, DGNodeLab)]
topsortedNodes DGraph
dgraph -- only change relevant nodes

{- | computes the diagram associated to a node N in a development graph,
   adding common origins for multiple occurences of nodes, whenever
   needed
-}
computeDiagram :: DGraph -> [Node] -> (GDiagram, Map.Map Node Node)
               -> (GDiagram, Map.Map Node Node)
  -- as described in the paper for now
computeDiagram :: DGraph
-> [Node] -> (GDiagram, Map Node Node) -> (GDiagram, Map Node Node)
computeDiagram dgraph :: DGraph
dgraph nodeList :: [Node]
nodeList (gd :: GDiagram
gd, g :: Map Node Node
g) =
 case [Node]
nodeList of
  [] -> (GDiagram
gd, Map Node Node
g)
  _ ->
   let -- defInEdges is list of pairs (n, edges of target g(n))
       defInEdges :: [(Node, [LEdge DGLinkLab])]
defInEdges = (Node -> (Node, [LEdge DGLinkLab]))
-> [Node] -> [(Node, [LEdge DGLinkLab])]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: Node
n -> (Node
n, (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ e :: LEdge DGLinkLab
e@(s :: Node
s, t :: Node
t, _) -> Node
s Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
t Bool -> Bool -> Bool
&&
                         (DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE ((DGLinkType -> Bool) -> (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
liftOr DGLinkType -> Bool
isGlobalDef DGLinkType -> Bool
isHidingDef) LEdge DGLinkLab
e) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$
                        DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dgraph (Node -> [LEdge DGLinkLab]) -> Node -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ Map Node Node
g Map Node Node -> Node -> Node
forall k a. Ord k => Map k a -> k -> a
Map.! Node
n)) [Node]
nodeList
       {- TO DO: no local links, and why edges with s=t are removed
       add normal form nodes
       sources of each edge must be added as new nodes -}
       nodeIds :: [(Node, (Node, LEdge DGLinkLab))]
nodeIds = [Node]
-> [(Node, LEdge DGLinkLab)] -> [(Node, (Node, LEdge DGLinkLab))]
forall a b. [a] -> [b] -> [(a, b)]
zip (Node -> GDiagram -> [Node]
forall (gr :: * -> * -> *) a b.
Graph gr =>
Node -> gr a b -> [Node]
newNodes ([LEdge DGLinkLab] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length ([LEdge DGLinkLab] -> Node) -> [LEdge DGLinkLab] -> Node
forall a b. (a -> b) -> a -> b
$ ((Node, [LEdge DGLinkLab]) -> [LEdge DGLinkLab])
-> [(Node, [LEdge DGLinkLab])] -> [LEdge DGLinkLab]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Node, [LEdge DGLinkLab]) -> [LEdge DGLinkLab]
forall a b. (a, b) -> b
snd [(Node, [LEdge DGLinkLab])]
defInEdges) GDiagram
gd)
                     ([(Node, LEdge DGLinkLab)] -> [(Node, (Node, LEdge DGLinkLab))])
-> [(Node, LEdge DGLinkLab)] -> [(Node, (Node, LEdge DGLinkLab))]
forall a b. (a -> b) -> a -> b
$ ((Node, [LEdge DGLinkLab]) -> [(Node, LEdge DGLinkLab)])
-> [(Node, [LEdge DGLinkLab])] -> [(Node, LEdge DGLinkLab)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (n :: Node
n, l :: [LEdge DGLinkLab]
l) -> (LEdge DGLinkLab -> (Node, LEdge DGLinkLab))
-> [LEdge DGLinkLab] -> [(Node, LEdge DGLinkLab)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: LEdge DGLinkLab
x -> (Node
n, LEdge DGLinkLab
x)) [LEdge DGLinkLab]
l ) [(Node, [LEdge DGLinkLab])]
defInEdges
       newLNodes :: [LNode G_theory]
newLNodes = [Node] -> [G_theory] -> [LNode G_theory]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Node, (Node, LEdge DGLinkLab)) -> Node)
-> [(Node, (Node, LEdge DGLinkLab))] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (Node, (Node, LEdge DGLinkLab)) -> Node
forall a b. (a, b) -> a
fst [(Node, (Node, LEdge DGLinkLab))]
nodeIds) ([G_theory] -> [LNode G_theory]) -> [G_theory] -> [LNode G_theory]
forall a b. (a -> b) -> a -> b
$
                   (LEdge DGLinkLab -> G_theory) -> [LEdge DGLinkLab] -> [G_theory]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Node
s, _, _) -> DGNodeLab -> G_theory
dgn_theory (DGNodeLab -> G_theory) -> DGNodeLab -> G_theory
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dgraph Node
s) ([LEdge DGLinkLab] -> [G_theory])
-> [LEdge DGLinkLab] -> [G_theory]
forall a b. (a -> b) -> a -> b
$
                   ((Node, [LEdge DGLinkLab]) -> [LEdge DGLinkLab])
-> [(Node, [LEdge DGLinkLab])] -> [LEdge DGLinkLab]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Node, [LEdge DGLinkLab]) -> [LEdge DGLinkLab]
forall a b. (a, b) -> b
snd [(Node, [LEdge DGLinkLab])]
defInEdges
       g0 :: Map Node Node
g0 = [(Node, Node)] -> Map Node Node
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Node, Node)] -> Map Node Node)
-> [(Node, Node)] -> Map Node Node
forall a b. (a -> b) -> a -> b
$
                     ((Node, (Node, LEdge DGLinkLab)) -> (Node, Node))
-> [(Node, (Node, LEdge DGLinkLab))] -> [(Node, Node)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (newS :: Node
newS, (_newT :: Node
_newT, (s :: Node
s, _t :: Node
_t, _))) -> (Node
newS, Node
s)) [(Node, (Node, LEdge DGLinkLab))]
nodeIds
       morphEdge :: (a, (a, (a, b, DGLinkLab))) -> (a, a, (Node, GMorphism))
morphEdge (n1 :: a
n1, (n2 :: a
n2, (_, _, el :: DGLinkLab
el))) =
         if DGLinkType -> Bool
isHidingDef (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
el
            then (a
n2, a
n1, (Node
x, DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
el))
            else (a
n1, a
n2, (Node
x, DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
el))
         where EdgeId x :: Node
x = DGLinkLab -> EdgeId
dgl_id DGLinkLab
el
       newLEdges :: [(Node, Node, (Node, GMorphism))]
newLEdges = ((Node, (Node, LEdge DGLinkLab))
 -> (Node, Node, (Node, GMorphism)))
-> [(Node, (Node, LEdge DGLinkLab))]
-> [(Node, Node, (Node, GMorphism))]
forall a b. (a -> b) -> [a] -> [b]
map (Node, (Node, LEdge DGLinkLab)) -> (Node, Node, (Node, GMorphism))
forall a a b.
(a, (a, (a, b, DGLinkLab))) -> (a, a, (Node, GMorphism))
morphEdge [(Node, (Node, LEdge DGLinkLab))]
nodeIds
       gd' :: GDiagram
gd' = [(Node, Node, (Node, GMorphism))] -> GDiagram -> GDiagram
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
[LEdge b] -> gr a b -> gr a b
insEdges [(Node, Node, (Node, GMorphism))]
newLEdges (GDiagram -> GDiagram) -> GDiagram -> GDiagram
forall a b. (a -> b) -> a -> b
$ [LNode G_theory] -> GDiagram -> GDiagram
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
[LNode a] -> gr a b -> gr a b
insNodes [LNode G_theory]
newLNodes GDiagram
gd
       g' :: Map Node Node
g' = Map Node Node -> Map Node Node -> Map Node Node
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Node Node
g Map Node Node
g0
   in DGraph
-> [Node] -> (GDiagram, Map Node Node) -> (GDiagram, Map Node Node)
computeDiagram DGraph
dgraph (((Node, (Node, LEdge DGLinkLab)) -> Node)
-> [(Node, (Node, LEdge DGLinkLab))] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (Node, (Node, LEdge DGLinkLab)) -> Node
forall a b. (a, b) -> a
fst [(Node, (Node, LEdge DGLinkLab))]
nodeIds) (GDiagram
gd', Map Node Node
g')

finalSubcateg :: GDiagram -> GDiagram
finalSubcateg :: GDiagram -> GDiagram
finalSubcateg graph :: GDiagram
graph = let
    leaves :: [LNode G_theory]
leaves = (LNode G_theory -> Bool) -> [LNode G_theory] -> [LNode G_theory]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (n :: Node
n, _) -> GDiagram -> Node -> Node
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Node -> Node
outdeg GDiagram
graph Node
n Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== 0) ([LNode G_theory] -> [LNode G_theory])
-> [LNode G_theory] -> [LNode G_theory]
forall a b. (a -> b) -> a -> b
$ GDiagram -> [LNode G_theory]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GDiagram
graph
 in GDiagram
-> [Node]
-> [LNode G_theory]
-> [(Node, Node, (Node, GMorphism))]
-> [Node]
-> GDiagram
buildGraph GDiagram
graph ((LNode G_theory -> Node) -> [LNode G_theory] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map LNode G_theory -> Node
forall a b. (a, b) -> a
fst [LNode G_theory]
leaves) [LNode G_theory]
leaves [] ([Node] -> GDiagram) -> [Node] -> GDiagram
forall a b. (a -> b) -> a -> b
$ GDiagram -> [Node]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Node]
nodes GDiagram
graph

predecs :: Gr a b -> Node -> [Node]
predecs :: Gr a b -> Node -> [Node]
predecs graph :: Gr a b
graph node :: Node
node = let
   descs :: [Node] -> [Node] -> [Node]
descs nList :: [Node]
nList descList :: [Node]
descList =
    case [Node]
nList of
      [] -> [Node]
descList
      _ -> let
             newDescs :: [Node]
newDescs = (Node -> [Node]) -> [Node] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Gr a b -> Node -> [Node]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [Node]
pre Gr a b
graph) [Node]
nList
             nList' :: [Node]
nList' = (Node -> Bool) -> [Node] -> [Node]
forall a. (a -> Bool) -> [a] -> [a]
filter (Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Node]
nList) [Node]
newDescs
             descList' :: [Node]
descList' = [Node] -> [Node]
forall a. Ord a => [a] -> [a]
nubOrd ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [Node]
descList [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
newDescs
           in [Node] -> [Node] -> [Node]
descs [Node]
nList' [Node]
descList'
 in [Node] -> [Node] -> [Node]
descs [Node
node] []

buildGraph :: GDiagram -> [Node]
           -> [LNode G_theory]
           -> [LEdge (Int, GMorphism)]
           -> [Node]
           -> GDiagram
buildGraph :: GDiagram
-> [Node]
-> [LNode G_theory]
-> [(Node, Node, (Node, GMorphism))]
-> [Node]
-> GDiagram
buildGraph oGraph :: GDiagram
oGraph leaves :: [Node]
leaves nList :: [LNode G_theory]
nList eList :: [(Node, Node, (Node, GMorphism))]
eList nodeList :: [Node]
nodeList =
 case [Node]
nodeList of
  [] -> [LNode G_theory] -> [(Node, Node, (Node, GMorphism))] -> GDiagram
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [LNode G_theory]
nList [(Node, Node, (Node, GMorphism))]
eList
  n :: Node
n : nodeList' :: [Node]
nodeList' ->
     case GDiagram -> Node -> Node
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Node -> Node
outdeg GDiagram
oGraph Node
n of
      1 -> GDiagram
-> [Node]
-> [LNode G_theory]
-> [(Node, Node, (Node, GMorphism))]
-> [Node]
-> GDiagram
buildGraph GDiagram
oGraph [Node]
leaves [LNode G_theory]
nList [(Node, Node, (Node, GMorphism))]
eList [Node]
nodeList'
       -- the node is simply removed
      0 -> GDiagram
-> [Node]
-> [LNode G_theory]
-> [(Node, Node, (Node, GMorphism))]
-> [Node]
-> GDiagram
buildGraph GDiagram
oGraph [Node]
leaves [LNode G_theory]
nList [(Node, Node, (Node, GMorphism))]
eList [Node]
nodeList'
       -- the leaves have already been added to nList
      _ -> let
            Just l :: G_theory
l = GDiagram -> Node -> Maybe G_theory
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
lab GDiagram
oGraph Node
n
            nList' :: [LNode G_theory]
nList' = (Node
n, G_theory
l) LNode G_theory -> [LNode G_theory] -> [LNode G_theory]
forall a. a -> [a] -> [a]
: [LNode G_theory]
nList
            accesLeaves :: [Node]
accesLeaves = (Node -> Bool) -> [Node] -> [Node]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: Node
x -> Node
n Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` GDiagram -> Node -> [Node]
forall a b. Gr a b -> Node -> [Node]
predecs GDiagram
oGraph Node
x) [Node]
leaves
            eList' :: [(Node, Node, (Node, GMorphism))]
eList' = (Node -> (Node, Node, (Node, GMorphism)))
-> [Node] -> [(Node, Node, (Node, GMorphism))]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: Node
x -> (Node
n, Node
x, (1 :: Int,
                       String -> Result GMorphism -> GMorphism
forall a. String -> Result a -> a
propagateErrors "buildGraph" (Result GMorphism -> GMorphism) -> Result GMorphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ GDiagram -> Node -> Node -> Result GMorphism
dijkstra GDiagram
oGraph Node
n Node
x)))
                       [Node]
accesLeaves
           in GDiagram
-> [Node]
-> [LNode G_theory]
-> [(Node, Node, (Node, GMorphism))]
-> [Node]
-> GDiagram
buildGraph GDiagram
oGraph [Node]
leaves [LNode G_theory]
nList' ([(Node, Node, (Node, GMorphism))]
eList [(Node, Node, (Node, GMorphism))]
-> [(Node, Node, (Node, GMorphism))]
-> [(Node, Node, (Node, GMorphism))]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, (Node, GMorphism))]
eList') [Node]
nodeList'
       -- branch, must add n to the nList and edges in eList