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