graph-rewriting-lambdascope 0.5.2 → 0.5.3
raw patch · 22 files changed
+86/−101 lines, 22 filesdep ~GLUTdep ~OpenGLdep ~basenew-component:exe:bad-context-sharing
Dependency ranges changed: GLUT, OpenGL, base, parsec
Files
- GL.hs +1/−9
- Graph.hs +3/−10
- Main.hs +1/−2
- Resolver.hs +1/−6
- Rules.hs +23/−51
- examples/2times2.l +2/−0
- examples/WW-beta-saving-0.l +1/−0
- examples/WW-beta-saving-1.l +1/−0
- examples/asperti_guerrini_p14.l +1/−0
- examples/exp.l +2/−11
- examples/exp_simpl.l +5/−0
- examples/lamping_p20r_qp.l +3/−0
- examples/lamping_p20r_qp_simpl.l +4/−0
- examples/lamping_p20r_qq.l +3/−0
- examples/lamping_p20r_qq_simpl.l +4/−0
- examples/lamping_simpl.l +4/−5
- examples/levy-1988-p184bottom.l +6/−0
- examples/sum1.l +5/−0
- examples/vincent-0-ww.l +3/−0
- examples/vincent-1-ww.l +4/−0
- examples/wadsworth-thesis-p172.l +2/−0
- graph-rewriting-lambdascope.cabal +7/−7
GL.hs view
@@ -17,7 +17,6 @@ Constant {} → sd n : [sd $ rm (alpha args*x) `mmul` sws | x <- [0..la args - 1]] Eraser {} → [sd n] Duplicator {} → [(Vector2 0 0.9, n), (Vector2 (-0.6) (-0.5), s), (Vector2 0.6 (-0.5), s)]- Delimiter {} → [sd $ Vector2 0 0.7, sd $ Vector2 0 (-0.7)] Case {} → sd n : sd e : [sd $ rm (alpha alts * x) `mmul` sws | x <- [0..la alts - 1]] Operator {} → sd n : [sd $ rm (alpha ops*x) `mmul` sws | x <- [0..la ops - 1]] where@@ -54,14 +53,7 @@ vertex2 (0,0.9) vertex2 (-1,-0.5) vertex2 (1,-0.5)- renderString $ show $ level node- Delimiter {} → do- GL.preservingMatrix $ GL.renderPrimitive GL.LineStrip $ do- vertex2 (-0.8,-0.3)- vertex2 (-0.8,0)- vertex2 (0.8,0)- vertex2 (0.8,-0.3)- renderString $ show $ level node+ renderString $ label node Case {} → drawNode ("case [" ++ foldr1 (\x y → x ++ ", " ++ y) (names node) ++ "]") Operator {} → drawNode (name node)
Graph.hs view
@@ -15,18 +15,15 @@ | Abstractor {inp, body, var ∷ Port, name ∷ String} | Constant {inp ∷ Port, args ∷ [Port], name ∷ String} | Eraser {inp ∷ Port}- | Duplicator {level ∷ Int, inp, out1, out2 ∷ Port}- | Delimiter {level ∷ Int, inp, out ∷ Port}+ | Duplicator {label ∷ String, inp, out1, out2 ∷ Port} | 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] → Maybe String, name ∷ String} --- | 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+ Eraser {} == Eraser {} = True+ Duplicator {label = l1} == Duplicator {label = l2} = l1 ≡ l2 _ == _ = False instance View [Port] NodeLS where@@ -37,7 +34,6 @@ Constant {inp = i, args = as} → i:as Eraser {inp = i} → [i] Duplicator {inp = i, out1 = o1, out2 = o2} → [i,o1,o2]- Delimiter {inp = i, out = o} → [i,o] Multiplexer {out = o, ins = is} → o:is Case {inp = i, out = o, alts = as} → i:o:as Operator {inp = i, ops = os} → i:os@@ -48,7 +44,6 @@ Constant {} → node {inp = i, args = as} where i:as = 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 Multiplexer {} → node {out = o, ins = is} where o:is = ports Case {} → node {inp = i, out = o, alts = as} where i:o:as = ports Operator {} → node {inp = i, ops = os} where i:os = ports@@ -64,7 +59,6 @@ Constant {inp = i, args = as} → i Eraser {inp = i} → i Duplicator {inp = i, out1 = o1, out2 = o2} → i- Delimiter {inp = i, out = o} → i Multiplexer {out = o, ins = is} → o Case {inp = i, out = o, alts = as} → o Operator {lmop = i, ops = os} → inspect node !! i@@ -79,6 +73,5 @@ Constant {inp = i, args = as} → Nothing Eraser {inp = i} → Just i Duplicator {inp = i, out1 = o1, out2 = o2} → Just i- Delimiter {inp = i, out = o} → Just i Case {inp = i, out = o, alts = as} → Just o Operator {lmop = i, ops = os} → Just $ inspect node !! i
Main.hs view
@@ -93,9 +93,8 @@ [Leaf "Beta Reduction" beta, Branch "All but Beta" [Leaf "Duplicate" duplicate,- Leaf "Eliminate" (eliminateDelimiterEraser <|> eliminateDelimiterConstant <|> eliminateDuplicator),+ Leaf "Eliminate" eliminateDuplicator, Leaf "Annihilate" annihilate,- Leaf "Commute Delimiter" commuteDelimiter, Leaf "Erase" eraser, Leaf "Case" caseNode, Branch "Primitive"
Resolver.hs view
@@ -44,12 +44,7 @@ [ ] → void $ newNode $ fromMaybe (Constant {inp = p, name = name, args = []}) (operator name p) n:ns → if name ≡ symbol n then mergeEdges p =<< reference n- else if boundByLambda n- then do- p' ← newEdge- void $ newNode Delimiter {level = 0, inp = p', out = p}- compile ns p' term- else compile ns p term+ else compile ns p term Term.Case exp cases → do let (pats, _) = unzip cases alts ← replicateM (length cases) newEdge -- edges going from the Case node to the CaseAlts
Rules.hs view
@@ -24,7 +24,7 @@ [i] → rewire [[o,i]] ins → let (ins1, ins2) = splitAt (length ins `div` 2) ins in replace $ do (o1,o2) ← (,) <$> byEdge <*> byEdge- byNode $ Duplicator {level = 0, inp = o, out1 = o1, out2 = o2}+ byNode $ Duplicator {label = "", inp = o, out1 = o1, out2 = o2} byNode $ Multiplexer {out = o1, ins = ins1} byNode $ Multiplexer {out = o2, ins = ins2} @@ -44,7 +44,7 @@ commute ∷ (View [Port] n, View NodeLS n) ⇒ Rule n commute = do n1 :-: n2 ← activePair- require (n1 ≢ n2) -- TODO: replace by linear+ require (n1 ≢ n2) let ports1 = inspect n1 ∷ [Port] let ports2 = inspect n2 ∷ [Port] let (pp1,pp1idx) = head [(p,i) | (p,i) ← ports1 `zip` [0..], p ≡ pp n1]@@ -57,16 +57,8 @@ edges ← replicateM (es1 * es2) byEdge let edges1 = split es1 es2 edges let edges2 = transpose' es1 edges1- mconcat [byNode $ updateLevel n2 $ update (insertIdx pp1idx pp1 auxs) n1 | (pp1,auxs) ← zip aux2 edges1]- mconcat [byNode $ updateLevel n1 $ update (insertIdx pp2idx 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+ mconcat [byNode $ update (insertIdx pp1idx pp1 auxs) n1 | (pp1,auxs) ← zip aux2 edges1]+ mconcat [byNode $ update (insertIdx pp2idx pp2 auxs) n2 | (pp2,auxs) ← zip aux1 edges2] annihilate ∷ (View [Port] n, View NodeLS n) ⇒ Rule n annihilate = do@@ -76,25 +68,6 @@ let aux2 = pp n2 `delete` inspect 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---- 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- 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- require (inp c ≢ iD)- replace $ byNode $ Eraser {inp = iD}- eliminateDuplicator ∷ (View [Port] n, View NodeLS n) ⇒ Rule n eliminateDuplicator = do Eraser {inp = iE} ← node@@ -111,23 +84,29 @@ return rewrite duplicate ∷ (View [Port] n, View NodeLS n) ⇒ Rule n-duplicate = do- rewrite ← commute- Duplicator {} ← liftReader . inspectNode =<< previous- return rewrite+duplicate = duplicateAbstractor <|> duplicateSthElse where+ duplicateAbstractor = do+ Duplicator {label = l, inp = di, out1 = o1, out2 = o2}+ :-: Abstractor {name = n, inp = ai, body = b, var = v} ← activePair+ replace $ do+ (b1,v1,b2,v2) ← (,,,) <$> byEdge <*> byEdge <*> byEdge <*> byEdge+ byNode Abstractor {name = n ⧺ "1", inp = o1, body = b1, var = v1}+ byNode Abstractor {name = n ⧺ "2", inp = o2, body = b2, var = v2}+ byNode Duplicator {label = n, inp = b, out1 = b1, out2 = b2}+ byNode Duplicator {label = n, inp = v, out1 = v1, out2 = v2}+ duplicateSthElse = do+ rewrite ← commute+ Duplicator {} ← liftReader . inspectNode =<< previous+ requireFailure $ do+ h ← history+ Abstractor {} ← liftReader $ inspectNode (h !! 1)+ return ()+ return rewrite beta ∷ (View [Port] n, View NodeLS n) ⇒ Rule n beta = do Applicator {inp = ai, func = f, arg = a} :-: Abstractor {body = b, var = v} ← activePair- replace $ do- byNode $ Delimiter {level = 0, inp = ai, out = b}- byNode $ Delimiter {level = 0, inp = a, out = v}--commuteDelimiter ∷ (View [Port] n, View NodeLS n) ⇒ Rule n-commuteDelimiter = do- rewrite ← commute- Delimiter {} ← liftReader . inspectNode =<< previous- return rewrite+ rewire [[ai,b], [a,v]] applyConstant ∷ (View [Port] n, View NodeLS n) ⇒ Rule n applyConstant = do@@ -191,10 +170,3 @@ 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]]---- | 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]]
+ examples/2times2.l view
@@ -0,0 +1,2 @@+let two = λx. λy. x (x y)+in two two
+ examples/WW-beta-saving-0.l view
@@ -0,0 +1,1 @@+(\F. (\f. f (f 0)) (F 0)) (\y. \x. x)
+ examples/WW-beta-saving-1.l view
@@ -0,0 +1,1 @@+(\F. (\f. f (f 0)) (F (F 0 0))) (\y. \x. x)
+ examples/asperti_guerrini_p14.l view
@@ -0,0 +1,1 @@+(λx. x (λi. i)) λy. (λd. d d) (y z)
examples/exp.l view
@@ -1,14 +1,5 @@ let id = λx.x- zero = λf x. x- one = λf x. f x- two = λf x. f (f x)+ two = λg y. g (g y) three = λf x. f (f (f x))- four = λf x. f (f (f (f x)))- five = λf x. f (f (f (f (f x))))- six = λf x. f (f (f (f (f (f x)))))- seven = λf x. f (f (f (f (f (f (f x))))))- eight = λf x. f (f (f (f (f (f (f (f x)))))))- nine = λf x. f (f (f (f (f (f (f (f (f x))))))))- ten = λf x. f (f (f (f (f (f (f (f (f (f x)))))))))-in (λx.x two two id id) four+in three two two id id
+ examples/exp_simpl.l view
@@ -0,0 +1,5 @@+let+ f x = let g y z = let h a = y (y a)+ in h (h z)+ in g (g x)+in f (f (λx.x)) (λx.x)
+ examples/lamping_p20r_qp.l view
@@ -0,0 +1,3 @@+(λx.(λy.((λf.((λh.(h(λp.(h(λq.p)))))+ (λl.(((f(λn.(l n))) x) y))))+ (λg.(λu.(λv.((g u) (g v))))))))
+ examples/lamping_p20r_qp_simpl.l view
@@ -0,0 +1,4 @@+let+ s = λd. let t = λe. d e+ in t (λco. λnst. co) (t (λk. λl. l))+in s (λc. s (λx. c)) 2 3
+ examples/lamping_p20r_qq.l view
@@ -0,0 +1,3 @@+(λx.(λy.((λf.((λh.(h(λp.(h(λq.q)))))+ (λl.(((f(λn.(l n))) x) y))))+ (λg.(λu.(λv.((g u) (g v))))))))
+ examples/lamping_p20r_qq_simpl.l view
@@ -0,0 +1,4 @@+let+ s = λd. let t = λe. d e+ in t (λco. λnst. co) (t (λk. λl. l))+in s (λc. s (λx. x)) 2 3
examples/lamping_simpl.l view
@@ -1,6 +1,5 @@ let- id = λx.x- shared = λa. let- shared = λb. a (b id)- in shared (shared id)-in shared (shared id)+ h = λh. let+ w = λw. h (w (λy.y))+ in w (w (λz.z))+in h (h (λx.x))
+ examples/levy-1988-p184bottom.l view
@@ -0,0 +1,6 @@+let I0 = \x0.x0+ I1 = \x1.x1+ J = \z.b+ Delta = \y.I1 (y y) +in (\f.(f I0)(f J)) (\x. Delta (x a))+
+ examples/sum1.l view
@@ -0,0 +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+in sum (Cons 1 Nil)
+ examples/vincent-0-ww.l view
@@ -0,0 +1,3 @@+let delta = \x. x x+ Delta = (\y. y y) (\z. z z)+in delta Delta
+ examples/vincent-1-ww.l view
@@ -0,0 +1,4 @@+let G = \g. g (g x) + F x = F x+ I x = x +in G (F I)
+ examples/wadsworth-thesis-p172.l view
@@ -0,0 +1,2 @@+let epsilon = (\f.f(f(f a)))((\x.\y.y x)b)+in epsilon
graph-rewriting-lambdascope.cabal view
@@ -1,5 +1,5 @@ Name: graph-rewriting-lambdascope-Version: 0.5.2+Version: 0.5.3 Copyright: (c) 2010, Jan Rochel License: BSD3 License-File: LICENSE@@ -10,22 +10,22 @@ 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 and "--bench" for non-graphical evaluation to weak head normal form.-Category: Graphs, Application+Category: Compilers/Interpreters, Application Cabal-Version: >= 1.6 Data-Files: examples/*.l -Executable lambdascope+Executable bad-context-sharing Main-Is: Main.hs Build-Depends:- base >= 4 && < 4.5,+ base >= 4 && < 4.6, base-unicode-symbols >= 0.2 && < 0.3, 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,- OpenGL >= 2.4 && < 2.5,+ parsec >= 2.1 && < 3.2,+ GLUT >= 2.2 && < 2.4,+ OpenGL >= 2.4 && < 2.6, IndentParser >= 0.2 && < 0.3 Extensions: UnicodeSyntax