From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 27 Sep 2002 16:59:23 +0000 (+0000)
Subject: Better handling of queries. Now both the locate and backward queries give
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~64
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2cad6cb43cd5ca2c2d371cc49a6354c95533c81f;p=helm.git

Better handling of queries. Now both the locate and backward queries give
the user the possibility to disambiguate the answer, and write it in the
input window. Some bugs in the disambiguation process have been fixed.
Finally the output of the query process in the outputhtml window is now
much more verbose.
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index ab4474dea..48c178918 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -47,9 +47,9 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
+let prooffile = "/public/sacerdot/currentproof";;
 (*CSC: the getter should handle the innertypes, not the FS *)
-let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
+let innertypesfile = "/public/sacerdot/innertypes";;
 
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
@@ -1085,44 +1085,71 @@ let check rendering_window scratch_window () =
         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+exception NoObjectsLocated;;
+
+let user_uri_choice uris =
+ let uri =
+  match uris with
+     [] -> raise NoObjectsLocated
+   | [uri] -> uri
+   | uris ->
+      let choice =
+       GToolbox.question_box ~title:"Ambiguous result."
+        ~buttons:uris ~default:1
+        "Ambiguous result. Please, choose one."
+      in
+       List.nth uris (choice-1)
+ in
+  String.sub uri 4 (String.length uri - 4)
+;;
+
 let locate rendering_window () =
  let inputt = (rendering_window#inputt : GEdit.text) in
  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
   let inputlen = inputt#length in
   let input = inputt#get_chars 0 inputlen in
-  output_html outputhtml (
-     try
-        match Str.split (Str.regexp "[ \t]+") input with
-           | [] -> ""
-           | head :: tail ->
-	       inputt#delete_text 0 inputlen;
-	       MQueryGenerator.locate_html head 
-     with
-        e -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
-  )
+   try
+    match Str.split (Str.regexp "[ \t]+") input with
+       [] -> ()
+     | head :: tail ->
+        inputt#delete_text 0 inputlen ;
+        let MathQL.MQRefs uris, html = MQueryGenerator.locate head in
+         output_html outputhtml html ;
+         let uri' = user_uri_choice uris in
+          ignore ((inputt#insert_text uri') ~pos:0)
+   with
+    e ->
+     output_html outputhtml
+      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 ;;
 
 let backward rendering_window () =
-   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) 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 (_, ey ,ty) =
-              List.find (function (m,_,_) -> m=metano) metasenv
-             in
-              MQueryGenerator.backward metasenv ey ty level
-       in 
-   output_html outputhtml result
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) 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
+   try
+    match !ProofEngine.goal with
+       None -> ()
+     | Some metano ->
+        let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
+         let MathQL.MQRefs uris, html =
+          MQueryGenerator.backward metasenv ey ty level
+         in
+          output_html outputhtml html ;
+          let uri' = user_uri_choice uris in
+           inputt#delete_text 0 inputlen ;
+           ignore ((inputt#insert_text uri') ~pos:0)
+    with
+     e -> 
+      output_html outputhtml 
+       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 ;;
       
 let choose_selection
@@ -1494,15 +1521,18 @@ end;;
 
 (* MAIN *)
 
+let rendering_window = ref None;;
+
 let initialize_everything () =
  let module U = Unix in
   let output = GMathView.math_view ~width:400 ~height:280 ()
   and proofw = GMathView.math_view ~width:400 ~height:275 ()
   and label = GMisc.label ~text:"gTopLevel" () in
-    let rendering_window =
+    let rendering_window' =
      new rendering_window output proofw label
     in
-     rendering_window#show () ;
+     rendering_window := Some rendering_window' ;
+     rendering_window'#show () ;
      GMain.Main.main ()
 ;;
 
@@ -1513,12 +1543,22 @@ let _ =
    MQueryGenerator.init () ;
    CicTextualParser0.set_locate_object
     (function id ->
-      let MathQL.MQRefs uris = MQueryGenerator.locate id in
+      let MathQL.MQRefs uris, html = MQueryGenerator.locate id in
+       begin
+        match !rendering_window with
+           None -> assert false
+         | Some rw -> output_html rw#outputhtml html ;
+       end ;
        let uri = 
         match uris with
            [] ->
-            (GToolbox.input_string ~title:"Unknown input"
-             ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
+            (match
+              (GToolbox.input_string ~title:"Unknown input"
+               ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
+             with
+                None -> None
+              | Some uri -> Some ("cic:" ^ uri)
+            )
          | [uri] -> Some uri
          | _ ->
            let choice =
diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index bb27633bb..eabc234aa 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -160,8 +160,8 @@ let build_result query =
    if ! issue query then
       let html = par () ^ out_query query ^ nl () in
       let result = Mqint.execute query in
-      save (html ^ out_result result)
-    else ""
+       result, save (html ^ out_result result)
+    else MQRefs [], ""
     
 let build_select (r, b, v) n  =
    let rvar = "ref" ^ string_of_int n in
@@ -220,8 +220,21 @@ let locate_query s =
                        )
              )
 
-let locate s = Mqint.execute (locate_query s)
-let locate_html s = build_result (locate_query s)
+let locate s =
+ let MQRefs uris, html = build_result (locate_query s) in
+(*CSC: here I am mapping .ind URIs to .ind#1/1, i.e. the first type of *)
+(*CSC: the mutual inductive block. It must be removed once the query   *)
+(*CSC: works reasonably.                                               *)
+  MQRefs (
+   List.map
+    (function uri ->
+      if String.sub uri (String.length uri - 4) 4 = ".ind" then
+       uri ^ "#1/1"
+      else
+       uri
+    ) uris
+  ), html
+;;
 
 let levels e c t =
    env := e; cont := c;
@@ -238,10 +251,11 @@ let backward e c t level =
    let query = build_inter 0 (il_restrict level il) in
    let query' = restrict_universe query il in
    let query'' = MQList query' in 
-   let r = build_result query'' in
-   if r <> "" then
+   let res = build_result query'' in
+   let r,html = res in
+   if html <> "" then
    begin
       print_endline ("GEN = " ^ string_of_int (List.length il) ^ ":" ^
          string_of_float (Sys.time () -. t0) ^ "s");
-      par () ^ il_out il ^ r
-   end else ""
+      r, par () ^ il_out il ^ html
+   end else res
diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index 69cbfeba5..694fdcf12 100644
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -42,8 +42,9 @@ val init      : unit -> unit     (* INIT database function *)
 
 val close     : unit -> unit     (* CLOSE database function *)
 
-val locate    : string -> MathQL.mqresult (* LOCATE query building function *)
-val locate_html : string -> string (* LOCATE query building function *)
+val locate    : string -> MathQL.mqresult * string
+                                 (* LOCATE query building function *)
 
-val backward  : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
+val backward  :
+ Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.mqresult * string
                                  (* BACKWARD query building function *)
diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 9992e4093..1fa790b64 100644
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -41,7 +41,7 @@ let pp_type_of uri =
 
 let locate name =
    check_db ();
-   print_endline (MQueryGenerator.locate_html name);
+   print_endline (snd (MQueryGenerator.locate name)) ;
    flush stdout
 
 let rec display = function
@@ -70,7 +70,7 @@ let mbackward n m l =
       | term :: tail -> 
          backward level tail;
          print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
-         print_endline (MQueryGenerator.backward [] [] term level);
+         print_endline (snd (MQueryGenerator.backward [] [] term level)) ;
          flush stdout
    in
    check_db ();