{-# LANGUAGE UnicodeSyntax, FlexibleInstances, FlexibleContexts #-}
-- | Rewrite rules are represented as nested monads: a 'Rule' is a 'Pattern' that returns a 'Rewrite' the latter directly defining the transformation of the graph.
--
-- For rule construction a few functions a provided: The most primitive one is 'rewrite'. In most cases 'erase', 'rewire', and 'replace' should be more convenient. These functions express rewrites that /replace/ the matched nodes of the 'Pattern', which comes quite close to the @L -> R@ form in which graph rewriting rules are usually expressed.
module GraphRewriting.Rule (Replace, module GraphRewriting.Rule) where

import Prelude.Unicode

import GraphRewriting.Graph.Read
import GraphRewriting.Graph.Write
import GraphRewriting.Rule.Internal
import GraphRewriting.Pattern
import Control.Monad.State
import Control.Monad.Reader
import Data.List (nub)


-- | A rewriting rule is defined as a 'Pattern' that returns a 'Rewrite'
type Rule n = Pattern n (Rewrite n ())

-- | Apply rule at an arbitrary position if applicable
apply ∷ Rule n → Rewrite n ()
apply :: forall n. Rule n -> Rewrite n ()
apply = let void :: m a -> m ()
void m a
m = m a
m forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return () in forall {m :: * -> *} {a}. Monad m => m a -> m ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. Rule n -> Rewrite n Bool
apply'

-- | Apply rule at an arbitrary position. Return value states whether the rule was applicable.
apply' ∷ Rule n → Rewrite n Bool
apply' :: forall n. Rule n -> Rewrite n Bool
apply' Rule n
r = do
	[Rewrite n ()]
contractions ← forall n a. Pattern n a -> Graph n -> [a]
evalPattern Rule n
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *). MonadReader r m => m r
ask
	if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Rewrite n ()]
contractions
		then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
		else forall a. [a] -> a
head [Rewrite n ()]
contractions forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

-- rule construction ---------------------------------------------------------

-- | primitive rule construction with the matched nodes of the left hand side as a parameter
rewrite ∷ (Match → Rewrite n a) → Rule n
rewrite :: forall n a. (Match -> Rewrite n a) -> Rule n
rewrite Match -> Rewrite n a
r = do
	Match
h ← forall (m :: * -> *) n. Monad m => PatternT n m Match
history
	forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Match -> Rewrite n a
r Match
h forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | constructs a rule that deletes all of the matched nodes from the graph
erase ∷ View [Port] n ⇒ Rule n
erase :: forall n. View [Port] n => Rule n
erase = forall n a. (Match -> Rewrite n a) -> Rule n
rewrite forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall n. View [Port] n => Node -> Rewrite n ()
deleteNode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [a]
nub

-- | Constructs a rule from a list of rewirings. Each rewiring specifies a list of hyperedges that are to be merged into a single hyperedge. All matched nodes of the left-hand side are removed.
rewire ∷ View [Port] n ⇒ [[Edge]] → Rule n
rewire :: forall n. View [Port] n => [[Port]] -> Rule n
rewire [[Port]]
ess = forall n a. (Match -> Rewrite n a) -> Rule n
rewrite forall a b. (a -> b) -> a -> b
$ \Match
hist → do
	forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall n. View [Port] n => [Port] -> Rewrite n ()
mergeEs forall a b. (a -> b) -> a -> b
$ [[Port]] -> [[Port]]
joinEdges [[Port]]
ess
	forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall n. View [Port] n => Node -> Rewrite n ()
deleteNode forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
nub Match
hist


instance Monad (Replace n) where
	return :: forall a. a -> Replace n a
return a
x = forall n a. Rewrite n (a, [[Port]]) -> Replace n a
Replace forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, [])
	Replace Rewrite n (a, [[Port]])
r1 >>= :: forall a b. Replace n a -> (a -> Replace n b) -> Replace n b
>>= a -> Replace n b
f = forall n a. Rewrite n (a, [[Port]]) -> Replace n a
Replace forall a b. (a -> b) -> a -> b
$ do
		(a
x1, [[Port]]
merges1) ← Rewrite n (a, [[Port]])
r1
		let Replace Rewrite n (b, [[Port]])
