{-# LANGUAGE UnicodeSyntax, FlexibleContexts #-}
module GraphRewriting.Strategies.LeftmostOutermost where

import GraphRewriting.Pattern
import GraphRewriting.Graph.Write
import GraphRewriting.Graph.Read
import GraphRewriting.Rule
import GraphRewriting.Strategies.Control
import Data.List (intersect, (\\))


-- | Gives us the the 'left' port for a given node
class LeftmostOutermost n where lmoPort ∷ n → Maybe Port

instance LeftmostOutermost n ⇒ LeftmostOutermost (Wrapper n) where lmoPort :: Wrapper n -> Maybe Port
lmoPort = n -> Maybe Port
forall n. LeftmostOutermost n => n -> Maybe Port
lmoPort (n -> Maybe Port) -> (Wrapper n -> n) -> Wrapper n -> Maybe Port
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapper n -> n
forall n. Wrapper n -> n
wrapped

getLmoPort ∷ (LeftmostOutermost n) ⇒ Node → Pattern n Port
getLmoPort :: forall n. LeftmostOutermost n => Node -> Pattern n Port
getLmoPort Node
n = do
	n
node ← Reader (Graph n) n -> PatternT n Identity n
forall (m :: * -> *) n a.
Monad m =>
Reader (Graph n) a -> PatternT n m a
liftReader (Reader (Graph n) n -> PatternT n Identity n)
-> Reader (Graph n) n -> PatternT n Identity n
forall a b. (a -> b) -> a -> b
$ Node -> Reader (Graph n) n
forall n (m :: * -> *).
(MonadReader (Graph n) m, MonadFail m) =>
Node -> m n
readNode Node
n
	case n -> Maybe Port
forall n. LeftmostOutermost n => n -> Maybe Port
lmoPort n
node of
		Maybe Port
Nothing → String -> Pattern n Port
forall a. String -> PatternT n Identity a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Term is in WHNF"
		Just Port
lo → Port -> Pattern n Port
forall a. a -> PatternT n Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Port
lo

-- It does not compile with this type signature, even when IncoherentInstances are given in Control.
moveControl ∷ (View [Port] n, View Control n, LeftmostOutermost n) => Rule n
moveControl :: forall n.
(View [Port] n, View Control n, LeftmostOutermost n) =>
Rule n
moveControl = do
	Control {stack :: Control -> [Node]
stack = [Node]
s} ← PatternT n Identity Control
forall (m :: * -> *) v n. (MonadFail m, View v n) => PatternT n m v
node
	Node
control ← PatternT n Identity Node
forall (m :: * -> *) n. Monad m => PatternT n m Node
previous
	Port
lmo1 ← Node -> Pattern n Port
forall n. LeftmostOutermost n => Node -> Pattern n Port
getLmoPort Node
control
	Node
n ← [Node] -> PatternT n Identity Node
forall (m :: * -> *) n. MonadFail m => [Node] -> PatternT n m Node
branchNodes ([Node] -> PatternT n Identity Node)
-> PatternT n Identity [Node] -> PatternT n Identity Node
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Reader (Graph n) [Node] -> PatternT n Identity [Node]
forall (m :: * -> *) n a.
Monad m =>
Reader (Graph n) a -> PatternT n m a
liftReader (Reader (Graph n) [Node] -> PatternT n Identity [Node])
-> (Port -> Reader (Graph n) [Node])
-> Port
-> PatternT n Identity [Node]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> Port -> Reader (Graph n) [Node]
forall n (m :: * -> *).
(MonadReader (Graph n) m, MonadFail m) =>
Node -> Port -> m [Node]
adverseNodes Node
control (Port -> PatternT n Identity [Node])
-> Pattern n Port -> PatternT n Identity [Node]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Node -> Pattern n Port
forall n. LeftmostOutermost n => Node -> Pattern n Port
getLmoPort Node
control
	Rewrite n () -> Rule n
forall a. a -> PatternT n Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rewrite n () -> Rule n) -> Rewrite n () -> Rule n
forall a b. (a -> b) -> a -> b
$ do
		Node -> Control -> Rewrite n ()
forall n v. (View [Port] n, View v n) => Node -> v -> Rewrite n ()
updateNode Node
control Control
NoControl
		Node -> Control -> Rewrite n ()
forall n v. (View [Port] n, View v n) => Node -> v -> Rewrite n ()
updateNode Node
n (Control {stack :: [Node]
stack = Node
control Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
s})

-- It does not compile with this type signature, even when IncoherentInstances are given in Control.
leftmostOutermost ∷ (View Control n, View [Port] n) ⇒ Rule n → Rule n
leftmostOutermost :: forall n. (View Control n, View [Port] n) => Rule n -> Rule n
leftmostOutermost Rule n
r = do
	Rewrite n ()
rewrite ← Rule n
r
	[Node]
ns ← PatternT n Identity [Node]
forall (m :: * -> *) n. Monad m => PatternT n m [Node]
history -- we want the first node of the matching pattern
	let topnode :: Node
topnode = [Node] -> Node
forall a. HasCallStack => [a] -> a
last [Node]
ns
	Control {stack :: Control -> [Node]
stack = [Node]
s} ← Reader (Graph n) Control -> PatternT n Identity Control
forall (m :: * -> *) n a.
Monad m =>
Reader (Graph n) a -> PatternT n m a
liftReader (Reader (Graph n) Control -> PatternT n Identity Control)
-> Reader (Graph n) Control -> PatternT n Identity Control
forall a b. (a -> b) -> a -> b
$ Node -> Reader (Graph n) Control
forall v n (m :: * -> *).
(View v n, MonadReader (Graph n) m, MonadFail m) =>
Node -> m v
inspectNode Node
topnode
	Rewrite n () -> Rule n
forall a. a -> PatternT n Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rewrite n () -> Rule n) -> Rewrite n () -> Rule n
forall a b. (a -> b) -> a -> b
$ do
		Node -> Control -> Rewrite n ()
forall n v. (View [Port] n, View v n) => Node -> v -> Rewrite n ()
updateNode Node
topnode Control
NoControl -- First we set the topnode to not be the control node any more
		[Node]
oldNodes ← Rewrite n [Node]
forall n (m :: * -> *). MonadReader (Graph n) m => m [Node]
readNodeList
		Rewrite n ()
rewrite -- then we perform the rewrite
		[Node]
newNodes ← Rewrite n [Node]
forall n (m :: * -> *). MonadReader (Graph n) m => m [Node]
readNodeList
		let s' :: [Node]
s' = [Node] -> [Node] -> [Node]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Node]
s [Node]
newNodes -- only consider nodes for the control marker that exist
		if [Node] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Node]
s' -- even the topmost node has been replaced
			then do -- we assign the control marker to one of the newly created nodes
				let addedNodes :: [Node]
addedNodes = [Node]
newNodes [Node] -> [Node] -> [Node]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Node]
oldNodes
				Node -> Control -> Rewrite n ()
forall n v. (View [Port] n, View v n) => Node -> v -> Rewrite n ()
updateNode ([Node] -> Node
forall a. HasCallStack => [a] -> a
head [Node]
addedNodes) (Control {stack :: [Node]
stack = []}) -- finally we set the previous node on the stack as the control node
			else do -- set the previous node on the stack as the control node
				Node -> Control -> Rewrite n ()
forall n v. (View [Port] n, View v n) => Node -> v -> Rewrite n ()
updateNode ([Node] -> Node
forall a. HasCallStack => [a] -> a
head [Node]
s') (Control {stack :: [Node]
stack = [Node] -> [Node]
forall a. HasCallStack => [a] -> [a]
tail [Node]
s'})