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