*** empty log message ***

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 083bbc7ebac6ccfc279d69cd00911210519ae7c6..789a65ba5c87330d11d00c027ea602f733fb9cac 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -990,31 +990,38 @@ let locate rendering_window () =
  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
   let inputlen = inputt#length in
   let input = inputt#get_chars 0 inputlen in
-   try   
-    output_html outputhtml (Mquery.locate input) ;
-    inputt#delete_text 0 inputlen 
-   with
-    e -> 
-     output_html outputhtml
-      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+  output_html outputhtml (
+     try
+        match Str.split (Str.regexp "[ \t]+") input with
+           | [] -> ""
+           | head :: tail ->
+              inputt#delete_text 0 inputlen;
+              Mquery.locate head 
+     with
+        e -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
+  )
 ;;
 
 let backward rendering_window () =
    let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
-   let metasenv =
-    match !ProofEngine.proof with
-       None -> assert false
-     | Some (_,metasenv,_,_) -> metasenv
-   in
-   let result =
-      match !ProofEngine.goal with
-         | None -> ""
-         | Some metano ->
-            let (_,_,ty) =
-             List.find (function (m,_,_) -> m=metano) metasenv
-            in
-             Mquery.backward ty
-      in 
+   let inputt = (rendering_window#inputt : GEdit.text) in
+    let inputlen = inputt#length in
+    let input = inputt#get_chars 0 inputlen in
+    let level = int_of_string input in
+    let metasenv =
+     match !ProofEngine.proof with
+        None -> assert false
+      | Some (_,metasenv,_,_) -> metasenv
+    in
+    let result =
+       match !ProofEngine.goal with
+          | None -> ""
+          | Some metano ->
+             let (_,_,ty) =
+              List.find (function (m,_,_) -> m=metano) metasenv
+             in
+              Mquery.backward ty level
+       in 
    output_html outputhtml result
       
 let choose_selection

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index 316588f2c9d2787f52edd5ea3d5eb1bdd0d22b63..e27c8e2c0baeff05a76cc23cfb412bf1f6a1c753 100644 (file)
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -72,9 +72,9 @@ let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"
 
 let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
 
-let nl = "<br>"
+let nl () = "<br>"
 
-let par = "<p>"
+let par () = "<p>"
 
 (* HTML representation of a query *)
 
@@ -108,7 +108,8 @@ let rec out_bool = function
 let rec out_list = function
    | MQSelect (r, l, b) -> 
       key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b
-   | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v 
+   | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v
+   | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ key "position" ^ out_svar v
    | MQPattern p -> key "pattern" ^ out_pat p
    | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
    | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
@@ -116,6 +117,17 @@ let rec out_list = function
 let out_query = function
    | MQList l -> out_list l
 
+(* HTML representation of a query result *)
+
+let rec out_list = function 
+   | []     -> ""
+   | u :: l -> res u ^ nl () ^ out_list l 
+
+let out_result qr =
+   par () ^ "Result:" ^ nl () ^
+   match qr with
+      | MQRefs l -> out_list l
+
 (* Converting functions *)
 
 let split s =
@@ -149,18 +161,18 @@ let tref_uref (u, i) =
 
 (* CIC term inspecting functions *)
 
-let out_ie (r, b) =
-   let pos = if b then "HEAD: " else "TAIL: " in
-   res (pos ^ str_uref r) ^ nl ^
-   con (pos ^ str_tref (tref_uref r)) ^ nl
+let out_ie (r, b, v) =
+   let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
+   res (pos ^ str_uref r) ^ nl () ^
+   con (pos ^ str_tref (tref_uref r)) ^ nl ()
 
 let rec out_il = function
    | []           -> ""
    | head :: tail -> out_ie head ^ out_il tail
 
-let tie_uie (r, b) = (tref_uref r, b)
+let tie_uie (r, b, v) = (tref_uref r, b, v)
 
-let ie_eq ((u1, f1), b1) ((u2, f2), b2) = 
+let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) = 
    UriManager.eq u1 u2 && f1 = f2 && b1 = b2 
 
 let rec ie_insert ie = function
