graph-rewriting-ww (empty) → 0.1
raw patch · 38 files changed
+573/−0 lines, 38 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 +55/−0
- Graph.hs +34/−0
- LICENSE +10/−0
- Main.hs +65/−0
- Resolver.hs +56/−0
- Rules.hs +146/−0
- Setup.hs +2/−0
- Term.hs +75/−0
- examples/2times2.l +1/−0
- examples/Omega.l +1/−0
- examples/WW-beta-saving-0.l +1/−0
- examples/WW-beta-saving-1.l +1/−0
- examples/asperti_guerrini_3011.l +3/−0
- examples/asperti_guerrini_3011_simpl.l +2/−0
- examples/asperti_guerrini_3012.l +3/−0
- examples/case.l +6/−0
- examples/exp.l +5/−0
- examples/exp_simpl.l +5/−0
- examples/fix.l +1/−0
- examples/flip_const_id.l +5/−0
- examples/head123.l +4/−0
- examples/lamping.l +3/−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 +5/−0
- examples/levy-1988-p184bottom.l +6/−0
- examples/repeat_naive.l +2/−0
- examples/repeat_optim.l +2/−0
- examples/sum.l +5/−0
- examples/sum1.l +5/−0
- examples/sum1234.l +5/−0
- examples/twice.l +1/−0
- examples/vincent-0-ww.l +3/−0
- examples/vincent-1-ww.l +4/−0
- examples/wadsworth-thesis-p172.l +2/−0
- graph-rewriting-ww.cabal +35/−0
+ GL.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE UnicodeSyntax #-}+module GL () where++import Graph+import GraphRewriting.Layout.PortSpec+import qualified Graphics.UI.GLUT as GL+import GraphRewriting.GL.Render+++instance PortSpec NodeWW 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]+ Primitive {} → [sd n]+ Eraser {} → [sd n]+ Duplicator {} → [sd n, (sw, s), (se, 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)++instance Render NodeWW where render = renderNode++renderNode node = drawPorts node >> case node of+ Initiator {} → drawNode "I"+ Applicator {} → drawNode "@"+ Abstractor {} → drawNode (name node)+ Primitive {} → drawNode (name node)+ Eraser {} → drawNode ""+ Duplicator {} → do+ GL.preservingMatrix $ GL.renderPrimitive GL.LineLoop $ do+ vertex2 (0,1)+ vertex2 (-1,-1)+ vertex2 (1,-1)+ renderString $ if active node then "*" else ""++drawPorts ∷ NodeWW -> 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)+ renderString label
+ Graph.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE UnicodeSyntax, FlexibleInstances, MultiParamTypeClasses #-}+module Graph where++import Prelude.Unicode+import Data.View+import GraphRewriting.Graph.Types+++data NodeWW+ = Initiator {out ∷ Port}+ | Applicator {inp, func, arg ∷ Port}+ | Abstractor {name ∷ String, inp, body, var ∷ Port}+ | Primitive {inp ∷ Port, name ∷ String}+ | Eraser {inp ∷ Port}+ | Duplicator {active ∷ Bool, inp, out1, out2 ∷ Port}+ | Multiplexer {out ∷ Port, ins ∷ [Port]} -- only intermediate compilation result++instance View [Port] NodeWW 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]+ Primitive {inp = i} → [i]+ Eraser {inp = i} → [i]+ Duplicator {inp = i, out1 = o1, out2 = o2} → [i,o1,o2]+ Multiplexer {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+ Primitive {} → node {inp = i} where [i] = ports+ Eraser {} → node {inp = i} where [i] = ports+ Duplicator {} → node {inp = i, out1 = o1, out2 = o2} where [i,o1,o2] = ports+ Multiplexer {} → node {out = o, ins = is} where o:is = ports
+ LICENSE view
@@ -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.
+ Main.hs view
@@ -0,0 +1,65 @@+{-# LANGUAGE UnicodeSyntax, FlexibleInstances, FlexibleContexts #-}+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 hiding (erase)+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 NodeWW) 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 50 id layoutStep graph ruleTree++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 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)++unshare ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+unshare = duplicatePrimitive <|> duplicateFunction where+ duplicateFunction = initDuplication >>> exhaustive (everywhere duplicate) >>> exhaustive (everywhere deactivate)+ duplicate = anyOf [duplicateAbstractor, duplicateApplicator, duplicateDuplicator, duplicateEraser, annihilate]++ruleTree = Branch "All"+ [Branch "Safe"+ [Leaf "Beta Reduction" beta,+ Leaf "Apply Primitive" applyPrimitive,+ Leaf "Unshare MFE" unshare,+ Leaf "Eliminate" eliminate,+ Leaf "Erase" erase],+ Branch "Unsafe Unsharing"+ [Leaf "Initiate" initDuplication,+ Branch "Intermediate"+ [Leaf "DuplicateAbstractor" duplicateAbstractor,+ Leaf "DuplicateApplicator" duplicateApplicator,+ Leaf "DuplicateDuplicator" duplicateDuplicator,+ Leaf "DuplicateEraser" duplicateEraser,+ Leaf "Annihilate" annihilate],+ Leaf "Finalise" deactivate]]
+ Resolver.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE UnicodeSyntax #-}+-- | 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 NodeWW++type Environment = [Name]+data Name = Name {symbol ∷ String, reference ∷ Compiler Edge}++resolve ∷ Λ → Graph NodeWW+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, n) ← bindName x+ newNode Abstractor {name = x, inp = p, body = b, var = v}+ compile (n : env) b e+ V var → case env of+ [ ] → newNode Primitive {inp = p, name = var} >> return ()+ n:ns → if var ≡ symbol n+ then mergeEdges p =<< reference n+ else compile ns p term+ L binds e → do+ (es, names) ← liftM unzip $ mapM bindName (map fst binds)+ let env' = names ⧺ env+ zipWithM (compile env') es (Prelude.map snd binds)+ compile env' p e++bindName ∷ String → Compiler (Edge, Name)+bindName sym = do+ v ← newEdge+ s ← newNode Multiplexer {out = v, ins = []}+ let ref = do+ e ← newEdge+ modifyNode s $ \s → s {ins = e : ins s}+ return e+ return (v, Name {symbol = sym, reference = ref})
+ Rules.hs view
@@ -0,0 +1,146 @@+{-# LANGUAGE UnicodeSyntax, FlexibleContexts #-}+module Rules where++import Prelude.Unicode+import Graph+import GraphRewriting.Rule as Rule+import GraphRewriting.Pattern+import GraphRewriting.Graph.Read+import Control.Applicative+import Data.Monoid.Unicode+++compileShare ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+compileShare = do+ Multiplexer {out = o, ins = is} ← node+ case is of+ [ ] → replace $ byNode Eraser {inp = o}+ [i] → rewire [[o,i]]+ ins → let (ins1, ins2) = splitAt (length ins `div` 2) ins in replace $ do+ (o1,o2) ← (,) <$> byEdge <*> byEdge+ byNode Duplicator {active = False, inp = o, out1 = o1, out2 = o2}+ byNode Multiplexer {out = o1, ins = ins1}+ byNode Multiplexer {out = o2, ins = ins2}++beta ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+beta = do+ abs@Abstractor {} ← node+ app@Applicator {} ← nodeWith $ inp abs+ require (inp abs ≡ func app)+ rewire [[inp app, body abs], [arg app, var abs]]++initDuplication ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+initDuplication = do+ dup@Duplicator {active = False} ← node+ abs@Abstractor {} ← nodeWith $ inp dup+ require $ inp abs ≡ inp dup+ replace $ do+ (b1,b2,v1,v2) ← (,,,) <$> byEdge <*> byEdge <*> byEdge <*> byEdge+ byNode abs {inp = out1 dup, body = b1, var = v1}+ byNode abs {inp = out2 dup, body = b2, var = v2}+ byNode Duplicator {out1 = b1, out2 = b2, inp = body abs, active = True}+ byNode Duplicator {out1 = v1, out2 = v2, inp = var abs, active = True}++duplicateAbstractor ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+duplicateAbstractor = do+ dup@Duplicator {active = True} ← node+ abs@Abstractor {} ← nodeWith $ inp dup+ require $ body abs ≡ inp dup+ replace $ do+ (i1,i2,v1,v2) ← (,,,) <$> byEdge <*> byEdge <*> byEdge <*> byEdge+ byNode dup {inp = inp abs, out1 = i1, out2 = i2}+ byNode abs {inp = i1, body = out1 dup, var = v1}+ byNode abs {inp = i2, body = out2 dup, var = v2}+ byNode dup {out1 = v1, out2 = v2, inp = var abs}++duplicateApplicator ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+duplicateApplicator = do+ dup@Duplicator {active = True} ← node+ app@Applicator {} ← nodeWith $ inp dup+ require $ inp dup ∈ [func app, arg app]+ if inp dup ≡ func app+ then do+ require $ func app ≡ inp dup+ replace $ do+ (i1,i2,a1,a2) ← (,,,) <$> byEdge <*> byEdge <*> byEdge <*> byEdge + byNode dup {inp = inp app, out1 = i1, out2 = i2}+ byNode Applicator {inp = i1, func = out1 dup, arg = a1}+ byNode Applicator {inp = i2, func = out2 dup, arg = a2}+ byNode dup {out1 = a1, out2 = a2, inp = arg app}+ else do+ require $ arg app ≡ inp dup+ replace $ do+ (i1,i2,a1,a2) ← (,,,) <$> byEdge <*> byEdge <*> byEdge <*> byEdge+ byNode dup {inp = inp app, out1 = i1, out2 = i2}+ byNode Applicator {inp = i1, func = a1, arg = out1 dup}+ byNode Applicator {inp = i2, func = a2, arg = out2 dup}+ byNode dup {out1 = a1, out2 = a2, inp = func app}++duplicateDuplicator ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+duplicateDuplicator = linear $ do+ dup1@Duplicator {active = True} ← node+ dup2@Duplicator {active = False} ← nodeWith $ inp dup1+ require $ inp dup1 ≡ inp dup2+ replace $ do+ (ll,lr,rl,rr) ← (,,,) <$> byEdge <*> byEdge <*> byEdge <*> byEdge+ byNode dup1 {inp = out1 dup2, out1 = ll, out2 = lr}+ byNode dup1 {inp = out2 dup2, out1 = rl, out2 = rr}+ byNode dup2 {inp = out1 dup1, out1 = ll, out2 = rl}+ byNode dup2 {inp = out2 dup1, out1 = lr, out2 = rr}++duplicatePrimitive ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+duplicatePrimitive = do+ d@Duplicator {} ← node+ p@Primitive {} ← nodeWith $ inp d+ replace $ byNode p {inp = out1 d} ⊕ byNode p {inp = out2 d}++duplicateEraser ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+duplicateEraser = do+ d@Duplicator {} ← node+ e@Eraser {} ← nodeWith $ inp d+ replace $ byNode Eraser {inp = out1 d} ⊕ byNode Eraser {inp = out2 d}++annihilate ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+annihilate = linear $ do+ dup1@Duplicator {active = True} ← node+ dup2@Duplicator {active = True} ← nodeWith $ inp dup1+ require $ inp dup1 ≡ inp dup2+ rewire [[out1 dup1, out1 dup2], [out2 dup1, out2 dup2]]++deactivate ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+deactivate = do+ dup@Duplicator {active = True} ← node+ replace $ byNode dup {active = False}++eliminate ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+eliminate = do+ e@Eraser {} ← node+ d@Duplicator {out1 = o1, out2 = o2} ← neighbour =<< previous+ require $ inp e ∈ [o1, o2]+ if inp e ≡ o1+ then rewire [[inp d, o2]]+ else rewire [[inp d, o1]]++erase ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+erase = linear $ do+ e@Eraser {} ← node+ let+ abstractor = do+ a@Abstractor {} ← nodeWith $ inp e+ require $ inp a ≡ inp e+ replace $ byNode Eraser {inp = body a} ⊕ byNode Eraser {inp = var a}+ applicator = do+ a@Applicator {} ← nodeWith $ inp e+ require $ inp a ≡ inp e+ replace $ byNode Eraser {inp = func a} ⊕ byNode Eraser {inp = arg a}+ eraser = do+ Eraser {} ← nodeWith $ inp e+ Rule.erase+ abstractor <|> applicator <|> eraser++applyPrimitive ∷ (View [Port] n, View NodeWW n) ⇒ Rule n+applyPrimitive = linear $ do+ a@Applicator {} ← node+ f@Primitive {} ← nodeWith $ func a+ x@Primitive {} ← nodeWith $ arg a+ replace $ byNode Primitive {name = "(" ⧺ name f ⧺ " " ⧺ name x ⧺ ")", inp = inp a}
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Term.hs view
@@ -0,0 +1,75 @@+{-# LANGUAGE UnicodeSyntax #-}+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, void)+++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+ void $ sym "λ" <|> sym "\\"+ vars ← many1 ident+ void $ sym "." <|> sym "→" <|> sym "->"+ body ← expression+ return $ foldr Λ body vars++ variable = liftM V $ ident <|> operator haskell <|> 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
+ examples/2times2.l view
@@ -0,0 +1,1 @@+(\x. \y. x(x y)) (\x. \y. x(x y))
+ examples/Omega.l view
@@ -0,0 +1,1 @@+let omega = λx.x x in omega omega
+ 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_3011.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/asperti_guerrini_3011_simpl.l view
@@ -0,0 +1,2 @@+λa b c d. let s = λa b c. let t = λx. a in (t c) (t b)+in s (λe. c (λf.e f) a b) (s d)
+ examples/asperti_guerrini_3012.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/case.l view
@@ -0,0 +1,6 @@+λx.case x of+ Test -> 1+ B y -> y y+ Cons x xs -> x xs+ Bla -> λy.y y+(Cons 5 Nil)
+ examples/exp.l view
@@ -0,0 +1,5 @@+let+ id = λx.x+ two = λg y. g (g y)+ three = λf x. f (f (f x))+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/fix.l view
@@ -0,0 +1,1 @@+let fix f = f (fix f) in fix
+ examples/flip_const_id.l view
@@ -0,0 +1,5 @@+let+ flip f x y = f y x+ const x y = x+ id x = x+in flip const a id b
+ examples/head123.l view
@@ -0,0 +1,4 @@+let+ Cons x xs = λcons nil. cons x xs+ Nil = λcons nil. nil+in (Cons 1 (Cons 2 (Cons 3 Nil))) (λx xs. x) 0
+ examples/lamping.l view
@@ -0,0 +1,3 @@+((λg.(g(g(λx.x))))+ (λh.((λf.(f(f(λz.z))))+ (λw.(h(w(λy.y)))))))
+ 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
@@ -0,0 +1,5 @@+let+ 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/repeat_naive.l view
@@ -0,0 +1,2 @@+let repeat x = Cons x (repeat x)+in repeat 7
+ examples/repeat_optim.l view
@@ -0,0 +1,2 @@+let repeat x = let loop = Cons x loop in loop+in repeat 7
+ examples/sum.l view
@@ -0,0 +1,5 @@+let+ sum list = case list of+ Nil -> 0+ Cons z zs -> (\x.λy -> + x y) z (sum zs)+in sum (Cons 1 (Cons 2 Nil))
+ 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/sum1234.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 . + x y) x (sum xs)) 0+in sum (Cons 1 (Cons 2 (Cons 3 Nil)))
+ examples/twice.l view
@@ -0,0 +1,1 @@+let twice f x = f (f x) in twice twice inc
+ 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-ww.cabal view
@@ -0,0 +1,35 @@+Name: graph-rewriting-ww+Version: 0.1+Copyright: (c) 2010, 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: Interactive reduction of lambda-calculus with explicit sharing+Description: Evaluate a λ-letrec term in an interactive graph reduction system. It uses duplicators to explicitely render sharing (and unsharing) according to Wadsworth's approach.+Category: Application, Compilers/Interpreters+Cabal-Version: >= 1.6+Data-Files: examples/*.l++Executable ww+ Main-Is: Main.hs+ Build-Depends:+ base >= 4 && < 4.5,+ base-unicode-symbols >= 0.2 && < 0.3,+ graph-rewriting >= 0.7 && < 0.8,+ graph-rewriting-layout >= 0.5.1 && < 0.6,+ graph-rewriting-gl >= 0.6.9 && < 0.8,+ parsec >= 2.1 && < 2.2,+ GLUT >= 2.2 && < 2.3,+ OpenGL >= 2.4 && < 2.5,+ IndentParser >= 0.2 && < 0.3+ Extensions:+ UnicodeSyntax+ FlexibleInstances+ FlexibleContexts+ MultiParamTypeClasses+ GHC-Options: -fno-warn-duplicate-exports -fwarn-unused-binds -fwarn-unused-imports -fwarn-unused-do-bind -fwarn-wrong-do-bind -fwarn-unrecognised-pragmas+ Other-Modules: GL Graph Resolver Rules Term