{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Double-pushout (DPO) rewriting.
--
-- A rewrite 'Rule' is a span @l \<~ a ~> r@: @a@ is the interface that's preserved by the
-- rewrite, @l@ is matched against the host object, and @r@ replaces it. Applying a rule at
-- a match @m :: l ~> g@ proceeds in two pushout steps, both performed by 'dpoStep':
--
-- 1. Compute the /pushout complement/ of the rule's left leg and the match, giving the
--    "rest of the world" object @d@ together with legs @a ~> d@ and @d ~> g@. This step
--    can fail if the match doesn't satisfy the gluing condition.
-- 2. Push @a ~> d@ out along the rule's right leg @a ~> r@ to get the result @h@, together
--    with legs @d ~> h@ and @r ~> h@.
--
-- The two legs out of @d@ (@d ~> g@ and @d ~> h@) exhibit the rewrite step as a cospan
-- @g \<- d -> h@ relating the object before and after the rewrite.
module Proarrow.Tools.DPO
  ( HasPushoutComplements (..)
  , Rule (..)
  , dpoStep
  ) 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 Numeric.Natural (Natural)

import Proarrow.Category.Enriched.Finitary (Finitary (..), FiniteCat, elements, foreachOb, objIndex)
import Proarrow.Category.Enriched.Finitary.Topos (FINITARY, withSubobject)
import Proarrow.Category.Instance.FinHask (FINHASK, FinHask (..), reifyList)
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (Sub (..))
import Proarrow.Colimit.Pushout (HasPushouts (..))
import Proarrow.Core (CategoryOf (..))
import Proarrow.Limit.Equalizer (factorEqualizer)

-- | A rewrite rule: a span @l \<~ a ~> r@. Both legs are conventionally mono: @a@ is the
-- shared interface, @l \\ a@ is what the rule deletes, @r \\ a@ is what it creates.
data Rule a l r where
  Rule :: a ~> l -> a ~> r -> Rule a l r

-- | Apply a 'Rule' at a match @l ~> g@. On success, the continuation receives the rewrite
-- step's cospan legs @d ~> g@, @d ~> h@ and the embedding @r ~> h@ of the newly created
-- pattern in the result @h@. Calls the failure continuation if the gluing condition fails.
dpoStep
  :: forall {k} (a :: k) l r g ans
   . (HasPushoutComplements k)
  => Rule a l r
  -> l ~> g
  -> (forall d h. d ~> g -> d ~> h -> r ~> h -> ans)
  -> ans
  -> ans
dpoStep :: forall {k} (a :: k) (l :: k) (r :: k) (g :: k) ans.
HasPushoutComplements k =>
Rule a l r
-> (l ~> g)
-> (forall (d :: k) (h :: k).
    (d ~> g) -> (d ~> h) -> (r ~> h) -> ans)
-> ans
-> ans
dpoStep (Rule a ~> l
left a ~> r
right) l ~> g
m forall (d :: k) (h :: k). (d ~> g) -> (d ~> h) -> (r ~> h) -> ans
ok ans
notGlueable =
  (a ~> l)
-> (l ~> g)
-> (forall (d :: k). (a ~> d) -> (d ~> g) -> ans)
-> ans
-> ans
forall (a :: k) (l :: k) (g :: k) ans.
(a ~> l)
-> (l ~> g)
-> (forall (d :: k). (a ~> d) -> (d ~> g) -> 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
pushoutComplement a ~> l
left l ~> g
m (\a ~> d
a2d d ~> g
d2g -> (a ~> d)
-> (a ~> r)
-> (forall (p :: k). (d ~> p) -> (r ~> p) -> ans)
-> ans
forall (o :: k) (a :: k) (b :: k) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
pushout a ~> d
a2d a ~> r
right \d ~> p
d2h r ~> p
r2h -> (d ~> g) -> (d ~> p) -> (r ~> p) -> ans
forall (d :: k) (h :: k). (d ~> g) -> (d ~> h) -> (r ~> h) -> ans
ok d ~> g
d2g d ~> p
d2h r ~> p
r2h) ans
notGlueable

-- | Whether a collection has no repeats. The match may identify two elements only if the rule
-- keeps both, so a repeated image among the deleted ones is an identification conflict.
allDistinct :: (P.Int, Set.Set a) -> P.Bool
allDistinct :: forall a. (Int, Set a) -> Bool
allDistinct (Int
n, Set a
s) = Set a -> Int
forall a. Set a -> Int
Set.size Set a
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
P.== Int
n

-- | Categories where pushout complements can be computed, or shown not to exist.
--
-- Given the left leg @ll :: a ~> l@ of a rule (assumed mono, i.e. @a@ embeds into @l@) and
-- a match @m :: l ~> g@, 'pushoutComplement' either succeeds with an object @d@ and legs
-- @a ~> d@, @d ~> g@ forming a pushout square with @ll@ and @m@, or calls the second
-- continuation when no such object exists (the gluing condition fails).
class (HasPushouts k) => HasPushoutComplements k where
  pushoutComplement :: a ~> l -> l ~> g -> (forall (d :: k). a ~> d -> d ~> g -> ans) -> ans -> ans

instance HasPushoutComplements FINHASK where
  pushoutComplement :: forall (a :: FINHASK) (l :: FINHASK) (g :: FINHASK) ans.
(a ~> l)
-> (l ~> g)
-> (forall (d :: FINHASK). (a ~> d) -> (d ~> g) -> ans)
-> ans
-> ans
pushoutComplement (FinHask Map a1 b1
ll) (FinHask Map a1 b1
m) forall (d :: FINHASK). (a ~> d) -> (d ~> g) -> ans
ok ans
notGlueable =
    let
      aToG :: Map a1 b1
aToG = (a1 -> b1) -> Map a1 a1 -> Map a1 b1
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 (Map a1 b1
m Map a1 b1 -> a1 -> b1
forall k a. Ord k => Map k a -> k -> a
M.!) Map a1 b1
Map a1 a1
ll
      keptLValues :: Set b1
keptLValues = [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
ll)
      deleteList :: [b1]
deleteList = [Map a1 b1
m Map a1 b1 -> a1 -> b1
forall k a. Ord k => Map k a -> k -> a
M.! a1
l | a1
l <- Map a1 b1 -> [a1]
forall k a. Map k a -> [k]
M.keys Map a1 b1
m, a1
l a1 -> Set a1 -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set b1
Set a1
keptLValues]
      deleteValues :: Set b1
deleteValues = [b1] -> Set b1
forall a. Ord a => [a] -> Set a
Set.fromList [b1]
deleteList
      keepValues :: Set b1
keepValues = [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
aToG)
      dValues :: [b1]
dValues = [b1
g | b1
g <- [b1]
forall a. Finite a => [a]
universeF, b1
g b1 -> Set b1 -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set b1
deleteValues]
    in
      -- the match must identify no two elements that the rule does not both keep: neither a kept one
      -- with a deleted one, nor two distinct deleted ones
      if Bool -> Bool
P.not (Set b1 -> Set b1 -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set b1
keepValues Set b1
deleteValues) Bool -> Bool -> Bool
P.|| Bool -> Bool
P.not ((Int, Set b1) -> Bool
forall a. (Int, Set a) -> Bool
allDistinct ([b1] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
P.length [b1]
deleteList, Set b1
deleteValues))
        then ans
notGlueable
        else [b1] -> (forall l. Ob (FH l) => Map l b1 -> ans) -> ans
forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList [b1]
dValues \Map l b1
d ->
          let gToD :: Map b1 l
gToD = [(b1, l)] -> Map b1 l
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Map l b1
d Map l b1 -> l -> b1
forall k a. Ord k => Map k a -> k -> a
M.! l
i, l
i) | l
i <- [l]
forall a. Finite a => [a]
universeF]
          in (a ~> FH l) -> (FH l ~> g) -> ans
