From ac37389ba6b4ef90aed1244de37b254645c51ab1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 24 Jun 2003 09:31:01 +0000 Subject: [PATCH] No longer in use. --- helm/gTopLevel/topLevel/topLevel.ml | 208 ---------------------------- 1 file changed, 208 deletions(-) delete mode 100644 helm/gTopLevel/topLevel/topLevel.ml diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml deleted file mode 100644 index 6db896d9b..000000000 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ /dev/null @@ -1,208 +0,0 @@ -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 = "

\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 -- 2.39.2