Simpler tests in simple_test.ml + Added diverging tests in simple.1

diff --git a/ocaml/problems/simple.1 b/ocaml/problems/simple.1
new file mode 100644 (file)
index 0000000..d3e9213
--- /dev/null
+++ b/ocaml/problems/simple.1
@@ -0,0 +1,11 @@
+$! simple: C diverges\r
+D v0 (x. x) (v1 (x. y. y v2)) (x. y. v1 v3)\r
+C v4 (v1 v5 v2 v1 (x. v1 x v2) (v0 (v1 v3) (v1 v5 v2) (v6 v2 (x. y. v0 (v1 v3)) (v3 v2 (x. v1 v3))))) (v1 (x. y. y v2) (v5 v5) (x. v5) (v0 (v1 v3) (v1 v5 v2)) (x. y. v0 (v1 v3))) (v6 v2 (x. y. v0 (v1 v3)) (v3 v2 (x. v1 v3)) (v7 (v0 (v1 v3) (v1 v5 v2))) (v1 v3)) (v1 (x. y. y v2) (v5 v5) (x. v5) (x. v8) (x. x v2) (x. v1 v5 v2)) (v1 (x. y. y v2) (v5 v5) (x. v5) (x. v8) (x. x v2) (x. v5) (x. y. z. v8))\r
+\r
+$! simple: C diverges in pure (1)\r
+D v0 v1 (x. y. z. v2 (y (v3 v4))) (v5 (x. v6))\r
+C v7 (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (x. v5 v8 v0) (x. v8 (v3 v4))) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (v5 v8 v0) (x. x (y. v2 (v8 (y v4))) (x (y. v2 (v8 (y v4)))))) (v8 (v3 v4) (v5 v8 (x. y. v6) (v8 (v3 v4)) (v5 v8 (x. y. v6) (v8 (v3 v4))) (v5 (x. v6 (v6 (y. v2 (x (y v4))))))) (v5 v8 (x. y. v6) (v8 (v3 v4)) (v5 v8 (x. y. v6) (v8 (v3 v4))) (v5 (x. v6 (v6 (y. v2 (x (y v4)))))) (v8 (v3 v4) (v5 v8 (x. y. v6) (v8 (v3 v4)) (v5 v8 (x. y. v6) (v8 (v3 v4))) (v5 (x. v6 (v6 (y. v2 (x (y v4))))))))) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (v5 v8 v0)) (v0 v1 (v5 v8 (x. y. v6)) (v8 (v3 v4)) (v5 v8)) (x. v6 (y. v2 (v8 (y v4))) (v8 (v3 v4)) (x (v0 x (v5 v8 (y. z. v6)) (v8 (v3 v4)))))) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (x. v5 v8 v0) (x. v8 (v3 v4)) v4) (v0 v1 (v5 v8 (x. y. v6)) (x. v2) (x. x (y. v1)) (x. v5 v8 v0) (x. v8 (v3 v4)) (x. y. v6))\r
+\r
+$! simple: C diverges in pure (2)\r
+D v0 (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1))) (x. v0 v1 v6 (v7 (v2 v5) (v0 v2)) (y. x v4 (v0 v1)))\r
+C v8 (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1))) (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v2 v5 (x. v0 v1 (v0 x) (v3 v4) v0 v1 v4))) (v0 v1 (v0 v2) (v3 v4) v0 (v3 v4) (x. y. v0) (v0 v1 (v0 v2) (v3 v4)) (v2 v5 (v0 v1 (v0 v2) (v3 v4) v0 v1 (v3 v4 (v0 v1)) (v2 (v0 v2 (v0 v1 (v0 v2)) v2))))) (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1)) (x. y. z. v0 v1 (v0 v2) (v3 z))) (v0 v1 (v0 v2) (v3 v4) v0 (v0 v1 (v0 v2) (v3 v4)) (x. v0 v2 (v0 v1 (v0 v2))) (v5 (v0 v1 (v0 v2) (v3 v4) v0 v1)) (x. y. z. v0 v1 (v0 v2) (v3 z)) (v0 v1 (v0 v2) (v3 v4) v0 v1 (v3 v4 (v0 v1)) (v2 (v0 v2 (v0 v1 (v0 v2)) v2))))\r

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index b5a508691ea31dd83a8c930017df85d81f687b73..efa5c25d88fd47912ed7b5d656074a1c9bc685f9 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -117,6 +117,7 @@ let rec no_leading_lambdas hd_var j = function
  | V n -> if n = hd_var then j else 0\r
  | B | C _ -> 0\r
 ;;\r
+\r
 let rec subst level delift sub =\r
  function\r
  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r

diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml
index d5cb66b6b8abc11173b9f4129a352cf6c1b68a4a..8bdefdcb426939e42a192c7e7e0c079c0a9c6863 100644 (file)
--- a/ocaml/simple_test.ml
+++ b/ocaml/simple_test.ml
@@ -38,8 +38,8 @@ let rec repeat f n =
 let main =
   Random.self_init ();
   let num = 100 in
-  let complex = 200 in
-  let no_bound_vars = 20 in
+  let complex = 100 in
+  let no_bound_vars = 10 in
   let vars = Array.to_list
    (Array.init no_bound_vars (fun x -> "x" ^ string_of_int x)) in