-- | Classical double-pushout rewriting of directed multigraphs.
module Proarrow.Tools.DPO.Graph
  ( Graph (..)
  , GraphHom (..)
  , pushoutGraph
  , GraphRule (..)
  , pushoutComplementGraph
  , dpoStepGraph
  ) where

import Data.Map.Strict qualified as M
import Data.Set qualified as Set
import Data.Universe.Class (Finite (..))
import Prelude qualified as P

import Proarrow.Core (CategoryOf (..))
import Proarrow.Category.Instance.FinHask (FH, FinHask (..))
import Proarrow.Colimit.Pushout (pushout)
import Proarrow.Tools.DPO (pushoutComplement)

-- | A finite directed multigraph: a vertex type @v@, an edge type @e@, and the incidence
-- functions @src, tgt :: e -> v@.
data Graph v e = Graph
  { forall v e. Graph v e -> FH e ~> FH v
graphSrc :: FH e ~> FH v
  , forall v e. Graph v e -> FH e ~> FH v
graphTgt :: FH e ~> FH v
  }

-- | A graph homomorphism: a pair of functions on vertices and edges. Well-formedness
-- (commuting with @src@/@tgt@) is a precondition of the functions below, not checked here —
-- the same convention 'Proarrow.Colimit.Pushout' uses for its own square-commutativity.
data GraphHom v1 e1 v2 e2 = GraphHom
  { forall v1 e1 v2 e2. GraphHom v1 e1 v2 e2 -> FH v1 ~> FH v2
vertexMap :: FH v1 ~> FH v2
  , forall v1 e1 v2 e2. GraphHom v1 e1 v2 e2 -> FH e1 ~> FH e2
edgeMap :: FH e1 ~> FH e2
  }

-- | The pushout of two graph homomorphisms sharing a domain: vertices and edges are pushed
-- out independently in @FINHASK@ (graph colimits, like all presheaf colimits, are computed
-- pointwise), and the incidence functions of the result are induced from the two input
-- graphs' incidence functions.
pushoutGraph
  :: forall vA eA vB eB vI eI ans
   . Graph vA eA
  -> Graph vB eB
  -> GraphHom vI eI vA eA
  -> GraphHom vI eI vB eB
  -> (forall vH eH. Graph vH eH -> GraphHom vA eA vH eH -> GraphHom vB eB vH eH -> ans)
  -> ans
pushoutGraph :: forall vA eA vB eB vI eI ans.
Graph vA eA
-> Graph vB eB
-> GraphHom vI eI vA eA
-> GraphHom vI eI vB eB
-> (forall vH eH.
    Graph vH eH -> GraphHom vA eA vH eH -> GraphHom vB eB vH eH -> ans)
-> ans
pushoutGraph Graph vA eA
a Graph vB eB
b (GraphHom FH vI ~> FH vA
vLegA FH eI ~> FH eA
eLegA) (GraphHom FH vI ~> FH vB
vLegB FH eI ~> FH eB
eLegB) forall vH eH.
Graph vH eH -> GraphHom vA eA vH eH -> GraphHom vB eB vH eH -> ans
ok =
  (FH vI ~> FH vA)
-> (FH vI ~> FH vB)
-> (forall (p :: FINHASK). (FH vA ~> p) -> (FH vB ~> p) -> ans)
-> ans
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
forall (o :: FINHASK) (a :: FINHASK) (b :: FINHASK) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: FINHASK). (a ~> p) -> (b ~> p) -> r)
-> r
pushout FH vI ~> FH vA
vLegA FH vI ~> FH vB
vLegB \vA2vH :: FH vA ~> p
vA2vH@(FinHask Map a1 b1
vA2vHMap) vB2vH :: FH vB ~> p
vB2vH@(FinHask Map a1 b1
vB2vHMap) ->
    (FH eI ~> FH eA)
-> (FH eI ~> FH eB)
-> (forall (p :: FINHASK). (FH eA ~> p) -> (FH eB ~> p) -> ans)
-> ans
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
forall (o :: FINHASK) (a :: FINHASK) (b :: FINHASK) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: FINHASK). (a ~> p) -> (b ~> p) -> r)
-> r
pushout FH eI ~> FH eA
eLegA FH eI ~> FH eB
eLegB \eA2eH :: FH eA ~> p
eA2eH@(FinHask Map a1 b1
eA2eHMap) eB2eH :: FH eB ~> p
eB2eH@(FinHask Map a1 b1
eB2eHMap) ->
      let
        -- every edge of a pushout has a preimage in A or B, since pushouts in Set are jointly surjective
        fromA :: Map b1 a1
