helm/gTopLevel/topLevel/topLevel.ml

   1 let show_queries = ref false
   2
   3 let use_db = ref true
   4
   5 let db_down = ref true
   6
   7 let nl = " <p>\n"
   8
   9 let check_db () =
  10    if ! db_down then
  11       if ! use_db then begin Mqint.init (); db_down := false; true end
  12       else begin print_endline "Not issuing in restricted mode"; false end
  13    else true
  14
  15 let default_confirm q =
  16    let module Util = MQueryUtil in
  17    if ! show_queries then print_string (Util.text_of_query q ^ nl);
  18    let b = check_db () in
  19    if ! db_down then print_endline "db_down"; b
  20
  21 let get_terms () =
  22    let terms = ref [] in
  23    let lexbuf = Lexing.from_channel stdin in
  24    try
  25       while true do
  26          match CicTextualParserContext.main
  27             (UriManager.uri_of_string "cic:/dummy") [] []
  28             CicTextualLexer.token lexbuf
  29             with
  30             | None           -> ()
  31             | Some (_, expr) -> terms := expr :: ! terms
  32       done;
  33       ! terms
  34    with
  35       CicTextualParser0.Eof -> ! terms
  36
  37 let pp_type_of uri =
  38    let u = UriManager.uri_of_string uri in
  39    let s = match (CicEnvironment.get_obj u) with
  40       | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty
  41       | Cic.Axiom (_, ty, _)         -> CicPp.ppterm ty
  42       | Cic.Variable (_, _, ty)      -> CicPp.ppterm ty
  43       | _                            -> "Current proof or inductive definition."
  44 (*
  45       | Cic.CurrentProof (_,conjs,te,ty) ->
  46       | C.InductiveDefinition _ ->
  47 *)
  48    in print_endline s; flush stdout
  49
  50 let dbc () =
  51    let on = check_db () in
  52    if on then ignore (Mqint.check ())
  53
  54 let rec display = function
  55    | []           -> ()
  56    | term :: tail ->
  57       display tail;
  58       print_string ("? " ^ CicPp.ppterm term ^ nl);
  59       flush stdout
  60
  61 let levels l =
  62    let module Gen = MQueryGenerator in
  63    let rec levels_aux = function
  64       | []           -> ()
  65       | term :: tail ->
  66          levels_aux tail;
  67          print_string ("? " ^ CicPp.ppterm term ^ nl);
  68          print_string (Gen.string_of_levels (Gen.levels_of_term [] [] term) nl);
  69          flush stdout
  70    in
  71    levels_aux l
  72
  73 let execute ich =
  74    let module Util = MQueryUtil in
  75    let module Gen = MQueryGenerator in
  76    Gen.set_confirm_query default_confirm;
  77    try
  78       let q = Util.query_of_text (Lexing.from_channel ich) in
  79       print_endline (Util.text_of_result (Gen.execute_query q) nl);
  80       flush stdout
  81    with Gen.Discard -> ()
  82
  83 let locate name =
  84    let module Util = MQueryUtil in
  85    let module Gen = MQueryGenerator in
  86    Gen.set_confirm_query default_confirm;
  87    try
  88       print_endline (Util.text_of_result (Gen.locate name) nl);
  89       flush stdout
  90    with Gen.Discard -> ()
  91
  92 let mbackward n m l =
  93    let module Util = MQueryUtil in
  94    let module Gen = MQueryGenerator in
  95    let queries = ref [] in
  96    let confirm query =
  97       if List.mem query ! queries then false
  98       else begin queries := query :: ! queries; default_confirm query end
  99    in
 100    let rec backward level = function
 101       | []           -> ()
 102       | term :: tail ->
 103          backward level tail;
 104          print_string ("? " ^ CicPp.ppterm term ^ nl);
 105          try
 106             let t0 = Sys.time () in
 107             let r = Gen.backward [] [] term level in
 108             let t1 = Sys.time () -. t0 in
 109             let info = List.nth (Gen.get_query_info ()) 0 in
 110             print_string ("GEN = " ^ info ^ ":" ^ string_of_float t1 ^ "s" ^ nl);
 111             print_string (Util.text_of_result r nl);
 112             flush stdout
 113          with Gen.Discard -> ()
 114    in
 115    Gen.set_confirm_query confirm;
 116    for level = max m n downto min m n do
 117       prerr_endline ("toplevel: backward: trying level " ^
 118                      string_of_int level);
 119       backward level l
 120    done;
 121    prerr_endline ("toplevel: backward: " ^
 122                   string_of_int (List.length ! queries) ^
 123                   " queries issued")
 124
 125 let prerr_help () =
 126    prerr_endline "\nUSAGE: toplevel.opt OPTIONS < INPUTFILE\n";
 127    prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
 128    prerr_endline "testing purposes. Toplevel reads its input from stdin and produces ith output";
 129    prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
 130    prerr_endline "OPTIONS:\n";
 131    prerr_endline "-h  -help               shows this help message";
 132    prerr_endline "-q  -show-queries       outputs the generated queries";
 133    prerr_endline "-c  -db-check           checks the database connection";
 134    prerr_endline "-r  -restricted -nodb   enables restricted mode: queries are not issued";
 135    prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
 136    prerr_endline "-x  -execute            issues a query given in the input file";
 137    prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
 138    prerr_endline "-l  -levels             outputs the cut levels of the CIC terms given in the input file";
 139    prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
 140    prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all CIC terms";
 141    prerr_endline "                        in the input file";
 142    prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all";
 143    prerr_endline "                        CIC terms in the input file\n";
 144    prerr_endline "NOTES: CIC terms are read with the HELM CIC Textual Parser";
 145    prerr_endline "       -typeof does not work with inductive types and proofs in progress\n"
 146
 147 let parse_args () =
 148    let rec parse = function
 149       | [] -> ()
 150       | ("-h"|"-help") :: rem -> prerr_help ()
 151       | ("-d"|"-display") :: rem -> display (get_terms ())
 152       | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
 153       | ("-l"|"-levels") :: rem -> levels (get_terms ())
 154       | ("-x"|"-execute") :: rem -> execute stdin; parse rem
 155       | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
 156       | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem
 157       | ("-c"|"-db-check") :: rem -> dbc (); parse rem
 158       | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
 159       | ("-B"|"-backward") :: arg :: rem ->
 160          let m = (int_of_string arg) in
 161          mbackward m m (get_terms ())
 162       | ("-MB"|"-multi-backward") :: arg :: rem ->
 163          let m = (int_of_string arg) in
 164          mbackward m 0 (get_terms ())
 165       | _ :: rem -> parse rem
 166    in
 167       parse (List.tl (Array.to_list Sys.argv))
 168
 169 let _ =
 170    let module Gen = MQueryGenerator in
 171    CicCooking.init () ;
 172    Logger.log_callback :=
 173       (Logger.log_to_html
 174       ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
 175    Gen.set_log_file "MQGenLog.htm";
 176    parse_args ();
 177    if not ! db_down then Mqint.close ();
 178    Gen.set_confirm_query (fun _ -> true);
 179    prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^
 180                   " seconds");
 181    exit 0