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 locate name = 
   print_endline (MQueryGenerator.locate_html name);
   flush stdout

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

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

let mbackward n m l =
   let queries = ref [] in
   let issue query = 
      if List.mem query ! queries then false
      else begin queries := query :: ! queries; true end
   in
   let rec backward level = function
      | []           -> ()
      | term :: tail -> 
         backward level tail;
         print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
         print_endline (MQueryGenerator.backward [] [] term level);
         flush stdout
   in
   MQueryGenerator.call_back issue;
   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");
   MQueryGenerator.call_back (fun _ -> true)
   
let parse_args () =
   let rec parse = function
      | [] -> ()
      | ("-d"|"-display") :: rem -> display (get_terms ())
      | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
      | ("-l"|"-levels") :: rem -> levels (get_terms ())
      | ("-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"|"-mbackward") :: 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 _ =
   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 ();
   prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^
                  " seconds");
   exit 0