(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+let _ = MQueryStandard.init
+let _ = MQueryHELM.init
+
let query_num = ref 1
let interp_file = ref "interp.cic"
let nl = " <p>\n"
+module IO = MQueryIO
module U = MQueryUtil
module I = MQueryInterpreter
module C = MQIConn
module P = MQGTopParser
module TL = CicTextualLexer
module TP = CicTextualParser
+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)
- (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;
+ 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
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 rec join f v1 v2 =
+ match v1, v2 with
+ | [], v -> f v
+ | v, [] -> f v
+ | h1 :: t1, h2 :: _ when h1 < h2 ->
+ let g h = f (h1 :: h) in join g t1 v2
+ | h1 :: _, h2 :: t2 when h1 > h2 ->
+ let g h = f (h2 :: h) in join g v1 t2
+ | h1 :: t1, _ :: t2 ->
+ let g h = f (h1 :: h) in join g t1 t2
+
+let rec diff f v1 v2 =
+ match v1, v2 with
+ | [], _ -> f []
+ | _, [] -> f v1
+ | h1 :: t1, h2 :: _ when h1 < h2 ->
+ let g h = f (h1 :: h) in diff g t1 v2
+ | h1 :: _, h2 :: t2 when h1 > h2 -> diff f v1 t2
+ | _ :: t1, _ :: t2 -> diff f t1 t2
+
+let add f r k l = join f r [M.string_of_uriref (k, l)]
+
+let rec add_cons f r k i j = function
+ | [] -> f r
+ | _ :: tl ->
+ let g s = add f s k [i; j] in
+ add_cons g r k i (succ j) tl
+
+let rec refobj_l refobj_t map f r = function
+ | [] -> f r
+ | h :: tail ->
+ let f r = refobj_l refobj_t map f r tail in
+ refobj_t f r (map h)
+
+let rec refobj_t f r = function
+ | Cic.Implicit _
+ | Cic.Meta _
+ | Cic.Sort _
+ | Cic.Rel _ -> f r
+ | Cic.Cast (t, u)
+ | Cic.Prod (_, t, u)
+ | Cic.Lambda (_, t, u)
+ | Cic.LetIn (_, t, u) ->
+ let f r = refobj_t f r u in refobj_t f r t
+ | Cic.Appl tl ->
+ refobj_l refobj_t (fun x -> x) f r tl
+ | Cic.Fix (_, tl) ->
+ let f r = refobj_l refobj_t (fun (_, _, _, u) -> u) f r tl in
+ refobj_l refobj_t (fun (_, _, t, _) -> t) f r tl
+ | Cic.CoFix (_, tl) ->
+ let f r = refobj_l refobj_t (fun (_, _, u) -> u) f r tl in
+ refobj_l refobj_t (fun (_, t, _) -> t) f r tl
+ | Cic.Var (k, tl) ->
+ let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
+ add f r k []
+ | Cic.Const (k, tl) ->
+ let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
+ add f r k []
+ | Cic.MutInd (k, i, tl) ->
+ let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
+ add f r k [i]
+ | Cic.MutConstruct (k, i, j, tl) ->
+ let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
+ add f r k [i; j]
+ | Cic.MutCase (k, i, t, u, tl) ->
+ let f r = refobj_l refobj_t (fun u -> u) f r tl in
+ let f r = refobj_t f r u in
+ let f r = refobj_t f r t in
+ let f r = add f r k [i] in
+ add_cons f r k i 1 tl
+
+let get_refobj f r uri =
+ let body, ty = M.get_object (M.uriref_of_string uri) in
+ let f r = diff f r [uri] in
+ let f r = refobj_t f r body in
+ refobj_t f r ty
+
+let rec get_refobj_l f r = function
+ | [] -> f r
+ | uri :: l ->
+ let f r = get_refobj_l f r l in
+ get_refobj f r uri
+
+let show_refobj uri =
+ let f = List.iter print_endline in
+ get_refobj f [] uri
+
+let compute_shells uri =
+ let rec aux r d n =
+ let f p r =
+ let l = List.length r in
+ Printf.printf "found %i objects\n" l; flush stdout;
+ let f d = if l > 0 then aux r d (succ n) in
+ join f d p
+ in
+ Printf.printf "shells: computing level %i ... " n; flush stdout;
+ let f r = get_refobj_l (f r) [] r in
+ diff f r d
+ in
+ aux [uri] [] 0
+
+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
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
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 univ = Some GU.universe_for_match_conclusion in
+ let univ = Some C1.universe in
let handle = get_handle () in
let rec backward level = function
| [] -> ()
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 "-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 "-r -refobj URI outputs the references in the given HELM object";
+ prerr_endline "-s -shells URI computes the reference shells 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";
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";
- prerr_endline "-U T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns\n";
+ 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
+ | ("-r"|"-refobj") :: arg :: rem -> show_refobj arg; parse rem
+ | ("-s"|"-shells") :: arg :: rem -> compute_shells 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
| ("-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_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
projects / helm.git / blobdiff