+let connection_param = "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
+
+let show_queries = ref false
+
+let use_db = ref true
+
+let db_down = ref true
+
+let nl = " <p>\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 Util.text_of_query print_string 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
try
while true do
- match CicTextualParser.main CicTextualLexer.token lexbuf with
- | None -> ()
- | Some expr -> terms := expr :: ! terms
- done;
+ let dom,mk_term =
+ CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
+ in
+ match dom with
+ [] -> terms := (snd (mk_term (function _ -> None))) :: !terms
+ | _ -> assert false
+ done ;
! terms
with
CicTextualParser0.Eof -> ! terms
-let locate name =
- print_endline (MQueryGenerator.locate name);
- flush stdout
+let pp_type_of uri =
+ let u = UriManager.uri_of_string uri in
+ let s = match (CicEnvironment.get_obj u) with
+ | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
+ | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
+ | _ -> "Current proof or inductive definition."
+(*
+ | Cic.CurrentProof (_,conjs,te,ty) ->
+ | C.InductiveDefinition _ ->
+*)
+ in print_endline s; 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 ^ "<p>");
+ print_string ("? " ^ CicPp.ppterm term ^ nl);
flush stdout
-let rec levels level = function
- | [] -> ()
- | term :: tail ->
- levels level tail;
- print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
- print_endline (MQueryGenerator.levels [] [] term level);
+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
+ Util.text_of_result print_string (Gen.execute_query q) nl;
flush stdout
+ with Gen.Discard -> ()
-let rec backward level = function
- | [] -> ()
- | term :: tail ->
- backward level tail;
- print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
- print_endline (MQueryGenerator.backward [] [] term level);
+let locate name =
+ let module Util = MQueryUtil in
+ let module Gen = MQueryGenerator in
+ Gen.set_confirm_query default_confirm;
+ try
+ Util.text_of_result print_string (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 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;
+ try
+ if Mqint.get_stat () then
+ print_string ("? " ^ CicPp.ppterm term ^ nl);
+ let t0 = Sys.time () in
+
+
+
+
+(* FG: Mettere a posto qui.
+ let list_of_must,can = MQueryLevels.out_restr [] [] term in
+ let len = List.length list_of_must in
+ let must = if level < len then List.nth list_of_must level else can in
+*)
+
+ let r = [] (* FG e anche qui: Gen.searchPattern must can *) 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);
+ Util.text_of_result print_string r nl;
+ flush stdout
+ with Gen.Discard -> ()
+ in
+ 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);
+ backward level l
+ done;
+ prerr_endline ("toplevel: backward: " ^
+ string_of_int (List.length ! queries) ^
+ " 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 -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
| [] -> ()
- | ("-l"|"-locate") :: arg :: rem ->
- locate arg; parse rem
- | ("-d"|"-display") :: rem ->
- display (get_terms ())
- | ("-t"|"-test") :: arg :: rem ->
- levels (int_of_string arg) (get_terms ())
- | ("-b"|"-backward") :: arg :: rem ->
- backward (int_of_string arg) (get_terms ())
+ | ("-h"|"-help") :: rem -> prerr_help ()
+ | ("-d"|"-display") :: rem -> display (get_terms ())
+ | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
+ | ("-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"|"-multi-backward") :: arg :: rem ->
+ let m = (int_of_string arg) in
+ mbackward m 0 (get_terms ())
| _ :: rem -> parse rem
in
parse (List.tl (Array.to_list Sys.argv))
let _ =
- CicCooking.init () ;
+ let module Gen = MQueryGenerator in
Logger.log_callback :=
(Logger.log_to_html
~print_and_flush:(function s -> print_string s ; flush stdout)) ;
- MQueryGenerator.init ();
+ 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
-;;
projects / helm.git / blobdiff