let nl = " <p>\n"
-module MQX = MQueryMisc
-module MQI = MQueryInterpreter
-module MQIC = MQIConn
-module MQG = MQueryGenerator
+module U = MQueryUtil
+module I = MQueryInterpreter
+module C = MQIConn
+module G = MQueryGenerator
+module L = MQGTopLexer
+module P = MQGTopParser
+module TL = CicTextualLexer
+module TP = CicTextualParser
+module C2 = MQueryLevels2
+module C1 = MQueryLevels
let get_handle () =
- MQIC.init (MQIC.flags_of_string ! int_options)
- (fun s -> print_string s; flush stdout)
+ C.init (C.flags_of_string ! int_options)
+ (fun s -> print_string s; flush stdout)
let issue handle q =
- let module U = MQueryUtil in
let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
let perm = 64 * 6 + 8 * 6 + 4 in
let time () =
close_out och
in
if ! show_queries then U.text_of_query (output_string stdout) q nl;
- let r = MQI.execute handle q in
+ let r = I.execute handle q in
U.text_of_result (output_string stdout) r nl;
if ! log_file <> "" then log q r;
incr query_num;
flush stdout
let get_interp () =
- let module L = CicTextualLexer in
- let module T = CicTextualParser in
- let module P = MQGTopParser in
let lexer = function
- | T.ID s -> P.ID s
- | T.CONURI u -> P.CONURI u
- | T.VARURI u -> P.VARURI u
- | T.INDTYURI (u, p) -> P.INDTYURI (u, p)
- | T.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s)
- | T.LETIN -> P.ALIAS
- | T.EOF -> P.EOF
+ | TP.ID s -> P.ID s
+ | TP.CONURI u -> P.CONURI u
+ | TP.VARURI u -> P.VARURI u
+ | TP.INDTYURI (u, p) -> P.INDTYURI (u, p)
+ | TP.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s)
+ | TP.LETIN -> P.ALIAS
+ | TP.EOF -> P.EOF
| _ -> assert false
in
let ich = open_in ! interp_file in
let lexbuf = Lexing.from_channel ich in
- let f = P.interp (fun x -> lexer (L.token x)) lexbuf in
+ let f = P.interp (fun x -> lexer (TL.token x)) lexbuf in
close_in ich; f
let get_terms interp =
flush stdout
let execute ich =
- let module U = MQueryUtil in
let lexbuf = Lexing.from_channel ich in
let handle = get_handle () in
let rec execute_aux () =
with End_of_file -> ()
in
execute_aux ();
- MQIC.close handle
-(*
+ C.close handle
+
let compose () =
- let module P = MQGTopParser in
- let module L = MQGTopLexer in
- let module G = MQueryGeneratorNew in
+ let handle = get_handle () in
let cl = P.specs L.spec_token (Lexing.from_channel stdin) in
- issue (G.compose cl)
-*)
+ issue handle (G.compose cl);
+ C.close handle
+
let locate name =
let handle = get_handle () in
- issue handle (MQG.locate name);
- MQIC.close handle
+ issue handle (G.locate name);
+ C.close handle
let mpattern n m l =
- let module C = MQueryLevels2 in
let queries = ref [] in
+ let univ = Some [G.builtin G.MainHypothesis; G.builtin G.InHypothesis;
+ G.builtin G.MainConclusion; G.builtin G.InConclusion] in
let handle = get_handle () in
let rec pattern level = function
| [] -> ()
| term :: tail ->
pattern level tail;
print_string ("? " ^ CicPp.ppterm term ^ nl);
- let t = MQX.start_time () in
- let om,rm,sm = C.get_constraints term in
+ let t = U.start_time () in
+ let om,rm,sm = C2.get_constraints term in
let oml,rml,sml = List.length om, List.length rm, List.length sm in
let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in
let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in
let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in
- let q = MQG.query_of_constraints None (om,rm,sm) (oo,ro,so) in
+ let q = G.query_of_constraints univ (om,rm,sm) (oo,ro,so) in
if not (List.mem q ! queries) then
begin
issue handle q;
Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
Printf.printf "%i GEN = %i: %s"
(pred ! query_num) (oml + rml + sml + ool + rol + sol)
- (MQX.stop_time t ^ nl);
+ (U.stop_time t ^ nl);
flush stdout; queries := q :: ! queries
end
in
Printf.eprintf "\nmqgtop: pattern: %i queries issued\n"
(List.length ! queries);
flush stderr;
- MQIC.close handle
-(*
+ C.close handle
+
let mbackward n m l =
- let module C = MQueryLevels in
- let module G = MQueryGenerator in
let queries = ref [] in
let torigth_restriction (u, b) =
- let p = if b
- then "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
- else "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
- in
+ let p = if b then G.builtin G.MainConclusion
+ else G.builtin G.InConclusion in
(u, p, None)
in
+ let univ = Some [G.builtin G.MainConclusion; G.builtin G.InConclusion] in
+ let handle = get_handle () in
let rec backward level = function
| [] -> ()
| term :: tail ->
backward level tail;
print_string ("? " ^ CicPp.ppterm term ^ nl);
- let t0 = Sys.time () in
- let list_of_must, only = C.out_restr [] [] term in
+ let t = U.start_time () in
+ let list_of_must, only = C1.out_restr [] [] term in
let max_level = pred (List.length list_of_must) in
let must = List.nth list_of_must (min level max_level) in
let rigth_must = List.map torigth_restriction must in
let rigth_only = Some (List.map torigth_restriction only) in
- let q = G.searchPattern (rigth_must, [], []) (rigth_only , None, None) in
+ let q = G.query_of_constraints univ (rigth_must, [], []) (rigth_only , None, None) in
if not (List.mem q ! queries) then
begin
- issue q;
- let t1 = Sys.time () -. t0 in
+ issue handle q;
Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
- Printf.printf "%i GEN = %i: %.2fs%s"
- (pred ! query_num) (List.length must) t1 nl;
+ Printf.printf "%i GEN = %i: %s"
+ (pred ! query_num) (List.length must)
+ (U.stop_time t ^ nl);
flush stdout; queries := q :: ! queries
end
in
done;
Printf.eprintf "\nmqgtop: backward: %i queries issued\n"
(List.length ! queries);
- flush stderr
-*)
-
+ flush stderr;
+ C.close handle
+
let check () =
let handle = get_handle () in
Printf.eprintf
"mqgtop: current options: %s, connection: %s\n"
- ! int_options (if MQIC.connected handle then "on" else "off");
- MQIC.close handle
+ ! int_options (if C.connected handle then "on" else "off");
+ C.close handle
let prerr_help () =
prerr_endline "\nUSAGE: mqgtop.opt OPTIONS < INPUTFILE\n";
prerr_endline "-i -interp FILE sets the CIC short names interpretation file";
prerr_endline "-d -disply outputs the CIC terms given in the input file";
prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias";
-(* prerr_endline "-C -compose issues the \"Compose\" query reading its specifications";
+ prerr_endline "-C -compose issues the \"Compose\" query reading its specifications";
prerr_endline " from the input file";
prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all";
prerr_endline " CIC terms in the input file";
prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0";
prerr_endline " on all CIC terms in the input file";
-*) prerr_endline "-P -pattern LEVEL issues the \"Pattern\" query for the given level on all";
+ prerr_endline "-P -pattern LEVEL issues the \"Pattern\" query for the given level on all";
prerr_endline " CIC terms in the input file";
prerr_endline "-MP -multi-pattern issues the \"Pattern\" query for each level from 7 to 0";
prerr_endline " on all CIC terms in the input file\n";
| ("-c"|"-check") :: rem -> check (); parse rem
| ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem
| ("-L"|"-Locate") :: arg :: rem -> locate arg; parse rem
-(* | ("-C"|"-compose") :: rem -> compose (); parse rem
+ | ("-C"|"-compose") :: rem -> compose (); parse rem
| ("-M"|"-backward") :: arg :: rem ->
let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem
| ("-MB"|"-multi-backward") :: arg :: rem ->
let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem
-*) | ("-P"|"-pattern") :: arg :: rem ->
+ | ("-P"|"-pattern") :: arg :: rem ->
let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem
| ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem
| _ :: rem -> parse rem
let _ =
- let t = MQX.start_time () in
+ let t = U.start_time () in
Logger.log_callback :=
(Logger.log_to_html
~print_and_flush:(fun s -> print_string s; flush stdout)) ;
parse (List.tl (Array.to_list Sys.argv));
- prerr_endline ("mqgtop: done in " ^ (MQX.stop_time t));
+ prerr_endline ("mqgtop: done in " ^ (U.stop_time t));
exit 0