Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

5 files changed, 138 insertions, 91 deletions

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 0df24c7a..28f97dc8 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -45,7 +45,7 @@ type handler = {
   evars : unit -> evar list option;
   hints : unit -> (hint list * hint) option;
   status : unit -> status;
-  search : search_flags -> search_answer list;
+  search : search_flags -> string coq_object list;
   get_options : unit -> (option_name * option_state) list;
   set_options : (option_name * option_value) list -> unit;
   inloadpath : string -> bool;
@@ -63,7 +63,7 @@ let goals : goals option call = Goal
 let evars : evar list option call = Evars
 let hints : (hint list * hint) option call = Hints
 let status : status call = Status
-let search flags : search_answer list call = Search flags
+let search flags : string coq_object list call = Search flags
 let get_options : (option_name * option_state) list call = GetOptions
 let set_options l : unit call = SetOptions l
 let inloadpath s : bool call = InLoadPath s
@@ -81,7 +81,7 @@ let abstract_eval_call handler c =
       | Evars -> Obj.magic (handler.evars () : evar list option)
       | Hints -> Obj.magic (handler.hints () : (hint list * hint) option)
       | Status -> Obj.magic (handler.status () : status)
-      | Search flags -> Obj.magic (handler.search flags : search_answer list)
+      | Search flags -> Obj.magic (handler.search flags : string coq_object list)
       | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list)
       | SetOptions opts -> Obj.magic (handler.set_options opts : unit)
       | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
@@ -130,6 +130,12 @@ let bool_arg tag b = if b then [tag, ""] else []
 
 (** Base types *)
 
+let of_unit () = Element ("unit", [], [])
+
+let to_unit = function
+  | Element ("unit", [], []) -> ()
+  | _ -> raise Marshal_error
+
 let of_bool b =
   if b then constructor "bool" "true" []
   else constructor "bool" "false" []
@@ -166,7 +172,8 @@ let to_string = function
 let of_int i = Element ("int", [], [PCData (string_of_int i)])
 
 let to_int = function
-| Element ("int", [], [PCData s]) -> int_of_string s
+| Element ("int", [], [PCData s]) ->
+  (try int_of_string s with Failure _ -> raise Marshal_error)
 | _ -> raise Marshal_error
 
 let of_pair f g (x, y) = Element ("pair", [], [f x; g y])
@@ -232,20 +239,20 @@ let to_search_constraint xml = do_match xml "search_constraint"
   | "include_blacklist" -> Include_Blacklist
   | _ -> raise Marshal_error)
 
-let of_search_answer ans =
-  let path = of_list of_string ans.search_answer_full_path in
-  let name = of_string ans.search_answer_base_name in
-  let tpe = of_string ans.search_answer_type in
-  Element ("search_answer", [], [path; name; tpe])
-
-let to_search_answer = function
-| Element ("search_answer", [], [path; name; tpe]) ->
-  let path = to_list to_string path in
-  let name = to_string name in
-  let tpe = to_string tpe in {
-    search_answer_full_path = path;
-    search_answer_base_name = name;
-    search_answer_type = tpe;
+let of_coq_object f ans =
+  let prefix = of_list of_string ans.coq_object_prefix in
+  let qualid = of_list of_string ans.coq_object_qualid in
+  let obj = f ans.coq_object_object in
+  Element ("coq_object", [], [prefix; qualid; obj])
+
+let to_coq_object f = function
+| Element ("coq_object", [], [prefix; qualid; obj]) ->
+  let prefix = to_list to_string prefix in
+  let qualid = to_list to_string qualid in
+  let obj = f obj in {
+    coq_object_prefix = prefix;
+    coq_object_qualid = qualid;
+    coq_object_object = obj;
   }
 | _ -> raise Marshal_error
 
@@ -412,51 +419,74 @@ let to_coq_info = function
   }
 | _ -> raise Marshal_error
 
