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 ab4474deaf95b9853bc6b5d7a60b2de447feb952..48c178918c019e9f6d3ad4ba1aac29d6ca8e9c7e 100644 (file)
--- 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 bb27633bb5c4694d0cc69f4866cfb4e7b3b5bb32..eabc234aa16a7edc793986c0d62b7894e2a16206 100644 (file)
--- 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 69cbfeba55e6f39496703fc96b84fd9697877adc..694fdcf1248fb49034ad9588030397cf7da3d719 100644 (file)
--- 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 9992e409369e8c33de911cc622840b8615c376a2..1fa790b64adc19e4614c402022d916dea9206d41 100644 (file)
--- 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 ();