open Printf

let mqi_debug_fun = ignore
let mqi_flags = []
let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun

let verbose = false

exception Failure of string
exception Multiple_interpretations
let fail msg = raise (Failure msg)

module DisambiguateCallbacks =
 struct
  let output_html ?(append_NL = true) msg =
    if verbose then
      (if append_NL then print_string else print_endline)
        (Ui_logger.string_of_html_msg msg)

  let interactive_user_uri_choice
   ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id =
     List.filter
      (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))

  let interactive_interpretation_choice _ = raise Multiple_interpretations
  let input_or_locate_uri ~title = fail "Unknown identifier"
 end

module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)

let debug_print s = prerr_endline ("^^^^^^ " ^ s)

let test_uri uri =
  let obj = CicCache.get_obj uri in
  let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
    Cic2acic.acic_object_of_cic_object obj
  in
  let ids_to_uris = Hashtbl.create 1023 in
  let round_trip annterm =
    debug_print "(1) acic -> ast";
    let (ast, _) =
      Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
    in
    debug_print ("ast: " ^ CicAstPp.pp_term ast);
    let (_, _, term) =
      Disambiguate'.disambiguate_term mqi_handle [] [] ast
        DisambiguateTypes.Environment.empty
    in
    debug_print ("term: " ^ CicPp.ppterm term)
  in
  match annobj with
  | Cic.AConstant (_, _, _, None, ty, _) ->
      debug_print "Cic.AConstant (ty)";
      round_trip ty
  | Cic.AConstant (_, _, _, Some bo, ty, _) ->
(*
      debug_print "Cic.AConstant (bo)";
      round_trip bo;
*)
      debug_print "Cic.AConstant (ty)";
      round_trip ty
  | Cic.AVariable (_, _, None, ty, _) ->
      debug_print "Cic.AVariable (ty)";
      round_trip ty
  | Cic.AVariable (_, _, Some bo, ty, _) ->
      debug_print "Cic.AVariable (bo)";
      round_trip bo;
      debug_print "Cic.AVariable (ty)";
      round_trip ty
  | Cic.ACurrentProof (_, _, _, _, proof, ty, _) ->
      debug_print "Cic.ACurrentProof (proof)";
      round_trip proof;
      debug_print "Cic.ACurrentProof (ty)";
      round_trip ty
  | Cic.AInductiveDefinition _ ->
      debug_print "AInductiveDefinition: boh ..."

let test_uri uri =
  try
    test_uri uri;
    `Ok
  with
  | Multiple_interpretations -> `Maybe
  | exn ->
      prerr_endline (sprintf "Top Level Uncaught Exception: %s"
        (Printexc.to_string exn));
      `Nok

let _ =
  let idx = ref 0 in
  let ok = ref [] in
  let nok = ref [] in
  let maybe = ref [] in
  try
    let mode = if Sys.argv.(1) = "-" then `Stdin else `Cmdline in
    while true do
      incr idx;
      let uri_str =
        match mode with
        | `Stdin -> input_line stdin
        | `Cmdline -> Sys.argv.(!idx)
      in
      printf "Testing URI: %-55s " (uri_str ^ " ..."); flush stdout;
      let uri = UriManager.uri_of_string uri_str in
      match test_uri uri with
      | `Ok ->
          print_endline "[   OK   ]";
          ok := uri_str :: !ok
      | `Nok ->
          print_endline "[ FAILED ]";
          nok := uri_str :: !nok
      | `Maybe ->
          print_endline "[  MANY  ]";
          maybe := uri_str :: !maybe
    done
  with Invalid_argument _ | End_of_file ->
    print_newline ();
    print_endline "TestLibrary report";
    print_endline "Succeeded URIs:";
    List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok);
    print_endline "Failed URIs:";
    List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
    print_endline "Multiple answers URIs:";
    List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
    print_newline ()