diff options
Diffstat (limited to 'tests/examples')
66 files changed, 588 insertions, 0 deletions
diff --git a/tests/examples/beta.lam b/tests/examples/beta.lam new file mode 100644 index 0000000..9d53b08 --- /dev/null +++ b/tests/examples/beta.lam @@ -0,0 +1,3 @@ +(\ x . (\ z . z z) x three) ((\ y . y y) (\ w . w)) + +-- Should reduce to three diff --git a/tests/examples/beta.out b/tests/examples/beta.out new file mode 100644 index 0000000..ac8f0f0 --- /dev/null +++ b/tests/examples/beta.out @@ -0,0 +1 @@ +(\x . (\z . z z) x three) ((\y . y y) (\w . w)) diff --git a/tests/examples/beta1.lam b/tests/examples/beta1.lam new file mode 100644 index 0000000..3ffc446 --- /dev/null +++ b/tests/examples/beta1.lam @@ -0,0 +1,3 @@ +(\x . x three) (\y . plus y y) + +-- Should reduce to plus three three diff --git a/tests/examples/beta1.out b/tests/examples/beta1.out new file mode 100644 index 0000000..6ceecd5 --- /dev/null +++ b/tests/examples/beta1.out @@ -0,0 +1 @@ +(\x . x three) (\y . plus y y) diff --git a/tests/examples/beta2.lam b/tests/examples/beta2.lam new file mode 100644 index 0000000..02ae576 --- /dev/null +++ b/tests/examples/beta2.lam @@ -0,0 +1,3 @@ +(\x . (\x . x) x) one + +-- should reduce to one diff --git a/tests/examples/beta2.out b/tests/examples/beta2.out new file mode 100644 index 0000000..3434328 --- /dev/null +++ b/tests/examples/beta2.out @@ -0,0 +1 @@ +(\x . (\x . x) x) one diff --git a/tests/examples/beta3.lam b/tests/examples/beta3.lam new file mode 100644 index 0000000..e112b5c --- /dev/null +++ b/tests/examples/beta3.lam @@ -0,0 +1,3 @@ +(\ x . \ y . x y ) y + +-- Should reduce to \z . y z (for some fresh z) diff --git a/tests/examples/beta3.out b/tests/examples/beta3.out new file mode 100644 index 0000000..322346c --- /dev/null +++ b/tests/examples/beta3.out @@ -0,0 +1 @@ +(\x . \y . x y) y diff --git a/tests/examples/bools-and-t-f.lam b/tests/examples/bools-and-t-f.lam new file mode 100644 index 0000000..fd9a29c --- /dev/null +++ b/tests/examples/bools-and-t-f.lam @@ -0,0 +1,16 @@ +(\ true false and or not . + + and true false + + -- Should reduce to false, i.e., \ x y . y +) +-- true +(\ x y . x) +-- false +(\ x y . y) +-- and +(\ p q . p q p) +-- or +(\ p q . p p q) +-- not +(\ p x y . p y x) diff --git a/tests/examples/bools-and-t-f.out b/tests/examples/bools-and-t-f.out new file mode 100644 index 0000000..e422fcc --- /dev/null +++ b/tests/examples/bools-and-t-f.out @@ -0,0 +1 @@ +(\true . \false . \and . \or . \not . and true false) (\x . \y . x) (\x . \y . y) (\p . \q . p q p) (\p . \q . p p q) (\p . \x . \y . p y x) diff --git a/tests/examples/bools-not-t.lam b/tests/examples/bools-not-t.lam new file mode 100644 index 0000000..9afcc48 --- /dev/null +++ b/tests/examples/bools-not-t.lam @@ -0,0 +1,16 @@ +(\ true false and or not . + + not true + + -- Should reduce to false, i.e., \ x y . y +) +-- true +(\ x y . x) +-- false +(\ x y . y) +-- and +(\ p q . p q p) +-- or +(\ p q . p p q) +-- not +(\ p x y . p y x) diff --git a/tests/examples/bools-not-t.out b/tests/examples/bools-not-t.out new file mode 100644 index 0000000..2a6a257 --- /dev/null +++ b/tests/examples/bools-not-t.out @@ -0,0 +1 @@ +(\true . \false . \and . \or . \not . not true) (\x . \y . x) (\x . \y . y) (\p . \q . p q p) (\p . \q . p p q) (\p . \x . \y . p y x) diff --git a/tests/examples/bools-or-f-t.lam b/tests/examples/bools-or-f-t.lam new file mode 100644 index 0000000..5c39cd8 --- /dev/null +++ b/tests/examples/bools-or-f-t.lam @@ -0,0 +1,16 @@ +(\ true false and or not . + + or false true + + -- Should reduce to true, i.e., \ x y . x +) +-- true +(\ x y . x) +-- false +(\ x y . y) +-- and +(\ p q . p q p) +-- or +(\ p q . p p q) +-- not +(\ p x y . p y x) diff --git a/tests/examples/bools-or-f-t.out b/tests/examples/bools-or-f-t.out new file mode 100644 index 0000000..78a2057 --- /dev/null +++ b/tests/examples/bools-or-f-t.out @@ -0,0 +1 @@ +(\true . \false . \and . \or . \not . or false true) (\x . \y . x) (\x . \y . y) (\p . \q . p q p) (\p . \q . p p q) (\p . \x . \y . p y x) diff --git a/tests/examples/currying.lam b/tests/examples/currying.lam new file mode 100644 index 0000000..5463ce7 --- /dev/null +++ b/tests/examples/currying.lam @@ -0,0 +1,3 @@ +(\x y. plus (plus x y) x) one two + +-- Should reduce to plus (plus one two) one diff --git a/tests/examples/currying.out b/tests/examples/currying.out new file mode 100644 index 0000000..5660f00 --- /dev/null +++ b/tests/examples/currying.out @@ -0,0 +1 @@ +(\x . \y . plus (plus x y) x) one two diff --git a/tests/examples/fac-three.lam b/tests/examples/fac-three.lam new file mode 100644 index 0000000..613c933 --- /dev/null +++ b/tests/examples/fac-three.lam @@ -0,0 +1,31 @@ +(\ zero one two three succ plus mult pred minus isZero yComb . + (\ fac . + fac three + -- NOTE: the y-combinator does not have a normal form + ) (yComb (\ f n . (isZero n) one (mult n (f (pred n))))) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) + +-- yComb +(\ f . (\ x . f (x x)) (\ x . f (x x))) diff --git a/tests/examples/fac-three.out b/tests/examples/fac-three.out new file mode 100644 index 0000000..5430f7f --- /dev/null +++ b/tests/examples/fac-three.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . \yComb . (\fac . fac three) (yComb (\f . \n . isZero n one (mult n (f (pred n)))))) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) (\f . (\x . f (x x)) (\x . f (x x))) diff --git a/tests/examples/head-normal-form.lam b/tests/examples/head-normal-form.lam new file mode 100644 index 0000000..bf859a0 --- /dev/null +++ b/tests/examples/head-normal-form.lam @@ -0,0 +1,6 @@ +-- normal form N +-- weak normal form N +-- head normal form Y +-- weak head normal form Y + +f ((\x . x x) (\x . x x)) diff --git a/tests/examples/head-normal-form.out b/tests/examples/head-normal-form.out new file mode 100644 index 0000000..574706c --- /dev/null +++ b/tests/examples/head-normal-form.out @@ -0,0 +1 @@ +f ((\x . x x) (\x . x x)) diff --git a/tests/examples/normal-form.lam b/tests/examples/normal-form.lam new file mode 100644 index 0000000..36afd00 --- /dev/null +++ b/tests/examples/normal-form.lam @@ -0,0 +1,6 @@ +-- normal form Y +-- weak normal form Y +-- head normal form Y +-- weak head normal form Y + +f (\x . x x) (\x . x x) diff --git a/tests/examples/normal-form.out b/tests/examples/normal-form.out new file mode 100644 index 0000000..07dc4b3 --- /dev/null +++ b/tests/examples/normal-form.out @@ -0,0 +1 @@ +f (\x . x x) (\x . x x) diff --git a/tests/examples/nums-env.lam b/tests/examples/nums-env.lam new file mode 100644 index 0000000..c8e8a7e --- /dev/null +++ b/tests/examples/nums-env.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + insert_your_expression_here + +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-env.out b/tests/examples/nums-env.out new file mode 100644 index 0000000..41b34f0 --- /dev/null +++ b/tests/examples/nums-env.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . insert_your_expression_here) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-isZero-one.lam b/tests/examples/nums-isZero-one.lam new file mode 100644 index 0000000..67e54dd --- /dev/null +++ b/tests/examples/nums-isZero-one.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + isZero one + -- Should evaluate to false, i.e., \ x y . y +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-isZero-one.out b/tests/examples/nums-isZero-one.out new file mode 100644 index 0000000..4d24c9e --- /dev/null +++ b/tests/examples/nums-isZero-one.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . isZero one) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-isZero-two.lam b/tests/examples/nums-isZero-two.lam new file mode 100644 index 0000000..086bdc0 --- /dev/null +++ b/tests/examples/nums-isZero-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + isZero two + -- Should evaluate to false, i.e., \ x y . y +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-isZero-two.out b/tests/examples/nums-isZero-two.out new file mode 100644 index 0000000..b897fd1 --- /dev/null +++ b/tests/examples/nums-isZero-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . isZero two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-isZero-zero.lam b/tests/examples/nums-isZero-zero.lam new file mode 100644 index 0000000..4cf9dd3 --- /dev/null +++ b/tests/examples/nums-isZero-zero.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + isZero zero + -- Should evaluate to true, i.e., \ x y . x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-isZero-zero.out b/tests/examples/nums-isZero-zero.out new file mode 100644 index 0000000..88be213 --- /dev/null +++ b/tests/examples/nums-isZero-zero.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . isZero zero) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-minus-one-two.lam b/tests/examples/nums-minus-one-two.lam new file mode 100644 index 0000000..cd54d34 --- /dev/null +++ b/tests/examples/nums-minus-one-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + minus one two + -- Should evaluate to zero, i.e., \ f x . x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-minus-one-two.out b/tests/examples/nums-minus-one-two.out new file mode 100644 index 0000000..04b0c6a --- /dev/null +++ b/tests/examples/nums-minus-one-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . minus one two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-minus-three-two.lam b/tests/examples/nums-minus-three-two.lam new file mode 100644 index 0000000..e2fe489 --- /dev/null +++ b/tests/examples/nums-minus-three-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + minus three two + -- Should evaluate to one, i.e., \ f x . f x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-minus-three-two.out b/tests/examples/nums-minus-three-two.out new file mode 100644 index 0000000..e924284 --- /dev/null +++ b/tests/examples/nums-minus-three-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . minus three two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-mult-two-three.lam b/tests/examples/nums-mult-two-three.lam new file mode 100644 index 0000000..f8ea7ed --- /dev/null +++ b/tests/examples/nums-mult-two-three.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + mult two three + -- Should evaluate to six, i.e., \ f x . f (f (f (f (f (f x))))) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-mult-two-three.out b/tests/examples/nums-mult-two-three.out new file mode 100644 index 0000000..1390573 --- /dev/null +++ b/tests/examples/nums-mult-two-three.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . mult two three) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-plus-three-two.lam b/tests/examples/nums-plus-three-two.lam new file mode 100644 index 0000000..70839a5 --- /dev/null +++ b/tests/examples/nums-plus-three-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + plus three two + -- Should evaluate to five, i.e., (\ f x . f (f (f (f (f x))))) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-plus-three-two.out b/tests/examples/nums-plus-three-two.out new file mode 100644 index 0000000..67ccb01 --- /dev/null +++ b/tests/examples/nums-plus-three-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . plus three two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-pred-four.lam b/tests/examples/nums-pred-four.lam new file mode 100644 index 0000000..02602c0 --- /dev/null +++ b/tests/examples/nums-pred-four.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + pred four + -- Should evaluate to three, i.e., \ f x . f (f (f x)) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-pred-four.out b/tests/examples/nums-pred-four.out new file mode 100644 index 0000000..f57d3e0 --- /dev/null +++ b/tests/examples/nums-pred-four.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred four) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-pred-one.lam b/tests/examples/nums-pred-one.lam new file mode 100644 index 0000000..413046d --- /dev/null +++ b/tests/examples/nums-pred-one.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + pred one + -- Should evaluate to zero, i.e., \ f x . x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-pred-one.out b/tests/examples/nums-pred-one.out new file mode 100644 index 0000000..5e72285 --- /dev/null +++ b/tests/examples/nums-pred-one.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred one) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-pred-two.lam b/tests/examples/nums-pred-two.lam new file mode 100644 index 0000000..d003d33 --- /dev/null +++ b/tests/examples/nums-pred-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + pred two + -- Should evaluate to zero, i.e., \ f x . f x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-pred-two.out b/tests/examples/nums-pred-two.out new file mode 100644 index 0000000..7c032fd --- /dev/null +++ b/tests/examples/nums-pred-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-pred-zero.lam b/tests/examples/nums-pred-zero.lam new file mode 100644 index 0000000..dd0a17b --- /dev/null +++ b/tests/examples/nums-pred-zero.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + pred zero + -- Should evaluate to zero, i.e., \ f x . x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-pred-zero.out b/tests/examples/nums-pred-zero.out new file mode 100644 index 0000000..7f3455b --- /dev/null +++ b/tests/examples/nums-pred-zero.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred zero) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-succ-two.lam b/tests/examples/nums-succ-two.lam new file mode 100644 index 0000000..89f5761 --- /dev/null +++ b/tests/examples/nums-succ-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + succ two + -- Should evaluate to three, i.e., \ f x . f (f (f x)) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-succ-two.out b/tests/examples/nums-succ-two.out new file mode 100644 index 0000000..3973621 --- /dev/null +++ b/tests/examples/nums-succ-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . succ two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-succ-zero.lam b/tests/examples/nums-succ-zero.lam new file mode 100644 index 0000000..28b0d8c --- /dev/null +++ b/tests/examples/nums-succ-zero.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + succ zero + -- Should evaluate to one, i.e., (\ f x . f x) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-succ-zero.out b/tests/examples/nums-succ-zero.out new file mode 100644 index 0000000..716960a --- /dev/null +++ b/tests/examples/nums-succ-zero.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . succ zero) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/omega-arg.lam b/tests/examples/omega-arg.lam new file mode 100644 index 0000000..8a7138a --- /dev/null +++ b/tests/examples/omega-arg.lam @@ -0,0 +1 @@ +(\a x . x) ((\z . z z) (\z . z z)) diff --git a/tests/examples/omega-arg.out b/tests/examples/omega-arg.out new file mode 100644 index 0000000..33d80d7 --- /dev/null +++ b/tests/examples/omega-arg.out @@ -0,0 +1 @@ +(\a . \x . x) ((\z . z z) (\z . z z)) diff --git a/tests/examples/omega.lam b/tests/examples/omega.lam new file mode 100644 index 0000000..29ed0ff --- /dev/null +++ b/tests/examples/omega.lam @@ -0,0 +1,6 @@ +-- normal form N +-- weak normal form N +-- head normal form N +-- weak head normal form N + +(\x . x x) (\x . x x) diff --git a/tests/examples/omega.out b/tests/examples/omega.out new file mode 100644 index 0000000..f7f18c2 --- /dev/null +++ b/tests/examples/omega.out @@ -0,0 +1 @@ +(\x . x x) (\x . x x) diff --git a/tests/examples/pairs-fst-snd.lam b/tests/examples/pairs-fst-snd.lam new file mode 100644 index 0000000..19791ad --- /dev/null +++ b/tests/examples/pairs-fst-snd.lam @@ -0,0 +1,15 @@ +(\ pair fst snd . + + fst (snd (pair (pair a b) (pair c d))) + + -- Should reduce to c +) + +-- pair +(\ x y f . f x y) + +-- fst +(\ p . p (\ x y . x)) + +-- snd +(\ p . p (\ x y . y)) diff --git a/tests/examples/pairs-fst-snd.out b/tests/examples/pairs-fst-snd.out new file mode 100644 index 0000000..cb53fb8 --- /dev/null +++ b/tests/examples/pairs-fst-snd.out @@ -0,0 +1 @@ +(\pair . \fst . \snd . fst (snd (pair (pair a b) (pair c d)))) (\x . \y . \f . f x y) (\p . p (\x . \y . x)) (\p . p (\x . \y . y)) diff --git a/tests/examples/pairs-fst.lam b/tests/examples/pairs-fst.lam new file mode 100644 index 0000000..5ee215a --- /dev/null +++ b/tests/examples/pairs-fst.lam @@ -0,0 +1,15 @@ +(\ pair fst snd . + + fst (pair a b) + + -- Should reduce to a +) + +-- pair +(\ x y f . f x y) + +-- fst +(\ p . p (\ x y . x)) + +-- snd +(\ p . p (\ x y . y)) diff --git a/tests/examples/pairs-fst.out b/tests/examples/pairs-fst.out new file mode 100644 index 0000000..c11f799 --- /dev/null +++ b/tests/examples/pairs-fst.out @@ -0,0 +1 @@ +(\pair . \fst . \snd . fst (pair a b)) (\x . \y . \f . f x y) (\p . p (\x . \y . x)) (\p . p (\x . \y . y)) diff --git a/tests/examples/pairs-snd.lam b/tests/examples/pairs-snd.lam new file mode 100644 index 0000000..b2f0a75 --- /dev/null +++ b/tests/examples/pairs-snd.lam @@ -0,0 +1,15 @@ +(\ pair fst snd . + + snd (pair a b) + + -- Should reduce to b +) + +-- pair +(\ x y f . f x y) + +-- fst +(\ p . p (\ x y . x)) + +-- snd +(\ p . p (\ x y . y)) diff --git a/tests/examples/pairs-snd.out b/tests/examples/pairs-snd.out new file mode 100644 index 0000000..ebfb43b --- /dev/null +++ b/tests/examples/pairs-snd.out @@ -0,0 +1 @@ +(\pair . \fst . \snd . snd (pair a b)) (\x . \y . \f . f x y) (\p . p (\x . \y . x)) (\p . p (\x . \y . y)) diff --git a/tests/examples/weak-head-normal-form.lam b/tests/examples/weak-head-normal-form.lam new file mode 100644 index 0000000..6b8c0e0 --- /dev/null +++ b/tests/examples/weak-head-normal-form.lam @@ -0,0 +1,6 @@ +-- normal form N +-- weak normal form Y +-- head normal form Y +-- weak head normal form Y + +\f . f ((\x . x x) (\x . x x)) diff --git a/tests/examples/weak-head-normal-form.out b/tests/examples/weak-head-normal-form.out new file mode 100644 index 0000000..6b4a7fc --- /dev/null +++ b/tests/examples/weak-head-normal-form.out @@ -0,0 +1 @@ +\f . f ((\x . x x) (\x . x x)) diff --git a/tests/examples/weak-normal-form.lam b/tests/examples/weak-normal-form.lam new file mode 100644 index 0000000..8d80a75 --- /dev/null +++ b/tests/examples/weak-normal-form.lam @@ -0,0 +1,6 @@ +-- normal form N +-- weak normal form Y +-- head normal form N +-- weak head normal form Y + +\f . (\x . x x) (\x . x x) diff --git a/tests/examples/weak-normal-form.out b/tests/examples/weak-normal-form.out new file mode 100644 index 0000000..54963a1 --- /dev/null +++ b/tests/examples/weak-normal-form.out @@ -0,0 +1 @@ +\f . (\x . x x) (\x . x x) diff --git a/tests/examples/y.lam b/tests/examples/y.lam new file mode 100644 index 0000000..996802d --- /dev/null +++ b/tests/examples/y.lam @@ -0,0 +1,7 @@ +-- normal form N +-- weak normal form Y +-- head normal form N +-- weak head normal form Y + +-- Y combinator +\ f . (\ x . f (x x)) (\ x . f (x x)) diff --git a/tests/examples/y.out b/tests/examples/y.out new file mode 100644 index 0000000..afe09a5 --- /dev/null +++ b/tests/examples/y.out @@ -0,0 +1 @@ +\f . (\x . f (x x)) (\x . f (x x)) |