helm/gTopLevel/topLevel/topLevel.ml

   1 let connection_param = "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema 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        let dom,mk_term =
  29         CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
  30        in
  31         match dom with
  32            [] -> terms := (snd (mk_term (function _ -> None))) :: !terms
  33          | _ -> assert false
  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.Constant (_, _, ty, _) -> CicPp.ppterm ty
  43       | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
  44       | _                          -> "Current proof or inductive definition."
  45 (*
  46       | Cic.CurrentProof (_,conjs,te,ty) ->
  47       | C.InductiveDefinition _ ->
  48 *)
  49    in print_endline s; flush stdout
  50
  51 let set_dbms i =
  52    if i = 1 then Mqint.set_database Mqint.postgres_db else
  53    if i = 2 then Mqint.set_database Mqint.galax_db else ()
  54
  55 let get_dbms s =
  56    if s = Mqint.postgres_db then 1 else
  57    if s = Mqint.galax_db then 2 else 0
  58
  59 let dbc () =
  60    let on = check_db () in
  61    if on then
  62    begin
  63       let dbms = Mqint.get_database () in
  64       prerr_endline ("toplevel: current dbms is n." ^
  65                      string_of_int (get_dbms dbms) ^ " (" ^ dbms ^ ")");
  66       Mqint.check ()
  67    end
  68
  69 let rec display = function
  70    | []           -> ()
  71    | term :: tail ->
  72       display tail;
  73       print_string ("? " ^ CicPp.ppterm term ^ nl);
  74       flush stdout
  75
  76 let levels l =
  77    let module Lev = MQueryLevels in
  78    let rec levels_aux = function
  79       | []           -> ()
  80       | term :: tail ->
  81          levels_aux tail;
  82          print_string ("? " ^ CicPp.ppterm term ^ nl);
  83          print_string (Lev.string_of_levels (Lev.levels_of_term [] [] term) nl);
  84          flush stdout
  85    in
  86    levels_aux l
  87
  88 let execute ich =
  89    let module Util = MQueryUtil in
  90    let module Gen = MQueryGenerator in
  91    Gen.set_confirm_query default_confirm;
  92    try
  93       let q = Util.query_of_text (Lexing.from_channel ich) in
  94       print_endline (Util.text_of_result (Gen.execute_query q) nl);
  95       flush stdout
  96    with Gen.Discard -> ()
  97
  98 let locate name =
  99    let module Util = MQueryUtil in
 100    let module Gen = MQueryGenerator in
 101    Gen.set_confirm_query default_confirm;
 102    try
 103       print_endline (Util.text_of_result (Gen.locate name) nl);
 104       flush stdout
 105    with Gen.Discard -> ()
 106
 107 let mbackward n m l =
 108    let module Util = MQueryUtil in
 109    let module Gen = MQueryGenerator in
 110    let queries = ref [] in
 111    let confirm query =
 112       if List.mem query ! queries then false
 113       else begin queries := query :: ! queries; default_confirm query end
 114    in
 115    let rec backward level = function
 116       | []           -> ()
 117       | term :: tail ->
 118          backward level tail;
 119          try
 120             if Mqint.get_stat () then
 121                print_string ("? " ^ CicPp.ppterm term ^ nl);
 122             let t0 = Sys.time () in
 123             let r = Gen.searchPattern [] [] term level in
 124             let t1 = Sys.time () -. t0 in
 125             let info = Gen.get_query_info () in
 126             let num = List.nth info 0 in
 127             let gen = List.nth info 1 in
 128             if Mqint.get_stat () then
 129                print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl);
 130             print_string (Util.text_of_result r nl);
 131             flush stdout
 132          with Gen.Discard -> ()
 133    in
 134    Gen.set_confirm_query confirm;
 135    for level = max m n downto min m n do
 136       prerr_endline ("toplevel: backward: trying level " ^
 137                      string_of_int level);
 138       backward level l
 139    done;
 140    prerr_endline ("toplevel: backward: " ^
 141                   string_of_int (List.length ! queries) ^
 142                   " queries issued")
 143
 144 let prerr_help () =
 145    prerr_endline "\nUSAGE: toplevel.opt OPTIONS < INPUTFILE\n";
 146    prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
 147    prerr_endline "testing purposes. Toplevel reads its input from stdin and produces ith output";
 148    prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
 149    prerr_endline "OPTIONS:\n";
 150    prerr_endline "-h  -help               shows this help message";
 151    prerr_endline "-q  -show-queries       outputs generated queries";
 152    prerr_endline "-s  -stat               outputs interpreter statistics";
 153    prerr_endline "-c  -db-check           checks the database connection";
 154    prerr_endline "-i  -interpreter NUMBER sets the dbms to be used (default 1)";
 155    prerr_endline "-r  -restricted -nodb   enables restricted mode: queries are not issued";
 156    prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
 157    prerr_endline "-x  -execute            issues a query given in the input file";
 158    prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
 159    prerr_endline "-l  -levels             outputs the cut levels of the CIC terms given in the input file";
 160    prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
 161    prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all CIC terms";
 162    prerr_endline "                        in the input file";
 163    prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all";
 164    prerr_endline "                        CIC terms in the input file\n";
 165    prerr_endline "NOTES: interpreter numbers are 1 for postgres and 2 for galax";
 166    prerr_endline "       CIC terms are read with the HELM CIC Textual Parser";
 167    prerr_endline "       -typeof does not work with inductive types and proofs in progress\n"
 168
 169 let parse_args () =
 170    let rec parse = function
 171       | [] -> ()
 172       | ("-h"|"-help") :: rem -> prerr_help ()
 173       | ("-d"|"-display") :: rem -> display (get_terms ())
 174       | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
 175       | ("-l"|"-levels") :: rem -> levels (get_terms ())
 176       | ("-x"|"-execute") :: rem -> execute stdin; parse rem
 177       | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
 178       | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem
 179       | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem
 180       | ("-i"|"-interpreter") :: dbms :: rem -> set_dbms (int_of_string dbms); parse rem
 181       | ("-c"|"-db-check") :: rem -> dbc (); parse rem
 182       | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
 183       | ("-B"|"-backward") :: arg :: rem ->
 184          let m = (int_of_string arg) in
 185          mbackward m m (get_terms ())
 186       | ("-MB"|"-multi-backward") :: arg :: rem ->
 187          let m = (int_of_string arg) in
 188          mbackward m 0 (get_terms ())
 189       | _ :: rem -> parse rem
 190    in
 191       parse (List.tl (Array.to_list Sys.argv))
 192
 193 let _ =
 194    let module Gen = MQueryGenerator in
 195    Logger.log_callback :=
 196       (Logger.log_to_html
 197       ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
 198    Mqint.set_stat false;
 199    Gen.set_log_file "MQGenLog.htm";
 200    set_dbms 1;
 201    parse_args ();
 202    if not ! db_down then Mqint.close ();
 203    Gen.set_confirm_query (fun _ -> true);
 204    prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^
 205                   " seconds");
 206    exit 0