fromA = [(b1, a1)] -> Map b1 a1
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(b1
h, a1
e) | (a1
e, b1
h) <- Map a1 b1 -> [(a1, b1)]
forall k a. Map k a -> [(k, a)]
M.toList Map a1 b1
eA2eHMap]
        fromB :: Map b1 a1
fromB = [(b1, a1)] -> Map b1 a1
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(b1
h, a1
e) | (a1
e, b1
h) <- Map a1 b1 -> [(a1, b1)]
forall k a. Map k a -> [(k, a)]
M.toList Map a1 b1
eB2eHMap]
        indexOf :: FinHask (FH eA) (FH vA) -> FinHask (FH eB) (FH vB) -> b1 -> b1
indexOf (FinHask Map a1 b1
fA) (FinHask Map a1 b1
fB) b1
h = case b1 -> Map b1 a1 -> Maybe a1
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup b1
h Map b1 a1
fromA of
          P.Just a1
e -> Map a1 b1
vA2vHMap Map a1 b1 -> a1 -> b1
forall k a. Ord k => Map k a -> k -> a
M.! (Map a1 a1
Map a1 b1
fA Map a1 a1 -> a1 -> a1
forall k a. Ord k => Map k a -> k -> a
M.! a1
a1
e)
          Maybe a1
P.Nothing -> case b1 -> Map b1 a1 -> Maybe a1
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup b1
b1
h Map b1 a1
fromB of
            P.Just a1
e -> Map a1 b1
vB2vHMap Map a1 b1 -> a1 -> b1
forall k a. Ord k => Map k a -> k -> a
M.! (Map a1 a1
Map a1 b1
fB Map a1 a1 -> a1 -> a1
forall k a. Ord k => Map k a -> k -> a
M.! a1
a1
e)
            Maybe a1
P.Nothing -> [Char] -> b1
forall a. HasCallStack => [Char] -> a
P.error [Char]
"pushoutGraph: every edge of a pushout has a preimage"
        hSrc :: FinHask (FH b1) (FH b1)
hSrc = Map b1 b1 -> FinHask (FH b1) (FH b1)
forall a1 b1.
(Ob (FH a1), Ob (FH b1)) =>
Map a1 b1 -> FinHask (FH a1) (FH b1)
FinHask ([(b1, b1)] -> Map b1 b1
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(b1
h, FinHask (FH eA) (FH vA) -> FinHask (FH eB) (FH vB) -> b1 -> b1
indexOf (Graph vA eA -> FH eA ~> FH vA
forall v e. Graph v e -> FH e ~> FH v
graphSrc Graph vA eA
a) (Graph vB eB -> FH eB ~> FH vB
forall v e. Graph v e -> FH e ~> FH v
graphSrc Graph vB eB
b) b1
h) | b1
h <- [b1]
forall a. Finite a => [a]
universeF])
        hTgt :: FinHask (FH b1) (FH b1)
hTgt = Map b1 b1 -> FinHask (FH b1) (FH b1)
forall a1 b1.
(Ob (FH a1), Ob (FH b1)) =>
Map a1 b1 -> FinHask (FH a1) (FH b1)
FinHask ([(b1, b1)] -> Map b1 b1
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(b1
h, FinHask (FH eA) (FH vA) -> FinHask (FH eB) (FH vB) -> b1 -> b1
indexOf (Graph vA eA -> FH eA ~> FH vA
forall v e. Graph v e -> FH e ~> FH v
graphTgt Graph vA eA
a) (Graph vB eB -> FH eB ~> FH vB
forall v e. Graph v e -> FH e ~> FH v
graphTgt Graph vB eB
b) b1
h) | b1
h <- [b1]
forall a. Finite a => [a]
universeF])
      in
        Graph b1 b1 -> GraphHom vA eA b1 b1 -> GraphHom vB eB b1 b1 -> ans
