CVS v1.0 tests

tests.in/001

@@ -0,0 +1,66 @@
+# Check parsing of maximally parenthesized expression
+X
+(X X)
+(X X X)
+(X (X X))
+(X ((X X) X))
+(X (X (X X)))
+((X (X X)) X)
+((X X)(X X))
+(((X   X ) X ) X )
+( X   ( ( X   X ) ( X   X ) ) )
+( X   ( ( X   ( X   X ) ) X ) )
+( X   ( ( ( X   X ) X ) X ) )
+( X   ( X   ( ( X   X ) X ) ) )
+( X   ( X   ( X   ( X   X ) ) ) )
+( ( X   ( X   X ) ) ( X   X ) )
+( ( X   ( X   ( X   X ) ) ) X )
+( ( X   ( ( X   X ) X ) ) X )
+( ( X   X ) ( ( X   X ) X ) )
+( ( X   X ) ( X   ( X   X ) ) )
+( ( ( X   ( X   X ) ) X ) X )
+( ( ( X   X ) ( X   X ) ) X )
+( ( ( X   X ) X ) ( X   X ) )
+( ( ( ( X   X ) X ) X ) X )
+( X   ( ( X   X ) ( X   ( X   X ) ) ) )
+( X   ( ( X   X ) ( ( X   X ) X ) ) )
+( X   ( ( X   ( ( X   X ) X ) ) X ) )
+( X   ( ( X   ( X   ( X   X ) ) ) X ) )
+( X   ( ( X   ( X   X ) ) ( X   X ) ) )
+( X   ( ( ( ( X   X ) X ) X ) X ) )
+( X   ( ( ( X   ( X   X ) ) X ) X ) )
+( X   ( ( ( X   X ) ( X   X ) ) X ) )
+( X   ( ( ( X   X ) X ) ( X   X ) ) )
+( X   ( X   ( ( X   X ) ( X   X ) ) ) )
+( X   ( X   ( ( X   ( X   X ) ) X ) ) )
+( X   ( X   ( ( ( X   X ) X ) X ) ) )
+( X   ( X   ( X   ( ( X   X ) X ) ) ) )
+( X   ( X   ( X   ( X   ( X   X ) ) ) ) )
+( ( X   ( X   X ) ) ( X   ( X   X ) ) )
+( ( X   ( X   X ) ) ( ( X   X ) X ) )
+( ( X   ( X   ( ( X   X ) X ) ) ) X )
+( ( X   ( X   ( X   ( X   X ) ) ) ) X )
+( ( X   ( X   ( X   X ) ) ) ( X   X ) )
+( ( X   ( ( ( X   X ) X ) X ) ) X )
+( ( X   ( ( X   ( X   X ) ) X ) ) X )
+( ( X   ( ( X   X ) ( X   X ) ) ) X )
+( ( X   ( ( X   X ) X ) ) ( X   X ) )
+( ( X   X ) ( ( X   X ) ( X   X ) ) )
+( ( X   X ) ( ( X   ( X   X ) ) X ) )
+( ( X   X ) ( ( ( X   X ) X ) X ) )
+( ( X   X ) ( X   ( ( X   X ) X ) ) )
+( ( X   X ) ( X   ( X   ( X   X ) ) ) )
+( ( ( X   ( X   X ) ) X ) ( X   X ) )
+( ( ( X   ( X   X ) ) ( X   X ) ) X )
+( ( ( X   ( X   ( X   X ) ) ) X ) X )
+( ( ( X   ( ( X   X ) X ) ) X ) X )
+( ( ( X   X ) ( X   X ) ) ( X   X ) )
+( ( ( X   X ) ( X   ( X   X ) ) ) X )
+( ( ( X   X ) ( ( X   X ) X ) ) X )
+( ( ( X   X ) X ) ( ( X   X ) X ) )
+( ( ( X   X ) X ) ( X   ( X   X ) ) )
+( ( ( ( X   ( X   X ) ) X ) X ) X )
+( ( ( ( X   X ) ( X   X ) ) X ) X )
+( ( ( ( X   X ) X ) ( X   X ) ) X )
+( ( ( ( X   X ) X ) X ) ( X   X ) )
+( ( ( ( ( X   X ) X ) X ) X ) X )

