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