From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 31 May 2018 19:11:29 +0000 (+0200)
Subject: Simpler tests in simple_test.ml + Added diverging tests in simple.1
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3ba5ecfc8372d4c9f380bad5cdf7387f2bbcea6a;p=fireball-separation.git

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
index 0000000..d3e9213
--- /dev/null
+++ b/ocaml/problems/simple.1
@@ -0,0 +1,11 @@
+$! simple: C diverges
+D v0 (x. x) (v1 (x. y. y v2)) (x. y. v1 v3)
+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))
+
+$! simple: C diverges in pure (1)
+D v0 v1 (x. y. z. v2 (y (v3 v4))) (v5 (x. v6))
+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))
+
+$! simple: C diverges in pure (2)
+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)))
+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))))
diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index b5a5086..efa5c25 100644
--- 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
  | B | C _ -> 0
 ;;
+
 let rec subst level delift sub =
  function
  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)
diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml
index d5cb66b..8bdefdc 100644
--- 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