let connection_param = "host=mowgli.cs.unibo.it dbname=helm user=helm"

let show_queries = ref false

let use_db = ref true

let db_down = ref true

let nl = " <p>\n"

let check_db () =
   if ! db_down then 
      if ! use_db then begin Mqint.init connection_param; db_down := false; true end 
      else begin print_endline "Not issuing in restricted mode"; false end
   else true

let default_confirm q =
   let module Util = MQueryUtil in   
   if ! show_queries then print_string (Util.text_of_query q ^ nl);
   let b = check_db () in
   if ! db_down then print_endline "db_down"; b 

let get_terms () =
   let terms = ref [] in
   let lexbuf = Lexing.from_channel stdin in
   try
      while true do
         match CicTextualParserContext.main  
	    (UriManager.uri_of_string "cic:/dummy") [] []
	    CicTextualLexer.token lexbuf
	    with
            | None           -> ()
            | Some (_, expr) -> terms := expr :: ! terms
      done;
      ! terms
   with
      CicTextualParser0.Eof -> ! terms

let pp_type_of uri = 
   let u = UriManager.uri_of_string uri in  
   let s = match (CicEnvironment.get_obj u) with
      | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty
      | Cic.Axiom (_, ty, _)         -> CicPp.ppterm ty
      | Cic.Variable (_, _, ty)      -> CicPp.ppterm ty
      | _                            -> "Current proof or inductive definition."      
(*
      | Cic.CurrentProof (_,conjs,te,ty) ->
      | C.InductiveDefinition _ ->
*)
   in print_endline s; flush stdout

let set_dbms i =
   if i = 1 then Mqint.set_database Mqint.postgres_db else
   if i = 2 then Mqint.set_database Mqint.galax_db else ()
   
let get_dbms s =
   if s = Mqint.postgres_db then 1 else
   if s = Mqint.galax_db then 2 else 0

let dbc () =
   let on = check_db () in 
   if on then
   begin
      let dbms = Mqint.get_database () in
      prerr_endline ("toplevel: current dbms is n." ^ 
                     string_of_int (get_dbms dbms) ^ " (" ^ dbms ^ ")");
      Mqint.check ()
   end

let rec display = function
   | []           -> ()
   | term :: tail -> 
      display tail;
      print_string ("? " ^ CicPp.ppterm term ^ nl);
      flush stdout

let levels l =
   let module Gen = MQueryGenerator in
   let rec levels_aux = function
      | []           -> ()
      | term :: tail -> 
         levels_aux tail;
         print_string ("? " ^ CicPp.ppterm term ^ nl);
         print_string (Gen.string_of_levels (Gen.levels_of_term [] [] term) nl);
         flush stdout
   in
   levels_aux l

let execute ich =
   let module Util = MQueryUtil in
   let module Gen = MQueryGenerator in
   Gen.set_confirm_query default_confirm;
   try 
      let q = Util.query_of_text (Lexing.from_channel ich) in
      print_endline (Util.text_of_result (Gen.execute_query q) nl);
      flush stdout
   with Gen.Discard -> ()

let locate name =
   let module Util = MQueryUtil in
   let module Gen = MQueryGenerator in
   Gen.set_confirm_query default_confirm;
   try 
      print_endline (Util.text_of_result (Gen.locate name) nl);
      flush stdout
   with Gen.Discard -> ()

let mbackward n m l = 
   let module Util = MQueryUtil in
   let module Gen = MQueryGenerator in
   let queries = ref [] in
   let confirm query = 
      if List.mem query ! queries then false 
      else begin queries := query :: ! queries; default_confirm query end
   in
   let rec backward level = function
      | []           -> ()
      | term :: tail -> 
         backward level tail;
	 try 
	    if Mqint.get_stat () then 
	       print_string ("? " ^ CicPp.ppterm term ^ nl);
	    let t0 = Sys.time () in
            let r = Gen.backward [] [] term level in
	    let t1 = Sys.time () -. t0 in
	    let info = Gen.get_query_info () in
	    let num = List.nth info 0 in
	    let gen = List.nth info 1 in
	    if Mqint.get_stat () then 
	       print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl);
	    print_string (Util.text_of_result r nl);
            flush stdout
	 with Gen.Discard -> ()
   in
   Gen.set_confirm_query confirm;
   for level = max m n downto min m n do
      prerr_endline ("toplevel: backward: trying level " ^
                     string_of_int level);
      backward level l
   done;
   prerr_endline ("toplevel: backward: " ^ 
                  string_of_int (List.length ! queries) ^
                  " queries issued")

let prerr_help () =
   prerr_endline "\nUSAGE: toplevel.opt OPTIONS < INPUTFILE\n"; 
   prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
   prerr_endline "testing purposes. Toplevel reads its input from stdin and produces ith output";
   prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
   prerr_endline "OPTIONS:\n";
   prerr_endline "-h  -help               shows this help message";
   prerr_endline "-q  -show-queries       outputs generated queries";
   prerr_endline "-s  -stat               outputs interpreter statistics";
   prerr_endline "-c  -db-check           checks the database connection";
   prerr_endline "-i  -interpreter NUMBER sets the dbms to be used (default 1)";
   prerr_endline "-r  -restricted -nodb   enables restricted mode: queries are not issued";
   prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
   prerr_endline "-x  -execute            issues a query given in the input file";
   prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
   prerr_endline "-l  -levels             outputs the cut levels of the CIC terms given in the input file";
   prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
   prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all CIC terms";
   prerr_endline "                        in the input file";
   prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all";
   prerr_endline "                        CIC terms in the input file\n";
   prerr_endline "NOTES: interpreter numbers are 1 for postgres and 2 for galax";
   prerr_endline "       CIC terms are read with the HELM CIC Textual Parser";
   prerr_endline "       -typeof does not work with inductive types and proofs in progress\n"

let parse_args () =
   let rec parse = function
      | [] -> ()
      | ("-h"|"-help") :: rem -> prerr_help ()
      | ("-d"|"-display") :: rem -> display (get_terms ())
      | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
      | ("-l"|"-levels") :: rem -> levels (get_terms ())
      | ("-x"|"-execute") :: rem -> execute stdin; parse rem
      | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
      | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem
      | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem
      | ("-i"|"-interpreter") :: dbms :: rem -> set_dbms (int_of_string dbms); parse rem
      | ("-c"|"-db-check") :: rem -> dbc (); parse rem
      | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
      | ("-B"|"-backward") :: arg :: rem ->
         let m = (int_of_string arg) in
         mbackward m m (get_terms ())
      | ("-MB"|"-multi-backward") :: arg :: rem ->
         let m = (int_of_string arg) in
         mbackward m 0 (get_terms ())
      | _ :: rem -> parse rem
   in  
      parse (List.tl (Array.to_list Sys.argv))

let _ =
   let module Gen = MQueryGenerator in
   CicCooking.init () ; 
   Logger.log_callback :=
      (Logger.log_to_html
      ~print_and_flush:(function s -> () (* print_string s ; flush stdout *) ));
   Mqint.set_stat false;
   Gen.set_log_file "MQGenLog.htm";
   set_dbms 1;
   parse_args ();
   if not ! db_down then Mqint.close ();
   Gen.set_confirm_query (fun _ -> true);
   prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^
                  " seconds");
   exit 0