open Printf

let time_out = ref 5;;

Helm_registry.load_from "gTopLevel.conf.xml";;

let mqi_debug_fun s =
 HelmLogger.log ~append_NL:true (`Msg (`T s))
let mqi_flags = []

let dbd = Mysql.quick_connect
    ~host:(Helm_registry.get "db.host")
    ~user:(Helm_registry.get "db.user")
    ~database:(Helm_registry.get "db.database")
    ()
(*
let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun ()
*)

let verbose = false

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

let uri_predicate = ref (BatchParser.constants_only ~prefix:"")

module DisambiguateCallbacks =
 struct
  let interactive_user_uri_choice
   ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices =
     List.filter !uri_predicate choices

  let interactive_interpretation_choice =
   let rec aux n =
    function
       [] -> []
     | _::tl -> n::(aux (n+1) tl)
   in
    aux 0

  let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title)
 end

module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)

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

let test_uri typecheck uri =
  if typecheck then
    try ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph);1
    with CicTypeChecker.TypeCheckerFailure s | 
         CicTypeChecker.AssertFailure s -> 0
  else
  let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
  let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
    Cic2acic.acic_object_of_cic_object ~eta_fix:false 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
    let new_pp = BoxPp.pp_term ast in
    debug_print ("ast:\n" ^ new_pp);
    let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
    debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
    let res =
     Disambiguate'.disambiguate_term ~dbd [] [] new_ast
      ~aliases:DisambiguateTypes.Environment.empty 
      ~initial_ugraph:CicUniv.empty_ugraph 
    in
    List.iter
     (fun (domain, _, term, _) ->
       debug_print
        ("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ;
       debug_print ("term: " ^ CicPp.ppterm term)
     ) res ;
    List.length  res
  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)";
      let n = round_trip bo in
*)
      debug_print "Cic.AConstant (ty)";
      round_trip ty (* + n *)
  | Cic.AVariable (_, _, None, ty, _) ->
      debug_print "Cic.AVariable (ty)";
      round_trip ty
  | Cic.AVariable (_, _, Some bo, ty, _) ->
(*
      debug_print "Cic.AVariable (bo)";
      let n = round_trip bo in
*)
      debug_print "Cic.AVariable (ty)";
      round_trip ty (* + n *)
  | Cic.ACurrentProof (_, _, _, _, _, _, _) ->
      assert false
  | Cic.AInductiveDefinition _ ->
      debug_print "AInductiveDefinition: boh ..." ;
      assert false

exception TimeOut;;
                                                                                
ignore
 (Sys.signal Sys.sigalrm
   (Sys.Signal_handle
     (fun _ ->
       (* We do this in case that some "with _" intercepts the first exception *)
       ignore (Unix.alarm 1) ;
       raise TimeOut)))
;;


let test_uri typecheck uri =
  try
   ignore (Unix.alarm !time_out) ;
   if test_uri typecheck uri = 1 then `Ok else `Maybe
  with
  | TimeOut ->
     (* We do this to clear the alarm set by the signal handler *)
     ignore (Unix.alarm 0) ;
     `TimeOut
     (*
  | exn ->
      prerr_endline (sprintf "Top Level Uncaught Exception: %s"
        (Printexc.to_string exn));
      `Nok*)
  | exn -> raise exn

let report (ok,nok,maybe,timeout) =
  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 ();
  print_endline ("URIs that timeout (" ^ string_of_int !time_out ^ "s):");
  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout);
  print_newline ()

let do_uri typecheck (ok, nok, maybe, timeout) uri =
  let uri_str = UriManager.string_of_uri uri in
  printf "Testing URI: %-55s %!" (uri_str ^ " ...");
  (match test_uri typecheck 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
  | `TimeOut ->
      print_endline "[TIMEOUT!]";
      timeout := uri_str :: !timeout)

let do_file typecheck status fname =
  try
    let ic = open_in fname in
    (try
      while true do
        let line = input_line ic in
        try
          let uri = UriManager.uri_of_string line in
          do_uri typecheck status uri
        with UriManager.IllFormedUri _ ->
          printf "Error parsing URI '%s', ignoring it" line
      done
    with End_of_file ->
     close_in ic)
  with exn ->
    printf "Error trying to access '%s' (%s), skipping the file\n%!"
      fname (Printexc.to_string exn)

let _ =
  HelmLogger.register_log_callback
   (fun ?(append_NL = true) msg ->
     (if append_NL then prerr_endline else prerr_string)
       (HelmLogger.string_of_html_msg msg));
  let names = ref [] in
  let tryvars = ref false in
  let typecheck = ref false in
  let prefix = ref "" in
  let varsprefix = ref "####" in
  let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
  let spec =
    [ "-vars", Arg.Set tryvars, "try also variables" ;
      "-novars", Arg.Clear tryvars, "do not try variables (default)" ;
      "-prefix", Arg.Set_string prefix,
        "limit object choices to URIs beginning with prefix" ; 
      "-varsprefix", Arg.Set_string varsprefix,
        "limit variable choices to URIs beginning with prefix; overrides -prefix" ;
      "-timeout", Arg.Set_int time_out,
       "number of seconds before a timeout; 0 means no timeout";
       "-typecheck", Arg.Set typecheck, "simply typechek the uri"
    ]
  in
  Arg.parse spec (fun name -> names := name :: !names) usage;
  let names = List.rev !names in
  if !varsprefix = "####" then varsprefix := !prefix ;
  uri_predicate :=
   BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix;
  let status = (ref [], ref [], ref [], ref []) in  (* <ok, nok, maybe, timeout> URIs *)
  List.iter
    (fun name ->
      try
        let uri = UriManager.uri_of_string name in
        do_uri !typecheck status uri
      with UriManager.IllFormedUri _ ->
        if Sys.file_exists name then
          do_file !typecheck status name
        else
          printf "Don't know what to do with '%s', ignoring it\n%!" name)
    names ;
  report status