helm/gTopLevel/testlibrary.ml

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