\n" + +let check_db () = + if ! db_down then + if ! use_db then begin Mqint.init connection_param; db_down := false; true end + else begin print_endline "Not issuing in restricted mode"; false end + else true + +let default_confirm q = + let module Util = MQueryUtil in + if ! show_queries then print_string (Util.text_of_query q ^ nl); + let b = check_db () in + if ! db_down then print_endline "db_down"; b + let get_terms () = let terms = ref [] in let lexbuf = Lexing.from_channel stdin in @@ -27,40 +49,90 @@ let pp_type_of uri = *) in print_endline s; flush stdout -let locate name = - print_endline (MQueryGenerator.locate name); - flush stdout +let set_dbms i = + if i = 1 then Mqint.set_database Mqint.postgres_db else + if i = 2 then Mqint.set_database Mqint.galax_db else () + +let get_dbms s = + if s = Mqint.postgres_db then 1 else + if s = Mqint.galax_db then 2 else 0 + +let dbc () = + let on = check_db () in + if on then + begin + let dbms = Mqint.get_database () in + prerr_endline ("toplevel: current dbms is n." ^ + string_of_int (get_dbms dbms) ^ " (" ^ dbms ^ ")"); + Mqint.check () + end let rec display = function | [] -> () | term :: tail -> display tail; - print_endline ("? " ^ CicPp.ppterm term ^ "
"); + print_string ("? " ^ CicPp.ppterm term ^ nl); flush stdout -let rec levels = function - | [] -> () - | term :: tail -> - levels tail; - print_endline ("? " ^ CicPp.ppterm term ^ "
"); - print_endline (MQueryGenerator.levels [] [] term); +let levels l = + let module Gen = MQueryGenerator in + let rec levels_aux = function + | [] -> () + | term :: tail -> + levels_aux tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + print_string (Gen.string_of_levels (Gen.levels_of_term [] [] term) nl); + flush stdout + in + levels_aux l + +let execute ich = + let module Util = MQueryUtil in + let module Gen = MQueryGenerator in + Gen.set_confirm_query default_confirm; + try + let q = Util.query_of_text (Lexing.from_channel ich) in + print_endline (Util.text_of_result (Gen.execute_query q) nl); flush stdout + with Gen.Discard -> () -let mbackward n m l = +let locate name = + let module Util = MQueryUtil in + let module Gen = MQueryGenerator in + Gen.set_confirm_query default_confirm; + try + print_endline (Util.text_of_result (Gen.locate name) nl); + flush stdout + with Gen.Discard -> () + +let mbackward n m l = + let module Util = MQueryUtil in + let module Gen = MQueryGenerator in let queries = ref [] in - let issue query = - if List.mem query ! queries then false - else begin queries := query :: ! queries; true end + let confirm query = + if List.mem query ! queries then false + else begin queries := query :: ! queries; default_confirm query end in let rec backward level = function | [] -> () | term :: tail -> backward level tail; - print_endline ("? " ^ CicPp.ppterm term ^ "
"); - print_endline (MQueryGenerator.backward [] [] term level); - flush stdout + try + if Mqint.get_stat () then + print_string ("? " ^ CicPp.ppterm term ^ nl); + let t0 = Sys.time () in + let r = Gen.backward [] [] term level in + let t1 = Sys.time () -. t0 in + let info = Gen.get_query_info () in + let num = List.nth info 0 in + let gen = List.nth info 1 in + if Mqint.get_stat () then + print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl); + print_string (Util.text_of_result r nl); + flush stdout + with Gen.Discard -> () in - MQueryGenerator.call_back issue; + Gen.set_confirm_query confirm; for level = max m n downto min m n do prerr_endline ("toplevel: backward: trying level " ^ string_of_int level); @@ -68,20 +140,51 @@ let mbackward n m l = done; prerr_endline ("toplevel: backward: " ^ string_of_int (List.length ! queries) ^ - " queries issued"); - MQueryGenerator.call_back (fun _ -> true) - + " queries issued") + +let prerr_help () = + prerr_endline "\nUSAGE: toplevel.opt OPTIONS < INPUTFILE\n"; + prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for"; + prerr_endline "testing purposes. Toplevel reads its input from stdin and produces ith output"; + prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n"; + prerr_endline "OPTIONS:\n"; + prerr_endline "-h -help shows this help message"; + prerr_endline "-q -show-queries outputs generated queries"; + prerr_endline "-s -stat outputs interpreter statistics"; + prerr_endline "-c -db-check checks the database connection"; + prerr_endline "-i -interpreter NUMBER sets the dbms to be used (default 1)"; + prerr_endline "-r -restricted -nodb enables restricted mode: queries are not issued"; + prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object"; + prerr_endline "-x -execute issues a query given in the input file"; + prerr_endline "-d -disply outputs the CIC terms given in the input file"; + prerr_endline "-l -levels outputs the cut levels of the CIC terms given in the input file"; + prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias"; + prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all CIC terms"; + prerr_endline " in the input file"; + prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all"; + prerr_endline " CIC terms in the input file\n"; + prerr_endline "NOTES: interpreter numbers are 1 for postgres and 2 for galax"; + prerr_endline " CIC terms are read with the HELM CIC Textual Parser"; + prerr_endline " -typeof does not work with inductive types and proofs in progress\n" + let parse_args () = let rec parse = function | [] -> () + | ("-h"|"-help") :: rem -> prerr_help () | ("-d"|"-display") :: rem -> display (get_terms ()) | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem | ("-l"|"-levels") :: rem -> levels (get_terms ()) + | ("-x"|"-execute") :: rem -> execute stdin; parse rem + | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem + | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem + | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem + | ("-i"|"-interpreter") :: dbms :: rem -> set_dbms (int_of_string dbms); parse rem + | ("-c"|"-db-check") :: rem -> dbc (); parse rem | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem | ("-B"|"-backward") :: arg :: rem -> let m = (int_of_string arg) in mbackward m m (get_terms ()) - | ("-MB"|"-mbackward") :: arg :: rem -> + | ("-MB"|"-multi-backward") :: arg :: rem -> let m = (int_of_string arg) in mbackward m 0 (get_terms ()) | _ :: rem -> parse rem @@ -89,13 +192,17 @@ let parse_args () = parse (List.tl (Array.to_list Sys.argv)) let _ = + let module Gen = MQueryGenerator in CicCooking.init () ; Logger.log_callback := (Logger.log_to_html - ~print_and_flush:(function s -> print_string s ; flush stdout)) ; - MQueryGenerator.init (); + ~print_and_flush:(function s -> () (* print_string s ; flush stdout *) )); + Mqint.set_stat false; + Gen.set_log_file "MQGenLog.htm"; + set_dbms 1; parse_args (); - MQueryGenerator.close (); + if not ! db_down then Mqint.close (); + Gen.set_confirm_query (fun _ -> true); prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^ " seconds"); exit 0