graph-rewriting-trs-0.1.2: 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 = case term of
		Var v | isLower v → return $ Map.singleton v inc
		Var v | otherwise → do
			c ← liftReader (edgeCardinality inc)
			require (c ≡ 2)
			Variable {name = n} ← nodeAt inc
			require (n ≡ v)
			return Map.empty
		App f x → do
			c ← liftReader (edgeCardinality inc)
			require (c ≡ 2)
			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]