graph-rewriting-lambdascope 0.5 → 0.5.2

raw patch · 8 files changed

+88/−98 lines, 8 filesdep ~graph-rewritingdep ~graph-rewriting-gldep ~graph-rewriting-layout

Dependency ranges changed: graph-rewriting, graph-rewriting-gl, graph-rewriting-layout

Files

• Graph.hs +1/−1
• Main.hs +31/−13
• Resolver.hs +13/−4
• Rules.hs +23/−60
• Term.hs +13/−13
• examples/sum.l +1/−1
• examples/sum1234.l +1/−1
• graph-rewriting-lambdascope.cabal +5/−5

@@ -20,7 +20,7 @@ 	| Multiplexer {out ∷ Port, ins ∷ [Port]} -- only intermediate compilation result 	| Case        {inp ∷ Port, out ∷ Port, alts ∷ [Port], names ∷ [String]} 	| Operator    {inp ∷ Port, ops ∷ [Port], arity ∷ Int, lmop ∷ Int,-	               function ∷ [String] → String, name ∷ String}+	               function ∷ [String] → Maybe String, name ∷ String}  -- | equality as defined in the paper with only the relevant cases included instance Eq NodeLS where

@@ -2,6 +2,8 @@ module Main where  import Prelude.Unicode+import Data.Foldable (toList)+import Data.Traversable (mapAccumL) import Data.List (delete) import GraphRewriting.Graph import GraphRewriting.GL.Render@@ -34,29 +36,45 @@ 	(prog,args) ← UI.initialise 	let lmo = "--lmo" ∈ args 	args ← return $ "--lmo" `delete` args+	let bench = "--bench" ∈ args+	args ← return $ "--bench" `delete` args 	file ← case args of 		[f] → return f-		___ → error "usage: lambdascope [GLUT-options] [--lmo] <file>"+		___ → error "usage: lambdascope [GLUT-options] [--lmo] [--bench] <file>" 	term ← parseFile file 	let hypergraph = execGraph (apply $ exhaustive compileShare) (resolve term)-	let layoutGraph = Layout.wrapGraph hypergraph -	if lmo-		then UI.run 50 id layoutStep (Control.wrapGraph layoutGraph) (lmoTree ruleTree)-		else UI.run 50 id layoutStep layoutGraph ruleTree+	if bench+		then do+			let tree = lmoTree ruleTree+			let indexes = evalGraph (benchmark $ toList tree) (Control.wrapGraph hypergraph)+			print indexes+			let indexTable = foldl (flip incIndex) [] indexes+			print indexTable+			let (_, numTree) = mapAccumL (\(i:is) _ → (is,i)) (indexTable ⧺ repeat 0) tree+			putStrLn $ showLabelledTree 2 0 (+) numTree+		else let layoutGraph = Layout.wrapGraph hypergraph in if lmo +			then UI.run 50 id layoutStep (Control.wrapGraph layoutGraph) (lmoTree ruleTree)+			else UI.run 50 id layoutStep layoutGraph ruleTree +incIndex ∷ Int → [Int] → [Int]+incIndex 0 (i:is) = i+1 : is+incIndex 0 [    ] = [1]+incIndex n (i:is) = i : incIndex (n-1) is+incIndex n [    ] = 0 : incIndex (n-1) []+ -- | Modifies the rules of the rule tree with a given function. -- This can be used to for example wrap a strategy rule around the existing rules.-mapRules :: (n -> m) -> LabeledTree n -> LabeledTree m+mapRules ∷ (n → m) → LabelledTree n → LabelledTree m mapRules f (Leaf n r)    = Leaf n (f r) mapRules f (Branch n rs) = Branch n (map (mapRules f) rs)  -- Appends a rule to the top branch of a rule tree-appendRule :: n -> LabeledTree n -> LabeledTree n-appendRule r l@(Leaf n rr) = Branch n [l, Leaf "moveControl" r]-appendRule r (Branch n rs) = Branch n (rs ++ [Leaf "moveControl" r])+appendRule ∷ n → LabelledTree n → LabelledTree n+appendRule r l@(Leaf n rr) = Branch n [l, Leaf "Move Control" r]+appendRule r (Branch n rs) = Branch n (rs ++ [Leaf "Move Control" r]) --- layoutStep :: (View Rotation n, View [Port] n, View Position n) => n -> IO ()+layoutStep ∷ (PortSpec n, View Position n, View Rotation n, View [Port] n) ⇒ Node → Rewrite n () layoutStep n = do 	(cgf, cf, sf, rot) ← readOnly $ do 		cgf ← centralGravitation n@@ -67,10 +85,10 @@ 	Unsafe.adjustNode n $ Position . sf (\x → min 10 (x*0.9)) . cgf (\x → min 10 (x*0.01)) . cf (\x → min 10 (100/(x^2+0.1))) . position 	Unsafe.adjustNode n $ rot (*0.9) -lmoTree ∷ (LeftmostOutermost n, View [Port] n, View Control n) ⇒ LabeledTree (Rule n) -> LabeledTree (Rule n)+lmoTree ∷ (LeftmostOutermost n, View [Port] n, View Control n) ⇒ LabelledTree (Rule n) → LabelledTree (Rule n) lmoTree = appendRule moveControl . mapRules leftmostOutermost -ruleTree :: (View NodeLS n, View [Port] n) => LabeledTree (Rule n)+ruleTree ∷ (View NodeLS n, View [Port] n) ⇒ LabelledTree (Rule n) ruleTree = Branch "All" 	[Leaf "Beta Reduction" beta, 	 Branch "All but Beta"@@ -84,4 +102,4 @@ 			[Leaf "Constant" applyConstant, 			 Leaf "Apply Operator" applyOperator, 			 Leaf "Exec Operator" execOperator,-			 Leaf "Reduce Operator Args" reduceOperatorArgs]]]+			 Leaf "Reduce Operand" reduceOperand]]]

