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