let get_terms () =
   let terms = ref [] in
   let lexbuf = Lexing.from_channel stdin in
   try
      while true do
         match CicTextualParser.main CicTextualLexer.token lexbuf with
            | None -> ()
            | Some expr -> terms := expr :: ! terms
      done;
      ! terms
   with
      CicTextualParser0.Eof -> ! terms

let locate name = 
   print_endline (MQueryGenerator.locate name);
   flush stdout

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

let rec levels level = function
   | []           -> ()
   | term :: tail -> 
      levels level tail;
      print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
      print_endline (MQueryGenerator.levels [] [] term level);
      flush stdout

let rec backward level = function
   | []           -> ()
   | term :: tail -> 
      backward level tail;
      print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
      print_endline (MQueryGenerator.backward [] [] term level);
      flush stdout
      
let parse_args () =
   let rec parse = function
      | [] -> ()
      | ("-l"|"-locate") :: arg :: rem -> 
         locate arg; parse rem
      | ("-d"|"-display") :: rem -> 
         display (get_terms ())
      | ("-t"|"-test") :: arg :: rem -> 
        levels (int_of_string arg) (get_terms ())
      | ("-b"|"-backward") :: arg :: rem -> 
         backward (int_of_string arg) (get_terms ())
      | _ :: rem -> parse rem
   in  
      parse (List.tl (Array.to_list Sys.argv))

let _ =
   CicCooking.init () ;
   Logger.log_callback :=
      (Logger.log_to_html
      ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
   MQueryGenerator.init ();
   parse_args ();
   MQueryGenerator.close ();
   exit 0
;;