forall vH eH.
Graph vH eH -> GraphHom vA eA vH eH -> GraphHom vB eB vH eH -> ans
ok ((FH b1 ~> FH b1) -> (FH b1 ~> FH b1) -> Graph b1 b1
forall v e. (FH e ~> FH v) -> (FH e ~> FH v) -> Graph v e
Graph FH b1 ~> FH b1
FinHask (FH b1) (FH b1)
hSrc FH b1 ~> FH b1
FinHask (FH b1) (FH b1)
hTgt) ((FH vA ~> FH b1) -> (FH eA ~> FH b1) -> GraphHom vA eA b1 b1
forall v1 e1 v2 e2.
(FH v1 ~> FH v2) -> (FH e1 ~> FH e2) -> GraphHom v1 e1 v2 e2
GraphHom FH vA ~> p
FH vA ~> FH b1
vA2vH FH eA ~> p
FH eA ~> FH b1
eA2eH) ((FH vB ~> FH b1) -> (FH eB ~> FH b1) -> GraphHom vB eB b1 b1
forall v1 e1 v2 e2.
(FH v1 ~> FH v2) -> (FH e1 ~> FH e2) -> GraphHom v1 e1 v2 e2
GraphHom FH vB ~> p
FH vB ~> FH b1
vB2vH FH eB ~> p
FH eB ~> FH b1
eB2eH)

