maxsharing 1.0.2 → 1.0.3

raw patch · 7 files changed

+25/−19 lines, 7 filesdep ~HaLeXdep ~processdep ~uuagc

Dependency ranges changed: HaLeX, process, uuagc

Files

• Lambda.ag +5/−7
• MaxSharing.hs +2/−2
• examples/not-ll-expr-1.l +1/−0
• examples/running_eff.l +1/−0
• examples/running_ineff.l +1/−0
• examples/sum.l +5/−0
• maxsharing.cabal +10/−10

@@ -4,6 +4,7 @@                  showNameless, showTR, showTRNameless, combinations, synthesise,                  scoped_Syn_R, deBruijn_Syn_R, dfa_Syn_R, readback_Syn_R, proof_Syn_R, unscoped_Syn_R} {+import Data.Maybe (mapMaybe) import Data.Set (Set) import qualified Data.Set as Set import Data.Map (Map)@@ -23,17 +24,13 @@ {type V = String} -- variables  --- <chunk: data>--- <chunk: simple-data> data Λ -- multi-purpose type for λ-terms 	| V  var ∷ V                   -- variable 	| A  fun ∷ Λ        arg   ∷ Λ  -- application 	| Λ  var ∷ V        body  ∷ Λ  -- lambda 	| L  binds ∷ Binds  body  ∷ Λ  -- let binding--- </chunk: simple-data> 	| S  var ∷ V        body  ∷ Λ  -- adbmal / scope delimiter 	| I  var ∷ V        body  ∷ Λ  -- indirection node--- </chunk: data>  type Binds = [Bind] type Bind  = (V,Λ)@@ -320,7 +317,7 @@ 	show lpl = case lpl of 		MaxPrefix → "maximal prefix lengths" 		MinPrefix → "minimal prefix lengths"-		MaxEagPre → "maximal prefix lengths while maintaining eager scope-closure"+		MaxEagPre → "maximal prefix lengths but eager scope" }  -- {type Prefix = [V]}@@ -587,8 +584,9 @@ 		else infer "S" [mkProof isLetVar name assumptions (tail prefix) term (numS - 1)] conclusion  mkPrefix ∷ Prefix → Box-mkPrefix prefix = text $ "(" ⧺ unwords (map showVar $ reverse prefix) ⧺ ")"-	where showVar (v,fs) = v ⧺ if Set.null fs then "" else "[" ⧺ unwords (Set.toList fs) ⧺ "]"+mkPrefix prefix = text $ "(" ⧺ unwords (mapMaybe showVar $ reverse prefix) ⧺ ")"+	where showVar (v,fs) = if v == "*" ∧ Set.null fs then Nothing+		else Just $ v ⧺ if Set.null fs then "" else "{" ⧺ unwords (Set.toList fs) ⧺ "}" }  attr R Λ Bind

@@ -63,8 +63,8 @@ 	let λTermSyn = syn λTerm 	putStrLn $ "translation used: " ⧺ show (letPrefixLengths params) ⧺ "\n" 	let scoped = scoped_Syn_R λTermSyn-	putStrLn ("scoped (with adbmals):") >> print scoped-	putStrLn ("scoped (with scope delimiters and nameless abstractions):") >> putStrLn (showNameless scoped)+	putStrLn ("scoped (adbmals):") >> print scoped+	putStrLn ("scoped (nameless):") >> putStrLn (showNameless scoped) 	putStrLn "derivation:" >> putStrLn (render $ proof_Syn_R λTermSyn) 	let dfa = dfa_Syn_R $ syn scoped 	putStr "DFA: " >> dot (f ⧺ ".dfa") dfa >> putStrLn ""

@@ -0,0 +1,1 @@+let f = \x.\y. f y x in f a b c d e g

@@ -0,0 +1,1 @@+\x. \f. let  r = f r x  in  r

@@ -0,0 +1,1 @@+\x. \f. let  r = f (f r x) x  in  r

@@ -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))

@@ -1,5 +1,5 @@ Name:           maxsharing-Version:        1.0.2+Version:        1.0.3 Copyright:      (c) 2013, Jan Rochel Author:         Jan Rochel Maintainer:     jan@rochel.info@@ -10,13 +10,13 @@ Build-type:     Custom Synopsis:       Maximal sharing of terms in the lambda calculus with letrec Description:    Parses a lambda-letrec term; transforms it into a first-order-                term graph representation; minimises the graph; reads back a-                lambda-letrec term which has the same unfolding as the original-                term, but exhibits maximal sharing.+                term graph representation; minimises the graph by bisimulation+                collapse; reads back a lambda-letrec term which has the same+                unfolding as the original term but is more (maximally) compact.                 If executable "dot" from graphviz is available, the graphs are-                displayed (tested for Linux).-                The approach is described in a technical report:-                http://arxiv.org/abs/1401.1460+                displayed (tested for Linux). The approach is described in an+                ICFP-paper (http://dx.doi.org/10.1145/2628136.2628148) and an+                extended version thereof (http://arxiv.org/abs/1401.1460). Category:       Graphs, Compiler Cabal-Version:  >= 1.6 Extra-Source-Files: uuagc_options@@ -32,10 +32,10 @@     containers-unicode-symbols < 0.4,     mtl < 2.3,     uuagc-cabal < 1.1,-    uuagc >= 0.9.50.2,-    HaLeX >= 1.2.1,+    uuagc >= 0.9.50.2 && < 0.10,+    HaLeX >= 1.2.1 && < 1.3,     boxes < 0.2,-    process < 1.2+    process < 1.5   Extensions: UnicodeSyntax   Other-Modules:  Lambda Parser Spanning   Main-Is: MaxSharing.hs