graph-rewriting-trs-0.1: TermRewriting.hs

{-# LANGUAGE UnicodeSyntax, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
module TermRewriting (buildRule) where

import Prelude.Unicode
import GraphRewriting
import GraphRewriting.Pattern
import GraphRewriting.Graph.Read
import GraphRewriting.Graph.Write
import Data.Char (isLower)
import Control.Monad
import Data.Map (Map)
import qualified Data.Map as Map
import Term
import Graph


type VarMap = Map Char Edge

buildRule ∷ (View Vertex n, View [Port] n) ⇒ Term → Term → Rule n
buildRule lhs rhs = do
	(inc, varMap) ← buildLHS lhs
	buildRHS varMap rhs inc

buildLHS ∷ (View Vertex n, View [Port] n) ⇒ Term → Pattern n (Edge, VarMap)
buildLHS term = do
	e ← edge
	varMap ← build term e
	return (e, varMap)
	where build term inc = do
		c ← liftReader (edgeCardinality inc)
		require (c ≡ 2)
		case term of
			Var v | isLower v → return $ Map.singleton v inc
			Var v | otherwise → do
				Variable {name = n} ← nodeAt inc
				require (n ≡ v)
				return Map.empty
			App f x → do
				Applicator {inp = i, out1 = o1, out2 = o2} ← nodeAt inc
				require (i ≡ inc)
				liftM2 (Map.unionWithKey nonLinear) (build f o1) (build x o2)
				where nonLinear v = error $ "Left-hand side is not linear as " ⧺ [v] ⧺ " occurs twice"

buildRHS ∷ (View Vertex n, View [Port] n) ⇒ VarMap → Term → Edge → Rule n
buildRHS bindings term inc = replace (reqEdges term) (build term inc) where

	reqEdges (App f x) = 2 + reqEdges f + reqEdges x
	reqEdges (Var v) = 0

	build (App f x) inc (fEdge:xEdge:edges) = let (fEdges,xEdges) = splitAt (reqEdges f) edges
		in Node Applicator {inp = inc, out1 = fEdge, out2 = xEdge} : build f fEdge fEdges ⧺ build x xEdge xEdges

	build (Var v) inc [] = singleton $ if isLower v
		then maybe freeVar (Wire inc) (Map.lookup v bindings)
		else Node Variable {inp = inc, name = v}
		where freeVar = error $ [v] ⧺ " occurs free on the right-hand side"

	singleton x = [x]