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