]> matita.cs.unibo.it Git - fireball-separation.git/blob - ocaml/test.ml
Tentative commit: tactics dropped and clean-up
[fireball-separation.git] / ocaml / test.ml
1 open Lambda4;;
2
3 let acaso l =
4     let n = Random.int (List.length l) in
5     List.nth l n
6 ;;
7
8 let acaso2 l1 l2 =
9   let n1 = List.length l1 in
10   let n = Random.int (n1 + List.length l2) in
11   if n >= n1 then List.nth l2 (n - n1) else List.nth l1 n
12 ;;
13
14 let rec take l n =
15   if n = 0 then []
16   else match l with
17   | [] -> []
18   | x::xs -> x :: (take xs (n-1))
19 ;;
20
21 let test3 n vars =
22   let rec aux n inerts lams =
23     if n = 0 then take (Util.sort_uniq inerts) 5
24     else let inerts, lams = if Random.int 2 = 0
25       then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams
26       else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams
27     in aux (n-1) inerts lams
28   in aux (2*n) vars []
29 ;;
30
31 let test4 n vars =
32   let rec take' l n =
33     if n = 0 then [], []
34     else match l with
35     | [] -> [], []
36     | [_] -> assert false
37     | x1::x2::xs -> let a, b = take' xs (n-1) in x1::a,x2::b in
38   let rec aux n inerts lams =
39     if n = 0 then List.hd inerts, take' (Util.sort_uniq (List.tl inerts)) 5
40     else let inerts, lams = if Random.int 2 = 0
41       then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams
42       else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams
43     in aux (n-1) inerts lams
44   in aux (2*n) vars []
45 ;;
46
47
48 let rec repeat f n =
49   prerr_endline "\n*************************** NEW TEST ***************************";
50   f () ;
51   if n > 0 then repeat f (n-1)
52 ;;
53
54 (* let call_main3 tms =
55   let _ = (
56   List.iter prerr_endline tms; prerr_newline ();
57   ) in Lambda3.main [Lambda3.magic tms ["*"]]
58 ;; *)
59 let call_main4 div convs nums =
60   let _ = (
61   (match div with Some div -> prerr_endline ("DIV: " ^ div) | None -> ());
62   print_endline "CONV:"; List.iter prerr_endline convs;
63   print_endline "NUMS:"; List.iter prerr_endline nums;
64   prerr_newline ();
65   ) in Lambda4.solve (Lambda4.problem_of div convs nums)
66 ;;
67
68 let main =
69   Random.self_init ();
70   let num = 100 in
71   let complex = 200 in
72   let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in
73
74   (* let open Parser in *)
75
76   (* if three then repeat (fun _ ->
77     let tms = test3 complex vars in
78     call_main3 tms
79   ) num
80   else *)
81   repeat (fun _ ->
82     let div, (conv, nums) = test4 complex vars in
83     call_main4 (Some div) conv nums
84   ) num
85   ;
86
87   prerr_endline "\n---- ALL TESTS COMPLETED ----"
88 ;;