helm/gTopLevel/testlibrary.ml

   1
   2 open Printf
   3
   4 Helm_registry.load_from "gTopLevel.conf.xml";;
   5
   6 let mqi_debug_fun s =
   7  HelmLogger.log ~append_NL:true (`Msg (`T s))
   8 let mqi_flags = []
   9 let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun ()
  10
  11 let verbose = false
  12
  13 exception Failure of string
  14 let fail msg = raise (Failure msg)
  15
  16 let uri_predicate = ref (BatchParser.constants_only ~prefix:"")
  17
  18 module DisambiguateCallbacks =
  19  struct
  20   let interactive_user_uri_choice
  21    ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices =
  22      List.filter !uri_predicate choices
  23
  24   let interactive_interpretation_choice =
  25    let rec aux n =
  26     function
  27        [] -> []
  28      | _::tl -> n::(aux (n+1) tl)
  29    in
  30     aux 0
  31
  32   let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title)
  33  end
  34
  35 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
  36
  37 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
  38
  39 let test_uri uri =
  40   let obj = CicEnvironment.get_obj uri in
  41   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
  42     Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
  43   in
  44   let ids_to_uris = Hashtbl.create 1023 in
  45   let round_trip annterm =
  46     debug_print "(1) acic -> ast";
  47     let (ast, _) =
  48       Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
  49     in
  50     let new_pp = BoxPp.pp_term ast in
  51     debug_print ("ast:\n" ^ new_pp);
  52     let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
  53     debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
  54     let res =
  55      Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
  56       DisambiguateTypes.Environment.empty in
  57     List.iter
  58      (fun (domain, _, term) ->
  59        debug_print
  60         ("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ;
  61        debug_print ("term: " ^ CicPp.ppterm term)
  62      ) res ;
  63     List.length  res
  64   in
  65   match annobj with
  66   | Cic.AConstant (_, _, _, None, ty, _) ->
  67       debug_print "Cic.AConstant (ty)";
  68       round_trip ty
  69   | Cic.AConstant (_, _, _, Some bo, ty, _) ->
  70 (*
  71       debug_print "Cic.AConstant (bo)";
  72       let n = round_trip bo in
  73 *)
  74       debug_print "Cic.AConstant (ty)";
  75       round_trip ty (* + n *)
  76   | Cic.AVariable (_, _, None, ty, _) ->
  77       debug_print "Cic.AVariable (ty)";
  78       round_trip ty
  79   | Cic.AVariable (_, _, Some bo, ty, _) ->
  80 (*
  81       debug_print "Cic.AVariable (bo)";
  82       let n = round_trip bo in
  83 *)
  84       debug_print "Cic.AVariable (ty)";
  85       round_trip ty (* + n *)
  86   | Cic.ACurrentProof (_, _, _, _, _, _, _) ->
  87       assert false
  88   | Cic.AInductiveDefinition _ ->
  89       debug_print "AInductiveDefinition: boh ..." ;
  90       assert false
  91
  92 let test_uri uri =
  93   try
  94    if test_uri uri = 1 then `Ok else `Maybe
  95   with
  96   | exn ->
  97       prerr_endline (sprintf "Top Level Uncaught Exception: %s"
  98         (Printexc.to_string exn));
  99       `Nok
 100
 101 let report (ok,nok,maybe) =
 102   print_newline ();
 103   print_endline "TestLibrary report";
 104   print_endline "Succeeded URIs:";
 105   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
 106   print_endline "Failed URIs:";
 107   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
 108   print_endline "Multiple answers URIs:";
 109   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
 110   print_newline ()
 111
 112 let do_uri (ok, nok, maybe) uri =
 113   let uri_str = UriManager.string_of_uri uri in
 114   printf "Testing URI: %-55s %!" (uri_str ^ " ...");
 115   match test_uri uri with
 116   | `Ok ->
 117       print_endline "\e[01;32m[   OK   ]\e[00m";
 118       ok := uri_str :: !ok
 119   | `Nok ->
 120       print_endline "\e[01;31m[ FAILED ]\e[00m";
 121       nok := uri_str :: !nok
 122   | `Maybe ->
 123       print_endline "\e[01;33m[  MANY  ]\e[00m";
 124       maybe := uri_str :: !maybe
 125
 126 let do_file status fname =
 127   try
 128     let ic = open_in fname in
 129     (try
 130       while true do
 131         let line = input_line ic in
 132         try
 133           let uri = UriManager.uri_of_string line in
 134           do_uri status uri
 135         with UriManager.IllFormedUri _ ->
 136           printf "Error parsing URI '%s', ignoring it" line
 137       done
 138     with End_of_file ->
 139      close_in ic)
 140   with exn ->
 141     printf "Error trying to access '%s' (%s), skipping the file\n%!"
 142       fname (Printexc.to_string exn)
 143
 144 let _ =
 145   HelmLogger.register_log_callback
 146    (fun ?(append_NL = true) msg ->
 147      (if append_NL then prerr_endline else prerr_string)
 148        (HelmLogger.string_of_html_msg msg));
 149   let names = ref [] in
 150   let tryvars = ref false in
 151   let prefix = ref "" in
 152   let varsprefix = ref "####" in
 153   let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
 154   let spec =
 155     [ "-vars", Arg.Set tryvars, "try also variables" ;
 156       "-novars", Arg.Clear tryvars, "do not try variables (default)" ;
 157       "-prefix", Arg.Set_string prefix,
 158         "limit object choices to URIs beginning with prefix" ;
 159       "-varsprefix", Arg.Set_string varsprefix,
 160         "limit variable choices to URIs beginning with prefix; overrides -prefix" ;
 161     ]
 162   in
 163   Arg.parse spec (fun name -> names := name :: !names) usage;
 164   let names = List.rev !names in
 165   if !varsprefix = "####" then varsprefix := !prefix ;
 166   uri_predicate :=
 167    BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix;
 168   let status = (ref [], ref [], ref []) in  (* <ok, nok, maybe> URIs *)
 169   List.iter
 170     (fun name ->
 171       try
 172         let uri = UriManager.uri_of_string name in
 173         do_uri status uri
 174       with UriManager.IllFormedUri _ ->
 175         if Sys.file_exists name then
 176           do_file status name
 177         else
 178           printf "Don't know what to do with '%s', ignoring it\n%!" name)
 179     names ;
 180   report status