forall (d :: FINHASK). (a ~> d) -> (d ~> g) -> ans
ok (Map a1 l -> FinHask (FH a1) (FH l)
forall a1 b1.
(Ob (FH a1), Ob (FH b1)) =>
Map a1 b1 -> FinHask (FH a1) (FH b1)
FinHask ((b1 -> l) -> Map a1 b1 -> Map a1 l
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 (Map b1 l
gToD Map b1 l -> b1 -> l
forall k a. Ord k => Map k a -> k -> a
M.!) Map a1 b1
aToG)) (Map l b1 -> FinHask (FH l) (FH b1)
forall a1 b1.
(Ob (FH a1), Ob (FH b1)) =>
Map a1 b1 -> FinHask (FH a1) (FH b1)
FinHask Map l b1
d)

-- | Pushout complements of finitary profunctors over any finite schema, so one instance gives
-- double-pushout rewriting of graphs, typed graphs, or the rows of a database.
--
-- The gluing condition has two halves:
--
-- * no /identification conflict/: the match identifies two elements only if the rule keeps both
--   (so never a kept element with a deleted one, nor two distinct deleted ones), and
-- * the /dangling condition/: the surviving elements are closed under the schema\'s arrows, i.e.
--   form a subprofunctor that 'Reindex' can carve out. For the schema @E \-\> V@ it says a
--   surviving edge keeps both its endpoints.
instance (FiniteCat j, FiniteCat k) => HasPushoutComplements (FINITARY j k) where
  pushoutComplement :: forall (a :: FINITARY j k) (l :: FINITARY j k) (g :: FINITARY j k)
       ans.