-- | A graph rewrite rule: a span @L \<- K -> R@ of graph homomorphisms, together with @R@
-- itself (needed, since gluing @R@ into the result requires @R@'s own incidence functions).
data GraphRule vK eK vL eL vR eR = GraphRule
  { forall vK eK vL eL vR eR.
GraphRule vK eK vL eL vR eR -> GraphHom vK eK vL eL
ruleLeft :: GraphHom vK eK vL eL
  , forall vK eK vL eL vR eR.
GraphRule vK eK vL eL vR eR -> GraphHom vK eK vR eR
ruleRight :: GraphHom vK eK vR eR
  , forall vK eK vL eL vR eR.
GraphRule vK eK vL eL vR eR -> Graph vR eR
ruleR :: Graph vR eR
  }

-- | Compute the pushout complement of a rule's left leg and a match into a host graph @g@.
-- Fails (calls the second continuation) if the gluing condition doesn't hold: either an
-- identification conflict (as in plain 'Proarrow.Category.Instance.FinHask.FINHASK', on
-- vertices or on edges), or the graph-specific /dangling condition/ — an edge that survives
-- the rewrite is still attached to a vertex that the rewrite deletes.
pushoutComplementGraph
  :: forall vK eK vL eL vG eG ans
   . Graph vG eG
  -> GraphHom vK eK vL eL
  -> GraphHom vL eL vG eG
  -> (forall vD eD. Graph vD eD -> GraphHom vK eK vD eD -> GraphHom vD eD vG eG -> ans)
  -> ans
  -> ans
pushoutComplementGraph :: forall vK eK vL eL vG eG ans.
Graph vG eG
-> GraphHom vK eK vL eL
-> GraphHom vL eL vG eG
-> (forall vD eD.
    Graph vD eD -> GraphHom vK eK vD eD -> GraphHom vD eD vG eG -> ans)
-> ans
-> ans
pushoutComplementGraph Graph vG eG
g (GraphHom FH vK ~> FH vL
vLeft FH eK ~> FH eL
eLeft) (GraphHom FH vL ~> FH vG
vMatch FH eL ~> FH eG
eMatch) forall vD eD.
Graph vD eD -> GraphHom vK eK vD eD -> GraphHom vD eD vG eG -> ans
ok ans
notGlueable =
  (FH vK ~> FH vL)
-> (FH vL ~> FH vG)
-> (forall (d :: FINHASK). (FH vK ~> d) -> (d ~> FH vG) -> ans)
-> ans
-> ans
forall k (a :: k) (l :: k) (g :: k) ans.
HasPushoutComplements k =>
(a ~> l)
-> (l ~> g)
-> (forall (d :: k). (a ~> d) -> (d ~> g) -> ans)
-> ans
-> ans
forall (a :: FINHASK) (l :: FINHASK) (g :: FINHASK) ans.
(a ~> l)
-> (l ~> g)
-> (forall (d :: FINHASK). (a ~> d) -> (d ~> g) -> ans)
-> ans
-> ans
pushoutComplement
    FH vK ~> FH vL
vLeft
    FH vL ~> FH vG
vMatch
    ( \FH vK ~> d
vK2vD vD2vG :: d ~> FH vG
vD2vG@(FinHask Map a1 b1
vD2vGMap) ->
        (FH eK ~> FH eL)
-> (FH eL ~> FH eG)
-> (forall (d :: FINHASK). (FH eK ~> d) -> (d ~> FH eG) -> ans)
-> ans
-> ans
forall k (a :: k) (l :: k) (g :: k) ans.
HasPushoutComplements k =>
(a ~> l)
-> (l ~> g)
-> (forall (d :: k). (a ~> d) -> (d ~> g) -> ans)
-> ans
-> ans
forall (a :: FINHASK) (l :: FINHASK) (g :: FINHASK) ans.
(a ~> l)
-> (l ~> g)
-> (forall (d :: FINHASK). (a ~> d) -> (d ~> g) -> ans)
-> ans
-> ans
pushoutComplement
          FH eK ~> FH eL
eLeft
          FH eL ~> FH eG
eMatch
          ( \FH eK ~> d
eK2eD eD2eG :: d ~> FH eG
eD2eG@(FinHask Map a1 b1
eD2eGMap) ->
              let
                vertexImage :: Set b1
vertexImage = [b1] -> Set b1
forall a. Ord a => [a] -> Set a
Set.fromList (Map a1 b1 -> [b1]
forall k a. Map k a -> [a]
M.elems Map a1 b1
vD2vGMap)
                endpointsSurvive :: b1 -> Bool
endpointsSurvive b1
eg =
                  b1 -> Set b1 -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (FinHask (FH b1) (FH b1) -> Map b1 b1
forall a b. FinHask (FH a) (FH b) -> Map a b
unFinHask (Graph vG eG -> FH eG ~> FH vG
forall v e. Graph v e -> FH e ~> FH v
graphSrc Graph vG eG
g) Map b1 b1 -> b1 -> b1
forall k a. Ord k => Map k a -> k -> a
M.! b1
eg) Set b1
vertexImage
                    Bool -> Bool -> Bool
P.&& b1 -> Set b1 -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (FinHask (FH b1) (FH b1) -> Map b1 b1
forall a b. FinHask (FH a) (FH b) -> Map a b
unFinHask (Graph vG eG -> FH eG ~> FH vG
forall v e. Graph v e -> FH e ~> FH v
graphTgt Graph vG eG
g) Map b1 b1 -> b1 -> b1
forall k a. Ord k => Map k a -> k -> a
M.! b1
eg) Set b1
vertexImage
              in
                if Bool -> Bool
P.not ((b1 -> Bool) -> [b1] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
P.all b1 -> Bool
endpointsSurvive (Map a1 b1 -> [b1]
forall k a. Map k a -> [a]
M.elems Map a1 b1
eD2eGMap))
                  then ans
notGlueable
                  else
                    let
                      vG2vD :: Map b1 a1
vG2vD = [(b1, a1)] -> Map b1 a1
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(b1
v, a1
k) | (a1
k, b1
v) <- Map a1 b1 -> [(a1, b1)]
forall k a. Map k a -> [(k, a)]
M.toList Map a1 b1
vD2vGMap]
                      dSrc :: FinHask (FH a1) (FH a1)
dSrc = Map a1 a1 -> FinHask (FH a1) (FH a1)
forall a1 b1.
(Ob (FH a1), Ob (FH b1)) =>
Map a1 b1 -> FinHask (FH a1) (FH b1)
FinHask ((b1 -> a1) -> Map a1 b1 -> Map a1 a1
forall a b. (a -> b) -> Map a1 a -> Map a1 b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (\b1
eg -> Map b1 a1
vG2vD Map b1 a1 -> b1 -> a1
forall k a. Ord k => Map k a -> k -> a
M.! (FinHask (FH b1) (FH b1) -> Map b1 b1
forall a b. FinHask (FH a) (FH b) -> Map a b
unFinHask (Graph vG eG -> FH eG ~> FH vG
forall v e. Graph v e -> FH e ~> FH v
graphSrc Graph vG eG
g) Map b1 b1 -> b1 -> b1
forall k a. Ord k => Map k a -> k -> a
M.! b1
eg)) Map a1 b1
eD2eGMap)
                      dTgt :: FinHask (FH a1) (FH a1)
dTgt = Map a1 a1 -> FinHask (FH a1) (FH a1)
forall a1 b1.
(Ob (FH a1), Ob (FH b1)) =>
Map a1 b1 -> FinHask (FH a1) (FH b1)
FinHask ((b1 -> a1) -> Map a1 b1 -> Map a1 a1
forall a b. (a -> b) -> Map a1 a -> Map a1 b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (\b1
eg -> Map b1 a1
vG2vD Map b1 a1 -> b1 -> a1
forall k a. Ord k => Map k a -> k -> a
M.! (FinHask (FH b1) (FH b1) -> Map b1 b1
forall a b. FinHask (FH a) (FH b) -> Map a b
unFinHask (Graph vG eG -> FH eG ~> FH vG
forall v e. Graph v e -> FH e ~> FH v
graphTgt Graph vG eG
g) Map b1 b1 -> b1 -> b1
forall k a. Ord k => Map k a -> k -> a
M.! b1
eg)) Map a1 b1
eD2eGMap)
                    in
                      Graph a1 a1 -> GraphHom vK eK a1 a1 -> GraphHom a1 a1 vG eG -> ans
forall vD eD.
Graph vD eD -> GraphHom vK eK vD eD -> GraphHom vD eD vG eG -> ans
ok ((FH a1 ~> FH a1) -> (FH a1 ~> FH a1) -> Graph a1 a1
forall v e. (FH e ~> FH v) -> (FH e ~> FH v) -> Graph v e
Graph FH a1 ~> FH a1
FinHask (FH a1) (FH a1)
dSrc FH a1 ~> FH a1
FinHask (FH a1) (FH a1)
dTgt) ((FH vK ~> FH a1) -> (FH eK ~> FH a1) -> GraphHom vK eK a1 a1
forall v1 e1 v2 e2.
(FH v1 ~> FH v2) -> (FH e1 ~> FH e2) -> GraphHom v1 e1 v2 e2
GraphHom FH vK ~> d
FH vK ~> FH a1
vK2vD FH eK ~> d
FH eK ~> FH a1
eK2eD) ((FH a1 ~> FH vG) -> (FH a1 ~> FH eG) -> GraphHom a1 a1 vG eG
forall v1 e1 v2 e2.
(FH v1 ~> FH v2) -> (FH e1 ~> FH e2) -> GraphHom v1 e1 v2 e2
GraphHom d ~> FH vG
FH a1 ~> FH vG
vD2vG d ~> FH eG
FH a1 ~> FH eG
eD2eG)
          )
          ans
notGlueable
    )
    ans
