]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/topLevel/topLevel.ml
MathQL query generator: new interface
[helm.git] / helm / gTopLevel / topLevel / topLevel.ml
index 78aceae26f52ecafd4d53e07055e688bcda95737..06ef93ab5f5571ec27a9455a2a7147c9773d7974 100644 (file)
@@ -1,4 +1,4 @@
-let connection_param = "host=mowgli.cs.unibo.it dbname=helm user=helm"
+let connection_param = "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
 
 let show_queries = ref false
 
@@ -16,7 +16,7 @@ let check_db () =
 
 let default_confirm q =
    let module Util = MQueryUtil in   
-   if ! show_queries then print_string (Util.text_of_query q ^ nl);
+   if ! show_queries then Util.text_of_query print_string q nl;
    let b = check_db () in
    if ! db_down then print_endline "db_down"; b 
 
@@ -25,13 +25,13 @@ let get_terms () =
    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;
+       let dom,mk_term =
+        CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
+       in
+        match dom with
+          [] -> terms := (snd (mk_term (function _ -> None))) :: !terms
+        | _ -> assert false
+      done ;
       ! terms
    with
       CicTextualParser0.Eof -> ! terms
@@ -73,25 +73,13 @@ let rec display = function
       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);
+      Util.text_of_result print_string (Gen.execute_query q) nl;
       flush stdout
    with Gen.Discard -> ()
 
@@ -100,7 +88,7 @@ let locate name =
    let module Gen = MQueryGenerator in
    Gen.set_confirm_query default_confirm;
    try 
-      print_endline (Util.text_of_result (Gen.locate name) nl);
+      Util.text_of_result print_string (Gen.locate name) nl;
       flush stdout
    with Gen.Discard -> ()
 
@@ -120,14 +108,24 @@ let mbackward n m l =
            if Mqint.get_stat () then 
               print_string ("? " ^ CicPp.ppterm term ^ nl);
            let t0 = Sys.time () in
-            let r = Gen.backward [] [] term level in
+           
+           
+           
+           
+(* FG: Mettere a posto qui.
+           let list_of_must,can = MQueryLevels.out_restr [] [] term in
+           let len = List.length list_of_must in
+           let must = if level < len then List.nth list_of_must level else can in
+*)        
+          
+           let r = [] (* FG e anche qui: Gen.searchPattern must can *) 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);
+           Util.text_of_result print_string r nl;
             flush stdout
         with Gen.Discard -> ()
    in
@@ -156,7 +154,6 @@ let prerr_help () =
    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";
@@ -172,7 +169,6 @@ let parse_args () =
       | ("-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
@@ -192,7 +188,6 @@ let parse_args () =
 
 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)) ;