maxsharing 1.0 → 1.0.2

raw patch · 35 files changed

+157/−33 lines, 35 filesdep ~basedep ~mtldep ~parsec

Dependency ranges changed: base, mtl, parsec

Files

• Lambda.ag +29/−24
• MaxSharing.hs +10/−5
• examples/2times2.l +2/−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/asperti_guerrini_p14.l +1/−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/morazan-fig1.l +6/−0
• examples/morazan-fig4.l +7/−0
• examples/morazan-fig6.l +7/−0
• examples/morazan-fig8.l +7/−0
• examples/repeat_naive.l +2/−0
• examples/repeat_optim.l +2/−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
• maxsharing.cabal +5/−4

@@ -22,13 +22,18 @@  {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-	| S  var ∷ V  body ∷ Λ       -- abdmal / scope delimiter-	| I  var ∷ V  body ∷ Λ       -- indirection node-	| L  binds ∷ Binds  body ∷ Λ -- let binding+	| 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,Λ)@@ -388,10 +393,10 @@ sem Λ 	| Λ A V L loc.scoped = churnr [S x | x <- @loc.killVars] @loc.scoped' 	| * loc.killVars = take (length @loc.parentPrefix - length @loc.prefix) (map fst @loc.parentPrefix)-  | Λ loc.scoped' = Λ @var @body.scoped-  | A loc.scoped' = A @fun.scoped @arg.scoped+	| Λ loc.scoped' = Λ @var @body.scoped+	| A loc.scoped' = A @fun.scoped @arg.scoped 	| V loc.scoped' = V @var-  | L loc.scoped' = L @binds.scoped @body.scoped+	| L loc.scoped' = L @binds.scoped @body.scoped 	| S I loc.scoped' = undefined  sem Bind | Tuple lhs.scoped = (@loc.binder, @x2.scoped)@@ -551,21 +556,21 @@  sem Λ 	| Λ lhs.bindings = tail @body.bindings-      lhs.readback = Λ @var $ @loc.addL @body.readback-      loc.addL = case head @body.bindings of-      				[] -> id-      				bs -> L bs-  | S lhs.bindings = [] : @body.bindings-      lhs.readback = S @var @body.readback-  | A lhs.bindings = zipWith (⧺) @fun.bindings @arg.bindings-      lhs.readback = A @fun.readback @arg.readback-  | I lhs.bindings = let (bs:bss) = @body.bindings in ((@var,@body.readback) : bs) : bss-      lhs.readback = V @var-  | V lhs.bindings = repeat []-      lhs.readback = V @var-  | L lhs.bindings = @loc.readbackError-      lhs.readback = @loc.readbackError-      loc.readbackError = error "readback is only defined for λ-spanning-trees"+	    lhs.readback = Λ @var $ @loc.addL @body.readback+	    loc.addL = case head @body.bindings of+	                 [] -> id+	                 bs -> L bs+	| S lhs.bindings = [] : @body.bindings+	    lhs.readback = S @var @body.readback+	| A lhs.bindings = zipWith (⧺) @fun.bindings @arg.bindings+	    lhs.readback = A @fun.readback @arg.readback+	| I lhs.bindings = let (bs:bss) = @body.bindings in ((@var,@body.readback) : bs) : bss+	    lhs.readback = V @var+	| V lhs.bindings = repeat []+	    lhs.readback = V @var+	| L lhs.bindings = @loc.readbackError+	    lhs.readback = @loc.readbackError+	    loc.readbackError = error "readback is only defined for λ-spanning-trees"  -- proof generation ---------------------------------------------------- 

