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 Util.text_of_query print_string 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 execute ich =
  77    let module Util = MQueryUtil in
  78    let module Gen = MQueryGenerator in
  79    Gen.set_confirm_query default_confirm;
  80    try
  81       let q = Util.query_of_text (Lexing.from_channel ich) in
  82       Util.text_of_result print_string (Gen.execute_query q) nl;
  83       flush stdout
  84    with Gen.Discard -> ()
  85
  86 let locate name =
  87    let module Util = MQueryUtil in
  88    let module Gen = MQueryGenerator in
  89    Gen.set_confirm_query default_confirm;
  90    try
  91       Util.text_of_result print_string (Gen.locate name) nl;
  92       flush stdout
  93    with Gen.Discard -> ()
  94
  95 let mbackward n m l =
  96    let module Util = MQueryUtil in
  97    let module Gen = MQueryGenerator in
  98    let queries = ref [] in
  99    let confirm query =
 100       if List.mem query ! queries then false
 101       else begin queries := query :: ! queries; default_confirm query end
 102    in
 103    let rec backward level = function
 104       | []           -> ()
 105       | term :: tail ->
 106          backward level tail;
 107          try
 108             if Mqint.get_stat () then
 109                print_string ("? " ^ CicPp.ppterm term ^ nl);
 110             let t0 = Sys.time () in
 111
 112
 113
 114
 115 (* FG: Mettere a posto qui.
 116             let list_of_must,can = MQueryLevels.out_restr [] [] term in
 117             let len = List.length list_of_must in
 118             let must = if level < len then List.nth list_of_must level else can in
 119 *)
 120
 121             let r = [] (* FG e anche qui: Gen.searchPattern must can *) in
 122             let t1 = Sys.time () -. t0 in
 123             let info = Gen.get_query_info () in
 124             let num = List.nth info 0 in
 125             let gen = List.nth info 1 in
 126             if Mqint.get_stat () then
 127                print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl);
 128             Util.text_of_result print_string r nl;
 129             flush stdout
 130          with Gen.Discard -> ()
 131    in
 132    Gen.set_confirm_query confirm;
 133    for level = max m n downto min m n do
 134       prerr_endline ("toplevel: backward: trying level " ^
 135                      string_of_int level);
 136       backward level l
 137    done;
 138    prerr_endline ("toplevel: backward: " ^
 139                   string_of_int (List.length ! queries) ^
 140                   " queries issued")
 141
 142 let prerr_help () =
 143    prerr_endline "\nUSAGE: toplevel.opt OPTIONS < INPUTFILE\n";
 144    prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
 145    prerr_endline "testing purposes. Toplevel reads its input from stdin and produces ith output";
 146    prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
 147    prerr_endline "OPTIONS:\n";
 148    prerr_endline "-h  -help               shows this help message";
 149    prerr_endline "-q  -show-queries       outputs generated queries";
 150    prerr_endline "-s  -stat               outputs interpreter statistics";
 151    prerr_endline "-c  -db-check           checks the database connection";
 152    prerr_endline "-i  -interpreter NUMBER sets the dbms to be used (default 1)";
 153    prerr_endline "-r  -restricted -nodb   enables restricted mode: queries are not issued";
 154    prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
 155    prerr_endline "-x  -execute            issues a query given in the input file";
 156    prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
 157    prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
 158    prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all CIC terms";
 159    prerr_endline "                        in the input file";
 160    prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all";
 161    prerr_endline "                        CIC terms in the input file\n";
 162    prerr_endline "NOTES: interpreter numbers are 1 for postgres and 2 for galax";
 163    prerr_endline "       CIC terms are read with the HELM CIC Textual Parser";
 164    prerr_endline "       -typeof does not work with inductive types and proofs in progress\n"
 165
 166 let parse_args () =
 167    let rec parse = function
 168       | [] -> ()
 169       | ("-h"|"-help") :: rem -> prerr_help ()
 170       | ("-d"|"-display") :: rem -> display (get_terms ())
 171       | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
 172       | ("-x"|"-execute") :: rem -> execute stdin; parse rem
 173       | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
 174       | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem
 175       | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem
 176       | ("-i"|"-interpreter") :: dbms :: rem -> set_dbms (int_of_string dbms); parse rem
 177       | ("-c"|"-db-check") :: rem -> dbc (); parse rem
 178       | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
 179       | ("-B"|"-backward") :: arg :: rem ->
 180          let m = (int_of_string arg) in
 181          mbackward m m (get_terms ())
 182       | ("-MB"|"-multi-backward") :: arg :: rem ->
 183          let m = (int_of_string arg) in
 184          mbackward m 0 (get_terms ())
 185       | _ :: rem -> parse rem
 186    in
 187       parse (List.tl (Array.to_list Sys.argv))
 188
 189 let _ =
 190    let module Gen = MQueryGenerator in
 191    Logger.log_callback :=
 192       (Logger.log_to_html
 193       ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
 194    Mqint.set_stat false;
 195    Gen.set_log_file "MQGenLog.htm";
 196    set_dbms 1;
 197    parse_args ();
 198    if not ! db_down then Mqint.close ();
 199    Gen.set_confirm_query (fun _ -> true);
 200    prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^
 201                   " seconds");
 202    exit 0