(* 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)
- (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
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
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 "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
| _ :: 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