helm/gTopLevel/topLevel/topLevel.ml

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