graph-rewriting-lambdascope (empty) → 0.4.3

raw patch · 9 files changed

+507/−0 lines, 9 filesdep +GLUTdep +IndentParserdep +OpenGLsetup-changed

Dependencies added: GLUT, IndentParser, OpenGL, base, base-unicode-symbols, graph-rewriting, graph-rewriting-gl, graph-rewriting-layout, parsec

Files

• GL.hs +69/−0
• Graph.hs +60/−0
• LICENSE +10/−0
• Main.hs +55/−0
• Resolver.hs +60/−0
• Rules.hs +142/−0
• Setup.hs +2/−0
• Term.hs +74/−0
• graph-rewriting-lambdascope.cabal +35/−0

@@ -0,0 +1,69 @@+module GL () where++import Graph+import GraphRewriting.Layout.PortSpec+import qualified Graphics.UI.GLUT as GL+import GraphRewriting.GL.Render+++instance PortSpec NodeLS where+	portSpec node = let sd = sameDir in case node of+		Initiator  {} → [sd s]+		Applicator {} → [sd n, sd s, sd e]+		Abstractor {} → [sd n, sd s, sd e]+		Constant   {} → [sd n]+		Function   {} → [sd n, sd s]+		Eraser     {} → [sd n]+		Duplicator {} → [sd n, (sw, s), (se, s)]+		Delimiter  {} → [sd $ Vector2 0 0.6, sd $ Vector2 0 (-0.6)]+		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)++instance Render NodeLS where render = renderNode++renderNode node = drawPorts node >> case node of+	Initiator  {} → drawNode "I"+	Applicator {} → drawNode "A"+	Abstractor {} → drawNode "L"+	Constant   {} → drawNode (name node)+	Function   {} → drawNode (name node)+	Eraser     {} → drawNode ""+	Duplicator {} → do+		GL.preservingMatrix $ GL.renderPrimitive GL.LineLoop $ do+			vertex2 (0,1)+			vertex2 (-1,-1)+			vertex2 (1,-1)+		drawString $ show $ level node+	Delimiter {} → do+		GL.renderPrimitive GL.LineStrip $ do+			vertex2 (-0.8,-0.3)+			vertex2 (-0.8,0)+			vertex2 (0.8,0)+			vertex2 (0.8,-0.3)+		drawString $ show $ level node++drawPorts ∷ NodeLS -> 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.007 0.007 (0 ∷ GL.GLdouble)+	GL.renderString GL.MonoRoman label

@@ -0,0 +1,60 @@+module Graph where++import Prelude.Unicode+import Data.View+import GraphRewriting.Graph.Types+import GraphRewriting.Pattern.InteractionNet+++data NodeLS+	= Initiator  {out ∷ Port}+	| Applicator {inp, func, arg ∷ Port}+	| Abstractor {inp, body, var ∷ Port}+	| Constant   {inp ∷ Port, name ∷ String}+	| Function   {inp ∷ Port, out ∷ Port , name ∷ String}+	| Eraser     {inp ∷ Port}+	| Duplicator {level ∷ Int, inp, out1, out2 ∷ Port}+	| Delimiter  {level ∷ Int, inp, out ∷ Port}+	| Multiplier {out ∷ Port, ins ∷ [Port]} -- only intermediate compilation result++-- | equality as defined in the paper with only the relevant cases included+instance Eq NodeLS where+	Eraser     {}           == Eraser     {} = True+	Duplicator {level = l1} == Duplicator {level = l2} = l1 ≡ l2+	Delimiter  {level = l1} == Delimiter  {level = l2} = l1 ≡ l2+	_ == _ = False++instance View [Port] NodeLS where+	inspect node = case node of+		Initiator  {out = o}                       → [o]+		Applicator {inp = i, func = f, arg = a}    → [i,f,a]+		Abstractor {inp = i, body = b, var = v}    → [i,b,v]+		Constant   {inp = i}                       → [i]+		Function   {inp = i, out = o}              → [i,o]+		Eraser     {inp = i}                       → [i]+		Duplicator {inp = i, out1 = o1, out2 = o2} → [i,o1,o2]+		Delimiter  {inp = i, out = o}              → [i,o]+		Multiplier {out = o, ins = is}             → o:is+	update ports node = case node of+		Initiator  {} → node {out = o}                       where [o]       = ports+		Applicator {} → node {inp = i, func = f, arg = a}    where [i,f,a]   = ports+		Abstractor {} → node {inp = i, body = b, var = v}    where [i,b,v]   = ports+		Constant   {} → node {inp = i}                       where [i]       = ports+		Function   {} → node {inp = i, out = o}              where [i,o]     = ports+		Eraser     {} → node {inp = i}                       where [i]       = ports+		Duplicator {} → node {inp = i, out1 = o1, out2 = o2} where [i,o1,o2] = ports+		Delimiter  {} → node {inp = i, out = o}              where [i,o]     = ports+		Multiplier {} → node {out = o, ins = is}             where o:is      = ports++instance INet NodeLS where principalPort = pp +	+pp ∷ NodeLS → Int +pp node = case node of+	Initiator  {} → 0+	Applicator {} → 1+	Abstractor {} → 0+	Delimiter  {} → 0+	Constant   {} → 0+	Function   {} → 1+	Duplicator {} → 0+	Eraser     {} → 0

