X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql_test%2Fmqgtop.ml;fp=helm%2Fmathql_test%2Fmqgtop.ml;h=16a5ea0a9862734c5965ca32096da18238ad1c4a;hb=381006cf8b418cfdeaf145ab7df9e8f2b19ae2e6;hp=ae06bc752b317f4f865d473e2afddba9400dc7b0;hpb=efdc3184ccd0738fe48aa0056fc444fba23329e8;p=helm.git

diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml
index ae06bc752..16a5ea0a9 100644
--- a/helm/mathql_test/mqgtop.ml
+++ b/helm/mathql_test/mqgtop.ml
@@ -26,6 +26,9 @@
 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  *)
 
+let _ = MQueryStandard.init
+let _ = MQueryHELM.init 
+
 let query_num = ref 1
 
 let interp_file = ref "interp.cic" 
@@ -51,6 +54,7 @@ module C3 = CGLocateInductive
 module C2 = CGSearchPattern
 module C1 = CGMatchConclusion
 module GU = MQGUtil
+module M  = MQueryMisc
 
 let get_handle () = 
    C.init (C.flags_of_string ! int_options)
@@ -116,16 +120,14 @@ let get_terms interp =
    in
    aux ()
 
-let pp_type_of uri = 
-   let u = UriManager.uri_of_string uri in  
-   let s = match (CicEnvironment.get_obj u) with
-      | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
-      | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
-      | _                          -> "Current proof or inductive definition."      
-(*
-      | Cic.CurrentProof (_,conjs,te,ty) ->
-      | C.InductiveDefinition _ ->
-*)
+let pp_term_of b uri = 
+   let s = try 
+      let body, ty = M.get_object (M.uriref_of_string uri) in
+      if b then CicPp.ppterm body else CicPp.ppterm ty 
+   with
+      | M.CurrentProof        -> "proof in progress"
+      | M.InductiveDefinition -> "inductive definition"
+      | M.IllFormedFragment   -> "ill formed fragment identifier"
    in print_endline s; flush stdout
 
 let rec display = function
@@ -277,6 +279,7 @@ let prerr_help () =
    prerr_endline "-o  -options STRING     sets the interpreter options";
    prerr_endline "-c  -check              checks the database connection";
    prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
+   prerr_endline "-b  -bodyof URI         outputs the CIC body of the given HELM object";
    prerr_endline "-x  -execute            issues a query given in the input file";
    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";
@@ -297,14 +300,15 @@ let prerr_help () =
    prerr_endline "NOTES: * current interpreter options are:";
    prerr_endline "         P (postgres), G (Galax), S (show statistics), Q (quiet)";
    prerr_endline "       * CIC terms are read with the HELM CIC Textual Parser";
-   prerr_endline "       * -typeof does not work with inductive types and proofs in progress\n"
+   prerr_endline "       * -typeof / -bodyof do not work with proofs in progress\n"
 
 let rec parse = function
    | [] -> ()
    | ("-h"|"-help") :: rem -> prerr_help (); parse rem
    | ("-i"|"-interp") :: arg :: rem -> interp_file := arg; parse rem
    | ("-d"|"-display") :: rem -> display (get_terms ()); parse rem
-   | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
+   | ("-t"|"-typeof") :: arg :: rem -> pp_term_of false arg; parse rem
+   | ("-b"|"-bodyof") :: arg :: rem -> pp_term_of true arg; parse rem
    | ("-x"|"-execute") :: rem -> execute stdin; parse rem
    | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
    | ("-o"|"-options") :: arg :: rem -> int_options := arg; parse rem
@@ -326,9 +330,9 @@ let rec parse = function
 
 let _ =
    let t = U.start_time () in
-   Logger.log_callback :=
+(*   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)); 
+*)   parse (List.tl (Array.to_list Sys.argv)); 
    prerr_endline ("mqgtop: done in " ^ (U.stop_time t));
    exit 0