X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql_test%2Fmqgtop.ml;fp=helm%2Fmathql_test%2Fmqgtop.ml;h=d478d59c3d8e6f1267a53e7c517af9e1f039784f;hb=03e2a78decd364cb401db8033b7e9472abfdcfd4;hp=16a5ea0a9862734c5965ca32096da18238ad1c4a;hpb=ad4c175433641f3b6668971bb7b3498c31390e0e;p=helm.git diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml index 16a5ea0a9..d478d59c3 100644 --- a/helm/mathql_test/mqgtop.ml +++ b/helm/mathql_test/mqgtop.ml @@ -120,6 +120,107 @@ let get_terms interp = in aux () +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 @@ -280,6 +381,8 @@ let prerr_help () = 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"; @@ -309,6 +412,8 @@ let rec parse = function | ("-d"|"-display") :: rem -> display (get_terms ()); 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 @@ -329,6 +434,7 @@ let rec parse = function | _ :: 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