native support for reference shells added to mqgtop

diff --git a/helm/mathql_test/Makefile b/helm/mathql_test/Makefile
index a4a0c181a73b920e6e7c79e6a36d90445bf3753d..eaeb5b81e796bea6fb2b2af4b55dac8d40808101 100644 (file)
--- a/helm/mathql_test/Makefile
+++ b/helm/mathql_test/Makefile
@@ -1,9 +1,9 @@
 BIN_DIR = /usr/local/bin
-REQUIRES = unix helm-cic_textual_parser helm-cic_proof_checking \
+REQUIRES = unix helm-registry helm-cic_textual_parser helm-cic_proof_checking \
           helm-mathql helm-mathql_interpreter helm-mathql_generator \
           helm-tactics
 PREDICATES =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
 OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
 OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
 OCAMLDEP = ocamldep

diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml
index 16a5ea0a9862734c5965ca32096da18238ad1c4a..d478d59c3d8e6f1267a53e7c517af9e1f039784f 100644 (file)
--- 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 

diff --git a/helm/mathql_test/mqitop.ml b/helm/mathql_test/mqitop.ml
index 4d45740cf2a7c68acb80324b769e12d4c9f14f14..0172472201a23fbae1380e0b1ef9765f242a019c 100644 (file)
--- a/helm/mathql_test/mqitop.ml
+++ b/helm/mathql_test/mqitop.ml
@@ -36,11 +36,12 @@ module C = MQIConn
 module F = MQueryIO
 
 let _ =
+   Helm_registry.load_from "/home/fguidi/miohelm/gTopLevel.conf.xml";
    let t = P.start_time () in
    let ich = Lexing.from_channel stdin in
    let flags = if Array.length Sys.argv >= 2 then Sys.argv.(1) else "" in
    let log s = print_string s; flush stdout in
-   let handle = C.init (C.flags_of_string flags) log in 
+   let handle = C.init_if_connected (C.flags_of_string flags) log in 
    if not (C.connected handle) then begin  
        print_endline "mqitop: no connection"; flush stdout
    end;