diff --git a/Lambda.ag b/Lambda.ag --- a/Lambda.ag +++ b/Lambda.ag @@ -22,13 +22,18 @@ {type V = String} -- variables + +-- +-- 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 +-- + | S var ∷ V body ∷ Λ -- adbmal / scope delimiter + | I var ∷ V body ∷ Λ -- indirection node +-- 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 ---------------------------------------------------- diff --git a/MaxSharing.hs b/MaxSharing.hs --- a/MaxSharing.hs +++ b/MaxSharing.hs @@ -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, diff --git a/examples/2times2.l b/examples/2times2.l new file mode 100644 --- /dev/null +++ b/examples/2times2.l @@ -0,0 +1,2 @@ +let two = λx. λy. x (x y) +in two two diff --git a/examples/Omega.l b/examples/Omega.l new file mode 100644 --- /dev/null +++ b/examples/Omega.l @@ -0,0 +1,1 @@ +let omega = λx.x x in omega omega diff --git a/examples/WW-beta-saving-0.l b/examples/WW-beta-saving-0.l new file mode 100644 --- /dev/null +++ b/examples/WW-beta-saving-0.l @@ -0,0 +1,1 @@ +(\F. (\f. f (f 0)) (F 0)) (\y. \x. x) diff --git a/examples/WW-beta-saving-1.l b/examples/WW-beta-saving-1.l new file mode 100644 --- /dev/null +++ b/examples/WW-beta-saving-1.l @@ -0,0 +1,1 @@ +(\F. (\f. f (f 0)) (F (F 0 0))) (\y. \x. x) diff --git a/examples/asperti_guerrini_3011.l b/examples/asperti_guerrini_3011.l new file mode 100644 --- /dev/null +++ b/examples/asperti_guerrini_3011.l @@ -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))) diff --git a/examples/asperti_guerrini_3011_simpl.l b/examples/asperti_guerrini_3011_simpl.l new file mode 100644 --- /dev/null +++ b/examples/asperti_guerrini_3011_simpl.l @@ -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) diff --git a/examples/asperti_guerrini_3012.l b/examples/asperti_guerrini_3012.l new file mode 100644 --- /dev/null +++ b/examples/asperti_guerrini_3012.l @@ -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))) diff --git a/examples/asperti_guerrini_p14.l b/examples/asperti_guerrini_p14.l new file mode 100644 --- /dev/null +++ b/examples/asperti_guerrini_p14.l @@ -0,0 +1,1 @@ +(λx. x (λi. i)) λy. (λd. d d) (y z) diff --git a/examples/exp.l b/examples/exp.l new file mode 100644 --- /dev/null +++ b/examples/exp.l @@ -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 diff --git a/examples/exp_simpl.l b/examples/exp_simpl.l new file mode 100644 --- /dev/null +++ b/examples/exp_simpl.l @@ -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) diff --git a/examples/fix.l b/examples/fix.l new file mode 100644 --- /dev/null +++ b/examples/fix.l @@ -0,0 +1,1 @@ +let fix f = f (fix f) in fix diff --git a/examples/flip_const_id.l b/examples/flip_const_id.l new file mode 100644 --- /dev/null +++ b/examples/flip_const_id.l @@ -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 diff --git a/examples/head123.l b/examples/head123.l new file mode 100644 --- /dev/null +++ b/examples/head123.l @@ -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 diff --git a/examples/lamping.l b/examples/lamping.l new file mode 100644 --- /dev/null +++ b/examples/lamping.l @@ -0,0 +1,3 @@ +((λg.(g(g(λx.x)))) + (λh.((λf.(f(f(λz.z)))) + (λw.(h(w(λy.y))))))) diff --git a/examples/lamping_p20r_qp.l b/examples/lamping_p20r_qp.l new file mode 100644 --- /dev/null +++ b/examples/lamping_p20r_qp.l @@ -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)))))))) diff --git a/examples/lamping_p20r_qp_simpl.l b/examples/lamping_p20r_qp_simpl.l new file mode 100644 --- /dev/null +++ b/examples/lamping_p20r_qp_simpl.l @@ -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 diff --git a/examples/lamping_p20r_qq.l b/examples/lamping_p20r_qq.l new file mode 100644 --- /dev/null +++ b/examples/lamping_p20r_qq.l @@ -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)))))))) diff --git a/examples/lamping_p20r_qq_simpl.l b/examples/lamping_p20r_qq_simpl.l new file mode 100644 --- /dev/null +++ b/examples/lamping_p20r_qq_simpl.l @@ -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 diff --git a/examples/lamping_simpl.l b/examples/lamping_simpl.l new file mode 100644 --- /dev/null +++ b/examples/lamping_simpl.l @@ -0,0 +1,5 @@ +let + h = λh. let + w = λw. h (w (λy.y)) + in w (w (λz.z)) +in h (h (λx.x)) diff --git a/examples/levy-1988-p184bottom.l b/examples/levy-1988-p184bottom.l new file mode 100644 --- /dev/null +++ b/examples/levy-1988-p184bottom.l @@ -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)) + diff --git a/examples/morazan-fig1.l b/examples/morazan-fig1.l new file mode 100644 --- /dev/null +++ b/examples/morazan-fig1.l @@ -0,0 +1,6 @@ +let R = λx y. + let + f = R x + g = R y + in f g +in R diff --git a/examples/morazan-fig4.l b/examples/morazan-fig4.l new file mode 100644 --- /dev/null +++ b/examples/morazan-fig4.l @@ -0,0 +1,7 @@ +let f x = + let + g = i + h = x + i = h + in g h +in f diff --git a/examples/morazan-fig6.l b/examples/morazan-fig6.l new file mode 100644 --- /dev/null +++ b/examples/morazan-fig6.l @@ -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 diff --git a/examples/morazan-fig8.l b/examples/morazan-fig8.l new file mode 100644 --- /dev/null +++ b/examples/morazan-fig8.l @@ -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 diff --git a/examples/repeat_naive.l b/examples/repeat_naive.l new file mode 100644 --- /dev/null +++ b/examples/repeat_naive.l @@ -0,0 +1,2 @@ +let repeat x = Cons x (repeat x) +in repeat 7 diff --git a/examples/repeat_optim.l b/examples/repeat_optim.l new file mode 100644 --- /dev/null +++ b/examples/repeat_optim.l @@ -0,0 +1,2 @@ +let repeat x = let loop = Cons x loop in loop +in repeat 7 diff --git a/examples/sum1.l b/examples/sum1.l new file mode 100644 --- /dev/null +++ b/examples/sum1.l @@ -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) diff --git a/examples/sum1234.l b/examples/sum1234.l new file mode 100644 --- /dev/null +++ b/examples/sum1234.l @@ -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))) diff --git a/examples/twice.l b/examples/twice.l new file mode 100644 --- /dev/null +++ b/examples/twice.l @@ -0,0 +1,1 @@ +let twice f x = f (f x) in twice twice inc diff --git a/examples/vincent-0-ww.l b/examples/vincent-0-ww.l new file mode 100644 --- /dev/null +++ b/examples/vincent-0-ww.l @@ -0,0 +1,3 @@ +let delta = \x. x x + Delta = (\y. y y) (\z. z z) +in delta Delta diff --git a/examples/vincent-1-ww.l b/examples/vincent-1-ww.l new file mode 100644 --- /dev/null +++ b/examples/vincent-1-ww.l @@ -0,0 +1,4 @@ +let G = \g. g (g x) + F x = F x + I x = x +in G (F I) diff --git a/examples/wadsworth-thesis-p172.l b/examples/wadsworth-thesis-p172.l new file mode 100644 --- /dev/null +++ b/examples/wadsworth-thesis-p172.l @@ -0,0 +1,2 @@ +let epsilon = (\f.f(f(f a)))((\x.\y.y x)b) +in epsilon diff --git a/maxsharing.cabal b/maxsharing.cabal --- a/maxsharing.cabal +++ b/maxsharing.cabal @@ -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,