graph-rewriting-lambdascope 0.4.11 → 0.5
raw patch · 9 files changed
+434/−193 lines, 9 filesdep +graph-rewriting-strategiesdep ~graph-rewritingdep ~graph-rewriting-gldep ~graph-rewriting-layout
Dependencies added: graph-rewriting-strategies
Dependency ranges changed: graph-rewriting, graph-rewriting-gl, graph-rewriting-layout
Files
- GL.hs +40/−21
- Graph.hs +62/−39
- Main.hs +46/−13
- Resolver.hs +30/−15
- Rules.hs +143/−49
- Term.hs +95/−50
- examples/case.l +6/−0
- examples/sum.l +5/−0
- graph-rewriting-lambdascope.cabal +7/−6
GL.hs view
@@ -1,10 +1,12 @@-{-# LANGUAGE UnicodeSyntax #-}+{-# LANGUAGE UnicodeSyntax, FlexibleInstances #-} module GL () where +import Prelude.Unicode import Graph import GraphRewriting.Layout.PortSpec import qualified Graphics.UI.GLUT as GL import GraphRewriting.GL.Render+import GraphRewriting.Strategies.Control instance PortSpec NodeLS where@@ -12,59 +14,76 @@ 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]+ 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- n = Vector2 0 1- w = Vector2 (-1) 0- e = Vector2 1 0- s = Vector2 0 (-1)+ n = Vector2 0 1+ w = Vector2 (-1) 0+ e = Vector2 1 0+ s = Vector2 0 (-1) sw = Vector2 (-1) (-1) se = Vector2 1 (-1) + la field = toEnum $ length (field node)+ alpha f = pi/(2*la f)+ rm t = ((cos t, sin t), (-sin t, cos t))+ mmul ((x1,y1),(x2,y2)) (Vector2 x y) = Vector2 (x1*x+x2*y) (y1*x+y2*y)+ sws = Vector2 (-0.7) (-0.7)+ instance Render NodeLS where render = renderNode +instance Render n ⇒ Render (Wrapper n) where+ render c = do+ render $ wrapped c+ case control c of+ NoControl → return ()+ Control {} → GL.renderPrimitive GL.LineLoop (circle 1.2 1.2 20)+ renderNode node = drawPorts node >> case node of Initiator {} → drawNode "I" Applicator {} → drawNode "@" Abstractor {} → drawNode (name node) Constant {} → drawNode (name node)- Function {} → drawNode (name node) Eraser {} → drawNode "" Duplicator {} → do GL.preservingMatrix $ GL.renderPrimitive GL.LineLoop $ do vertex2 (0,0.9) vertex2 (-1,-0.5) vertex2 (1,-0.5)- drawString $ show $ level node+ renderString $ show $ level node Delimiter {} → do- GL.renderPrimitive GL.LineStrip $ 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)- drawString $ show $ level node+ renderString $ show $ level node+ Case {} → drawNode ("case [" ++ foldr1 (\x y → x ++ ", " ++ y) (names node) ++ "]")+ Operator {} → drawNode (name node) -drawPorts ∷ NodeLS -> IO ()-drawPorts = mapM_ drawPort . relPortPos+drawPorts ∷ NodeLS → IO ()+drawPorts n = sequence_ [drawPort (factor p) pos | (pos, p) ← positions `zip` ports] where+ positions = relPortPos n+ ports = inspect n+ isLmo p = maybe False (p ≡) (lmo n)+ factor p+ | isLmo p = 1.5+ | p ≡ pp n = 2.0+ | otherwise = 1 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+drawPort factor pos = GL.preservingMatrix $ do GL.translate $ vector pos- GL.renderPrimitive GL.Polygon (circle 0.15 0.15 10)+ GL.renderPrimitive GL.Polygon (circle (factor * 0.15) (factor * 0.15) 20) 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+ renderString label
Graph.hs view
@@ -5,18 +5,22 @@ import Data.View import GraphRewriting.Graph.Types import GraphRewriting.Pattern.InteractionNet-+-- import Control+import GraphRewriting.Strategies.LeftmostOutermost +-- | The signature of our graph data NodeLS- = Initiator {out ∷ Port}- | Applicator {inp, func, arg ∷ Port}- | Abstractor {inp, body, var ∷ Port, name ∷ String}- | 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+ = Initiator {out ∷ Port}+ | Applicator {inp, func, arg ∷ Port}+ | 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}+ | 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} -- | equality as defined in the paper with only the relevant cases included instance Eq NodeLS where@@ -27,35 +31,54 @@ 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+ 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, 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 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+ 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, 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 -instance INet NodeLS where principalPort = pp - -pp ∷ NodeLS → Int +instance INet NodeLS where principalPort = pp++-- The number is an index that specifies which port is the principal port out of the list of ports+pp ∷ NodeLS → Port pp node = case node of- Initiator {} → 0- Applicator {} → 1- Abstractor {} → 0- Delimiter {} → 0- Constant {} → 0- Function {} → 1- Duplicator {} → 0- Eraser {} → 0+ Initiator {out = o} → o+ Applicator {inp = i, func = f, arg = a} → f+ Abstractor {inp = i, body = b, var = v} → i+ 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++instance LeftmostOutermost NodeLS where lmoPort = lmo++lmo ∷ NodeLS → Maybe Port+lmo node = case node of+ Initiator {out = o} → Just o+ Applicator {inp = i, func = f, arg = a} → Just f+ Abstractor {inp = i, body = b, var = v} → Nothing+ 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
@@ -1,6 +1,8 @@-{-# LANGUAGE UnicodeSyntax, FlexibleInstances #-}+{-# LANGUAGE UnicodeSyntax, MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-} module Main where +import Prelude.Unicode+import Data.List (delete) import GraphRewriting.Graph import GraphRewriting.GL.Render import GraphRewriting.GL.UI as UI@@ -16,22 +18,45 @@ import GraphRewriting.Layout.Coulomb import GraphRewriting.Layout.SpringEmbedder import GraphRewriting.Layout.Gravitation-import GraphRewriting.Layout.Wrapper+import GraphRewriting.Layout.Wrapper as Layout +import GraphRewriting.Strategies.Control as Control+import GraphRewriting.Strategies.LeftmostOutermost -instance Render (Wrapper NodeLS) where render = render . wrappee +instance Render n ⇒ Render (Layout.Wrapper n) where render = render . wrappee+instance PortSpec n ⇒ PortSpec (Control.Wrapper n) where portSpec = portSpec . wrapped+instance LeftmostOutermost n ⇒ LeftmostOutermost (Layout.Wrapper n) where lmoPort = lmoPort . wrappee++ main ∷ IO () main = do (prog,args) ← UI.initialise+ let lmo = "--lmo" ∈ args+ args ← return $ "--lmo" `delete` args file ← case args of [f] → return f- ___ → error "usage: lambdascope [GLUT-options] <file>"+ ___ → error "usage: lambdascope [GLUT-options] [--lmo] <file>" term ← parseFile file- let hypergraph = resolve term- let graph = execGraph (apply $ exhaustive compileShare) (wrapGraph hypergraph)- UI.run 50 id layoutStep graph ruleTree+ 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++-- | 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 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])++-- layoutStep :: (View Rotation n, View [Port] n, View Position n) => n -> IO () layoutStep n = do (cgf, cf, sf, rot) ← readOnly $ do cgf ← centralGravitation n@@ -39,16 +64,24 @@ sf ← springForce 1.5 n rot ← angularMomentum n return (cgf, cf, sf, rot)- Unsafe.adjustNode (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) n- Unsafe.adjustNode (rot (*0.9)) n+ 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 = appendRule moveControl . mapRules leftmostOutermost++ruleTree :: (View NodeLS n, View [Port] n) => LabeledTree (Rule n) ruleTree = Branch "All" [Leaf "Beta Reduction" beta, Branch "All but Beta" [Leaf "Duplicate" duplicate,- Leaf "Eliminate" (eliminateDelimiter <|> eliminateDuplicator),+ Leaf "Eliminate" (eliminateDelimiterEraser <|> eliminateDelimiterConstant <|> 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 "Erase" eraser,+ Leaf "Case" caseNode,+ Branch "Primitive"+ [Leaf "Constant" applyConstant,+ Leaf "Apply Operator" applyOperator,+ Leaf "Exec Operator" execOperator,+ Leaf "Reduce Operator Args" reduceOperatorArgs]]]
Resolver.hs view
@@ -7,7 +7,8 @@ import Graph import GraphRewriting.Graph import GraphRewriting.Graph.Write-import Control.Monad (liftM, zipWithM)+import Control.Monad+import Data.Maybe (fromMaybe) type Compiler = Rewrite NodeLS@@ -26,34 +27,48 @@ A func arg → do f ← newEdge x ← newEdge- newNode Applicator {inp = p, func = f, arg = x}+ void $ 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, name = x}+ void $ newNode Abstractor {inp = p, body = b, var = v, name = x} 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)+ void $ zipWithM (compile env') es (Prelude.map snd binds) compile env' p e+ C name [] → case env of+ [ ] → 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+ Term.Case exp cases → do+ let (pats, _) = unzip cases+ alts ← replicateM (length cases) newEdge -- edges going from the Case node to the CaseAlts+ o ← newEdge+ void $ newNode Graph.Case {inp = p, out = o, alts = alts, names = map constr pats}+ mapM_ (\(alt, (pat,exp)) → compile env alt (foldr Λ exp (vars pat))) (zip alts cases) -- compile the different cases+ 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)+ _ → Nothing+ where op a f = Just Operator+ {inp = p, ops = [], arity = a, lmop = 0, function = f, name = "+"}+ bindName ∷ Bool → String → Compiler (Edge, Name) bindName lambda sym = do v ← newEdge- s ← newNode Multiplier {out = v, ins = []}+ s ← newNode Multiplexer {out = v, ins = []} let ref = do e ← newEdge modifyNode s $ \s → s {ins = e : ins s}
Rules.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE UnicodeSyntax, FlexibleContexts #-}+{-# LANGUAGE UnicodeSyntax, FlexibleContexts, ScopedTypeVariables #-} module Rules where import Prelude.Unicode@@ -7,19 +7,26 @@ import GraphRewriting.Pattern import GraphRewriting.Pattern.InteractionNet import GraphRewriting.Graph.Read-import Data.List (transpose)+import GraphRewriting.Graph.Write+import Data.List (transpose, elemIndex, delete)+import Control.Applicative+import Data.Monoid+import Control.Monad +import Data.Maybe (fromJust) + compileShare ∷ (View [Port] n, View NodeLS n) ⇒ Rule n compileShare = do- Multiplier {out = o, ins = is} ← node+ Multiplexer {out = o, ins = is} ← node case is of- [ ] → replace0 [Node $ Eraser {inp = o}]+ [ ] → replace $ byNode 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}]+ 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 $ Multiplexer {out = o1, ins = ins1}+ byNode $ Multiplexer {out = o2, ins = ins2} withoutIdx ∷ [a] → Int → [a] withoutIdx xs i = let (ys,zs) = splitAt i xs in ys ⧺ tail zs@@ -37,16 +44,21 @@ 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+ require (n1 ≢ n2) -- TODO: replace by linear+ let ports1 = inspect n1 ∷ [Port]+ let ports2 = inspect n2 ∷ [Port]+ let (pp1,pp1idx) = head [(p,i) | (p,i) ← ports1 `zip` [0..], p ≡ pp n1]+ let (pp2,pp2idx) = head [(p,i) | (p,i) ← ports2 `zip` [0..], p ≡ pp n2]+ let aux1 = pp1 `delete` inspect n1+ let aux2 = pp2 `delete` inspect 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]+ replace $ do+ 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@@ -59,9 +71,9 @@ 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+ require (n1 ≡ n2) -- TODO: ???+ let aux1 = pp n1 `delete` inspect n1+ let aux2 = pp n2 `delete` inspect n2 rewire $ [[a1,a2] | (a1,a2) ← aux1 `zip` aux2] annihilateDelimiters ∷ (View [Port] n, View NodeLS n) ⇒ Rule n@@ -70,20 +82,19 @@ 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}]+-- 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@@ -107,17 +118,10 @@ 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+ 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@@ -127,17 +131,107 @@ 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}]+ Applicator {inp = i, arg = a} :-: Constant {name = n, args = as} ← activePair+ replace $ byNode $ Constant {inp = i, name = n, args = as ++ [a]} -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}]+applyOperator ∷ (View [Port] n, View NodeLS n) ⇒ Rule n+applyOperator = do+ Applicator {inp = i, arg = a} :-: Operator {ops = os, arity = ar, lmop = l, function = fn, name = n} ← activePair+ require (ar > length os)+ replace $ byNode $ Operator {inp = i, ops = os ++ [a], arity = ar, lmop = l, function = fn, name = n} +-- 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]+ 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+ -- we require that at least one node attached to the operator is not a constant+ requireFailure $ do+ 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})++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+ require (length os == ar)+ -- check that all args are constants+ argss ← forM os $ \o -> do+ c@Constant {} <- adverse o opid+ return c+ replace $ byNode $ Constant {inp = i, args = [], name = fn (map name argss)}++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+ let matchingport = alts !! (fromJust $ elemIndex n names)+ let nn = length alts+ let m = length as+ -- We generate m new applicator nodes with m+1 new edges connecting them+ if m > 0 then+ replace $ do+ 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]]+ 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]]+ -- | 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]]++-- 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'})+--
Term.hs view
@@ -3,73 +3,118 @@ import Prelude.Unicode import Text.ParserCombinators.Parsec as Parsec+ hiding (space, eof, notFollowedBy, anyChar, many, optional, (<|>)) import Text.ParserCombinators.Parsec.IndentParser as Indent import Text.ParserCombinators.Parsec.Language import Text.ParserCombinators.Parsec.IndentParser.Token-import Control.Monad (liftM)+import qualified Text.ParserCombinators.Parsec.Token as T+import Control.Monad+import Data.Functor+import Control.Applicative +instance Applicative (GenParser s a) where+ pure = return+ (<*>) = ap++instance Alternative (GenParser s a) where+ empty = mzero+ (<|>) = mplus++-- | The AST of a lambda expression data Λ = A Λ Λ -- ^ application- | Λ String Λ -- ^ abstraction- | V String -- ^ variable- | L [(String,Λ)] Λ -- ^ let binding+ | Λ String Λ -- ^ abstraction+ | L [(String,Λ)] Λ -- ^ let binding+ | Case Λ [(Pattern,Λ)] -- ^ case expression+ | C String [Λ] -- ^ constructor deriving (Show,Eq,Ord) -parse ∷ String → Λ-parse str = either (error ∘ show) id (Indent.parse parser "(null)" str)+-- | The LHS of a case expression. Numbers are parsed as strings.+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)++parse :: [Char] -> Λ+parse str = testParser str expression+ parseFile ∷ FilePath → IO Λ-parseFile = liftM (either (error ∘ show) id) ∘ Indent.parseFromFile parser+parseFile = liftM (either (error ∘ show) id) ∘ Indent.parseFromFile expression -parser ∷ IndentCharParser st Λ-parser = expression where+expression ∷ IndentCharParser st Λ+expression = flip label "expression" $ letBinding <|> caseExpr <|> application - expression = flip label "expression" $ application <|> letBinding+application ∷ IndentCharParser st Λ+application = foldl1 A <$> many1 (parenthetic <|> abstraction <|> variable <|> numeral) - application = liftM (foldl1 A) $ many1 $ choice [parenthetic, abstraction, variable]+variable ∷ IndentCharParser st Λ+variable = C <$> ident <*> pure [] - parenthetic = parens haskell expression+numeral ∷ IndentCharParser st Λ+numeral = C <$> numeric <*> pure [] - abstraction = flip label "abstraction" $ do- sym "λ" <|> sym "\\"- vars ← many1 ident- sym "." <|> sym "→" <|> sym "->"- body ← expression- return $ foldr Λ body vars+numeric ∷ IndentCharParser st String+numeric = either show show <$> naturalOrFloat haskell - variable = liftM V $ ident <|> liftM (either show show) (naturalOrFloat haskell)+parenthetic ∷ IndentCharParser st Λ+parenthetic = parens haskell expression - -- 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+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 = semiOrNewLineSep tokP pattern++arrow ∷ IndentCharParser st String+arrow = sym "->" <|> sym "→"++pattern :: IndentCharParser st (Pattern, Λ)+pattern = (,) <$> lhs <*> (arrow *> expression) where+ lhs = Pat <$> (ident <|> numeric) <*> many (ident <|> numeric)++lambda ∷ IndentCharParser st String+lambda = sym "λ" <|> sym "\\"++abstraction ∷ IndentCharParser st Λ+abstraction = flip label "abstraction" $+ flip (foldr Λ) <$> (lambda *> many1 ident) <*> ((sym "." <|> arrow) *> expression)++-- Ugly, but works. Keyword "in" terminates binding blocks and bindings. Allows empty lets+letBinding ∷ IndentCharParser st Λ+letBinding = flip label "let binding" $ do+ let parseBindings = do+ e ← optionMaybe $ keyword "in" *> expression case e of- Nothing → liftM (L binds) (keyword "in" >> expression)- Just je → return $ L binds je+ Just je → return ([], Just je)+ Nothing → do+ (b,e) ← lineFold $ (,) <$> binding <*> (optionMaybe $ keyword "in" *> expression)+ 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) ← keyword "let" *> block parseBindings+ case e of+ Nothing → 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)+binding ∷ IndentCharParser st (String,Λ)+binding = flip label "binding" $ do+ funct ← ident+ rhs ← flip (foldr Λ) <$> many ident <*> (sym "=" *> expression)+ return (funct, rhs) - keyword = reserved haskell- ident = identifier haskell- sym = symbol haskell+keyword :: String -> IndentCharParser st ()+keyword = reserved haskell++ident :: IndentCharParser st String+ident = identifier haskell++sym :: String -> IndentCharParser st String+sym = symbol haskell
+ 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/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 Nil)
graph-rewriting-lambdascope.cabal view
@@ -1,5 +1,5 @@ Name: graph-rewriting-lambdascope-Version: 0.4.11+Version: 0.5 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".+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 Category: Graphs, Application Cabal-Version: >= 1.6 Data-Files: examples/*.l@@ -19,9 +19,10 @@ Build-Depends: base >= 4 && < 4.5, base-unicode-symbols >= 0.2 && < 0.3,- graph-rewriting >= 0.4.4 && < 0.6,- graph-rewriting-layout >= 0.4.1 && < 0.5,- graph-rewriting-gl >= 0.6.7 && < 0.7,+ graph-rewriting >= 0.7 && < 0.8,+ graph-rewriting-layout >= 0.5.0 && < 0.6,+ graph-rewriting-gl >= 0.6.9 && < 0.7,+ graph-rewriting-strategies >= 0.2 && < 0.3, parsec >= 2.1 && < 2.2, GLUT >= 2.2 && < 2.3, OpenGL >= 2.4 && < 2.5,@@ -31,5 +32,5 @@ FlexibleInstances FlexibleContexts MultiParamTypeClasses- GHC-Options: -fno-warn-duplicate-exports+ 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