tests.in/002

@@ -0,0 +1,66 @@
+# Check parsing of minimally parenthesized expressions
+X
+X X
+X X X
+X (X X)
+X (X X X)
+X (X (X X))
+X (X X) X
+X X (X X)
+X X X X
+X (X X (X X))
+X (X (X X) X)
+X (X X X X)
+X (X (X X X))
+X (X (X (X X)))
+X (X X) (X X)
+X (X (X X)) X
+X (X X X) X
+X X (X X X)
+X X (X (X X))
+X (X X) X X
+X X (X X) X
+X X X (X X)
+X X X X X
+X (X X (X (X X)))
+X (X X (X X X))
+X (X (X X X) X)
+X (X (X (X X)) X)
+X (X (X X) (X X))
+X (X X X X X)
+X (X (X X) X X)
+X (X X (X X) X)
+X (X X X (X X))
+X (X (X X (X X)))
+X (X (X (X X) X))
+X (X (X X X X))
+X (X (X (X X X)))
+X (X (X (X (X X))))
+X (X X) (X (X X))
+X (X X) (X X X)
+X (X (X X X)) X
+X (X (X (X X))) X
+X (X (X X)) (X X)
+X (X X X X) X
+X (X (X X) X) X
+X (X X (X X)) X
+X (X X X) (X X)
+X X (X X (X X))
+X X (X (X X) X)
+X X (X X X X)
+X X (X (X X X))
+X X (X (X (X X)))
+X (X X) X (X X)
+X (X X) (X X) X
+X (X (X X)) X X
+X (X X X) X X
+X X (X X) (X X)
+X X (X (X X)) X
+X X (X X X) X
+X X X (X X X)
+X X X (X (X X))
+X (X X) X X X
+X X (X X) X X
+X X X (X X) X
+X X X X (X X)
+X X X X X X

tests.in/003

@@ -0,0 +1,3 @@
+# Single reduction rule
+rule: C 1 2 3 -> 1 3 2
+rules

tests.in/004

@@ -0,0 +1,6 @@
+# multiple reduction rules
+rule: B 1 2 3 -> 1 (2 3)
+rule: W 1 2 -> 1 2 2
+rule: C 1 2 3 -> 1 3 2
+rule: K 1 2 -> 1
+rules

tests.in/005

@@ -0,0 +1,11 @@
+rule: I 1 -> 1
+I x
+I x y z
+a I
+a I b
+I I
+I I I I I I I
+# This crashed an early version:
+I (a b)
+# As did this:
+I (I (I I))

tests.in/006

@@ -0,0 +1,22 @@
+# Test a few common combinators
+rule: M 1 -> 1 1
+rule: T 1 2 -> 2 1
+rule: K 1 2 -> 1
+M x
+T x y
+T T T
+T T T T
+T T T T T
+T x y  # -> y x
+T T x y  # -> y T x, as do all the T* x y below...
+T T T x y
+T T T T x y
+T T T T T x y
+K x y
+K K K
+K K K K
+K K K K K
+K K K K K K
+K K K K K K K K K K K K K K
+K (K (K (K (K (K (K (K (K (K (K (K (K K))))))))))))  # already in normal form
+M (K K K)

tests.in/007

@@ -0,0 +1,24 @@
+# SKI basis.
+rule: S 1 2 3 -> 1 3 (2 3)
+rule: K 1 2 -> 1
+rule: I 1 -> 1
+rules
+# Check whether each individual combinator "fires" with appropriate number
+# of arguments or not.
+S a
+S a b
+S a b c
+a S a b c
+I
+I a
+I a b
+a I a
+K
+K a
+K a b
+K a b c
+a K a b
+# Do they act right in unison?
+S (S K K) (S K K) x
+S I I x
+S (S K x) (S K x) y

tests.in/008

@@ -0,0 +1,7 @@
+# "Egotistical bird" or "Ogre" or "Eater"
+rule: F 1 2 -> 1 1
+rules
+F a b
+F F x
+F F a b c d e f g
+F F F F F F F F F F F F F F x

tests.in/009