@@ -19,7 +19,8 @@   data Opt-	= OptNoVarBacklinks+	= Help+	| OptNoVarBacklinks 	| OptNoSBacklinks 	| OptSharedVars 	| OptMaxPrefix@@ -27,7 +28,8 @@ 	deriving Eq  options = let option s o d = Option [] [s] (NoArg o) d in-	[option "no-var-backlinks" OptNoVarBacklinks "no backlinks for variable occurrences",+	[Option ['h'] ["help"]     (NoArg Help)      "show this usage information",+	 option "no-var-backlinks" OptNoVarBacklinks "no backlinks for variable occurrences", 	 option "no-s-backlinks"   OptNoSBacklinks   "no backlinks for delimiter vertices", 	 option "shared-variables" OptSharedVars     "implicit sharing of variable occurrences", 	 option "max-prefix"       OptMaxPrefix      "maximal (same) prefix lengths for let-bindings",@@ -39,11 +41,14 @@ main = do 	args ← getArgs -	let (params, files) = case getOpt Permute options args of-		(options, files, []) → (processOptions options, files)+	case getOpt Permute options args of+		(opts, files, []) → do+			let params = processOptions opts+			if Help ∈ opts+				then putStr $ usageInfo usage options+				else mapM_ (processFile params) files 		(_,_,errs) → error (concat errs ++ usageInfo usage options) -	mapM_ (processFile params) files  processOptions options = let has opt = opt ∈ options in Params 	{letPrefixLengths   = if has OptMaxPrefix then MaxPrefix else if has OptMinPrefix then MinPrefix else MaxEagPre,

@@ -0,0 +1,2 @@+let two = λx. λy. x (x y)+in two two

@@ -0,0 +1,1 @@+let omega = λx.x x in omega omega

@@ -0,0 +1,1 @@+(\F. (\f. f (f 0)) (F 0)) (\y. \x. x) 

@@ -0,0 +1,1 @@+(\F. (\f. f (f 0)) (F (F 0 0))) (\y. \x. x) 

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

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

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

@@ -0,0 +1,1 @@+(λx. x (λi. i)) λy. (λd. d d) (y z)

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

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

@@ -0,0 +1,1 @@+let fix f = f (fix f) in fix

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

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

@@ -0,0 +1,3 @@+((λg.(g(g(λx.x))))+ (λh.((λf.(f(f(λz.z))))+      (λw.(h(w(λy.y)))))))

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

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

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

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

@@ -0,0 +1,5 @@+let+	h = λh. let+			w = λw. h (w (λy.y))+		in w (w (λz.z))+in h (h (λx.x))

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

@@ -0,0 +1,6 @@+let R = λx y.+	let+		f = R x+		g = R y+	in f g+in R

@@ -0,0 +1,7 @@+let f x =+	let+		g = i+		h = x+		i = h+	in g h+in f

@@ -0,0 +1,7 @@+let f x y z =+	let g a b =+		let h c d =+			let i e = h g in i+		in h+	in g+in f

@@ -0,0 +1,7 @@+let f x y z =+	let+		g = x i+		h = y f+		i = z f g+	in g h+in f

@@ -0,0 +1,2 @@+let repeat x = Cons x (repeat x)+in repeat 7

@@ -0,0 +1,2 @@+let repeat x = let loop = Cons x loop in loop+in repeat 7

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

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

@@ -0,0 +1,1 @@+let twice f x = f (f x) in twice twice inc

@@ -0,0 +1,3 @@+let delta = \x. x x+    Delta = (\y. y y) (\z. z z)+in  delta Delta

@@ -0,0 +1,4 @@+let G = \g. g (g x) +    F x = F x+    I x = x +in  G (F I)

@@ -0,0 +1,2 @@+let epsilon = (\f.f(f(f a)))((\x.\y.y x)b)+in  epsilon

@@ -1,5 +1,5 @@ Name:           maxsharing-Version:        1.0+Version:        1.0.2 Copyright:      (c) 2013, Jan Rochel Author:         Jan Rochel Maintainer:     jan@rochel.info@@ -20,16 +20,17 @@ Category:       Graphs, Compiler Cabal-Version:  >= 1.6 Extra-Source-Files: uuagc_options+Data-Files:     examples/*.l  Executable maxsharing   Build-Depends:-    base < 4.7,+    base < 4.8,     base-unicode-symbols < 0.3,-    parsec < 3.2,+    parsec < 2.2,     IndentParser < 0.3,     containers < 0.6,     containers-unicode-symbols < 0.4,-    mtl < 2.2,+    mtl < 2.3,     uuagc-cabal < 1.1,     uuagc >= 0.9.50.2,     HaLeX >= 1.2.1,