X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql_test%2Fmqgtop.ml;h=16a5ea0a9862734c5965ca32096da18238ad1c4a;hb=381006cf8b418cfdeaf145ab7df9e8f2b19ae2e6;hp=9a7c8d9db87814db876f1deacd63cf4e866a7780;hpb=0e74e8e94eada756157addce67e4adeb8dff1feb;p=helm.git diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml index 9a7c8d9db..16a5ea0a9 100644 --- a/helm/mathql_test/mqgtop.ml +++ b/helm/mathql_test/mqgtop.ml @@ -26,6 +26,9 @@ (* AUTOR: Ferruccio Guidi *) +let _ = MQueryStandard.init +let _ = MQueryHELM.init + let query_num = ref 1 let interp_file = ref "interp.cic" @@ -38,6 +41,7 @@ let int_options = ref "" let nl = "

\n" +module IO = MQueryIO module U = MQueryUtil module I = MQueryInterpreter module C = MQIConn @@ -46,9 +50,11 @@ module L = MQGTopLexer module P = MQGTopParser module TL = CicTextualLexer module TP = CicTextualParser -module C2 = MQueryLevels2 -module C1 = MQueryLevels +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) @@ -72,14 +78,14 @@ let issue handle q = let out = output_string och in if ! query_num = 1 then out (time () ^ nl); out ("Query: " ^ string_of_int ! query_num ^ nl); - U.text_of_query out q nl; + IO.text_of_query out nl q; out ("Result: " ^ nl); - U.text_of_result out r nl; + IO.text_of_result out nl r; close_out och in - if ! show_queries then U.text_of_query (output_string stdout) q nl; + if ! show_queries then IO.text_of_query (output_string stdout) nl q; let r = I.execute handle q in - U.text_of_result (output_string stdout) r nl; + IO.text_of_result (output_string stdout) nl r; if ! log_file <> "" then log q r; incr query_num; flush stdout @@ -114,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 @@ -138,7 +142,7 @@ let execute ich = let handle = get_handle () in let rec execute_aux () = try - let q = U.query_of_text lexbuf in + let q = IO.query_of_text lexbuf in issue handle q; execute_aux () with End_of_file -> () in @@ -156,9 +160,14 @@ let locate name = issue handle (G.locate name); C.close handle +let unreferred target source = + let handle = get_handle () in + issue handle (G.unreferred target source); + C.close handle + let mpattern n m l = let queries = ref [] in - let univ = Some GU.universe_for_search_pattern in + let univ = Some C2.universe in let handle = get_handle () in let rec pattern level = function | [] -> () @@ -193,10 +202,7 @@ let mpattern n m l = let mbackward n m l = let queries = ref [] in - let torigth_restriction (u, b) = - let p = if b then `MainConclusion None else `InConclusion in (p, u) - in - let univ = Some GU.universe_for_match_conclusion in + let univ = Some C1.universe in let handle = get_handle () in let rec backward level = function | [] -> () @@ -204,12 +210,10 @@ let mbackward n m l = backward level tail; print_string ("? " ^ CicPp.ppterm term ^ nl); let t = U.start_time () in - let list_of_must, only = C1.out_restr [] [] term in + let list_of_must, only = C1.get_constraints [] [] 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.query_of_constraints univ (rigth_must, [], []) (rigth_only , None, None) in + let q = G.query_of_constraints univ (must, [], []) (Some only , None, None) in if not (List.mem q ! queries) then begin issue handle q; @@ -229,6 +233,33 @@ let mbackward n m l = flush stderr; C.close handle +let inductive l = + let queries = ref [] in + let univ = None in + let handle = get_handle () in + let rec aux = function + | [] -> () + | term :: tail -> + aux tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + let t = U.start_time () in + let m = C3.get_constraints term in + let q = G.query_of_constraints univ m (None, None, None) in + if not (List.mem q ! queries) then + begin + issue handle q; + Printf.eprintf "[%i] " (pred ! query_num); flush stderr; + Printf.printf "%i GEN: %s" + (pred ! query_num) (U.stop_time t ^ nl); + flush stdout; queries := q :: ! queries + end + in + aux l; + Printf.eprintf "\nmqgtop: inductive: %i queries issued\n" + (List.length ! queries); + flush stderr; + C.close handle + let check () = let handle = get_handle () in Printf.eprintf @@ -248,10 +279,12 @@ 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"; prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias"; + prerr_endline "-U T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns"; 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"; @@ -261,18 +294,21 @@ let prerr_help () = 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"; + prerr_endline " on all CIC terms in the input file"; + prerr_endline "-I issues the \"Inductive\" query on all CIC terms in the"; + prerr_endline " input file\n"; 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 @@ -280,20 +316,23 @@ let rec parse = function | ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem | ("-L"|"-Locate") :: arg :: rem -> locate arg; parse rem | ("-C"|"-compose") :: rem -> compose (); parse rem - | ("-M"|"-backward") :: arg :: rem -> + | ("-B"|"-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 -> 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 + | ("-U"|"-unreferred") :: arg1 :: arg2 :: rem -> + unreferred arg1 arg2; parse rem + | ("-I"|"-inductive") :: rem -> inductive (get_terms ()); parse rem | _ :: rem -> 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