graph-rewriting-trs (empty) → 0.1

raw patch · 11 files changed

+379/−0 lines, 11 filesdep +GLUTdep +OpenGLdep +basesetup-changed

Dependencies added: GLUT, OpenGL, base, base-unicode-symbols, containers, directory, filepath, graph-rewriting, graph-rewriting-gl, graph-rewriting-layout, uu-parsinglib

Files

• GL.hs +51/−0
• Graph.hs +42/−0
• LICENSE +10/−0
• Main.hs +77/−0
• Rules.hs +33/−0
• Setup.hs +2/−0
• Term.hs +57/−0
• TermRewriting.hs +58/−0
• examples/peano.trs +9/−0
• examples/ski.trs +3/−0
• graph-rewriting-trs.cabal +37/−0

@@ -0,0 +1,51 @@+{-# LANGUAGE UnicodeSyntax #-}+module GL () where++import Graph+import GraphRewriting.Layout.PortSpec+import qualified Graphics.UI.GLUT as GL+import GraphRewriting.GL.Render+++instance PortSpec Vertex where+	portSpec node = let sd = sameDir in case node of+		Applicator {} → [sd n, sd (sw*0.7), sd (se*0.7)]+		Variable   {} → [sd n]+		Root       {} → [sd s]+		where+			n = Vector2 0 1+			w = Vector2 (-1) 0+			e = Vector2 1 0+			s = Vector2 0 (-1)+			sw = Vector2 (-1) (-1)+			se = Vector2 1 (-1)+			nw = Vector2 (-1) 1+			ne = Vector2 1 1++instance Render Vertex where render = renderNode++renderNode Root {} = return ()+renderNode node = drawPorts node >> case node of+	Applicator {} → drawNode "*"+	Variable   {} → drawNode [name node]++drawPorts ∷ Vertex -> IO ()+drawPorts = mapM_ drawPort . relPortPos++circle r1 r2 step = mapM_ vertex2 vs where+	is = take (truncate step + 1) [0, i' .. ]+	i' = 2 * pi / step+	vs = [ (r1 * cos i, r2 * sin i) | i <- is ]++drawPort pos = GL.preservingMatrix $ do+	GL.translate $ vector pos+	GL.renderPrimitive GL.Polygon (circle 0.15 0.15 10)++drawNode label = do+	GL.renderPrimitive GL.LineLoop (circle 1 1 20)+	drawString label++drawString label = GL.preservingMatrix $ do+	GL.translate $ vector2 (-0.3,-0.3)+	GL.scale 0.0065 0.0065 (0 ∷ GL.GLdouble)+	GL.renderString GL.MonoRoman label

@@ -0,0 +1,42 @@+{-# LANGUAGE UnicodeSyntax, FlexibleInstances, MultiParamTypeClasses #-}+module Graph where++import Data.View+import GraphRewriting.Graph+import GraphRewriting.Graph.Write+import Term+import Data.Maybe (listToMaybe)++data Vertex+	= Applicator {inp, out1, out2 ∷ Port}+	| Variable   {inp ∷ Port, name ∷ Char}+	| Root       {out ∷ Port}++instance View [Port] Vertex where+	inspect node = case node of+		Applicator {inp = i, out1 = o1, out2 = o2} → [i,o1,o2]+		Variable   {inp = i}                       → [i]+		Root       {out = o}                       → [o]+	update ports node = case node of+		Applicator {} → node {inp = i, out1 = o1, out2 = o2} where [i,o1,o2] = ports+		Variable   {} → node {inp = i}                       where [i]       = ports+		Root       {} → node {out = o}                       where [o]       = ports++fromTerm ∷ Term → Graph Vertex+fromTerm term = flip execGraph emptyGraph $ do+	e ← compile term+	newNode Root {out = e}++compile ∷ Term → Rewrite Vertex Edge+compile term = do+	e ← newEdge+	case term of+		Var v → newNode Variable {inp = e, name = v}+		App f x → do+			ef ← compile f+			ex ← compile x+			newNode Applicator {inp = e, out1 = ef, out2 = ex}+	return e++maybeRead :: Read a => String -> Maybe a+maybeRead = fmap fst . listToMaybe . reads

@@ -0,0 +1,10 @@+Copyright (c) 2010, Jan Rochel+All rights reserved.++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++* Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.+* Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.+* Neither the name of the University of Utrecht nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,77 @@+{-# LANGUAGE UnicodeSyntax, FlexibleInstances, FlexibleContexts #-}+module Main where++import Prelude.Unicode+import Control.Monad+import GraphRewriting.GL.Render+import GraphRewriting.GL.UI as UI+import Term+import Graph+import GL ()+import Rules+import TermRewriting+import GraphRewriting+import GraphRewriting.Graph.Write.Unsafe as Unsafe+import GraphRewriting.Layout.Coulomb+import GraphRewriting.Layout.SpringEmbedder+import GraphRewriting.Layout.Gravitation+import GraphRewriting.Layout.Wrapper+import System.FilePath.Posix+import System.Directory+import qualified Data.Set as Set+import Data.Set (Set)+import Data.Maybe (catMaybes)+++instance Render (Wrapper Vertex) where render = render . wrappee++parseFiles ∷ (View Vertex n, View [Port] n) ⇒ Set FilePath → Set FilePath → IO [LabeledTree (Rule n)]+parseFiles done todo = if Set.null todo+	then return [Branch "Beaurocratic" [Leaf "Erase" eraseRule, Leaf "Unshare" unshare]]+	else let f = Set.findMin todo in do+		(imports, branch) ← parseFile f+		let done' = Set.insert f done+		let todo' = Set.union todo imports `Set.difference` done'+		liftM (branch:) (parseFiles done' todo')++parseFile ∷ (View Vertex n, View [Port] n) ⇒ FilePath → IO (Set FilePath, LabeledTree (Rule n))+parseFile f = do+	((imports,rules),parseErrors) ← liftM (parse ruleset) (readFile f)+	when (not $ null parseErrors) $ do+		putStrLn $ "Parse errors in " ⧺ f ⧺ ":"+		putStr $ unlines $ map show parseErrors+	imports ← liftM (Set.fromList . catMaybes) (mapM checkImport imports)+	return (imports, Branch (takeBaseName f) [Leaf (show l ⧺ " -> " ⧺ show r) (buildRule l r) | (l,r) ← rules])+	where checkImport i = do+		i ← canonicalizePath $ takeDirectory f `combine` i+		exists ← doesFileExist i+		if not exists+			then do+				putStrLn $ "Import error in " ⧺ f ⧺ ": " ⧺ i ⧺ " missing"+				return Nothing+			else return $ Just i++main ∷ IO ()+main = do+	(prog,args) ← UI.initialise+	let (files,termInput) = if length args ≥ 2+		then (init args, last args)+		else error $ "usage: " ⧺ prog ⧺ " [GLUT-options] <rules.trs> ... <term>"++	trsRules ← parseFiles Set.empty . Set.fromList =<< mapM canonicalizePath files++	let (t,parseErrors) = parse term termInput+	when (not $ null parseErrors) $ do+		putStrLn "Parse errors in input term:"+		putStr $ unlines $ map show parseErrors++	UI.run 40 id layoutStep (wrapGraph $ fromTerm t) (Branch "All" trsRules)++layoutStep n = do+	(cgf, cf, sf, rot) ← readOnly $ do+		cgf ← centralGravitation n+		cf ← coulombForce n+		sf ← springForce 1.5 n+		rot ← angularMomentum n+		return (cgf, cf, sf, rot)+	Unsafe.adjustNode (Position . sf (*0.9) . cgf (*0.01) . cf (\x → min (100/(x^2+0.1)) 10) . position) n

@@ -0,0 +1,33 @@+{-# LANGUAGE UnicodeSyntax, FlexibleContexts #-}+module Rules where++import Prelude.Unicode+import Graph+import GraphRewriting+import GraphRewriting.Graph.Read+import GraphRewriting.Graph.Write+import GraphRewriting.Graph.Write.Unsafe as Unsafe+import Control.Monad (liftM, replicateM)+import Data.Maybe (catMaybes)+++unshare ∷ (View [Port] n, View Vertex n) ⇒ Rule n+unshare = do+	e ← edge+	c ← liftReader $ edgeCardinality e+	require (c > 2)+	v ← nodeAt e+	require (e ≡ inp v)+	rewrite $ \[n] → do+		es ← deleteEdge e+		v' ← inspectNode n+		mapM (copyNode n) [v {inp = i} | i ← es, i ≢ inp v']+		deleteNode n++eraseRule ∷ (View [Port] n, View Vertex n) ⇒ Rule n+eraseRule = do+	e ← edge+	c ← liftReader $ edgeCardinality e+	require (c ≡ 1)+	nodeAt e ∷ View Vertex n ⇒ Pattern n Vertex+	erase

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,57 @@+{-# LANGUAGE UnicodeSyntax #-}+module Term where++import Prelude.Unicode+import Text.ParserCombinators.UU as UU+++data Term = App Term Term | Var Char deriving (Ord, Eq)++type Import = FilePath++instance Show Term where+	show = showComp False where+		showComp :: Bool → Term → String+		showComp isComponent expr = case expr of+			App (App e1 e2) e3 → maybeWrap $ show e1 ⧺ diverge e2 ⧺ diverge e3+			App e1 e2 → maybeWrap $ diverge e1 ⧺ diverge e2+			Var v → [v]+			where+			maybeWrap str = if isComponent then "(" ⧺ str ⧺ ")" else str+			diverge = showComp True++parse ∷ Parser a → String → (a, [Error (Int,Int)])+parse p inp = UU.parse ((,) <$> p <*> pEnd) (listToStr inp (0,0))++var ∷ Parser Term+var = Var <$> alphaNum <?> "variable"++term ∷ Parser Term+term = foldl1 App <$> pList1 (var <|> parens term) <?> "term"+	where parens p = pSym '(' *> p <* pSym ')'++pImport ∷ Parser Import+pImport = pToken "import" *>ε*> pList1 asciiPrintable++ruleset ∷ Parser ([Import], [(Term,Term)])+ruleset = (,) <$> pList (pImport <* newlines) <*> pList1 (rule <* newlines)++rule ∷ Parser (Term,Term)+rule = (,) <$> term <*ε<* arrow <*ε<*> term++-- primitive parsers++newlines ∷ Parser ()+newlines = const () <$> pMunch (`elem` "\n\r")++ε ∷ Parser () -- spaces+ε = const () <$> pMunch (`elem` "\t ")++arrow ∷ Parser String+arrow = pToken "->" <|> pToken "→" <?> "arrow"++alphaNum ∷ Parser Char+alphaNum = pSym ('a','z') <|> pSym ('A','Z') <|> pSym ('0','9') <?> "alphaNum"++asciiPrintable ∷ Parser Char+asciiPrintable = pSym ('!', '~')

@@ -0,0 +1,58 @@+{-# 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]

@@ -0,0 +1,9 @@+1 → S0+2 → S1+3 → S2+4 → S3+5 → S4+6 → S5+7 → S6+8 → S7+9 → S8

@@ -0,0 +1,3 @@+Sfgx → fx(gx)+Kxy → x+Ix → x

@@ -0,0 +1,37 @@+Name:           graph-rewriting-trs+Version:        0.1+Copyright:      (c) 2011, Jan Rochel+License:        BSD3+License-File:   LICENSE+Author:         Jan Rochel+Maintainer:     jan@rochel.info+Homepage:       http://rochel.info/#graph-rewriting+Stability:      alpha+Build-Type:     Simple+Synopsis:       Evaluate a first-order term rewrite system interactively using graph reduction+Description:    Given a set of term rewriting rules (see examples) and a term with this tool you can interactively evaluate the corresponding term graph by applying the rules, which are translated into their graph rewriting equivalents.+Category:       Graphs, Application+Cabal-Version:  >= 1.6+Data-Files:     examples/*.trs++Executable trs+  Main-Is:        Main.hs+  Build-Depends:+    base >= 4 && < 4.4,+    base-unicode-symbols >= 0.2 && < 0.3,+    graph-rewriting >= 0.5.2 && < 0.6,+    graph-rewriting-layout >= 0.4.1 && < 0.5,+    graph-rewriting-gl >= 0.6 && < 0.7,+    uu-parsinglib >= 2.5 && < 2.6,+    containers >= 0.4 && < 0.5,+    GLUT >= 2.2 && < 2.3,+    OpenGL >= 2.4 && < 2.5,+    filepath >= 1.1 && < 1.2,+    directory >= 1.0 && < 1.1+  Extensions:+    UnicodeSyntax+    FlexibleInstances+    FlexibleContexts+    MultiParamTypeClasses+  GHC-Options:    -fno-warn-duplicate-exports+  Other-Modules:  GL Graph Rules Term TermRewriting