@@ -59,11 +59,20 @@ 		compile env o exp -- compile the scrutiny  operator ∷ String → Edge → Maybe NodeLS-operator name p = case name of-	"+" → op 2 $ show . sum . map (read :: String → Int)+operator n p = case n of+	"+" → op 2 $ liftM (show . sum) . mapM read+	"-" → op 2 $ liftM (show . minus) . mapM read where minus [x,y] = x - y+	"==" → op 2 $ \[x,y] → Just $ if x ≡ y then "T" else "F" 	_ → Nothing-	where op a f = Just Operator-		{inp = p, ops = [], arity = a, lmop = 0, function = f, name = "+"}+	where++	read ∷ Read a ⇒ String → Maybe a+	read str = case [ x | (x, "") ← reads str ] of+		[] → Nothing+		x:_ → Just x++	op a f = Just Operator+		{inp = p, ops = [], arity = a, lmop = 0, function = f, name = n}  bindName ∷ Bool → String → Compiler (Edge, Name) bindName lambda sym = do

@@ -85,13 +85,13 @@ -- This rule doesn't trigger for constants with arguments eliminateDelimiterConstant ∷ (View [Port] n, View NodeLS n) ⇒ Rule n eliminateDelimiterConstant = do-	c@Constant {args = as, name = n} :-: Delimiter {inp = iD} <- activePair+	c@Constant {args = as, name = n} :-: Delimiter {inp = iD} ← activePair 	require (inp c ≢ iD && as == []) 	replace $ byNode $ Constant {inp = iD, args = [], name = n}  eliminateDelimiterEraser ∷ (View [Port] n, View NodeLS n) ⇒ Rule n eliminateDelimiterEraser = do-	c@Eraser {} :-: Delimiter {inp = iD} <- activePair+	c@Eraser {} :-: Delimiter {inp = iD} ← activePair 	require (inp c ≢ iD) 	replace $ byNode $ Eraser {inp = iD} @@ -142,39 +142,40 @@  -- TODO: Require that the lmoPort is not on one of the unreduced ports yet -- Do we only reduce operator args, if the operator has all args already?-reduceOperatorArgs ∷ (View [Port] n, View NodeLS n) ⇒ Rule n-reduceOperatorArgs = do-	o@(Operator {ops = os, lmop = lmo}) <- node-	opid <- previous-	let ports = inspect o :: [Port]+reduceOperand ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+reduceOperand = do+	o@(Operator {ops = os, lmop = lmo}) ← node+	opid ← previous+	let ports = inspect o ∷ [Port] 	let lmoport = ports !! lmo 	-- only change the lmo port if it is on top or if it is attached to a Constant-	require (lmo == 0) <|> do {Constant {} <- nodeWith lmoport; return ()}-	port <- branch os -- get a pattern that matches each port in os+	require (lmo == 0) <|> do {Constant {} ← nodeWith lmoport; return ()}+	port ← branch os -- get a pattern that matches each port in os 	-- we require that at least one node attached to the operator is not a constant 	requireFailure $ do-		Constant {} <- nodeWith port+		Constant {} ← nodeWith port 		return () 	-- we need to add one, since the input port is not part of os, but is part of the port numbering 	let unreducedport = 1 + fromJust (elemIndex port os)-	return $ do-		updateNode opid (o {lmop = unreducedport})+	return $ updateNode opid (o {lmop = unreducedport})  execOperator ∷ forall n. (View [Port] n, View NodeLS n) ⇒ Rule n execOperator = do-	Operator {inp = i, ops = os, arity = ar, function = fn, name = n} <- node-	opid <- previous+	Operator {inp = i, ops = os, arity = ar, function = fn, name = n} ← node+	opid ← previous 	require (length os == ar) 	-- check that all args are constants-	argss ← forM os $ \o -> do-			c@Constant {} <- adverse o opid+	argss ← forM os $ \o → do+			c@Constant {} ← adverse o opid 			return c-	replace $ byNode $ Constant {inp = i, args = [], name = fn (map name argss)}+	case fn (map name argss) of+		Nothing → mempty+		Just n' → replace $ byNode $ Constant {inp = i, args = [], name = n'} -caseNode :: (View [Port] n, View NodeLS n) ⇒ Rule n+caseNode ∷ (View [Port] n, View NodeLS n) ⇒ Rule n caseNode = do 	-- the order of constant and case here is important, otherwise strategies don't work-	Case {inp = i, alts = alts, names = names} :-: Constant {name = n, args = as} <- activePair+	Case {inp = i, alts = alts, names = names} :-: Constant {name = n, args = as} ← activePair 	let matchingport = alts !! (fromJust $ elemIndex n names) 	let nn = length alts 	let m = length as@@ -184,12 +185,12 @@ 			es ← replicateM (m+1) byEdge 			byWire matchingport (es !! 0) -- We merge the first new edge with the matching port from the Case node 			byWire i (es !! m) -- We merge the last new edge with the input edge of the Case node-			mconcat [byNode $ Applicator {inp = es !! (i+1), func = es !! i, arg = as !! i} | i <- [0..m-1]]-			mconcat [byNode $ Eraser {inp = alts !! i} | i <- filter (/= fromJust (elemIndex n names)) [0..nn-1]]+			mconcat [byNode $ Applicator {inp = es !! (i+1), func = es !! i, arg = as !! i} | i ← [0..m-1]]+			mconcat [byNode $ Eraser {inp = alts !! i} | i ← filter (/= fromJust (elemIndex n names)) [0..nn-1]] 			 else do 		replace $ do 			byWire i matchingport -- Attach the alternative directly to the input of the case node-			mconcat [byNode $ Eraser {inp = alts !! i} | i <- filter (/= fromJust (elemIndex n names)) [0..nn-1]]+			mconcat [byNode $ Eraser {inp = alts !! i} | i ← filter (/= fromJust (elemIndex n names)) [0..nn-1]]  -- | Not the readback semantics as defined in the paper. Just a non semantics preserving erasure of all -- delimiters to make the graph more readable@@ -197,41 +198,3 @@ readback = do 	Delimiter {inp = i, out = o} ← node 	rewire [[i,o]]---- getLmoPort ∷ (View [Port] n, LeftmostOutermost n) ⇒ Node → Pattern n Port--- getLmoPort n = do--- 	node ← liftReader $ readNode n--- 	let ports = inspect node--- 	case lmoPort node of--- 		Nothing → fail "Term is in WHNF"--- 		Just ix → return $ ports !! ix------ moveControl :: (View [Port] n, View Control n, LeftmostOutermost n, View NodeLS n) => Rule n--- moveControl = do--- 	Control {stack = s} ← node--- 	control ← previous--- 	lmo1 ← getLmoPort control--- 	n ← branchNodes =<< liftReader . adverseNodes control =<< getLmoPort control--- 	return $ do--- 		updateNode control NoControl--- 		updateNode n (Control {stack = control : s})------ leftmostOutermost :: (View [Port] n, View Control n, LeftmostOutermost n, View NodeLS n) => Rule n -> Rule n--- leftmostOutermost r = do--- 	rewrite <- r--- 	ns <- history -- we want the first node of the matching pattern--- 	let topnode = last ns--- 	Control {stack = s} ← liftReader $ inspectNode topnode--- 	return $ do--- 		updateNode topnode NoControl -- First we set the topnode to not be the control node any more--- 		oldNodes ← readNodeList--- 		rewrite -- then we perform the rewrite--- 		newNodes ← readNodeList--- 		let s' = intersect s newNodes -- only consider nodes for the control marker that exist--- 		if null s' -- even the topmost node has been replaced--- 			then do -- we assign the control marker to one of the newly created nodes--- 				let addedNodes = newNodes \\ oldNodes--- 				updateNode (head addedNodes) (Control {stack = []}) -- finally we set the previous node on the stack as the control node--- 			else do -- set the previous node on the stack as the control node--- 				updateNode (head s') (Control {stack = tail s'})---

