-- Now we are going to specify rewriting rules that implement the SKI combinator reductions. Refer to the module decumentation of GraphRewriting.Pattern and GraphRewriting.Rule for more detailed information about the functions used here.
module Rules where

import Prelude.Unicode
import Graph
import GraphRewriting
import GraphRewriting.Pattern.InteractionNet -- This gives us the 'activePair' pattern.


-- The simplest of the SKI combinators is the I combinator. We match on the active pair of an I node and an applicator using the 'activePair' function which resides in the 'Pattern' monad. Note that the :-: is an infix constructor and is just an alternative representation of a pair. With the left-hand side of the rule given, we build a rule out of it that erases the matched nodes and connects the edges at the input port and the right output port of the applicator using the 'rewire' function.
ruleI ∷ (View [Port] n, View SKI n) ⇒ Rule n
ruleI = do
	I {} :-: A {inp = iA, out2 = o2} ← activePair
	rewire [[iA,o2]]

-- The K0 node represents a K combinator that has not yet accumulated an argument, which is what this rule does. Again, we match an active pair of a K0 node and an applicator. Then we replace these nodes by a K1 node that has the right-hand subgraph of the applicator as an argument (at its output port).
ruleK0 ∷ (View [Port] n, View SKI n) ⇒ Rule n
ruleK0 = do
	K0 {} :-: A  {inp = iA, out2 = o2} ← activePair
	replace0 [Node $ K1 {inp = iA, out = o2}]

-- The 'replace*' functions can be used replace the matched nodes by a combination of new nodes and rewirings, hence the constructors 'Wire' and 'Node'.
ruleK1 ∷ (View [Port] n, View SKI n) ⇒ Rule n
ruleK1 = do
	K1 {out = oK} :-: A {inp = iA, out2 = o2A} ← activePair
	replace0 [Wire iA oK, Node $ E {inp = o2A}]

ruleS0 ∷ (View [Port] n, View SKI n) ⇒ Rule n
ruleS0 = do
	S0 {} :-: A {inp = iA, out2 = o2A} ← activePair
	replace0 [Node $ S1 {inp = iA, out = o2A}]

ruleS1 ∷ (View [Port] n, View SKI n) ⇒ Rule n
ruleS1 = do
	S1 {out = oS} :-: A {inp = iA, out2 = o2A} ← activePair
	replace0 [Node $ S2 {inp = iA, out1 = oS, out2 = o2A}]

-- If we need new edges for the right-hand side of the rewrite rule you can use 'replaceN' with N > 0.
ruleS2 ∷ (View [Port] n, View SKI n) ⇒ Rule n
ruleS2 = do
	S2 {inp = iS, out1 = oS1, out2 = o2S} :-: a@A {out1 = o1A, out2 = o2A} ← activePair
	replace3 $ \i1D iB i2D →
		[Node $ A {inp = iS, out1 = oS1, out2 = i1D},
		 Node $ a {out2 = iB},
		 Node $ D {inp1 = i1D, inp2 = i2D, out = o2A},
		 Node $ A {inp = iB, out1 = o2S, out2 = i2D}]

-- This is an abstraction to match any active pair that involves a node with arity 0.
arity0 ∷ (View [Port] n, View SKI n) ⇒ Pattern n (Pair SKI)
arity0 = anyOf [e,i,k,s] where
	e = do {pair@(n :-: E  {}) ← activePair; return pair}
	i = do {pair@(n :-: I  {}) ← activePair; return pair}
	k = do {pair@(n :-: K0 {}) ← activePair; return pair}
	s = do {pair@(n :-: S0 {}) ← activePair; return pair}

arity1 ∷ (View [Port] n, View SKI n) ⇒ Pattern n (Pair SKI)
arity1 = k <|> s where
	k = do {pair@(n :-: K1 {}) ← activePair; return pair}
	s = do {pair@(n :-: S1 {}) ← activePair; return pair}

-- If the left-hand side is to be erased completely without any rewirings or new nodes to be replaced with, use the 'erase'.
ruleE0 ∷ (View [Port] n, View SKI n) ⇒ Rule n 
ruleE0 = do
	E {inp = iE} :-: n ← arity0
	erase
	
ruleE1 ∷ (View [Port] n, View SKI n) ⇒ Rule n 
ruleE1 = do
	E {} :-: n ← arity1
	replace0 [Node $ E {inp = out n}]
	
ruleE2 ∷ (View [Port] n, View SKI n) ⇒ Rule n 
ruleE2 = do
	E {inp = iE} :-: S2 {inp = iS, out1 = o1, out2 = o2} ← activePair
	replace0 [Node $ E {inp = o1}, Node E {inp = o2}]

ruleD0  ∷ (View [Port] n, View SKI n) ⇒ Rule n
ruleD0 = do
	D {inp1 = iD1, inp2 = iD2, out = oD} :-: n ← arity0
	replace0 [Node $ n {inp = iD1}, Node $ n {inp = iD2}]

ruleD1  ∷ (View [Port] n, View SKI n) ⇒ Rule n
ruleD1 = do
	D {inp1 = iD1, inp2 = iD2, out = oD} :-: n ← arity1
	replace2 $ \iD1' iD2' →
		[Node $ n {inp = iD1, out = iD1'},
		 Node $ n {inp = iD2, out = iD2'},
		 Node $ D {inp1 = iD1', inp2 = iD2', out = out n}]
	
ruleD2 ∷ (View [Port] n, View SKI n) ⇒ Rule n 
ruleD2 = do
	D {inp1 = iD1, inp2 = iD2, out = oD} :-: S2 {inp = iS, out1 = o1, out2 = o2} ← activePair
	replace4 $ \l1 l2 x1 x2 →
		[Node $ S2 {inp = iD1, out1 = l1, out2 = x1},
		 Node $ S2 {inp = iD2, out1 = x2, out2 = l2},
		 Node $ D {inp1 = l1, inp2 = x2, out = o1},
		 Node $ D {inp1 = x1, inp2 = l2, out = o2}]

-- Here is the only rule that is not an interaction-net reduction, hence it does not rely on the 'activePair' pattern. First we match on an eraser node anywhere in the graph. Next we require a duplicator node that is connected to the eraser. Therefore we use the 'previous' pattern that returns a reference to the previously matched node and feed it to the 'neighbour' function that matches on nodes connected to the referenced node.
eliminate ∷ (View [Port] n, View SKI n) ⇒ Rule n
eliminate = do
	E {inp = iE} ← node
	D {out = oD, inp1 = i1, inp2 = i2} ← neighbour =<< previous
	require (iE ≡ i1 ∨ iE ≡ i2)
	if iE ≡ i1
		then rewire [[oD,i2]]
		else rewire [[oD,i1]]

-- Together with the signature defined in Graph.hs these rules can be used to actually perform graph transformations. Therefore use the 'GraphRewriting.Graph.execGraph' and 'GraphRewriting.Rule.apply' functions. In GL.hs we're going to provide the layouting and graphics engines information on how to arrange and display the nodes.