-- | 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 Proarrow.Category.Instance.FinHask (FINHASK, FinHask (..), reifyList)
import Proarrow.Colimit.Pushout (HasPushouts (..))
import Proarrow.Core (CategoryOf (..))

-- | 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

-- | 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)
      deleteValues :: Set b1
deleteValues = [b1] -> Set b1
forall a. Ord a => [a] -> Set a
Set.fromList [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]
      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
      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)
        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)