notGlueable

-- | Apply a 'GraphRule' to a host graph at a match @L -> G@. On success, the continuation
-- receives the rewrite's cospan legs @D -> G@, @D -> H@ and the embedding @R -> H@ of the
-- newly created pattern into the result @H@ (given explicitly, since unlike a bare object in
-- a kind-indexed category, a 'Graph' carries data the caller needs to keep rewriting).
--
-- ==== Example: deleting an edge
--
-- The host graph @g@ is a single edge between two vertices:
--
-- >  g:   0 --e0--> 1
--
-- The rule deletes that edge but keeps both endpoints: @L@ has the edge, @K@ and @R@ don't.
--
-- >  L:   0 --e--> 1        K:   0   1        R:   0   1
--
-- Matching @L@'s edge @e@ onto @g@'s @e0@ and applying the rule keeps both vertices (tracked
-- by @r2h@, the embedding of @R@ into the result) and leaves no edges behind:
--
-- >>> import Proarrow.Category.Instance.FinHask (Fin, fromList, toList)
-- >>> import Proarrow.Core ((\\))
-- >>> let g = Graph (fromList [(0 :: Fin 1, 0 :: Fin 2)]) (fromList [(0 :: Fin 1, 1 :: Fin 2)]) :: Graph (Fin 2) (Fin 1)
-- >>> let k = Graph (fromList []) (fromList []) :: Graph (Fin 2) (Fin 0)
-- >>> let idV = fromList [(0 :: Fin 2, 0 :: Fin 2), (1 :: Fin 2, 1 :: Fin 2)]
-- >>> let rule = GraphRule (GraphHom idV (fromList [])) (GraphHom idV (fromList [])) k :: GraphRule (Fin 2) (Fin 0) (Fin 2) (Fin 1) (Fin 2) (Fin 0)
-- >>> let m = GraphHom idV (fromList [(0 :: Fin 1, 0 :: Fin 1)]) :: GraphHom (Fin 2) (Fin 1) (Fin 2) (Fin 1)
-- >>> (dpoStepGraph g rule m (\h _ _ r2h -> (P.show (toList (vertexMap r2h), toList (graphSrc h), toList (graphTgt h))) \\ graphSrc h) "gluing failed") :: P.String
-- "([(0,0),(1,1)],[],[])"
--
-- ==== Example: the dangling condition
--
-- Same host graph @g@, but the rule instead deletes vertex @0@ in isolation: @L@ has one
-- vertex and no edges, @K@ and @R@ are empty.
--
-- >  L:   0                 K:   (empty)       R:   (empty)
--
-- Vertex @0@ still has @e0@ attached to it in @g@, and @e0@ isn't part of the match, so
-- deleting the vertex would leave @e0@ dangling — the gluing condition fails:
--
-- >>> let k' = Graph (fromList []) (fromList []) :: Graph (Fin 0) (Fin 0)
-- >>> let rule' = GraphRule (GraphHom (fromList []) (fromList [])) (GraphHom (fromList []) (fromList [])) k' :: GraphRule (Fin 0) (Fin 0) (Fin 1) (Fin 0) (Fin 0) (Fin 0)
-- >>> let m' = GraphHom (fromList [(0 :: Fin 1, 0 :: Fin 2)]) (fromList []) :: GraphHom (Fin 1) (Fin 0) (Fin 2) (Fin 1)
-- >>> dpoStepGraph g rule' m' (\_ _ _ _ -> "glued (unexpected)") "gluing failed"
-- "gluing failed"
dpoStepGraph
  :: forall vK eK vL eL vR eR vG eG ans
   . Graph vG eG
  -> GraphRule vK eK vL eL vR eR
  -> GraphHom vL eL vG eG
  -> (forall vD eD vH eH. Graph vH eH -> GraphHom vD eD vG eG -> GraphHom vD eD vH eH -> GraphHom vR eR vH eH -> ans)
  -> ans
  -> ans
