Changed logic of entrypoint in Lambda4

[fireball-separation.git] / ocaml / problems.ml

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 7cb068f72485f4e055d9578894ce10b438bcae16..e01a741339652a74cdcbe5497971090d70dc7bda 100644 (file)
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -1,9 +1,37 @@
 open Lambda4;;
-let solve_many = List.iter solve;;
+open Util;;
+
+let assert_separable x =
+ match solve x with
+ | `Separable _ -> ()
+ | `Unseparable s ->
+   failwith ("assert_separable: unseparable because: " ^ s ^ ".")
+;;
+
+let assert_unseparable x =
+ match solve x with
+ | `Unseparable _ -> ()
+ | `Separable _ ->
+   failwith ("assert_unseparable: separable.")
+;;
+
+let solve_many = List.iter assert_separable;;
+
+(* TODO *)
+(* div under a lambda in conv *)
+(* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *)
+
+assert_unseparable (problem_of None [] (* 32 *)
+ ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))";
+ "(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)";
+ "(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))";
+ "((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))";
+ "((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))"
+ ]);;
 
 (* p-series problems *)
-let f x = problem_of None [] x in
-solve_many (List.map f [
+let f x = assert_separable (problem_of None [] x) in
+List.iter f [
  (* 2 *) [ "x y"; "x z" ; "x (y z)"];
  (* 4 *) [ "x y"; "x (a. a x)" ; "y (y z)" ];
  (* 5 *) ["a (x. x a) b"; "b (x. x b) a"];
@@ -70,13 +98,6 @@ solve_many (List.map f [
   "(((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))";
   "(((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))";
   "((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"];
- (* 32 *)
-  ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))";
-  "(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)";
-  "(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))";
-  "((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))";
-  "((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))"
-  ];
  (* 33 *)
   (* Shows an error when the strategy that minimizes special_k is NOT used *)
   [ "((((((v (y. v)) (w. (c. y))) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b))) (((y (y (v w))) z) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)))) (b c)) (((v w) (z (a (c. y)))) ((y b) (b (z (a (c. y)))))))";
@@ -100,8 +121,7 @@ solve_many (List.map f [
   "(((((((z v) (y a)) (b a)) w) b) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y)))))) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) x))"];
  (* 37 *) (* issue with eta-equality of terms in ps *)
   ["x (a y) z"; "x (a z. y z) w"; "a c"];
-
-]);;
+];;
 
 (* q-series problems *)
 
@@ -130,13 +150,13 @@ let q4 () = problem_of
  ;;
 
 let q5 () = problem_of
- (Some"x")
- ["(y. x)"]
+ (Some"x x")
+ ["x"]
  ["x"]
  ;;
 
 let q6 () = problem_of
- (Some"x")
+ (Some"x x")
  ["(y. x z)"]
  ["y"]
  ;;