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   | exn ->
 116       prerr_endline (sprintf "Top Level Uncaught Exception: %s"
 117         (Printexc.to_string exn));
 118       `Nok
 119
 120 let report (ok,nok,maybe,timeout) =
 121   print_newline ();
 122   print_endline "TestLibrary report";
 123   print_endline "Succeeded URIs:";
 124   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
 125   print_endline "Failed URIs:";
 126   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
 127   print_endline "Multiple answers URIs:";
 128   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
 129   print_newline ();
 130   print_endline ("URIs that timeout (" ^ string_of_int !time_out ^ "s):");
 131   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout);
 132   print_newline ()
 133
 134 let do_uri (ok, nok, maybe, timeout) uri =
 135   let uri_str = UriManager.string_of_uri uri in
 136   printf "Testing URI: %-55s %!" (uri_str ^ " ...");
 137   match test_uri uri with
 138   | `Ok ->
 139       print_endline "\e[01;32m[   OK   ]\e[00m";
 140       ok := uri_str :: !ok
 141   | `Nok ->
 142       print_endline "\e[01;31m[ FAILED ]\e[00m";
 143       nok := uri_str :: !nok
 144   | `Maybe ->
 145       print_endline "\e[01;33m[  MANY  ]\e[00m";
 146       maybe := uri_str :: !maybe
 147   | `TimeOut ->
 148       print_endline "\e[01;34m[TIMEOUT!]\e[00m";
 149       timeout := uri_str :: !timeout
 150
 151 let do_file status fname =
 152   try
 153     let ic = open_in fname in
 154     (try
 155       while true do
 156         let line = input_line ic in
 157         try
 158           let uri = UriManager.uri_of_string line in
 159           do_uri status uri
 160         with UriManager.IllFormedUri _ ->
 161           printf "Error parsing URI '%s', ignoring it" line
 162       done
 163     with End_of_file ->
 164      close_in ic)
 165   with exn ->
 166     printf "Error trying to access '%s' (%s), skipping the file\n%!"
 167       fname (Printexc.to_string exn)
 168
 169 let _ =
 170   HelmLogger.register_log_callback
 171    (fun ?(append_NL = true) msg ->
 172      (if append_NL then prerr_endline else prerr_string)
 173        (HelmLogger.string_of_html_msg msg));
 174   let names = ref [] in
 175   let tryvars = ref false in
 176   let prefix = ref "" in
 177   let varsprefix = ref "####" in
 178   let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
 179   let spec =
 180     [ "-vars", Arg.Set tryvars, "try also variables" ;
 181       "-novars", Arg.Clear tryvars, "do not try variables (default)" ;
 182       "-prefix", Arg.Set_string prefix,
 183         "limit object choices to URIs beginning with prefix" ;
 184       "-varsprefix", Arg.Set_string varsprefix,
 185         "limit variable choices to URIs beginning with prefix; overrides -prefix" ;
 186       "-timeout", Arg.Set_int time_out,
 187        "number of seconds before a timeout; 0 means no timeout"
 188     ]
 189   in
 190   Arg.parse spec (fun name -> names := name :: !names) usage;
 191   let names = List.rev !names in
 192   if !varsprefix = "####" then varsprefix := !prefix ;
 193   uri_predicate :=
 194    BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix;
 195   let status = (ref [], ref [], ref [], ref []) in  (* <ok, nok, maybe, timeout> URIs *)
 196   List.iter
 197     (fun name ->
 198       try
 199         let uri = UriManager.uri_of_string name in
 200         do_uri status uri
 201       with UriManager.IllFormedUri _ ->
 202         if Sys.file_exists name then
 203           do_file status name
 204         else
 205           printf "Don't know what to do with '%s', ignoring it\n%!" name)
 206     names ;
 207   report status