@@ -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 <ORGANIZATION> 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,55 @@+module Main where++import GraphRewriting.Graph+import GraphRewriting.GL.Render+import GraphRewriting.GL.UI as UI+import Term (parseFile)+import Resolver (resolve)+import Graph+import GL ()+import Rules+import GraphRewriting.Rule+import GraphRewriting.Pattern+import GraphRewriting.Graph.Read+import GraphRewriting.Graph.Write.Unsafe as Unsafe+import GraphRewriting.Layout.Coulomb+import GraphRewriting.Layout.SpringEmbedder+import GraphRewriting.Layout.Gravitation+import GraphRewriting.Layout.Wrapper+++instance Render (Wrapper NodeLS) where render = render . wrappee++main ∷ IO ()+main = do+	(prog,args) ← UI.initialise+	file ← case args of+		[f] → return f+		___ → error "usage: vle [GLUT-options] <file>"+	term ← parseFile file+	let hypergraph = resolve term+	let graph = execGraph (apply $ exhaustive compileShare) (wrapGraph hypergraph)+	UI.run 40 id layoutStep graph ruleTree++layoutStep = do+	withNodes $ \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+		Unsafe.adjustNode (rot (*0.9)) n++ruleTree = Branch "All"+	[Branch "All but Beta"+	 	[Leaf "Duplicate" duplicate,+	 	 Leaf "Eliminate" (eliminateDelimiter <|> eliminateDuplicator),+	 	 Leaf "Annihilate" annihilate,+	 	 Leaf "Commute Delimiter" commuteDelimiter,+	 	 Leaf "Erase" eraser, +	 	 Branch "Primitive" [Leaf "Constant" applyConstant, Leaf "Function" applyFunction]],+	 Leaf "All but Beta (exhaustively)" $ exhaustive $ anyOf [duplicate, eliminateDelimiter, eliminateDuplicator, annihilate, commuteDelimiter, eraser, applyConstant, applyFunction],+	 Leaf "Beta Reduction" beta]+--	 Leaf "\"Readback\"" readback]

