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 CicTextualParserContext.main
   7             (UriManager.uri_of_string "cic:/dummy") [] []
   8             CicTextualLexer.token lexbuf
   9             with
  10             | None           -> ()
  11             | Some (_, expr) -> terms := expr :: ! terms
  12       done;
  13       ! terms
  14    with
  15       CicTextualParser0.Eof -> ! terms
  16
  17 let pp_type_of uri =
  18    let u = UriManager.uri_of_string uri in
  19    let s = match (CicEnvironment.get_obj u) with
  20       | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty
  21       | Cic.Axiom (_, ty, _)         -> CicPp.ppterm ty
  22       | Cic.Variable (_, _, ty)      -> CicPp.ppterm ty
  23       | _                            -> "Current proof or inductive definition."
  24 (*
  25       | Cic.CurrentProof (_,conjs,te,ty) ->
  26       | C.InductiveDefinition _ ->
  27 *)
  28    in print_endline s; flush stdout
  29
  30 let locate name =
  31    print_endline (MQueryGenerator.locate name);
  32    flush stdout
  33
  34 let rec display = function
  35    | []           -> ()
  36    | term :: tail ->
  37       display tail;
  38       print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
  39       flush stdout
  40
  41 let rec levels = function
  42    | []           -> ()
  43    | term :: tail ->
  44       levels tail;
  45       print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
  46       print_endline (MQueryGenerator.levels [] [] term);
  47       flush stdout
  48
  49 let mbackward n m l =
  50    let queries = ref [] in
  51    let issue query =
  52       if List.mem query ! queries then false
  53       else begin queries := query :: ! queries; true end
  54    in
  55    let rec backward level = function
  56       | []           -> ()
  57       | term :: tail ->
  58          backward level tail;
  59          print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
  60          print_endline (MQueryGenerator.backward [] [] term level);
  61          flush stdout
  62    in
  63    MQueryGenerator.call_back issue;
  64    for level = max m n downto min m n do
  65       prerr_endline ("toplevel: backward: trying level " ^
  66                      string_of_int level);
  67       backward level l
  68    done;
  69    prerr_endline ("toplevel: backward: " ^
  70                   string_of_int (List.length ! queries) ^
  71                   " queries issued");
  72    MQueryGenerator.call_back (fun _ -> true)
  73
  74 let parse_args () =
  75    let rec parse = function
  76       | [] -> ()
  77       | ("-d"|"-display") :: rem -> display (get_terms ())
  78       | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
  79       | ("-l"|"-levels") :: rem -> levels (get_terms ())
  80       | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
  81       | ("-B"|"-backward") :: arg :: rem ->
  82          let m = (int_of_string arg) in
  83          mbackward m m (get_terms ())
  84       | ("-MB"|"-mbackward") :: arg :: rem ->
  85          let m = (int_of_string arg) in
  86          mbackward m 0 (get_terms ())
  87       | _ :: rem -> parse rem
  88    in
  89       parse (List.tl (Array.to_list Sys.argv))
  90
  91 let _ =
  92    CicCooking.init () ;
  93    Logger.log_callback :=
  94       (Logger.log_to_html
  95       ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
  96    MQueryGenerator.init ();
  97    parse_args ();
  98    MQueryGenerator.close ();
  99    prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^
 100                   " seconds");
 101    exit 0