dpoStepGraph :: forall vK eK vL eL vR eR vG eG ans.
Graph vG eG
-> GraphRule vK eK vL eL vR eR
-> GraphHom vL eL vG eG
-> (forall vD eD vH eH.
    Graph vH eH
    -> GraphHom vD eD vG eG
    -> GraphHom vD eD vH eH
    -> GraphHom vR eR vH eH
    -> ans)
-> ans
-> ans
dpoStepGraph Graph vG eG
g (GraphRule GraphHom vK eK vL eL
left GraphHom vK eK vR eR
right Graph vR eR
r) GraphHom vL eL vG eG
m forall vD eD vH eH.
Graph vH eH
-> GraphHom vD eD vG eG
-> GraphHom vD eD vH eH
-> GraphHom vR eR vH eH
-> ans
ok ans
notGlueable =
  Graph vG eG
-> GraphHom vK eK vL eL
-> GraphHom vL eL vG eG
-> (forall vD eD.
    Graph vD eD -> GraphHom vK eK vD eD -> GraphHom vD eD vG eG -> ans)
-> ans
-> ans
forall vK eK vL eL vG eG ans.
Graph vG eG
-> GraphHom vK eK vL eL
-> GraphHom vL eL vG eG
-> (forall vD eD.
    Graph vD eD -> GraphHom vK eK vD eD -> GraphHom vD eD vG eG -> ans)
-> ans
-> ans
pushoutComplementGraph
    Graph vG eG
g
    GraphHom vK eK vL eL
left
    GraphHom vL eL vG eG
m
    (\Graph vD eD
d GraphHom vK eK vD eD
k2d GraphHom vD eD vG eG
d2g -> Graph vD eD
-> Graph vR eR
-> GraphHom vK eK vD eD
-> GraphHom vK eK vR eR
-> (forall vH eH.
    Graph vH eH -> GraphHom vD eD vH eH -> GraphHom vR eR vH eH -> ans)
-> ans
forall vA eA vB eB vI eI ans.
Graph vA eA
-> Graph vB eB
-> GraphHom vI eI vA eA
-> GraphHom vI eI vB eB
-> (forall vH eH.
    Graph vH eH -> GraphHom vA eA vH eH -> GraphHom vB eB vH eH -> ans)
-> ans
pushoutGraph Graph vD eD
d Graph vR eR
r GraphHom vK eK vD eD
k2d GraphHom vK eK vR eR
right \Graph vH eH
h GraphHom vD eD vH eH
d2h GraphHom vR eR vH eH
r2h -> Graph vH eH
-> GraphHom vD eD vG eG
-> GraphHom vD eD vH eH
-> GraphHom vR eR vH eH
-> ans
forall vD eD vH eH.
Graph vH eH
-> GraphHom vD eD vG eG
-> GraphHom vD eD vH eH
-> GraphHom vR eR vH eH
-> ans
ok Graph vH eH
h GraphHom vD eD vG eG
d2g GraphHom vD eD vH eH
d2h GraphHom vR eR vH eH
r2h)
    ans
notGlueable