helm/gTopLevel/topLevel/topLevel.ml

   1 let get_terms () =
   2    let terms = ref [] in
   3    let lexbuf = Lexing.from_channel stdin in
   4    try
   5       while true do
   6          match CicTextualParser.main CicTextualLexer.token lexbuf with
   7             | None -> ()
   8             | Some expr -> terms := expr :: ! terms
   9       done;
  10       ! terms
  11    with
  12       CicTextualParser0.Eof -> ! terms
  13
  14 let locate name =
  15    print_endline (MQueryGenerator.locate name);
  16    flush stdout
  17
  18 let rec display = function
  19    | []           -> ()
  20    | term :: tail ->
  21       display tail;
  22       print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
  23       flush stdout
  24
  25 let rec levels level = function
  26    | []           -> ()
  27    | term :: tail ->
  28       levels level tail;
  29       print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
  30       print_endline (MQueryGenerator.levels [] [] term level);
  31       flush stdout
  32
  33 let rec backward level = function
  34    | []           -> ()
  35    | term :: tail ->
  36       backward level tail;
  37       print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
  38       print_endline (MQueryGenerator.backward [] [] term level);
  39       flush stdout
  40
  41 let parse_args () =
  42    let rec parse = function
  43       | [] -> ()
  44       | ("-l"|"-locate") :: arg :: rem ->
  45          locate arg; parse rem
  46       | ("-d"|"-display") :: rem ->
  47          display (get_terms ())
  48       | ("-t"|"-test") :: arg :: rem ->
  49         levels (int_of_string arg) (get_terms ())
  50       | ("-b"|"-backward") :: arg :: rem ->
  51          backward (int_of_string arg) (get_terms ())
  52       | _ :: rem -> parse rem
  53    in
  54       parse (List.tl (Array.to_list Sys.argv))
  55
  56 let _ =
  57    CicCooking.init () ;
  58    Logger.log_callback :=
  59       (Logger.log_to_html
  60       ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
  61    MQueryGenerator.init ();
  62    parse_args ();
  63    MQueryGenerator.close ();
  64    exit 0
  65 ;;