Updated simple with current parser

[fireball-separation.git] / ocaml / problems / simple.0

diff --git a/ocaml/problems/simple.0 b/ocaml/problems/simple.0
new file mode 100644 (file)
index 0000000..4942099
--- /dev/null
+++ b/ocaml/problems/simple.0
@@ -0,0 +1,46 @@
+$ simple.0/0\r
+D x x\r
+C x y\r
+C y y\r
+C y x\r
+\r
+$ simple.0/1\r
+D x y\r
+C x (_. x)\r
+C y z\r
+C y x\r
+\r
+$ simple.0/2\r
+D a (x. x b) (x. x c)\r
+C a (x. b b) @\r
+C a @ c\r
+C a (x. x x) a\r
+C a (a a a) (a c c)\r
+\r
+$ simple.0/3\r
+D x (y. x y y)\r
+C x (y. x y x)\r
+\r
+$ simple.0/4\r
+D x a a a a\r
+C x b a a a\r
+C x a b a a\r
+C x a a b a\r
+C x a a a b\r
+\r
+$ simple.0/5\r
+# Controesempio ad usare un conto dei lambda che non considera le permutazioni\r
+D x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b\r
+C x a a a a (_. a) b b b\r
+C x a a a a (_. _. _. _. x. y. x y)\r
+\r
+$ simple.0/6\r
+# bug in eat that was erasing terms in convergent that then diverged\r
+D x y z\r
+C x @ @\r
+C z (y @ (y @))\r
+\r
+$ simple.0/7\r
+# bug in no_leading_lambdas where x in j-th position\r
+D v0 (v1 v2) (x. y. v0 v3 v4 v2)\r
+C v5 (v6 (x. v6) v7 v8 (x. v9) (x. v9 (v10 v10))) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y))) (v9 (x. v11) (v4 v8) (x. y. z. v12) (v4 v6 (x. v7 v11) v12) (x. x v8)) (v0 v3 v4 v9 (v7 v11) (v0 v3 v4 v2) v10) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y)) (v9 (x. v11) (v4 v8)))\r