X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fproblems.ml;h=eda359ae00d08dc3b92c19eba633c44d1bec1ee1;hb=7051416c234181eaf79dedfd18005cdf0a3e0863;hp=3505605e674050f8d8bc4b55de565159399776e5;hpb=f7a60345135a4032bf63a7dc650bcc9fe30aa30a;p=fireball-separation.git

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 3505605..eda359a 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -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 (fst 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 (fst 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 *)
@@ -44,6 +34,6 @@ let assert_depends x =
 if Array.length Sys.argv = 1
  then failwith "no command line args. Please use e.g. ./a.out problems/*"
 else Array.iteri (fun i filename -> if i > 0 then
- List.iter (assert_depends ++ Lambda4.tmp) (Parser.from_file filename)
+ List.iter (assert_depends ++ problem_of) (Parser.from_file filename)
  ) Sys.argv
 ;;