From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 24 Jul 2017 14:17:53 +0000 (+0200)
Subject: Test --with-pac fails if unseparable+uncomplete
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=46f57e51b457e7f1c225eb0467c1b0b286d11af1;p=fireball-separation.git

Test --with-pac fails if unseparable+uncomplete
---

diff --git a/ocaml/test.ml b/ocaml/test.ml
index 32d60aa..629bf89 100644
--- a/ocaml/test.ml
+++ b/ocaml/test.ml
@@ -68,15 +68,18 @@ let rec repeat f n =
   if n > 0 then repeat f (n-1)
 ;;
 
-let solve div convs nums =
+let solve div convs nums label =
  let p = String.concat "\n" (
-  "$! randomly generated test" ::
+  ("$! randomly generated test " ^ label) ::
   ("D " ^ div) ::
   List.map ((^) "C ") convs @
   List.map (fun s -> "N " ^ s ^ " Z") nums
  ) in
  prerr_endline p;
- (Lambda4.solve ++ Lambda4.problem_of ++ Parser.problem_of_string) p
+ match (Lambda4.solve ++ Lambda4.problem_of ++ Parser.problem_of_string) p with
+ | `Uncomplete, `Unseparable _ ->
+    failwith ("Test4.solve: unseparable, and cannot tell if that's right or not.")
+ | _ -> ()
 ;;
 
 let main =
@@ -86,20 +89,20 @@ let main =
  (* if flag --with-pac active, then more general tests *)
  let with_pac = List.mem "--with-pac" (Array.to_list Sys.argv) in
 
- let f = if with_pac
+ let label, f = if with_pac
   then (
    let complex = 10 in
    let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in
-   fun () -> gen_pac complex vars
+   "with pacmans & bombs", fun () -> gen_pac complex vars
   ) else (
    let complex = 200 in
    let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in
-   fun () -> gen complex vars
+   "", fun () -> gen complex vars
    ) in
 
  repeat (fun _ ->
    let div, (conv, nums) = f () in
-   solve div conv nums
+   solve div conv nums label
  ) num;
 
  prerr_endline "\n---- ALL TESTS COMPLETED ----"