@@ -30,13 +30,13 @@ 	deriving (Show,Eq,Ord)  -- | The LHS of a case expression. Numbers are parsed as strings.-data Pattern = Pat {constr :: String, vars :: [String]} deriving (Show, Eq, Ord)+data Pattern = Pat {constr ∷ String, vars ∷ [String]} deriving (Show, Eq, Ord) -testParser :: [tok] -> IndentParser tok () c -> c-testParser str parser = either (error ∘ show) id (Indent.parse parser "(null)" str)+testParser ∷ IndentParser tok () c → [tok] → c+testParser parser str = either (error ∘ show) id (Indent.parse parser "(null)" str) -parse :: [Char] -> Λ-parse str = testParser str expression+parse ∷ [Char] → Λ+parse = testParser expression  parseFile ∷ FilePath → IO Λ parseFile = liftM (either (error ∘ show) id) ∘ Indent.parseFromFile expression@@ -48,7 +48,7 @@ application = foldl1 A <$> many1 (parenthetic <|> abstraction <|> variable <|> numeral)  variable ∷ IndentCharParser st Λ-variable = C <$> ident <*> pure []+variable = C <$> (ident <|> operator haskell) <*> pure []  numeral ∷ IndentCharParser st Λ numeral = C <$> numeric <*> pure []@@ -59,20 +59,20 @@ parenthetic ∷ IndentCharParser st Λ parenthetic = parens haskell expression -tokP :: T.TokenParser st+tokP ∷ T.TokenParser st tokP = T.makeTokenParser haskellDef  caseExpr ∷ IndentCharParser st Λ caseExpr = flip label "case expression" $ 	Case <$> (keyword "case" *> expression <* keyword "of") <*> bracesOrBlock tokP patterns -patterns :: IndentCharParser st [(Pattern, Λ)]+patterns ∷ IndentCharParser st [(Pattern, Λ)] patterns = semiOrNewLineSep tokP pattern  arrow ∷ IndentCharParser st String-arrow = sym "->" <|> sym "→"+arrow = sym "→" <|> sym "->" -pattern :: IndentCharParser st (Pattern, Λ)+pattern ∷ IndentCharParser st (Pattern, Λ) pattern = (,) <$> lhs <*> (arrow *> expression) where 	lhs = Pat <$> (ident <|> numeric) <*> many (ident <|> numeric) @@ -110,11 +110,11 @@ 	rhs ← flip (foldr Λ) <$> many ident <*> (sym "=" *> expression) 	return (funct, rhs) -keyword :: String -> IndentCharParser st ()+keyword ∷ String → IndentCharParser st () keyword = reserved haskell -ident :: IndentCharParser st String+ident ∷ IndentCharParser st String ident = identifier haskell -sym :: String -> IndentCharParser st String+sym ∷ String → IndentCharParser st String sym = symbol haskell

