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
let get_handle () =
- C.init (C.flags_of_string ! int_options)
- (fun s -> print_string s; flush stdout)
+ C.init ~flags:(C.flags_of_string ! int_options)
+ ~log:(fun s -> print_string s; flush stdout) ()
let issue handle q =
let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
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;
+ U.text_of_query out nl q;
out ("Result: " ^ nl);
- U.text_of_result out r nl;
+ U.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 U.text_of_query (output_string stdout) nl q;
let r = I.execute handle q in
- U.text_of_result (output_string stdout) r nl;
+ U.text_of_result (output_string stdout) nl r;
if ! log_file <> "" then log q r;
incr query_num;
flush stdout
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
| [] -> ()
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
| [] -> ()
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;
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
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";
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";
| ("-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 _ =
+ Helm_registry.load_from "/home/fguidi/miohelm/gTopLevel.conf.xml";
let t = U.start_time () in
- Logger.log_callback :=
- (Logger.log_to_html
+(*
+ CicLogger.log_callback :=
+ (CicLogger.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 " ^ (U.stop_time t));
exit 0
projects / helm.git / blobdiff