@@ -0,0 +1,60 @@+-- | Term to graph transformation where variable names are resolved to graph edges (or constants)+module Resolver (resolve) where++import Prelude.Unicode+import Term+import Graph+import GraphRewriting.Graph+import GraphRewriting.Graph.Write+import Control.Monad (liftM, zipWithM)+++type Compiler = Rewrite NodeLS++type Environment = [Name]+data Name = Name {symbol ∷ String, boundByLambda ∷ Bool, reference ∷ Compiler Edge}++resolve ∷ Λ → Graph NodeLS+resolve term = flip execGraph emptyGraph $ do+	o ← newEdge+	i ← newNode Initiator {out = o}+	compile [] o term++compile ∷ Environment → Edge → Λ → Compiler ()+compile env p term = case term of+	A func arg → do+		f ← newEdge+		x ← newEdge+		newNode Applicator {inp = p, func = f, arg = x}+		compile env f func+		compile env x arg+	Λ x e → do+		b ← newEdge+		(v, name) ← bindName True x+		newNode Abstractor {inp = p, body = b, var = v}+		compile (name : env) b e+	V var → case env of+		[  ] → newNode Constant {inp = p, name = var} >> return ()+		n:ns → if var ≡ symbol n+			then mergeEdges p =<< reference n+			else if boundByLambda n+				then do+					p' ← newEdge+					newNode Delimiter {level = 0, inp = p', out = p}+					compile ns p' term+				else compile ns p term+	L binds e → do+		(es, names) ← liftM unzip $ mapM (bindName False) (map fst binds)+		let env' = names ⧺ env+		zipWithM (compile env') es (Prelude.map snd binds)+		compile env' p e++bindName ∷ Bool → String → Compiler (Edge, Name)+bindName lambda sym = do+	v ← newEdge+	s ← newNode Multiplier {out = v, ins = []}+	let ref = do+		e ← newEdge+		modifyNode s $ \s → s {ins = e : ins s}+		return e+	return (v, Name {symbol = sym, boundByLambda = lambda, reference = ref})

@@ -0,0 +1,142 @@+module Rules where++import Prelude.Unicode+import Graph+import GraphRewriting.Rule+import GraphRewriting.Pattern+import GraphRewriting.Pattern.InteractionNet+import GraphRewriting.Graph.Read+import Data.List (transpose)+++compileShare ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+compileShare = do+	Multiplier {out = o, ins = is} ← node+	case is of+		[ ] → replace0 [Node $ Eraser {inp = o}]+		[i] → rewire [[o,i]]+		ins → let (ins1, ins2) = splitAt (length ins `div` 2) ins in replace2 $ \o1 o2 → +			[Node $ Duplicator {level = 0, inp = o, out1 = o1, out2 = o2},+			 Node $ Multiplier {out = o1, ins = ins1},+			 Node $ Multiplier {out = o2, ins = ins2}]++withoutIdx ∷ [a] → Int → [a]+withoutIdx xs i = let (ys,zs) = splitAt i xs in ys ⧺ tail zs++insertIdx ∷ Int → a → [a] → [a]+insertIdx i x xs = let (l,r) = splitAt i xs in l ⧺ [x] ⧺ r++split ∷ Int → Int → [a] → [[a]]+split i n [] = replicate n []+split i n xs = let (x,xs') = splitAt i xs in x : split i n xs'++transpose' n [] = replicate n []+transpose' n xs = transpose xs++commute ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+commute = do+	n1 :-: n2 ← activePair+	require (n1 ≢ n2)+	let aux1 = inspect n1 `withoutIdx` pp n1+	let aux2 = inspect n2 `withoutIdx` pp n2+	let es1 = length aux1+	let es2 = length aux2+	replace (es1 * es2) $ \edges → let+			edges1 = split es1 es2 edges+			edges2 = transpose' es1 edges1+		in [Node $ updateLevel n2 $ update (insertIdx (pp n1) pp1 auxs) n1 | (pp1,auxs) ← zip aux2 edges1]+		 ⧺ [Node $ updateLevel n1 $ update (insertIdx (pp n2) pp2 auxs) n2 | (pp2,auxs) ← zip aux1 edges2]+	where updateLevel you me = case me of+		Duplicator {} → maybeLevelUp+		Delimiter  {} → maybeLevelUp+		_ → me+		where maybeLevelUp = case you of+			Delimiter  {} → if level you ≤ level me then me {level = level me + 1} else me+			Abstractor {} → me {level = level me + 1}+			_ → me++annihilate ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+annihilate = do+	n1 :-: n2 ← activePair+	require (n1 ≡ n2)+	let aux1 = inspect n1 `withoutIdx` pp n1+	let aux2 = inspect n2 `withoutIdx` pp n2+	rewire $ [[a1,a2] | (a1,a2) ← aux1 `zip` aux2]++annihilateDelimiters ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+annihilateDelimiters = do+	rewrite ← annihilate+	Delimiter {} ← liftReader . inspectNode =<< previous+	return rewrite++eliminateDelimiter ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+eliminateDelimiter = do+	let+		eraser = do+			e@Eraser {} ← node+			return e+		constant = do+			c@Constant {} ← node+			return c+	n ← eraser <|> constant+	Delimiter {inp = iD} ← neighbour =<< previous+	require (inp n ≢ iD)+	replace0 [Node $ n {inp = iD}]++eliminateDuplicator ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+eliminateDuplicator = do+	Eraser {inp = iE} ← node+	Duplicator {inp = iD, out1 = o1, out2 = o2} ← neighbour =<< previous+	require (iE ≡ o1 ∨ iE ≡ o2)+	if iE ≡ o1+		then rewire [[iD,o2]]+		else rewire [[iD,o1]]++eraser ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+eraser = do+	rewrite ← commute+	Eraser {} ← liftReader . inspectNode =<< previous+	return rewrite++duplicate ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+duplicate = do+	rewrite ← commute+	Duplicator {} ← liftReader . inspectNode =<< previous+	return rewrite++beta ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+beta = do+	Abstractor {body = b, var = v} :-: Applicator {inp = ai, func = f, arg = a} ← activePair+	replace0+		[Node $ Delimiter {level = 0, inp = ai, out = b},+		 Node $ Delimiter {level = 0, inp = a, out = v}]++commuteDelimiterRed ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+commuteDelimiterRed = do+	rewrite ← commuteDelimiter+	ports ← liftReader . inspectNode . (!!1) =<< history -- next to previous+	require $ length (ports ∷ [Port]) ≤ 2+	return rewrite++commuteDelimiter ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+commuteDelimiter = do+	rewrite ← commute+	Delimiter {} ← liftReader . inspectNode =<< previous+	return rewrite++applyConstant ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+applyConstant = do+	Constant {name = n} :-: Applicator {inp = i, arg = a} ← activePair+	replace0 [Node $ Function {inp = i, out = a, name = n}]++applyFunction ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+applyFunction = do+	Function {inp = i, name = fn} :-: Constant {name = cn} ← activePair+	replace0 [Node $ Constant {inp = i, name = fn ⧺ " " ⧺ cn}]++-- | Not the readback semantics as defined in the paper. Just a non semantics preserving erasure of all+-- delimiters to make the graph more readable+readback ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+readback = do+	Delimiter {inp = i, out = o} ← node+	rewire [[i,o]]

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

@@ -0,0 +1,74 @@+module Term where++import Prelude.Unicode+import Text.ParserCombinators.Parsec as Parsec+import Text.ParserCombinators.Parsec.IndentParser as Indent+import Text.ParserCombinators.Parsec.Language+import Text.ParserCombinators.Parsec.IndentParser.Token+import Control.Monad (liftM)+++data Λ = A Λ Λ            -- ^ application+       | Λ String Λ       -- ^ abstraction+       | V String         -- ^ variable+       | L [(String,Λ)] Λ -- ^ let binding+	deriving (Show,Eq,Ord)++parse ∷ String → Λ+parse str = either (error ∘ show) id (Indent.parse parser "(null)" str)++parseFile ∷ FilePath → IO Λ+parseFile = liftM (either (error ∘ show) id) ∘ Indent.parseFromFile parser++parser ∷ IndentCharParser st Λ+parser = expression where++	expression = flip label "expression" $ application <|> letBinding++	application = liftM (foldl1 A) $ many1 $ choice [parenthetic, abstraction, variable]++	parenthetic = parens haskell expression++	abstraction = flip label "abstraction" $ do+		sym "λ" <|> sym "\\"+		vars ← many1 ident+		sym "." <|> sym "→" <|> sym "->"+		body ← expression+		return $ foldr Λ body vars++	variable = liftM V $ ident <|> liftM (either show show) (naturalOrFloat haskell)++	-- Ugly, but works. Keyword "in" terminates binding blocks and bindings. Allows empty lets+	letBinding = flip label "let binding" $ do+		keyword "let"+		let parseBindings = do+			e ← optionMaybe $ keyword "in" >> expression+			case e of+				Just je → return ([], Just je)+				Nothing → do+					(b,e) ← lineFold $ do+						b ← binding+						e ← optionMaybe $ keyword "in" >> expression+						return (b,e)+					case e of+						Nothing → do+							rec ← optionMaybe parseBindings+							case rec of+								Nothing → return ([b], Nothing)+								Just (bs, me) → return (b:bs, me)+						Just je → return ([b], Just je)+		(binds, e) ← block parseBindings+		case e of+			Nothing → liftM (L binds) (keyword "in" >> expression)+			Just je → return $ L binds je++	binding ∷ IndentCharParser st (String,Λ)+	binding = flip label "binding" $ do+		funct  ← ident+		params ← many ident+		body   ← sym "=" >> expression+		return (funct, foldr Λ body params)++	keyword = reserved haskell+	ident = identifier haskell+	sym = symbol haskell

@@ -0,0 +1,35 @@+Name:           graph-rewriting-lambdascope+Version:        0.4.3+Copyright:      (c) 2010, Jan Rochel+License:        BSD3+License-File:	LICENSE+Author:         Jan Rochel+Maintainer:     jan@rochel.info+Stability:      alpha+Build-Type:     Simple+Synopsis:       Implementation of Lambdascope as an interactive graph-rewriting system+Description:+	Lambdascope is an optimal implementation of the λβ-calculus described in the paper "Lambdascope - Another optimal implementation of the lambda-calculus" by Vincent van Oostrom, Kees-Jan van de Looij, and Marijn Zwitserlood.+Category:       Graphs, Application+Extensions:     UnicodeSyntax+Cabal-Version:  >= 1.6+Build-Depends:+	base >= 4 && < 4.3,+	base-unicode-symbols >= 0.2 && < 0.3,+	graph-rewriting >= 0.4.4 && < 0.5,+	graph-rewriting-layout >= 0.4.1 && < 0.5,+	graph-rewriting-gl >= 0.5 && < 0.6,+	parsec >= 2.1 && < 2.2,+	GLUT >= 2.2 && < 2.3,+	OpenGL >= 2.4 && < 2.5,+	IndentParser >= 0.2 && < 0.3++Executable:     lambdascope+Main-Is:        Main.hs+Extensions:+	UnicodeSyntax+	FlexibleInstances+	FlexibleContexts+	MultiParamTypeClasses+GHC-Options:    -fno-warn-duplicate-exports -fwarn-unused-imports+Other-Modules:	 GL Graph Resolver Rules Term