Changed logic of entrypoint in Lambda4

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

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index b49cf7733578832c022cc994b87ccc6599660a3e..55ed9e934c82f1efd66484052ce989e58e0836d0 100644 (file)
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -1,9 +1,29 @@
 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)"] []);; *)
 
 (* 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"];
@@ -100,8 +120,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 *)
 
@@ -260,9 +279,9 @@ solve_many (List.map ((|>) ()) [
  o1; o2; o3; o4; o5; o6
 ]);;
 
-should_fail(fun () -> problem_of None ["BOT"] []);;
-should_fail(fun () -> problem_of (Some"x y") ["x BOMB"] []);;
-should_fail(fun () -> problem_of (Some"x y z") ["x BOMB z"; "x y y"] []);;
+assert_unseparable(problem_of None ["BOT"] []);;
+assert_unseparable(problem_of (Some"x y") ["x BOMB"] []);;
+assert_unseparable(problem_of (Some"x y z") ["x BOMB z"; "x y y"] []);;
 
 solve_many [
  problem_of