(a ~> l)
-> (l ~> g)
-> (forall (d :: FINITARY j k). (a ~> d) -> (d ~> g) -> ans)
-> ans
-> ans
pushoutComplement (Sub (Prof @av @lv a1 :~> b1
ll)) (Sub (Prof @_ @gv b1 :~> b1
m)) forall (d :: FINITARY j k). (a ~> d) -> (d ~> g) -> ans
ok ans
notGlueable
    | Bool
noSharedImage Bool -> Bool -> Bool
P.&& Bool
noDoubleDelete =
        -- the complement is the subobject of the host that survives, and the interface lands in it
        -- by its own universal property
        forall {j} {k} (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool)
-> (forall (q :: j +-> k). Finitary q => (FIN q ~> FIN p) -> r)
-> r
-> r
forall (p :: k -> j -> Type) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool)
-> (forall (q :: k -> j -> Type).
    Finitary q =>
    (FIN q ~> FIN p) -> r)
-> r
-> r
withSubobject @gv b1 a b -> Bool
forall (a :: k) (b :: j). (Ob a, Ob b) => b1 a b -> Bool
kept (\FIN q ~> SUB b1
incl -> (a ~> FIN q) -> (FIN q ~> g) -> ans
forall (d :: FINITARY j k). (a ~> d) -> (d ~> g) -> ans
ok ((FIN q ~> SUB b1) -> (SUB a1 ~> SUB b1) -> SUB a1 ~> FIN q
forall k (e :: k) (x :: k) (e' :: k).
HasEqualizers k =>
(e ~> x) -> (e' ~> x) -> e' ~> e
forall (e :: FINITARY j k) (x :: FINITARY j k)
       (e' :: FINITARY j k).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer FIN q ~> SUB b1
incl (Prof a1 b1 -> Sub Prof (SUB a1) (SUB b1)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((a1 :~> b1) -> Prof a1 b1
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (b1 a b -> b1 a b
b1 :~> b1
m (b1 a b -> b1 a b) -> (a1 a b -> b1 a b) -> a1 a b -> b1 a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
P.. a1 a b -> b1 a b
a1 :~> b1
ll)))) FIN q ~> g
FIN q ~> SUB b1
incl) ans
notGlueable
    | Bool
P.otherwise = ans
notGlueable
    where
      -- what the match sends the rule's deleted part to, as a set per pair of objects: the checks
      -- below ask about it once per element of every hom-set, and it is not cheap
      deleted :: forall (x :: k) (y :: j). (Ob x, Ob y) => [Natural]
      deleted :: forall (x :: k) (y :: j). (Ob x, Ob y) => [Natural]
deleted =
        let keptImages :: Set Natural
keptImages = [Natural] -> Set Natural
forall a. Ord a => [a] -> Set a
Set.fromList ((a1 x y -> Natural) -> [a1 x y] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
P.map (b1 x y -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => b1 a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex (b1 x y -> Natural) -> (a1 x y -> b1 x y) -> a1 x y -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
P.. a1 x y -> b1 x y
a1 :~> b1
ll) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @av @x @y))
        in [b1 x y -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => b1 a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex (b1 x y -> b1 x y
b1 :~> b1
m b1 x y
w) | b1 x y
w <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @lv @x @y, b1 x y -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => b1 a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex b1 x y
w Natural -> Set Natural -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set Natural
keptImages]
      deletedAt :: M.Map (Natural, Natural) (P.Int, Set.Set Natural)
      deletedAt :: Map (Natural, Natural) (Int, Set Natural)
deletedAt =
        [((Natural, Natural), (Int, Set Natural))]
-> Map (Natural, Natural) (Int, Set Natural)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
          ( forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k \ @x -> forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @y ->
              [((forall (a :: k). (Enumerable k, Ob a) => Natural
forall {k} (a :: k). (Enumerable k, Ob a) => Natural
objIndex @x, forall (a :: j). (Enumerable j, Ob a) => Natural
forall {k} (a :: k). (Enumerable k, Ob a) => Natural
objIndex @y), ([Natural] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
P.length (forall (x :: k) (y :: j). (Ob x, Ob y) => [Natural]
deleted @x @y), [Natural] -> Set Natural
forall a. Ord a => [a] -> Set a
Set.fromList (forall (x :: k) (y :: j). (Ob x, Ob y) => [Natural]
deleted @x @y)))]
          )
      at :: forall (x :: k) (y :: j). (Ob x, Ob y) => (P.Int, Set.Set Natural)
      at :: forall (x :: k) (y :: j). (Ob x, Ob y) => (Int, Set Natural)
at = Map (Natural, Natural) (Int, Set Natural)
deletedAt Map (Natural, Natural) (Int, Set Natural)
-> (Natural, Natural) -> (Int, Set Natural)
forall k a. Ord k => Map k a -> k -> a
M.! (forall (a :: k). (Enumerable k, Ob a) => Natural
forall {k} (a :: k). (Enumerable k, Ob a) => Natural
objIndex @x, forall (a :: j). (Enumerable j, Ob a) => Natural
forall {k} (a :: k). (Enumerable k, Ob a) => Natural
objIndex @y)
      kept :: forall (x :: k) (y :: j). (Ob x, Ob y) => gv x y -> P.Bool
      kept :: forall (a :: k) (b :: j). (Ob a, Ob b) => b1 a b -> Bool
kept b1 x y
z = b1 x y -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => b1 a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex b1 x y
z Natural -> Set Natural -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` (Int, Set Natural) -> Set Natural
forall a b. (a, b) -> b
P.snd (forall (x :: k) (y :: j). (Ob x, Ob y) => (Int, Set Natural)
at @x @y)
      -- nothing the rule keeps may share an image with something it deletes ...
      noSharedImage :: Bool
noSharedImage =
        [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
P.and (forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k \ @x -> forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @y -> [forall (a :: k) (b :: j). (Ob a, Ob b) => b1 a b -> Bool
kept @x @y (b1 a a -> b1 a a
b1 :~> b1
m (a1 a a -> b1 a a
a1 :~> b1
ll a1 a a
v)) | a1 a a
v <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @av @x @y])
      -- ... and no two deleted elements may share one either
      noDoubleDelete :: Bool
noDoubleDelete =
        [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
P.and (forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k \ @x -> forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @y -> [(Int, Set Natural) -> Bool
forall a. (Int, Set a) -> Bool
allDistinct (forall (x :: k) (y :: j). (Ob x, Ob y) => (Int, Set Natural)
at @x @y)])