r2 = a -> Replace n b
f a
x1
		(b
y, [[Port]]
merges2) ← Rewrite n (b, [[Port]])
r2
		forall (m :: * -> *) a. Monad m => a -> m a
return (b
y, [[Port]]
merges1 forall α. [α] -> [α] -> [α]
⧺ [[Port]]
merges2)

instance Functor (Replace n) where
	fmap :: forall a b. (a -> b) -> Replace n a -> Replace n b
fmap a -> b
f (Replace Rewrite n (a, [[Port]])
r) = forall n a. Rewrite n (a, [[Port]]) -> Replace n a
Replace forall a b. (a -> b) -> a -> b
$ do
		(a
x, [[Port]]
merges) ← Rewrite n (a, [[Port]])
r
		forall (m :: * -> *) a. Monad m => a -> m a
return (a -> b
f a
x, [[Port]]
merges)

instance Applicative (Replace n) where
	Replace Rewrite n (a -> b, [[Port]])
rf <*> :: forall a b. Replace n (a -> b) -> Replace n a -> Replace n b
<*> Replace Rewrite n (a, [[Port]])
rx = forall n a. Rewrite n (a, [[Port]]) -> Replace n a
Replace forall a b. (a -> b) -> a -> b
$ do
		(a -> b
f, [[Port]]
merges1) ← Rewrite n (a -> b, [[Port]])
rf
		(a
x, [[Port]]
merges2) ← Rewrite n (a, [[Port]])
rx
		forall (m :: * -> *) a. Monad m => a -> m a
return (a -> b
f a
x, [[Port]]
merges1 forall α. [α] -> [α] -> [α]
⧺ [[Port]]
merges2)
	pure :: forall a. a -> Replace n a
pure = forall (m :: * -> *) a. Monad m => a -> m a
return

instance Semigroup (Replace n ()) where
	<> :: Replace n () -> Replace n () -> Replace n ()
(<>) = forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>)

instance Monoid (Replace n ()) where
	mempty :: Replace n ()
mempty = forall (m :: * -> *) a. Monad m => a -> m a
return ()
	mappend :: Replace n () -> Replace n () -> Replace n ()
mappend = forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>)

replace ∷ View [Port] n ⇒ Replace n () → Rule n
replace :: forall n. View [Port] n => Replace n () -> Rule n
replace (Replace Rewrite n ((), [[Port]])
rhs) = do
	Match
lhs ← forall a. Eq a => [a] -> [a]
nub forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) n. Monad m => PatternT n m Match
history
	forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Match
lhs) (forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"replace: must match at least one node")
	forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
		forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall n. View [Port] n => [Port] -> Rewrite n ()
mergeEs forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [[Port]] -> [[Port]]
joinEdges forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rewrite n ((), [[Port]])
rhs
		forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall n. View [Port] n => Node -> Rewrite n ()
deleteNode Match
lhs

byNode ∷ (View [Port] n, View v n) ⇒ v → Replace n ()
byNode :: forall n v. (View [Port] n, View v n) => v -> Replace n ()
byNode v
v = forall n a. Rewrite n (a, [[Port]]) -> Replace n a
Replace forall a b. (a -> b) -> a -> b
$ do
	Node
n ← forall a. [a] -> a
head forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall n (m :: * -> *). MonadReader (Graph n) m => m Match
readNodeList
	Node
_ ← forall n v.
(View [Port] n, View v n) =>
Node -> v -> Rewrite n Node
copyNode Node
n v
v
	forall (m :: * -> *) a. Monad m => a -> m a
return ((), [])

byNewNode ∷ View [Port] n ⇒ n → Replace n ()
byNewNode :: forall n. View [Port] n => n -> Replace n ()
byNewNode n
n = forall n a. Rewrite n (a, [[Port]]) -> Replace n a
Replace forall a b. (a -> b) -> a -> b
$ forall n. View [Port] n => n -> Rewrite n Node
newNode n
n forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return ((), [])

