Fakultas Ilmu Komputer UI
Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
Ari Angga Nugraha
ariangganugraha-funpro2020-lambda
Commits
435251b3
Commit
435251b3
authored
Dec 31, 2016
by
Sean Gillespie
Browse files
Refactor based on static analysis
parent
6cc049ac
Changes
3
Hide whitespace changes
Inline
Side-by-side
test/Language/Lambda/Examples/BoolSpec.hs
View file @
435251b3
...
...
@@ -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"
test/Language/Lambda/Examples/NatSpec.hs
View file @
435251b3
...
...
@@ -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"
test/Language/Lambda/Examples/PairSpec.hs
View file @
435251b3
...
...
@@ -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"
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment