helm/gTopLevel/topLevel/topLevel.ml

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