]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Test --with-pac fails if unseparable+uncomplete
authoracondolu <andrea.condoluci@unibo.it>
Mon, 24 Jul 2017 14:17:53 +0000 (16:17 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 24 Jul 2017 15:22:35 +0000 (17:22 +0200)
ocaml/test.ml

index 32d60aa62c054c28579858b1666e9f5962ab3b4c..629bf894ac082d9dfe564b0a31c349c3e7e6b812 100644 (file)
@@ -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 ----"