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