From c4569c7b0745a53324e6f4375b7cc5795031f6fd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 17 Sep 2002 10:46:30 +0000 Subject: [PATCH] new toplevel with -help option instead of the Readme --- helm/gTopLevel/topLevel/topLevel.ml | 129 ++++++++++++++++++++-------- 1 file changed, 94 insertions(+), 35 deletions(-) diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml index 9992e4093..57c9d41bf 100644 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -1,15 +1,22 @@ +let show_queries = ref false + let use_db = ref true let db_down = ref true +let nl = "

\n" + let check_db () = - if ! db_down then begin - if ! use_db then begin - MQueryGenerator.init (); db_down := false - end else - raise (Failure "Operation impossible in restricted mode") - end - + if ! db_down then + if ! use_db then begin Mqint.init (); 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); + check_db () + let get_terms () = let terms = ref [] in let lexbuf = Lexing.from_channel stdin in @@ -39,42 +46,68 @@ let pp_type_of uri = *) in print_endline s; flush stdout -let locate name = - check_db (); - print_endline (MQueryGenerator.locate_html name); - flush stdout - 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 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 - -let mbackward n m l = + 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 + print_string ("? " ^ CicPp.ppterm term ^ nl); + try + let t0 = Sys.time () in + let r = Gen.backward [] [] term level in + let t1 = Sys.time () -. t0 in + let info = List.nth (Gen.get_query_info ()) 0 in + print_string ("GEN = " ^ info ^ ":" ^ string_of_float t1 ^ "s" ^ nl); + print_string (Util.text_of_result r nl); + flush stdout + with Gen.Discard -> () in - check_db (); - 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); @@ -82,21 +115,44 @@ 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 the generated queries"; + 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: 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 ()) - | ("-r"|"-restricted") :: rem -> use_db := false; parse rem + | ("-x"|"-execute") :: rem -> execute stdin; parse rem + | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem + | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; 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 @@ -104,12 +160,15 @@ 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)) ; + Gen.set_log_file "MQGenLog.htm"; parse_args (); - if not ! db_down then 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 -- 2.39.2