@@ -0,0 +1,7 @@
+# test rule replacement
+rule: A 1 2 3 4 -> 1 3 (2 3 4)
+rule: M 1 2 3 -> 1 (2 3)
+rule: E 1 2 -> 2 1
+rules
+rule: A 1 2 3 4 -> 2 3 (1 3 4)
+rules

tests.in/010

@@ -0,0 +1,10 @@
+rule: S 1 2 3 -> 1 3 (2 3)
+length a b c
+length a b c d
+length a (b c) d
+length a (b c d)
+length a (b (c d))
+length a b (c d) e
+length S a b c
+length (reduce S a b c)
+length (reduce S (K a) (K b))

tests.in/011

@@ -0,0 +1,10 @@
+# Test size-of-tree function
+rule: I 1 -> 1
+size I
+size (K I)
+size (I K)
+size (S a b c)
+size (S (a b) c)
+size (S (a b c))
+size (S a (b c))
+size (reduce I I I I I I I)

tests.in/012

@@ -0,0 +1,43 @@
+# From Johannes Waldmann's thesis, "The Combinator S", section 5.4, "Monsters".
+# "A monster is a term with a normal form that is very large and many reduction
+# steps away.
+# Section 5.4.1. Ax Ay S are monsters.
+rule: S 1 2 3 -> 1 3 (2 3)
+def A0 S
+def T1 (S S)
+def A1 (T1 A0)
+def A2 (T1 A1)
+def A3 (T1 A2)
+def A4 (T1 A3)
+def A5 (T1 A4)
+def A6 (T1 A5)
+
+size (reduce A0 A0 S)
+size (reduce A0 A1 S)
+size (reduce A0 A2 S)
+size (reduce A1 A0 S)
+size (reduce A1 A1 S)
+size (reduce A1 A2 S)
+size (reduce A2 A0 S)
+size (reduce A2 A1 S)
+size (reduce A2 A2 S)
+size (reduce A3 A4 S)
+size (reduce A4 A3 S)
+size (reduce A4 A5 S)
+size (reduce A5 A4 S)
+size (reduce A5 A5 S)
+#size (reduce A6 A6 S) # 3843197 - takes forever
+
+# Section 5.4.10  Terms like S A1 Tn S S S are monsters
+# T1 defined above.
+def T2 (T1 T1)
+def T3 (T1 T2)
+def T4 (T1 T3)
+def T5 (T1 T4)
+def T6 (T1 T5)
+
+size reduce (S A1 T1 S S S)
+size reduce (S A1 T2 S S S)
+size reduce (S A1 T3 S S S)
+size reduce (S A1 T4 S S S)
+# size reduce (S A1 T5 S S S)

tests.in/013

@@ -0,0 +1,32 @@
+rule: C 1 2 3 -> 1 3 2
+rule: W 1 2  -> 1 2 2
+rules
+
+cycles on
+
+W C (W C) (W C) # period 2, pure - WC
+W (C C) (W (C C)) (W (C C)) # period 3, pure - WCC
+W (C (C C)) (W (C (C C))) (W (C (C C))) # period 4, pure - WCCC
+W (C (C (C C))) (W (C (C (C C)))) (W (C (C (C C)))) # period 5, pure - WCCCC
+
+W C (W  C)        (W (C C))          # period 5, pure - WCWCC
+W C (W  C)        (W (C (C C)))      # period 6, pure - WCWCCC
+W C (W (C C))     (W (C (C C)))      # period 7, pure - WCCWCCC
+W C (W C)         (W (C (C (C C))))  # period 7, pure - WCWCCCC
+W C (W (C C))     (W (C (C (C C))))  # period 8, pure - WCCWCCCC
+W C (W (C (C C))) (W (C (C (C C))))  # period 9, pure - WCCCWCCCC
+W C (W C)             (W (C (C (C (C C)))))  # period 8, pure - CWCWCCCC
+W C (W (C C))         (W (C (C (C (C C)))))  # period 9, pure - CWCCWCCCC
+W C (W (C (C C)))     (W (C (C (C (C C)))))  # period 10, pure - CWCCCWCCCC
+W C (W (C (C (C C)))) (W (C (C (C (C C)))))  # period 11, pure - CWCCCCWCCCC
+W C (W C)                 (W (C (C (C (C (C C))))))  # period 9, pure  - WCWCWCCCC
+W C (W (C C))             (W (C (C (C (C (C C))))))  # period 10, pure - WCCWCCCCCC
+W C (W (C (C C)))         (W (C (C (C (C (C C))))))  # period 11, pure - WCCCWCCCCCC
+W C (W (C (C (C C))))     (W (C (C (C (C (C C))))))  # period 12, pure - WCCCCWCCCCCC
+W C (W (C (C (C (C C))))) (W (C (C (C (C (C C))))))  # period 13, pure - WCCCCCWCCCCCC
+
+C W (C W) (C W) # period 2, pure - CW
+C (C C) W (C (C C) W) (C (C C) W) # period 4, pure - CCCW
+(C (C (C (C C)))) W ((C (C (C (C C)))) W) ((C (C (C (C C)))) W) # period 6, pure - CCCCCW
+(C (C (C (C (C (C C)))))) W ((C (C (C (C (C (C C)))))) W) ((C (C (C (C (C (C C)))))) W) # period 8, pure - CCCCCCCW
+