@@ -168,69 +180,77 @@ let rec ie_insert ie = function
    | head :: tail -> 
       head :: if ie_eq head ie then tail else ie_insert ie tail
 
-let inspect_uri main l uri t c =
-   let fi = 
+let level = ref 0
+
+let inspect_uri main l uri t c v =
+   if v > !level then l else
+   let fi =
       match (t, c) with
          | (None, _) -> (None, None)
         | (Some t0, c0) -> (Some (t0 + 1), c0) 
-      in
-   ie_insert ((uri, fi), main) l 
+   in
+   ie_insert ((uri, fi), main, v) l 
 
-let rec inspect_term main l = function
+let rec inspect_term main l v = function
    | Rel i                        -> l 
-   | Meta (i,_)                   -> l 
+   | Meta (i, _)                  -> l 
    | Sort s                       -> l 
    | Implicit                     -> l 
    | Abst u                       -> l 
-   | Var u                        -> inspect_uri main l u None None
-   | Const (u, i)                 -> inspect_uri main l u None None 
-   | MutInd (u, i, t)             -> inspect_uri main l u (Some t) None
-   | MutConstruct (u, i, t, c)    -> inspect_uri main l u (Some t) (Some c)
+   | Var u                        -> inspect_uri main l u None None v
+   | Const (u, i)                 -> inspect_uri main l u None None v
+   | MutInd (u, i, t)             -> inspect_uri main l u (Some t) None v
+   | MutConstruct (u, i, t, c)    -> inspect_uri main l u (Some t) (Some c) v
    | Cast (uu, tt)                -> 
-      let luu = inspect_term main l uu in
-      inspect_term false luu tt
+      let luu = inspect_term main l (v + 1) uu in
+      inspect_term false luu (v + 1) tt 
    | Prod (n, uu, tt)             ->
-      let luu = inspect_term false l uu in
-      inspect_term false luu tt
+      let luu = inspect_term false l (v + 1) uu in
+      inspect_term false luu (v + 1) tt
    | Lambda (n, uu, tt)           ->
-      let luu = inspect_term false l uu in
-      inspect_term false luu tt
+      let luu = inspect_term false l (v + 1) uu in
+      inspect_term false luu (v + 1) tt 
    | LetIn (n, uu, tt)            ->
-      let luu = inspect_term false l uu in
-      inspect_term false luu tt
-   | Appl m                       -> inspect_list main l m
+      let luu = inspect_term false l (v + 1) uu in
+      inspect_term false luu (v + 1) tt
+   | Appl m                       -> inspect_list main l (v + 1) m 
    | MutCase (u, i, t, tt, uu, m) -> 
-      let lu = inspect_uri main l u (Some t) None in
-      let ltt = inspect_term false lu tt in
-      let luu = inspect_term false ltt uu in
-      inspect_list main luu m
-   | Fix (i, m)                   -> inspect_ind l m
-   | CoFix (i, m)                 -> inspect_coind l m
-and inspect_list main l = function
+      let lu = inspect_uri main l u (Some t) None (v + 1) in
+      let ltt = inspect_term false lu (v + 1) tt in
+      let luu = inspect_term false ltt (v + 1) uu in
+      inspect_list main luu (v + 1) m
+   | Fix (i, m)                   -> inspect_ind l (v + 1) m 
+   | CoFix (i, m)                 -> inspect_coind l (v + 1) m 
+and inspect_list main l v = function
    | []      -> l
    | tt :: m -> 
-      let ltt = inspect_term main l tt in
-      inspect_list false ltt m
-and inspect_ind l = function
+      let ltt = inspect_term main l v tt in
+      inspect_list false ltt v m
+and inspect_ind l v = function
    | []                  -> l
    | (n, i, tt, uu) :: m ->  
-      let ltt = inspect_term false l tt in
-      let luu = inspect_term false ltt uu in
-      inspect_ind luu m
-and inspect_coind l = function
+      let ltt = inspect_term false l v tt in
+      let luu = inspect_term false ltt v uu in
+      inspect_ind luu v m
+and inspect_coind l v = function
    | []               -> l
    | (n, tt, uu) :: m ->
