X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_test%2Fmqgtop.ml;h=0ef1ca981f4f86377d3aac9141b5d773e18a8def;hb=65e3c9976212e04a4678ff9ce9e3c2f436d06d33;hp=be35ac6c874586a74d165989c8722599cf85b265;hpb=cab4eba3c7da115ecc1973d989b321b46835e1eb;p=helm.git diff --git a/helm/ocaml/mathql_test/mqgtop.ml b/helm/ocaml/mathql_test/mqgtop.ml index be35ac6c8..0ef1ca981 100644 --- a/helm/ocaml/mathql_test/mqgtop.ml +++ b/helm/ocaml/mathql_test/mqgtop.ml @@ -38,17 +38,22 @@ let int_options = ref "" let nl = "

\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 () = @@ -72,29 +77,26 @@ let issue handle q = 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 = @@ -131,7 +133,6 @@ let rec display = function 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 () = @@ -141,43 +142,43 @@ let execute ich = 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 @@ -188,38 +189,36 @@ let mpattern n m l = 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 @@ -229,15 +228,15 @@ let mbackward n m l = 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"; @@ -255,13 +254,13 @@ let prerr_help () = 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"; @@ -282,21 +281,21 @@ let rec parse = function | ("-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