tests.in/014

@@ -0,0 +1,22 @@
+# This tests whether a duplicated term gets
+# copied, or if referencing of a common sub-expression
+# takes place.
+rule: I 1 -> 1
+rule: T 1 2 -> 2 1
+rule: W 1 2 -> 1 2 2
+rules
+trace on
+W T (I I I I)
+# Simplest case that left an expression
+# in non-normal form:
+W I (I I)
+# These expressions caused original cl to have trouble:
+rule: M 1 -> 1 1
+rule: K 1 2 -> 1
+M (M (K I))
+W I (W I (K I))
+rule: wx 1 2 3 -> 1 2 3 3
+wx a b c
+wx I I (W I (K I))
+rule: wy 1 2 3 -> 1 2 2 3
+wy I (W I (K I)) a

tests.in/015

@@ -0,0 +1,16 @@
+# Simple abcf bracket abstraction in, {S, K, I} basis.
+rule: I 1 -> 1
+rule: K 1 2 -> 1
+rule: S 1 2 3 -> 1 3 (2 3)
+abstraction: [_] *- -> K 1
+abstraction: [_] _ -> I
+abstraction: [_] *- _ -> 1
+abstraction: [_] * * -> S ([_]1) ([_]2)
+rules
+abstractions
+[x] U
+[x] x
+[x] U x
+[x] x U
+[x] (x m) x
+[x] (x x) (x x)

tests.in/016

@@ -0,0 +1,26 @@
+# Bracket abstraction in {B, W, C, K}
+rule: B 1 2 3 -> 1 (2 3)
+rule: C 1 2 3 -> 1 3 2
+rule: W 1 2 -> 1 2 2
+rule: K 1 2 -> 1
+rules
+
+# Grzegorzyk "G" algorithm, 
+abstraction: [_] *- -> K 1
+abstraction: [_] _ -> W K
+abstraction: [_] *- _ -> 1
+abstraction: [_] *- *+ -> B 1 ([_]2)
+abstraction: [_] *+ *- -> C ([_]1) 2
+abstraction: [_] * * -> W (B (C ([_]1)) ([_]2))
+abstractions
+
+[x] U
+[x] F N
+[x] x
+[x] U x
+[x] (m n) (x x)
+[x] (x x) (m n)
+[p,q,r] p (q r)
+[p,q,r] p r q
+[x] (a x) (b x)
+[p,q,r] p r (q r)

tests.in/017

@@ -0,0 +1,11 @@
+rule: I 1 -> 1
+rule: K 1 2 -> 1
+rule: S 1 2 3 -> 1 3 (2 3)
+abstraction: [_] *- -> K 1
+abstraction: [_] _ -> I
+abstraction: [_] *- _ -> 1
+abstraction: [_] * * -> S ([_]1) ([_]2)
+# Original problematic test case:
+(reduce ([x] ( x   ( x   ( x   ( a   a ) ) ) )) b) = (reduce ( ( b   ( b   ( b   ( a   a ) ) ) )) )
+# As simple as possible, this exhibits the problem:
+[x] (a a)