-      let ltt = inspect_term false l tt in
-      let luu = inspect_term false ltt uu in
-      inspect_coind luu m
+      let ltt = inspect_term false l v tt in
+      let luu = inspect_term false ltt v uu in
+      inspect_coind luu v m
 
-let inspect t = inspect_term true [] t 
+let inspect t = inspect_term true [] 0 t  
 
 (* query building functions *)
 
-let build_select (r, b) n =
-   let rvar = "uri" ^ string_of_int n in
-   let svar = "s" ^ string_of_int n in
+let save s = 
+   let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
+                          (64 * 6 + 8 * 6 + 4) "mquery.htm" in
+   output_string och s; flush och; s
+
+let build_select (r, b, v) n =
+   let rvar = "ref" ^ string_of_int n in
+   let svar = "str" ^ string_of_int n in
    let mqs = if b then MQMConclusion else MQConclusion in
    MQSelect (rvar, 
              MQUse (MQPattern r, svar),
@@ -242,38 +262,30 @@ let rec build_inter n = function
    | [ie]     -> build_select ie n
    | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
 
+let build_result query =
+   let html = par () ^ out_query query ^ nl () in
+   let result = Mqint.execute query in
+   save (html ^ out_result result)
+
+let init = Mqint.init
+
+let close = Mqint.close
+
 let locate s = 
-   let locate_aux txt =
-      let query = 
-         MQList (MQSelect ("uri", 
-                          MQPattern ("cic", [MQAstAst], "con", (None, None)), 
-                          MQIs (MQFunc (MQName, "uri"),
-                                MQCons txt
-                               )
-                         )
-               )
-      in
-       match Mqint.execute query with
-          MQStrUri l ->
-           out_query query ^ nl ^ "Result: " ^  nl ^
-            String.concat nl l ^ nl
-        | MQRefs _ -> assert false (*CSC: ????????????????????????????? *)
+   let query = 
+      MQList (MQSelect ("ref", 
+                        MQPattern ("cic", [MQAstAst], "con", (None, None)),
+                        MQIs (MQFunc (MQName, "ref"),
+                              MQCons s
+                             )
+                       )
+             )
    in
-   match Str.split (Str.regexp "[ \t]+") s with
-      | [] -> ""
-      | head :: tail -> par ^ locate_aux head 
-;;
+   build_result query
 
-let backward t =
+let backward t n =
+   level := n;
    let uil = inspect t in
    let til = List.map tie_uie uil in
-   let query = MQList (build_inter 0 til) in
-    match Mqint.execute query with
-       MQStrUri l ->
-        par ^ out_query query ^ nl ^ (* ^ par ^ out_il uil ^ *)
-        "Result: " ^  nl ^ String.concat nl l ^ nl
-     | MQRefs _ -> assert false (*CSC: ????????????????????????????? *)
-;;
-
-let init = Mqint.init;;
-let close = Mqint.close;;
+   let query = MQList (build_inter 0 til) in 
+   par () ^ out_il uil ^ build_result query

diff --git a/helm/gTopLevel/mquery.mli b/helm/gTopLevel/mquery.mli
index bfdf89597e4c43cb910f46d7a2bd2fe83aa05284..3ea31b8d214585ed73f15b32cc27d745fcb11153 100644 (file)
--- a/helm/gTopLevel/mquery.mli
+++ b/helm/gTopLevel/mquery.mli
@@ -39,9 +39,10 @@ val out_query : Mathql.mquery -> string        (* HTML representation of a query
 
 val tref_uref : Mathql.mquref -> Mathql.mqtref (* "tref of uref" conversion *)
 
-val locate    : string -> string               (* LOCATE query building function *)
+val init      : unit -> unit                   (* INIT database function *)
+
+val close     : unit -> unit                   (* CLOSE database function *)
 
-val backward  : Cic.term -> string             (* BACKWARD query building function *)
+val locate    : string -> string               (* LOCATE query building function *)
 
-val init : unit -> unit
-val close : unit -> unit
+val backward  : Cic.term -> int -> string      (* BACKWARD query building function *)