From 3ba5ecfc8372d4c9f380bad5cdf7387f2bbcea6a Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 31 May 2018 21:11:29 +0200 Subject: [PATCH] Simpler tests in simple_test.ml + Added diverging tests in simple.1 --- ocaml/problems/simple.1 | 11 +++++++++++ ocaml/simple.ml | 1 + ocaml/simple_test.ml | 4 ++-- 3 files changed, 14 insertions(+), 2 deletions(-) create mode 100644 ocaml/problems/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 -- 2.39.2