Cleanup in w, added names, uncommented test for low special_k

diff --git a/ocaml/problems/w b/ocaml/problems/w
index c10a3f6b1e72a4f19e2e3b8bc5b305edd10601a7..e3a5dd234e53bdfae17ffd61cd3dc8fe66160af6 100644 (file)
--- a/ocaml/problems/w
+++ b/ocaml/problems/w
@@ -1,60 +1,44 @@
-$?\r
+$? w1\r
 D x y\r
 C x BOMB\r
 \r
-$?\r
+$? w2\r
 D x y z\r
 C x BOMB z\r
   x y y\r
 \r
-$!\r
- (* DISPLAY PROBLEM (main) - measure=965\r
-    Discriminating sets (deltas):\r
-    0 <> 1 <> 2 <> 3 <> 4\r
- *)(* DIVERGENT  *)\r
+$! w3\r
 D b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (k. b c d (l. c (l k)) (b c (l. e e) (b c d (l. e l) (e e (b (l. m. b)) d (l. d))) (l. c)))\r
-#   (* CONVERGENT *) [\r
 C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. e e) (k. g (l. g (m. b c)) (l. i (f g)))\r
 C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h))) (b c (k. c (e h)))\r
 C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. e e)\r
 C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h)))\r
 C b (k. l. b) (e f) (b c d) (e e (b (k. l. b)) d) (e (k. l. b c) (k. l. b k) (b c)) d (e e (e e) (d (k. f)) (b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))))) (e e (b (k. l. b)) (b (k. l. b) (e f) (b c d)) (e e (b (k. l. b)) d (k. d) (b (k. l. b))) (k. b c k (l. e l) (e e (b (l. m. b)) k (l. k)) (f g (c (e h))) (k b (l. b) (f g (e f))) (c (e h))) (k. i (f g) (l. l)))\r
-#  ] (* NUMERIC    *) [\r
 N b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. l. c (l k)) Z\r
   b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) Z\r
   b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) Z\r
   b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) Z\r
   b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) Z\r
-#  ];\r
 \r
-$!\r
- problem_of\r
- (* DISPLAY PROBLEM (main) - measure=561\r
-    Discriminating sets (deltas):\r
-    0 <> 1 <> 2 <> 3 <> 4\r
- *)(* DIVERGENT  *)\r
+$! w4\r
 D b (c b) (k. d) (e f (k. e) (k. b) (f d)) (e f (k. g k) d) (k. c k (c k g))\r
-#   (* CONVERGENT *) [\r
 C c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g) (e f (k. k (g e) h) b (e (k. g) (h c (g c) f)))\r
   e f (k. k) (k. l. c b) (k. l. l (k b) g) (k. e f (l. l)) (h c (c (k. l. l b k) (k. l. d) (e f (k. k) (g e))) (k. g e (g e))) (k. g (l. e f g) (l. h c) (g (l. e f g) (l. h c)))\r
   e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (k. l. g l (g l) (m. c b))\r
   c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g)\r
   e f (k. k) (g e) (e f (k. e)) (e f (k. e)) (h c (b (g e) h (k. c (l. m. m k l))))\r
-# ] (* NUMERIC    *) [\r
 N c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. i) Z\r
   e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (h (c b) g i) Z\r
   e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) Z\r
   e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) Z\r
   g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f Z\r
-#  ]\r
- ];\r
 \r
-# This fails, but shouldnt: commented out\r
-# $!\r
- D x PAC PAC PAC PAC PAC a\r
- C x PAC PAC PAC PAC PAC b\r
- N y x\r
-   y z\r
+# This was failing because special_k was too low\r
+$! low special_k\r
+D x PAC PAC PAC PAC PAC a\r
+C x PAC PAC PAC PAC PAC b\r
+N y x\r
+  y z\r
 # In general:\r
   DIV x (n times PAC) a\r
   CON x (n times PAC) b\r
@@ -64,13 +48,13 @@ N c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e
   y must apply n+m+1 variables\r
   Thus special_k must be >=n+m+1\r
 \r
-# todo:\r
-  (* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *)\r
+$! eatable right away\r
+D y y\r
+C x (_. y y)\r
 \r
 \r
-#$! new failing problem\r
-# it is backtracking, but it shouldn't\r
-# why? well, D occurs in some C's\r
+#$? should raise a parsing error\r
+# (div occurs as subterm at top-level in conv and ps)\r
  D (a b)\r
  C ((((((((a (v (y. y))) (v c)) ((x ((a (v (y. y))) (v c))) y)) (((a (v (y. y))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))) (((v (x. (v c))) (v (x. (v c)))) (((((z z) b) (c. a)) (z z)) (b c))))) (a. ((((z z) b)(c. a)) (z z)))) (y. (z z))) (((a (v (y. y))) w) (z. x))) (w. (z. (v (y. y)))))\r
  C ((((((((z z) b) (c. a)) (z z)) ((v (y. y)) a)) (v (y. y))) ((((a (v (y. y))) (v c)) (z z)) ((a (v (y. y))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))))) (z. ((v (y. y)) a)))\r