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