+ 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"
+