From 435251b3091f7bcd3ffe9a75507b8c83687e9cb1 Mon Sep 17 00:00:00 2001
From: Sean Gillespie <sean@mistersg.net>
Date: Sat, 31 Dec 2016 00:26:57 -0500
Subject: [PATCH] Refactor based on static analysis
---
test/Language/Lambda/Examples/BoolSpec.hs | 199 +++++++++++-----------
test/Language/Lambda/Examples/NatSpec.hs | 189 ++++++++++----------
test/Language/Lambda/Examples/PairSpec.hs | 55 +++---
3 files changed, 220 insertions(+), 223 deletions(-)
diff --git a/test/Language/Lambda/Examples/BoolSpec.hs b/test/Language/Lambda/Examples/BoolSpec.hs
index 1715ff4..e7ecc35 100644
--- a/test/Language/Lambda/Examples/BoolSpec.hs
+++ b/test/Language/Lambda/Examples/BoolSpec.hs
@@ -5,105 +5,104 @@ import Test.Hspec
import Language.Lambda.HspecUtils
spec :: Spec
-spec = do
- describe "Bool" $ do
- -- Bool is the definition of Booleans. We represent bools
- -- using Church Encodings:
+spec = describe "Bool" $ do
+ -- Bool is the definition of Booleans. We represent bools
+ -- using Church Encodings:
+ --
+ -- true: \t f. t
+ -- false: \t f. f
+ describe "and" $ do
+ -- The function and takes two Bools and returns true
+ -- iff both arguments are true
+ --
+ -- and(true, true) = true
+ -- and(false, true) = false
+ -- and(true, false) = false
+ -- and(false, false) = false
--
- -- true: \t f. t
- -- false: \t f. f
- describe "and" $ do
- -- The function and takes two Bools and returns true
- -- iff both arguments are true
- --
- -- and(true, true) = true
- -- and(false, true) = false
- -- and(true, false) = false
- -- and(false, false) = false
- --
- -- and is defined by
- -- and = \x y. x y x
- it "true and true = true" $ do
- "(\\x y. x y x) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"
-
- it "true and false = false" $ do
- "(\\x y. x y x) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. f"
-
- it "false and true = false" $ do
- "(\\x y. x y x) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. f"
-
- it "false and false = false" $ do
- "(\\x y. x y x) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"
-
- it "false and p = false" $ do
- "(\\x y. x y x) (\\t f. f) p" `shouldEvalTo` "\\t f. f"
-
- it "true and p = false" $ do
- "(\\x y. x y x) (\\t f. t) p" `shouldEvalTo` "p"
-
- describe "or" $ do
- -- or takes two Bools and returns true iff either argument is true
- --
- -- or(true, true) = true
- -- or(true, false) = true
- -- or(false, true) = true
- -- or(false, false) = false
- --
- -- or is defined by
- -- or = \x y. x x y
- it "true or true = true" $ do
- "(\\x y. x x y) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"
+ -- and is defined by
+ -- and = \x y. x y x
+ it "true and true = true" $
+ "(\\x y. x y x) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"
+
+ it "true and false = false" $
+ "(\\x y. x y x) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. f"
- it "true or false = true" $ do
- "(\\x y. x x y) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. t"
-
- it "false or true = true" $ do
- "(\\x y. x x y) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. t"
-
- it "false or false = false" $ do
- "(\\x y. x x y) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"
-
- it "true or p = true" $ do
- "(\\x y. x x y) (\\t f. t) p" `shouldEvalTo` "\\t f. t"
-
- it "false or p = p" $ do
- "(\\x y. x x y) (\\t f. f) p" `shouldEvalTo` "p"
-
-
- describe "not" $ do
- -- not takes a Bool and returns its opposite value
- --
- -- not(true) = false
- -- not(false) = true
- --
- -- not is defined by
- -- not = \x. x (\t f. f) (\t f. t)
- it "not true = false" $ do
- "(\\x. x (\\t f. f) (\\t f. t)) \\t f. t" `shouldEvalTo` "\\t f. f"
-
- it "not false = true"$ do
- "(\\x. x (\\t f. f) (\\t f. t)) \\t f. f" `shouldEvalTo` "\\t f. t"
-
- describe "if" $ do
- -- if takes a Bool and two values. If returns the first value
- -- if the Bool is true, and the second otherwise. In other words,
- -- if p x y = if p then x else y
- --
- -- if(true, x, y) = x
- -- if(false, x, y) = y
- --
- -- if is defined by
- -- if = \p x y. p x y
- it "if true 0 1 = 0" $ do
- "(\\p x y. p x y) (\\t f. t) (\\f x. x) (\\f x. f x)"
- `shouldEvalTo` "\\f x. x"
-
- it "if false 0 1 = 1" $ do
- "(\\p x y. p x y) (\\t f. f) (\\f x. x) (\\f x. f x)"
- `shouldEvalTo` "\\f x. f x"
-
- it "it true p q = p" $ do
- "(\\p x y. p x y) (\\t f. t) p q" `shouldEvalTo` "p"
-
- it "it false p q = q" $ do
- "(\\p x y. p x y) (\\t f. f) p q" `shouldEvalTo` "q"
+ it "false and true = false" $
+ "(\\x y. x y x) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. f"
+
+ it "false and false = false" $
+ "(\\x y. x y x) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"
+
+ it "false and p = false" $
+ "(\\x y. x y x) (\\t f. f) p" `shouldEvalTo` "\\t f. f"
+
+ it "true and p = false" $
+ "(\\x y. x y x) (\\t f. t) p" `shouldEvalTo` "p"
+
+ describe "or" $ do
+ -- or takes two Bools and returns true iff either argument is true
+ --
+ -- or(true, true) = true
+ -- or(true, false) = true
+ -- or(false, true) = true
+ -- or(false, false) = false
+ --
+ -- or is defined by
+ -- or = \x y. x x y
+ it "true or true = true" $
+ "(\\x y. x x y) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"
+
+ it "true or false = true" $
+ "(\\x y. x x y) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. t"
+
+ it "false or true = true" $
+ "(\\x y. x x y) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. t"
+
+ it "false or false = false" $
+ "(\\x y. x x y) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"
+
+ it "true or p = true" $
+ "(\\x y. x x y) (\\t f. t) p" `shouldEvalTo` "\\t f. t"
+
+ it "false or p = p" $
+ "(\\x y. x x y) (\\t f. f) p" `shouldEvalTo` "p"
+
+
+ describe "not" $ do
+ -- not takes a Bool and returns its opposite value
+ --
+ -- not(true) = false
+ -- not(false) = true
+ --
+ -- not is defined by
+ -- not = \x. x (\t f. f) (\t f. t)
+ it "not true = false" $
+ "(\\x. x (\\t f. f) (\\t f. t)) \\t f. t" `shouldEvalTo` "\\t f. f"
+
+ it "not false = true" $
+ "(\\x. x (\\t f. f) (\\t f. t)) \\t f. f" `shouldEvalTo` "\\t f. t"
+
+ describe "if" $ do
+ -- if takes a Bool and two values. If returns the first value
+ -- if the Bool is true, and the second otherwise. In other words,
+ -- if p x y = if p then x else y
+ --
+ -- if(true, x, y) = x
+ -- if(false, x, y) = y
+ --
+ -- if is defined by
+ -- if = \p x y. p x y
+ it "if true 0 1 = 0" $
+ "(\\p x y. p x y) (\\t f. t) (\\f x. x) (\\f x. f x)"
+ `shouldEvalTo` "\\f x. x"
+
+ it "if false 0 1 = 1" $
+ "(\\p x y. p x y) (\\t f. f) (\\f x. x) (\\f x. f x)"
+ `shouldEvalTo` "\\f x. f x"
+
+ it "it true p q = p" $
+ "(\\p x y. p x y) (\\t f. t) p q" `shouldEvalTo` "p"
+
+ it "it false p q = q" $
+ "(\\p x y. p x y) (\\t f. f) p q" `shouldEvalTo` "q"
diff --git a/test/Language/Lambda/Examples/NatSpec.hs b/test/Language/Lambda/Examples/NatSpec.hs
index a456bc9..01b8c5d 100644
--- a/test/Language/Lambda/Examples/NatSpec.hs
+++ b/test/Language/Lambda/Examples/NatSpec.hs
@@ -5,99 +5,98 @@ import Test.Hspec
import Language.Lambda.HspecUtils
spec :: Spec
-spec = do
- describe "Nat" $ do
- -- Nat is the definition of natural numbers. More precisely, Nat
- -- is the set of nonnegative integers. We represent nats using
- -- Church Encodings:
+spec = describe "Nat" $ do
+ -- Nat is the definition of natural numbers. More precisely, Nat
+ -- is the set of nonnegative integers. We represent nats using
+ -- Church Encodings:
+ --
+ -- 0: \f x. x
+ -- 1: \f x. f x
+ -- 2: \f x. f (f x)
+ -- ...and so on
+
+ describe "successor" $ do
+ -- successor is a function that adds 1
+ -- succ(0) = 1
+ -- succ(1) = 2
+ -- ... and so forth
--
- -- 0: \f x. x
- -- 1: \f x. f x
- -- 2: \f x. f (f x)
- -- ...and so on
-
- describe "successor" $ do
- -- successor is a function that adds 1
- -- succ(0) = 1
- -- succ(1) = 2
- -- ... and so forth
- --
- -- successor is defined by
- -- succ = \n f x. f (n f x)
- it "succ 0 = 1" $ do
- "(\\n f x. f (n f x)) (\\f x. x)" `shouldEvalTo` "\\f x. f x"
-
- it "succ 1 = 2" $ do
- "(\\n f x. f (n f x)) (\\f x. f x)" `shouldEvalTo` "\\f x. f (f x)"
-
- describe "add" $ do
- -- add(m, n) = m + n
- --
- -- It is defined by applying successor m times on n:
- -- add = \m n f x. m f (n f x)
- it "add 0 2 = 2" $ do
- "(\\m n f x. m f (n f x)) (\\f x. x) (\\f x. f (f x))"
- `shouldEvalTo` "\\f x. f (f x)"
-
- it "add 3 2 = 5" $ do
- "(\\m n f x. m f (n f x)) (\\f x. f (f (f x))) (\\f x. f (f x))"
- `shouldEvalTo` "\\f x. f (f (f (f (f x))))"
-
- -- Here, we use `\f x. n f x` instead of `n`. This is because
- -- I haven't implemented eta conversion
- it "add 0 n = n" $ do
- "(\\m n f x. m f (n f x)) (\\f x. x) n"
- `shouldEvalTo` "\\f x. n f x"
-
- describe "multiply" $ do
- -- multiply(m, n) = m * n
- --
- -- multiply is defined by applying add m times
- -- multiply = \m n f x. m (n f x) x)
- --
- -- Using eta conversion, we can omit the parameter x
- -- multiply = \m n f. m (n f)
- it "multiply 0 2 = 0" $ do
- "(\\m n f. m (n f)) (\\f x. x) (\\f x. f (f x))"
- `shouldEvalTo` "\\f x. x"
-
- it "multiply 2 3 = 6" $ do
- "(\\m n f. m (n f)) (\\f x. f (f x)) (\\f x. f (f (f x)))"
- `shouldEvalTo` "\\f x. f (f (f (f (f (f x)))))"
-
- it "multiply 0 n = 0" $ do
- "(\\m n f. m (n f)) (\\f x. x) n"
- `shouldEvalTo` "\\f x. x"
-
- it "multiply 1 n = n" $ do
- "(\\m n f. m (n f)) (\\f x. f x) n"
- `shouldEvalTo` "\\f x. n f x"
-
- describe "power" $ do
- -- The function power raises m to the power of n.
- -- power(m, n) = m^n
- --
- -- power is defined by applying multiply n times
- -- power = \m n f x. (n m) f x
- --
- -- Using eta conversion again, we can omit the parameter f
- -- power = \m n = n m
-
- -- NOTE: Here we use the first form to get more predictable
- -- variable names. Otherwise, alpha conversion will choose a random
- -- unique variable.
- it "power 0 1 = 0" $ do
- "(\\m n f x. (n m) f x) (\\f x. x) (\\f x. f x)"
- `shouldEvalTo` "\\f x. x"
-
- it "power 2 3 = 8" $ do
- "(\\m n f x. (n m) f x) (\\f x. f (f x)) (\\f x. f (f (f x)))"
- `shouldEvalTo` "\\f x. f (f (f (f (f (f (f (f x)))))))"
-
- it "power n 0 = 1" $ do
- "(\\m n f x. (n m) f x) n (\\f x. x)"
- `shouldEvalTo` "\\f x. f x"
-
- it "power n 1 = n" $ do
- "(\\m n f x. (n m) f x) n (\\f x. f x)"
- `shouldEvalTo` "\\f x. n f x"
+ -- successor is defined by
+ -- succ = \n f x. f (n f x)
+ it "succ 0 = 1" $
+ "(\\n f x. f (n f x)) (\\f x. x)" `shouldEvalTo` "\\f x. f x"
+
+ it "succ 1 = 2" $
+ "(\\n f x. f (n f x)) (\\f x. f x)" `shouldEvalTo` "\\f x. f (f x)"
+
+ describe "add" $ do
+ -- add(m, n) = m + n
+ --
+ -- It is defined by applying successor m times on n:
+ -- add = \m n f x. m f (n f x)
+ it "add 0 2 = 2" $
+ "(\\m n f x. m f (n f x)) (\\f x. x) (\\f x. f (f x))"
+ `shouldEvalTo` "\\f x. f (f x)"
+
+ it "add 3 2 = 5" $
+ "(\\m n f x. m f (n f x)) (\\f x. f (f (f x))) (\\f x. f (f x))"
+ `shouldEvalTo` "\\f x. f (f (f (f (f x))))"
+
+ -- Here, we use `\f x. n f x` instead of `n`. This is because
+ -- I haven't implemented eta conversion
+ it "add 0 n = n" $
+ "(\\m n f x. m f (n f x)) (\\f x. x) n"
+ `shouldEvalTo` "\\f x. n f x"
+
+ describe "multiply" $ do
+ -- multiply(m, n) = m * n
+ --
+ -- multiply is defined by applying add m times
+ -- multiply = \m n f x. m (n f x) x)
+ --
+ -- Using eta conversion, we can omit the parameter x
+ -- multiply = \m n f. m (n f)
+ it "multiply 0 2 = 0" $
+ "(\\m n f. m (n f)) (\\f x. x) (\\f x. f (f x))"
+ `shouldEvalTo` "\\f x. x"
+
+ it "multiply 2 3 = 6" $
+ "(\\m n f. m (n f)) (\\f x. f (f x)) (\\f x. f (f (f x)))"
+ `shouldEvalTo` "\\f x. f (f (f (f (f (f x)))))"
+
+ it "multiply 0 n = 0" $
+ "(\\m n f. m (n f)) (\\f x. x) n"
+ `shouldEvalTo` "\\f x. x"
+
+ it "multiply 1 n = n" $
+ "(\\m n f. m (n f)) (\\f x. f x) n"
+ `shouldEvalTo` "\\f x. n f x"
+
+ describe "power" $ do
+ -- The function power raises m to the power of n.
+ -- power(m, n) = m^n
+ --
+ -- power is defined by applying multiply n times
+ -- power = \m n f x. (n m) f x
+ --
+ -- Using eta conversion again, we can omit the parameter f
+ -- power = \m n = n m
+
+ -- NOTE: Here we use the first form to get more predictable
+ -- variable names. Otherwise, alpha conversion will choose a random
+ -- unique variable.
+ it "power 0 1 = 0" $
+ "(\\m n f x. (n m) f x) (\\f x. x) (\\f x. f x)"
+ `shouldEvalTo` "\\f x. x"
+
+ it "power 2 3 = 8" $
+ "(\\m n f x. (n m) f x) (\\f x. f (f x)) (\\f x. f (f (f x)))"
+ `shouldEvalTo` "\\f x. f (f (f (f (f (f (f (f x)))))))"
+
+ it "power n 0 = 1" $
+ "(\\m n f x. (n m) f x) n (\\f x. x)"
+ `shouldEvalTo` "\\f x. f x"
+
+ it "power n 1 = n" $
+ "(\\m n f x. (n m) f x) n (\\f x. f x)"
+ `shouldEvalTo` "\\f x. n f x"
diff --git a/test/Language/Lambda/Examples/PairSpec.hs b/test/Language/Lambda/Examples/PairSpec.hs
index 17a1a04..1c66e9a 100644
--- a/test/Language/Lambda/Examples/PairSpec.hs
+++ b/test/Language/Lambda/Examples/PairSpec.hs
@@ -5,35 +5,34 @@ import Language.Lambda.HspecUtils
import Test.Hspec
spec :: Spec
-spec = do
- describe "Pair" $ do
- -- Pair is the definition of tuples with two items. Pairs,
- -- again are represented using Church Encodings:
+spec = describe "Pair" $ do
+ -- Pair is the definition of tuples with two items. Pairs,
+ -- again are represented using Church Encodings:
+ --
+ -- pair = \x y f. f x y
+ describe "first" $ do
+ -- The function first returns the first item in a pair
+ -- first(x, y) = x
--
- -- pair = \x y f. f x y
- describe "first" $ do
- -- The function first returns the first item in a pair
- -- first(x, y) = x
- --
- -- first is defined by
- -- first = \p. p (\t f. t)
- it "first 0 1 = 0" $ do
- "(\\p. p (\\t f. t)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"
- `shouldEvalTo` "\\f x. x"
+ -- first is defined by
+ -- first = \p. p (\t f. t)
+ it "first 0 1 = 0" $
+ "(\\p. p (\\t f. t)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"
+ `shouldEvalTo` "\\f x. x"
- it "first x y = x" $ do
- "(\\p. p (\\t f. t)) ((\\x y f. f x y) x y)" `shouldEvalTo` "x"
+ it "first x y = x" $
+ "(\\p. p (\\t f. t)) ((\\x y f. f x y) x y)" `shouldEvalTo` "x"
- describe "second" $ do
- -- The function second returns the second item in a pair
- -- second(x, y) = y
- --
- -- second is defined by
- -- second = \p. p (\t f. f)
- it "second 0 1 = 1" $ do
- "(\\p. p (\\t f. f)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"
- `shouldEvalTo` "\\f x. f x"
+ describe "second" $ do
+ -- The function second returns the second item in a pair
+ -- second(x, y) = y
+ --
+ -- second is defined by
+ -- second = \p. p (\t f. f)
+ it "second 0 1 = 1" $
+ "(\\p. p (\\t f. f)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"
+ `shouldEvalTo` "\\f x. f x"
- it "second x y = y" $ do
- "(\\p. p (\\t f. f)) ((\\x y f. f x y) x y)" `shouldEvalTo` "y"
- "(\\p. p (\\x y z. x)) ((\\x y z f. f x y z) x y z)" `shouldEvalTo` "x"
+ it "second x y = y" $ do
+ "(\\p. p (\\t f. f)) ((\\x y f. f x y) x y)" `shouldEvalTo` "y"
+ "(\\p. p (\\x y z. x)) ((\\x y z f. f x y z) x y z)" `shouldEvalTo` "x"
--
GitLab