+++ /dev/null
-let connection_param = "host=mowgli.cs.unibo.it dbname=helm 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 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
- try
- while true do
- match CicTextualParserContext.main
- (UriManager.uri_of_string "cic:/dummy") [] []
- CicTextualLexer.token lexbuf
- with
- | None -> ()
- | Some (_, expr) -> terms := expr :: ! terms
- done;
- ! terms
- with
- CicTextualParser0.Eof -> ! terms
-
-let pp_type_of uri =
- let u = UriManager.uri_of_string uri in
- let s = match (CicEnvironment.get_obj u) with
- | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty
- | Cic.Axiom (_, 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_string ("? " ^ CicPp.ppterm term ^ nl);
- flush stdout
-
-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 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 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
- 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
- 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 -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"|"-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 _ =
- let module Gen = MQueryGenerator in
- CicCooking.init () ;
- Logger.log_callback :=
- (Logger.log_to_html
- ~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 ();
- 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 / commitdiff