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