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 module DisambiguateCallbacks =
  15  struct
  16   let output_html ?(append_NL = true) msg =
  17     if verbose then
  18       (if append_NL then print_string else print_endline)
  19         (Ui_logger.string_of_html_msg msg)
  20
  21   let interactive_user_uri_choice
  22    ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id =
  23      List.filter
  24       (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
  25
  26   let interactive_interpretation_choice _ = raise Multiple_interpretations
  27   let input_or_locate_uri ~title = fail "Unknown identifier"
  28  end
  29
  30 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
  31
  32 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
  33
  34 let test_uri uri =
  35   let obj = CicCache.get_obj uri in
  36   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
  37     Cic2acic.acic_object_of_cic_object obj
  38   in
  39   let ids_to_uris = Hashtbl.create 1023 in
  40   let round_trip annterm =
  41     debug_print "(1) acic -> ast";
  42     let (ast, _) =
  43       Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
  44     in
  45     debug_print ("ast: " ^ CicAstPp.pp_term ast);
  46     let (_, _, term) =
  47       Disambiguate'.disambiguate_term mqi_handle [] [] ast
  48         DisambiguateTypes.Environment.empty
  49     in
  50     debug_print ("term: " ^ CicPp.ppterm term)
  51   in
  52   match annobj with
  53   | Cic.AConstant (_, _, _, None, ty, _) ->
  54       debug_print "Cic.AConstant (ty)";
  55       round_trip ty
  56   | Cic.AConstant (_, _, _, Some bo, ty, _) ->
  57 (*
  58       debug_print "Cic.AConstant (bo)";
  59       round_trip bo;
  60 *)
  61       debug_print "Cic.AConstant (ty)";
  62       round_trip ty
  63   | Cic.AVariable (_, _, None, ty, _) ->
  64       debug_print "Cic.AVariable (ty)";
  65       round_trip ty
  66   | Cic.AVariable (_, _, Some bo, ty, _) ->
  67       debug_print "Cic.AVariable (bo)";
  68       round_trip bo;
  69       debug_print "Cic.AVariable (ty)";
  70       round_trip ty
  71   | Cic.ACurrentProof (_, _, _, _, proof, ty, _) ->
  72       debug_print "Cic.ACurrentProof (proof)";
  73       round_trip proof;
  74       debug_print "Cic.ACurrentProof (ty)";
  75       round_trip ty
  76   | Cic.AInductiveDefinition _ ->
  77       debug_print "AInductiveDefinition: boh ..."
  78
  79 let test_uri uri =
  80   try
  81     test_uri uri;
  82     `Ok
  83   with
  84   | Multiple_interpretations -> `Maybe
  85   | exn ->
  86       prerr_endline (sprintf "Top Level Uncaught Exception: %s"
  87         (Printexc.to_string exn));
  88       `Nok
  89
  90 let _ =
  91   let idx = ref 0 in
  92   let ok = ref [] in
  93   let nok = ref [] in
  94   let maybe = ref [] in
  95   try
  96     let mode = if Sys.argv.(1) = "-" then `Stdin else `Cmdline in
  97     while true do
  98       incr idx;
  99       let uri_str =
 100         match mode with
 101         | `Stdin -> input_line stdin
 102         | `Cmdline -> Sys.argv.(!idx)
 103       in
 104       printf "Testing URI: %-55s " (uri_str ^ " ..."); flush stdout;
 105       let uri = UriManager.uri_of_string uri_str in
 106       match test_uri uri with
 107       | `Ok ->
 108           print_endline "\e[01;32m[   OK   ]\e[00m";
 109           ok := uri_str :: !ok
 110       | `Nok ->
 111           print_endline "\e[01;31m[ FAILED ]\e[00m";
 112           nok := uri_str :: !nok
 113       | `Maybe ->
 114           print_endline "\e[01;33m[  MANY  ]\e[00m";
 115           maybe := uri_str :: !maybe
 116     done
 117   with Invalid_argument _ | End_of_file ->
 118     print_newline ();
 119     print_endline "TestLibrary report";
 120     print_endline "Succeeded URIs:";
 121     List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
 122     print_endline "Failed URIs:";
 123     List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
 124     print_endline "Multiple answers URIs:";
 125     List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
 126     print_newline ()
 127