From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 7 Jun 2018 09:13:09 +0000 (+0200)
Subject: Added tests with constants
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f3bb4936d8b5aa478f16bb0e9fefc8b40a9af58d;p=fireball-separation.git

Added tests with constants

- Enabled with flag --with-const
- Stores failing problems in problems/ folder
---

diff --git a/ocaml/simple.mli b/ocaml/simple.mli
index bdc6328..fba2470 100644
--- a/ocaml/simple.mli
+++ b/ocaml/simple.mli
@@ -1,4 +1,5 @@
 type problem
+exception Fail of int * string
 val solve : problem -> unit
 val problem_of :
   string * Num.i_var option * Num.i_n_var list * Num.i_n_var list *
diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml
index 49ea28f..3ec4bb7 100644
--- a/ocaml/simple_test.ml
+++ b/ocaml/simple_test.ml
@@ -1,6 +1,10 @@
 open Simple;;
 open Util;;
 
+let with_const =
+ List.mem "--with-const" (Array.to_list Sys.argv)
+ ;;
+
 let acaso l =
     let n = Random.int (List.length l) in
     List.nth l n
@@ -24,8 +28,9 @@ let gen n vars =
     else let inerts, lams = if Random.int 2 = 0
       then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams
       else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams
-    in aux (n-1) inerts lams
-  in aux (2*n) vars []
+    in aux (n-1) inerts lams in
+  let inerts = if with_const then "C" :: vars else vars in
+  aux (2*n) inerts []
 ;;
 
 
@@ -43,13 +48,28 @@ let main =
   let vars = Array.to_list
    (Array.init no_bound_vars (fun x -> "x" ^ string_of_int x)) in
 
+  let file = Filename.temp_file ~temp_dir:"./problems/" "simple.constants.auto." "" in
+  let oc = open_out file in
+  print_endline ("\n\n---- <TESTS> " ^ file) ;
+
   repeat (fun _ ->
     let div, convs = gen complex vars in
-    let str = "$ random simple test \nD " ^ div ^ String.concat "\nC " convs ^ "\n" in
+    let str = " \nD " ^ div ^ String.concat "\nC " convs ^ "\n" in
     print_endline str;
-    let open Simple in
-    (solve ++ problem_of ++ Parser.problem_of_string) str
+    try
+     (solve ++ problem_of ++ Parser.problem_of_string) ("$" ^ str)
+    with Simple.Fail _ as e ->
+     let str = "$ failing test problem \n# Failed because: " ^ Printexc.to_string e ^ str in
+     Printf.fprintf oc "%s\n" str
   ) num ;
 
-  print_endline "\n---- ALL TESTS COMPLETED ----"
+  close_out oc;
+  print_endline ("\n\n---- </TESTS> " ^ file);
+  let filesize filename =
+    let ic = open_in filename in
+    let size = in_channel_length ic in
+    close_in ic ; size in
+  if filesize file = 0
+   then (print_endline "---- All tests succeeded."; Sys.remove file )
+   else (print_endline ("---- Not all tests succeeded. See " ^ file))
 ;;