-let of_hints =
-  let of_hint = of_list (of_pair of_string of_string) in
-  of_option (of_pair (of_list of_hint) of_hint)
-
-let of_answer (q : 'a call) (r : 'a value) =
-  let convert = match q with
-  | Interp _ -> Obj.magic (of_string : string -> xml)
-  | Rewind _ -> Obj.magic (of_int : int -> xml)
-  | Goal -> Obj.magic (of_option of_goals : goals option -> xml)
-  | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml)
-  | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml)
-  | Status -> Obj.magic (of_status : status -> xml)
-  | Search _ -> Obj.magic (of_list of_search_answer : search_answer list -> xml)
-  | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml)
-  | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], []))
-  | InLoadPath _ -> Obj.magic (of_bool : bool -> xml)
-  | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml)
-  | Quit -> Obj.magic (fun _ -> Element ("unit", [], []))
-  | About -> Obj.magic (of_coq_info : coq_info -> xml)
+(** Conversions between ['a value] and xml answers
+
+  When decoding an xml answer, we dynamically check that it is compatible
+  with the original call. For that we now rely on the fact that all
+  sub-fonctions [to_xxx : xml -> xxx] check that the current xml element
+  is "xxx", and raise [Marshal_error] if anything goes wrong.
+*)
+
+type value_type =
+  | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info
+  | Option of value_type
+  | List of value_type
+  | Coq_object of value_type
+  | Pair of value_type * value_type
+
+let hint = List (Pair (String, String))
+let option_name = List String
+
+let expected_answer_type = function
+  | Interp _ -> String
+  | Rewind _ -> Int
+  | Goal -> Option Goals
+  | Evars -> Option (List Evar)
+  | Hints -> Option (Pair (List hint, hint))
+  | Status -> State
+  | Search _ -> List (Coq_object String)
+  | GetOptions -> List (Pair (option_name, Option_state))
+  | SetOptions _ -> Unit
+  | InLoadPath _ -> Bool
+  | MkCases _ -> List (List String)
+  | Quit -> Unit
+  | About -> Coq_info
+
+let of_answer (q : 'a call) (r : 'a value) : xml =
+  let rec convert ty : 'a -> xml = match ty with
+    | Unit -> Obj.magic of_unit
+    | Bool -> Obj.magic of_bool
+    | String -> Obj.magic of_string
+    | Int -> Obj.magic of_int
+    | State -> Obj.magic of_status
+    | Option_state -> Obj.magic of_option_state
+    | Coq_info -> Obj.magic of_coq_info
+    | Goals -> Obj.magic of_goals
+    | Evar -> Obj.magic of_evar
+    | List t -> Obj.magic (of_list (convert t))
+    | Option t -> Obj.magic (of_option (convert t))
+    | Coq_object t -> Obj.magic (of_coq_object (convert t))
+    | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2))
   in