@@ -2,4 +2,4 @@ 	sum list = case list of 		Nil -> 0 		Cons z zs -> (\x.λy -> + x y) z (sum zs)-in sum (Cons 1 Nil)+in sum (Cons 1 (Cons 2 Nil))

@@ -1,5 +1,5 @@ let 	Cons x xs = λcons nil. cons x xs 	Nil = λcons nil. nil-	sum list = list (λx xs . (λx y . Plus x y) x (sum xs)) 0+	sum list = list (λx xs . (λx y . + x y) x (sum xs)) 0 in sum (Cons 1 (Cons 2 (Cons 3 Nil)))

@@ -1,5 +1,5 @@ Name:           graph-rewriting-lambdascope-Version:        0.5+Version:        0.5.2 Copyright:      (c) 2010, Jan Rochel License:        BSD3 License-File:   LICENSE@@ -9,7 +9,7 @@ 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. Call "lambdascope" with one of the files from the "examples" directory as an argument. For usage of the GUI see "GraphRewriting.GL.UI". Use the "--lmo" flag for leftmost outermost evalution+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. Call "lambdascope" with one of the files from the "examples" directory as an argument. For usage of the GUI see "GraphRewriting.GL.UI". Use the "--lmo" flag for leftmost outermost evalution and "--bench" for non-graphical evaluation to weak head normal form. Category:       Graphs, Application Cabal-Version:  >= 1.6 Data-Files:     examples/*.l@@ -19,9 +19,9 @@   Build-Depends:     base >= 4 && < 4.5,     base-unicode-symbols >= 0.2 && < 0.3,-    graph-rewriting >= 0.7 && < 0.8,-    graph-rewriting-layout >= 0.5.0 && < 0.6,-    graph-rewriting-gl >= 0.6.9 && < 0.7,+    graph-rewriting >= 0.7.1 && < 0.8,+    graph-rewriting-layout >= 0.5.1 && < 0.6,+    graph-rewriting-gl >= 0.7.1 && < 0.8,     graph-rewriting-strategies >= 0.2 && < 0.3,     parsec >= 2.1 && < 2.2,     GLUT >= 2.2 && < 2.3,