byEdge ∷ Replace n Edge
byEdge :: forall n. Replace n Port
byEdge = forall n a. Rewrite n (a, [[Port]]) -> Replace n a
Replace forall a b. (a -> b) -> a -> b
$ do
	Port
e ← forall n. Rewrite n Port
newEdge
	forall (m :: * -> *) a. Monad m => a -> m a
return (Port
e, [])

byWire ∷ Edge → Edge → Replace n ()
byWire :: forall n. Port -> Port -> Replace n ()
byWire Port
e1 Port
e2 = forall n. [Port] -> Replace n ()
byConnector [Port
e1,Port
e2]

byConnector ∷ [Edge] → Replace n ()
byConnector :: forall n. [Port] -> Replace n ()
byConnector [Port]
es = forall n a. Rewrite n (a, [[Port]]) -> Replace n a
Replace forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ((), [[Port]
es])

-- combinators ---------------------------------------------------------------

-- | Apply two rules consecutively. Second rule is only applied if first one succeeds. Fails if (and only if) first rule fails.
(>>>) ∷ Rule n → Rule n → Rule n
Rule n
r1 >>> :: forall n. Rule n -> Rule n -> Rule n
>>> Rule n
r2 = do
	Rewrite n ()
rw1 ← Rule n
r1
	forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Rewrite n ()
rw1 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall n. Rule n -> Rewrite n ()
apply Rule n
r2

-- | Make a rule exhaustive, i.e. such that (when applied) it reduces redexes until no redexes are occur in the graph.
exhaustive ∷ Rule n → Rule n
exhaustive :: forall n. Rule n -> Rule n
exhaustive = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall n. Rule n -> Rule n -> Rule n
(>>>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a]
repeat

-- | Make a rule parallel, i.e. such that (when applied) all current redexes are contracted one by one. Neither new redexes or destroyed redexes are reduced.
everywhere ∷ Rule n → Rule n
everywhere :: forall n. Rule n -> Rule n
everywhere Rule n
r = do
	[Match]
ms ← forall (m :: * -> *) n a.
Monad m =>
PatternT n m a -> PatternT n m a
amnesia forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) n a.
Monad m =>
PatternT n m a -> PatternT n m [Match]
matches Rule n
r
	forall n. Rule n -> Rule n
exhaustive forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) n a.
Monad m =>
(Match -> Match -> Bool) -> PatternT n m a -> PatternT n m a
restrictOverlap (\Match
hist Match
future → Match
future forall α. Eq α => α -> [α] -> Bool
∈ [Match]
ms) Rule n
r

-- | Repeatedly apply the rules from the given list prefering earlier entries.
-- Returns a list of indexes reporting the sequence of rules that has applied.
benchmark ∷ [Rule n] → Rewrite n [Int]
benchmark :: forall n. [Rule n] -> Rewrite n [Int]
benchmark [Rule n]
rules = Rewrite n [Int]
rec where

	rec :: Rewrite n [Int]
rec = do
		[(Int, Rewrite n ())]
contractions ← forall n a. Pattern n a -> Graph n -> [a]
evalPattern (forall (f :: * -> *) a. Alternative f => [f a] -> f a
anyOf [PatternT n Identity (Int, Rewrite n ())]
indexedRules) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *). MonadReader r m => m r
ask
		case [(Int, Rewrite n ())]
contractions of
			[] → forall (m :: * -> *) a. Monad m => a -> m a
return []
			(Int
i,Rewrite n ()
rw) : [(Int, Rewrite n ())]
_ → forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int
iforall a. a -> [a] -> [a]
:) (Rewrite n ()
rw forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Rewrite n [Int]
rec)

	indexedRules :: [PatternT n Identity (Int, Rewrite n ())]
indexedRules = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {m :: * -> *} {a} {b}. Monad m => a -> m b -> m (a, b)
addIndex [Int
0..] [Rule n]
rules where
		addIndex :: a -> m b -> m (a, b)
addIndex a
i m b
rule = do
			b
rw ← m b
rule
			forall (m :: * -> *) a. Monad m => a -> m a
return (a
i, b
rw)