-  of_value convert r
-
-let to_answer xml =
-  let rec convert elt = match elt with
-  | Element (tpe, attrs, l) ->
-    begin match tpe with
-    | "unit" -> Obj.magic ()
-    | "string" -> Obj.magic (to_string elt : string)
-    | "int" -> Obj.magic (to_int elt : int)
-    | "status" -> Obj.magic (to_status elt : status)
-    | "bool" -> Obj.magic (to_bool elt : bool)
-    | "list" -> Obj.magic (to_list convert elt : 'a list)
-    | "option" -> Obj.magic (to_option convert elt : 'a option)
-    | "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b))
-    | "goals" -> Obj.magic (to_goals elt : goals)
-    | "evar" -> Obj.magic (to_evar elt : evar)
-    | "option_value" -> Obj.magic (to_option_value elt : option_value)
-    | "option_state" -> Obj.magic (to_option_state elt : option_state)
-    | "coq_info" -> Obj.magic (to_coq_info elt : coq_info)
-    | "search_answer" -> Obj.magic (to_search_answer elt : search_answer)
-    | _ -> raise Marshal_error
-    end
-  | _ -> raise Marshal_error
+  of_value (convert (expected_answer_type q)) r
+
+let to_answer xml (c : 'a call) : 'a value =
+  let rec convert ty : xml -> 'a = match ty with
+    | Unit -> Obj.magic to_unit
+    | Bool -> Obj.magic to_bool
+    | String -> Obj.magic to_string
+    | Int -> Obj.magic to_int
+    | State -> Obj.magic to_status
+    | Option_state -> Obj.magic to_option_state
+    | Coq_info -> Obj.magic to_coq_info
+    | Goals -> Obj.magic to_goals
+    | Evar -> Obj.magic to_evar
+    | List t -> Obj.magic (to_list (convert t))
+    | Option t -> Obj.magic (to_option (convert t))
+    | Coq_object t -> Obj.magic (to_coq_object (convert t))
+    | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2))
   in
-  to_value convert xml
+  to_value (convert (expected_answer_type c)) xml
 
 (** * Debug printing *)
 
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 26c6b671..7d0685b1 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -77,7 +77,7 @@ type handler = {
   evars : unit -> evar list option;
   hints : unit -> (hint list * hint) option;
   status : unit -> status;
-  search : search_flags -> search_answer list;
+  search : search_flags -> string coq_object list;
   get_options : unit -> (option_name * option_state) list;
   set_options : (option_name * option_value) list -> unit;
   inloadpath : string -> bool;
@@ -104,7 +104,7 @@ val of_call : 'a call -> xml
 val to_call : xml -> 'a call
 
 val of_answer : 'a call -> 'a value -> xml
-val to_answer : xml -> 'a value
+val to_answer : xml -> 'a call -> 'a value
 
 (** * Debug printing *)
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 681eec0d..d67b272e 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -127,25 +127,25 @@ let hyp_next_tac sigma env (id,_,ast) =
   let id_s = Names.string_of_id id in
   let type_s = string_of_ppcmds (pr_ltype_env env ast) in
   [
-    ("clear "^id_s),("clear "^id_s^".\n");
-    ("apply "^id_s),("apply "^id_s^".\n");
-    ("exact "^id_s),("exact "^id_s^".\n");
-    ("generalize "^id_s),("generalize "^id_s^".\n");
-    ("absurd <"^id_s^">"),("absurd "^type_s^".\n")
+    ("clear "^id_s),("clear "^id_s^".");
+    ("apply "^id_s),("apply "^id_s^".");
+    ("exact "^id_s),("exact "^id_s^".");
+    ("generalize "^id_s),("generalize "^id_s^".");
+    ("absurd <"^id_s^">"),("absurd "^type_s^".")
   ] @ [
-    ("discriminate "^id_s),("discriminate "^id_s^".\n");
-    ("injection "^id_s),("injection "^id_s^".\n")
+    ("discriminate "^id_s),("discriminate "^id_s^".");
+    ("injection "^id_s),("injection "^id_s^".")
   ] @ [
-    ("rewrite "^id_s),("rewrite "^id_s^".\n");
-    ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n")
+    ("rewrite "^id_s),("rewrite "^id_s^".");
+    ("rewrite <- "^id_s),("rewrite <- "^id_s^".")
   ] @ [
-    ("elim "^id_s), ("elim "^id_s^".\n");
-    ("inversion "^id_s), ("inversion "^id_s^".\n");
-    ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n")
+    ("elim "^id_s), ("elim "^id_s^".");
+    ("inversion "^id_s), ("inversion "^id_s^".");
+    ("inversion clear "^id_s), ("inversion_clear "^id_s^".")
   ]
 
 let concl_next_tac sigma concl =
-  let expand s = (s,s^".\n") in
+  let expand s = (s,s^".") in
   List.map expand ([
     "intro";
     "intros";
@@ -312,16 +312,26 @@ let search flags =
   in
   let ans = ref [] in
   let print_function ref env constr =
-    let name = Names.string_of_id (Nametab.basename_of_global ref) in
-    let make_path = Names.string_of_id in
-    let path =
-      List.rev_map make_path (Names.repr_dirpath (Nametab.dirpath_of_global ref))
-    in
-    let answer = {
-      Interface.search_answer_full_path = path;
-      Interface.search_answer_base_name = name;
-      Interface.search_answer_type = string_of_ppcmds (pr_lconstr_env env constr);
-    } in
+     let fullpath = repr_dirpath (Nametab.dirpath_of_global ref) in
+     let qualid = Nametab.shortest_qualid_of_global Idset.empty ref in
+     let (shortpath, basename) = Libnames.repr_qualid qualid in
+     let shortpath = repr_dirpath shortpath in
+     (* [shortpath] is a suffix of [fullpath] and we're looking for the missing
+        prefix *)
+     let rec prefix full short accu = match full, short with
+     | _, [] ->
+       let full = List.rev_map string_of_id full in
+       (full, accu)
+     | _ :: full, m :: short ->
+       prefix full short (string_of_id m :: accu)
+     | _ -> assert false
+     in
+     let (prefix, qualid) = prefix fullpath shortpath [string_of_id basename] in
+     let answer = {
+       Interface.coq_object_prefix = prefix;
+       Interface.coq_object_qualid = qualid;
+       Interface.coq_object_object = string_of_ppcmds (pr_lconstr_env env constr);
+     } in
     ans := answer :: !ans;
   in
   let () = Search.gen_filtered_search filter_function print_function in
@@ -432,6 +442,9 @@ let loop () =
           let () = pr_debug ("--> " ^ Ide_intf.pr_full_value q r) in
           Ide_intf.of_answer q r
         with
+	| Xml_parser.Error (Xml_parser.Empty, _) ->
+	  pr_debug ("End of input, exiting");
+	  exit 0
         | Xml_parser.Error (err, loc) ->
           let msg = "Syntax error in query: " ^ Xml_parser.error_msg err in
           fail msg
diff --git a/toplevel/interface.mli b/toplevel/interface.mli
index 39fb2a0e..7b4312a3 100644
--- a/toplevel/interface.mli
+++ b/toplevel/interface.mli
@@ -86,10 +86,14 @@ type search_constraint =
     the flag should be negated. *)
 type search_flags = (search_constraint * bool) list
 
-type search_answer = {
-  search_answer_full_path : string list;
-  search_answer_base_name : string;
-  search_answer_type : string;
+(** A named object in Coq. [coq_object_qualid] is the shortest path defined for 
+    the user. [coq_object_prefix] is the missing part to recover the fully 
+    qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid].
+    [coq_object_object] is the actual content of the object. *)
+type 'a coq_object = {
+  coq_object_prefix : string list;
+  coq_object_qualid : string list;
+  coq_object_object : 'a;
 }
 
 type coq_info = {
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fe6bf7db..6618b695 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -208,7 +208,7 @@ let show_match id =
     str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
   in
   msg (v 1 (str "match # with" ++ fnl () ++
-	    prlist_with_sep fnl pr_branch patterns ++ fnl ()))
+	    prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ()))
 
 (* "Print" commands *)