]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Code clean-up
authoracondolu <andrea.condoluci@unibo.it>
Sat, 15 Jul 2017 14:41:53 +0000 (16:41 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 09:09:01 +0000 (11:09 +0200)
(cherry picked from commit 5d8249a042beefbe21bfeed48619ed1917ebbcb7)

ocaml/problems.ml

index 5f86177db4e18de320e94239a4f80d4fcf1744c0..9ff47787f995e34bf7222d6d495dc7c1ba7a9da9 100644 (file)
@@ -17,25 +17,15 @@ 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.")
-;;
-
+(* assert_depends solves the problem, and checks if the result was expected *)
 let assert_depends x =
- let c = String.sub (Lambda4.label_of_problem x) 0 1 in
- if c = "!" then assert_separable x
-  else if c = "?" then assert_unseparable x
-   else (solve x; ())
+ let c = String.sub (label_of_problem x) 0 1 in
+ match solve x with
+ | `Unseparable s when c = "!" ->
+    failwith ("assert_depends: unseparable because: " ^ s ^ ".")
+ | `Separable _  when c = "?" ->
+    failwith ("assert_depends: separable.")
+ | _ -> ()
 ;;
 
 (* TODO *)