]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/testlibrary.ml
snapshot (notably: ported to mysql instead of dbi)
[helm.git] / helm / gTopLevel / testlibrary.ml
1
2 open Printf
3
4 let time_out = ref 5;;
5
6 Helm_registry.load_from "gTopLevel.conf.xml";;
7
8 let mqi_debug_fun s =
9  HelmLogger.log ~append_NL:true (`Msg (`T s))
10 let mqi_flags = []
11 let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun ()
12
13 let verbose = false
14
15 exception Failure of string
16 let fail msg = raise (Failure msg)
17
18 let uri_predicate = ref (BatchParser.constants_only ~prefix:"")
19
20 module DisambiguateCallbacks =
21  struct
22   let interactive_user_uri_choice
23    ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices =
24      List.filter !uri_predicate choices
25
26   let interactive_interpretation_choice =
27    let rec aux n =
28     function
29        [] -> []
30      | _::tl -> n::(aux (n+1) tl)
31    in
32     aux 0
33
34   let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title)
35  end
36
37 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
38
39 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
40
41 let test_uri uri =
42   let obj = CicEnvironment.get_obj uri in
43   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
44     Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
45   in
46   let ids_to_uris = Hashtbl.create 1023 in
47   let round_trip annterm =
48     debug_print "(1) acic -> ast";
49     let (ast, _) =
50       Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
51     in
52     let new_pp = BoxPp.pp_term ast in
53     debug_print ("ast:\n" ^ new_pp);
54     let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
55     debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
56     let res =
57      Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
58       DisambiguateTypes.Environment.empty in
59     List.iter
60      (fun (domain, _, term) ->
61        debug_print
62         ("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ;
63        debug_print ("term: " ^ CicPp.ppterm term)
64      ) res ;
65     List.length  res
66   in
67   match annobj with
68   | Cic.AConstant (_, _, _, None, ty, _) ->
69       debug_print "Cic.AConstant (ty)";
70       round_trip ty
71   | Cic.AConstant (_, _, _, Some bo, ty, _) ->
72 (*
73       debug_print "Cic.AConstant (bo)";
74       let n = round_trip bo in
75 *)
76       debug_print "Cic.AConstant (ty)";
77       round_trip ty (* + n *)
78   | Cic.AVariable (_, _, None, ty, _) ->
79       debug_print "Cic.AVariable (ty)";
80       round_trip ty
81   | Cic.AVariable (_, _, Some bo, ty, _) ->
82 (*
83       debug_print "Cic.AVariable (bo)";
84       let n = round_trip bo in
85 *)
86       debug_print "Cic.AVariable (ty)";
87       round_trip ty (* + n *)
88   | Cic.ACurrentProof (_, _, _, _, _, _, _) ->
89       assert false
90   | Cic.AInductiveDefinition _ ->
91       debug_print "AInductiveDefinition: boh ..." ;
92       assert false
93
94 exception TimeOut;;
95                                                                                 
96 ignore
97  (Sys.signal Sys.sigalrm
98    (Sys.Signal_handle
99      (fun _ ->
100        (* We do this in case that some "with _" intercepts the first exception *)
101        ignore (Unix.alarm 1) ;
102        raise TimeOut)))
103 ;;
104
105
106 let test_uri uri =
107   try
108    ignore (Unix.alarm !time_out) ;
109    if test_uri uri = 1 then `Ok else `Maybe
110   with
111   | TimeOut ->
112      (* We do this to clear the alarm set by the signal handler *)
113      ignore (Unix.alarm 0) ;
114      `TimeOut
115      (*
116   | exn ->
117       prerr_endline (sprintf "Top Level Uncaught Exception: %s"
118         (Printexc.to_string exn));
119       `Nok*)
120   | exn -> raise exn
121
122 let report (ok,nok,maybe,timeout) =
123   print_newline ();
124   print_endline "TestLibrary report";
125   print_endline "Succeeded URIs:";
126   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
127   print_endline "Failed URIs:";
128   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
129   print_endline "Multiple answers URIs:";
130   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
131   print_newline ();
132   print_endline ("URIs that timeout (" ^ string_of_int !time_out ^ "s):");
133   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout);
134   print_newline ()
135
136 let do_uri (ok, nok, maybe, timeout) uri =
137   let uri_str = UriManager.string_of_uri uri in
138   printf "Testing URI: %-55s %!" (uri_str ^ " ...");
139   match test_uri uri with
140   | `Ok ->
141       print_endline "\e[01;32m[   OK   ]\e[00m";
142       ok := uri_str :: !ok
143   | `Nok ->
144       print_endline "\e[01;31m[ FAILED ]\e[00m";
145       nok := uri_str :: !nok
146   | `Maybe ->
147       print_endline "\e[01;33m[  MANY  ]\e[00m";
148       maybe := uri_str :: !maybe
149   | `TimeOut ->
150       print_endline "\e[01;34m[TIMEOUT!]\e[00m";
151       timeout := uri_str :: !timeout
152
153 let do_file status fname =
154   try
155     let ic = open_in fname in
156     (try
157       while true do
158         let line = input_line ic in
159         try
160           let uri = UriManager.uri_of_string line in
161           do_uri status uri
162         with UriManager.IllFormedUri _ ->
163           printf "Error parsing URI '%s', ignoring it" line
164       done
165     with End_of_file ->
166      close_in ic)
167   with exn ->
168     printf "Error trying to access '%s' (%s), skipping the file\n%!"
169       fname (Printexc.to_string exn)
170
171 let _ =
172   HelmLogger.register_log_callback
173    (fun ?(append_NL = true) msg ->
174      (if append_NL then prerr_endline else prerr_string)
175        (HelmLogger.string_of_html_msg msg));
176   let names = ref [] in
177   let tryvars = ref false in
178   let prefix = ref "" in
179   let varsprefix = ref "####" in
180   let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
181   let spec =
182     [ "-vars", Arg.Set tryvars, "try also variables" ;
183       "-novars", Arg.Clear tryvars, "do not try variables (default)" ;
184       "-prefix", Arg.Set_string prefix,
185         "limit object choices to URIs beginning with prefix" ; 
186       "-varsprefix", Arg.Set_string varsprefix,
187         "limit variable choices to URIs beginning with prefix; overrides -prefix" ;
188       "-timeout", Arg.Set_int time_out,
189        "number of seconds before a timeout; 0 means no timeout"
190     ]
191   in
192   Arg.parse spec (fun name -> names := name :: !names) usage;
193   let names = List.rev !names in
194   if !varsprefix = "####" then varsprefix := !prefix ;
195   uri_predicate :=
196    BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix;
197   let status = (ref [], ref [], ref [], ref []) in  (* <ok, nok, maybe, timeout> URIs *)
198   List.iter
199     (fun name ->
200       try
201         let uri = UriManager.uri_of_string name in
202         do_uri status uri
203       with UriManager.IllFormedUri _ ->
204         if Sys.file_exists name then
205           do_file status name
206         else
207           printf "Don't know what to do with '%s', ignoring it\n%!" name)
208     names ;
209   report status