(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+let _ = MQueryStandard.init
+let _ = MQueryHELM.init
+
let query_num = ref 1
let interp_file = ref "interp.cic"
module C2 = CGSearchPattern
module C1 = CGMatchConclusion
module GU = MQGUtil
+module M = MQueryMisc
let get_handle () =
C.init (C.flags_of_string ! int_options)
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
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";
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
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