helm/gTopLevel/testlibrary.ml

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