1 let connection_param = "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
3 let show_queries = ref false
13 if ! use_db then begin Mqint.init connection_param; db_down := false; true end
14 else begin print_endline "Not issuing in restricted mode"; false end
17 let default_confirm q =
18 let module Util = MQueryUtil in
19 if ! show_queries then print_string (Util.text_of_query q ^ nl);
20 let b = check_db () in
21 if ! db_down then print_endline "db_down"; b
25 let lexbuf = Lexing.from_channel stdin in
29 CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
32 [] -> terms := (snd (mk_term (function _ -> None))) :: !terms
37 CicTextualParser0.Eof -> ! terms
40 let u = UriManager.uri_of_string uri in
41 let s = match (CicEnvironment.get_obj u) with
42 | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
43 | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
44 | _ -> "Current proof or inductive definition."
46 | Cic.CurrentProof (_,conjs,te,ty) ->
47 | C.InductiveDefinition _ ->
49 in print_endline s; flush stdout
52 if i = 1 then Mqint.set_database Mqint.postgres_db else
53 if i = 2 then Mqint.set_database Mqint.galax_db else ()
56 if s = Mqint.postgres_db then 1 else
57 if s = Mqint.galax_db then 2 else 0
60 let on = check_db () in
63 let dbms = Mqint.get_database () in
64 prerr_endline ("toplevel: current dbms is n." ^
65 string_of_int (get_dbms dbms) ^ " (" ^ dbms ^ ")");
69 let rec display = function
73 print_string ("? " ^ CicPp.ppterm term ^ nl);
77 let module Lev = MQueryLevels in
78 let rec levels_aux = function
82 print_string ("? " ^ CicPp.ppterm term ^ nl);
83 print_string (Lev.string_of_levels (Lev.levels_of_term [] [] term) nl);
89 let module Util = MQueryUtil in
90 let module Gen = MQueryGenerator in
91 Gen.set_confirm_query default_confirm;
93 let q = Util.query_of_text (Lexing.from_channel ich) in
94 print_endline (Util.text_of_result (Gen.execute_query q) nl);
96 with Gen.Discard -> ()
99 let module Util = MQueryUtil in
100 let module Gen = MQueryGenerator in
101 Gen.set_confirm_query default_confirm;
103 print_endline (Util.text_of_result (Gen.locate name) nl);
105 with Gen.Discard -> ()
107 let mbackward n m l =
108 let module Util = MQueryUtil in
109 let module Gen = MQueryGenerator in
110 let queries = ref [] in
112 if List.mem query ! queries then false
113 else begin queries := query :: ! queries; default_confirm query end
115 let rec backward level = function
120 if Mqint.get_stat () then
121 print_string ("? " ^ CicPp.ppterm term ^ nl);
122 let t0 = Sys.time () in
123 let list_of_must,can = MQueryLevels.out_restr [] [] term in
124 let len = List.length list_of_must in
125 let must = if level < len then List.nth list_of_must level else can in
126 let r = Gen.searchPattern [] [] term must can in
127 let t1 = Sys.time () -. t0 in
128 let info = Gen.get_query_info () in
129 let num = List.nth info 0 in
130 let gen = List.nth info 1 in
131 if Mqint.get_stat () then
132 print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl);
133 print_string (Util.text_of_result r nl);
135 with Gen.Discard -> ()
137 Gen.set_confirm_query confirm;
138 for level = max m n downto min m n do
139 prerr_endline ("toplevel: backward: trying level " ^
140 string_of_int level);
143 prerr_endline ("toplevel: backward: " ^
144 string_of_int (List.length ! queries) ^
148 prerr_endline "\nUSAGE: toplevel.opt OPTIONS < INPUTFILE\n";
149 prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
150 prerr_endline "testing purposes. Toplevel reads its input from stdin and produces ith output";
151 prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
152 prerr_endline "OPTIONS:\n";
153 prerr_endline "-h -help shows this help message";
154 prerr_endline "-q -show-queries outputs generated queries";
155 prerr_endline "-s -stat outputs interpreter statistics";
156 prerr_endline "-c -db-check checks the database connection";
157 prerr_endline "-i -interpreter NUMBER sets the dbms to be used (default 1)";
158 prerr_endline "-r -restricted -nodb enables restricted mode: queries are not issued";
159 prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object";
160 prerr_endline "-x -execute issues a query given in the input file";
161 prerr_endline "-d -disply outputs the CIC terms given in the input file";
162 prerr_endline "-l -levels outputs the cut levels of the CIC terms given in the input file";
163 prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias";
164 prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all CIC terms";
165 prerr_endline " in the input file";
166 prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all";
167 prerr_endline " CIC terms in the input file\n";
168 prerr_endline "NOTES: interpreter numbers are 1 for postgres and 2 for galax";
169 prerr_endline " CIC terms are read with the HELM CIC Textual Parser";
170 prerr_endline " -typeof does not work with inductive types and proofs in progress\n"
173 let rec parse = function
175 | ("-h"|"-help") :: rem -> prerr_help ()
176 | ("-d"|"-display") :: rem -> display (get_terms ())
177 | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
178 | ("-l"|"-levels") :: rem -> levels (get_terms ())
179 | ("-x"|"-execute") :: rem -> execute stdin; parse rem
180 | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
181 | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem
182 | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem
183 | ("-i"|"-interpreter") :: dbms :: rem -> set_dbms (int_of_string dbms); parse rem
184 | ("-c"|"-db-check") :: rem -> dbc (); parse rem
185 | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
186 | ("-B"|"-backward") :: arg :: rem ->
187 let m = (int_of_string arg) in
188 mbackward m m (get_terms ())
189 | ("-MB"|"-multi-backward") :: arg :: rem ->
190 let m = (int_of_string arg) in
191 mbackward m 0 (get_terms ())
192 | _ :: rem -> parse rem
194 parse (List.tl (Array.to_list Sys.argv))
197 let module Gen = MQueryGenerator in
198 Logger.log_callback :=
200 ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
201 Mqint.set_stat false;
202 Gen.set_log_file "MQGenLog.htm";
205 if not ! db_down then Mqint.close ();
206 Gen.set_confirm_query (fun _ -> true);
207 prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^