]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_test/mqgtop.ml
MathQL 1.3 ready for use
[helm.git] / helm / ocaml / mathql_test / mqgtop.ml
index be35ac6c874586a74d165989c8722599cf85b265..9e1dcde0d99dba624ffc4225169dc9ca33d55915 100644 (file)
@@ -38,17 +38,22 @@ let int_options = ref ""
 
 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 () =
@@ -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 "MH"; G.builtin "IH";
+                    G.builtin "MC"; G.builtin "IC"] 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,35 @@ 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 "MC" else G.builtin "IC" in
       (u, p, None)
    in
+   let univ = Some [G.builtin "MC"; G.builtin "IC"] 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 +227,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 +253,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 +280,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