Added hint support in the API. You can now query a goal to see the tactics that may be used.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14686 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 40 insertions, 0 deletions

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index cd0d7103ef..7a3afa7fbf 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -31,6 +31,8 @@ type goals =
   | Uninstantiated_evars of string list
   | Goals of goal list
 
+type hint = (string * string) list
+
 (** We use phantom types and GADT to protect ourselves against wild casts *)
 
 type raw = bool
@@ -40,6 +42,7 @@ type 'a call =
   | Interp of raw * verbose * string
   | Rewind of int
   | Goal
+  | Hints
   | Status
   | InLoadPath of string
   | MkCases of string
@@ -47,6 +50,7 @@ type 'a call =
 let interp (r,b,s) : string call = Interp (r,b,s)
 let rewind i : int call = Rewind i
 let goals : goals call = Goal
+let hints : (hint list * hint) option call = Hints
 let status : status call = Status
 let inloadpath s : bool call = InLoadPath s
 let mkcases s : string list list call = MkCases s
@@ -63,6 +67,7 @@ type handler = {
   interp : raw * verbose * string -> string;
   rewind : int -> int;
   goals : unit -> goals;
+  hints : unit -> (hint list * hint) option;
   status : unit -> status;
   inloadpath : string -> bool;
   mkcases : string -> string list list;
@@ -75,6 +80,7 @@ let abstract_eval_call handler c =
       | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s))
       | Rewind i -> Obj.magic (handler.rewind i)
       | Goal -> Obj.magic (handler.goals ())
+      | Hints -> Obj.magic (handler.hints ())
       | Status -> Obj.magic (handler.status ())
       | InLoadPath s -> Obj.magic (handler.inloadpath s)
       | MkCases s -> Obj.magic (handler.mkcases s)
@@ -162,6 +168,8 @@ let of_call = function
   Element ("call", ("val", "rewind") :: ["steps", string_of_int n], [])
 | Goal ->
   Element ("call", ["val", "goal"], [])
+| Hints ->
+  Element ("call", ["val", "hints"], [])
 | Status ->
   Element ("call", ["val", "status"], [])
 | InLoadPath file ->
@@ -184,6 +192,7 @@ let to_call = function
   | "status" -> Status
   | "inloadpath" -> InLoadPath (raw_string l)
   | "mkcases" -> MkCases (raw_string l)
+  | "hints" -> Hints
   | _ -> raise Marshal_error
   end
 | _ -> raise Marshal_error
@@ -270,11 +279,16 @@ let to_goals = function
   Goals l
 | _ -> 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_goals : goals -> xml)
+  | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml)
   | Status -> Obj.magic (of_status : status -> xml)
   | InLoadPath _ -> Obj.magic (of_bool : bool -> xml)
   | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml)
@@ -291,6 +305,8 @@ let to_answer xml =
     | "status" -> Obj.magic (to_status elt)
     | "bool" -> Obj.magic (to_bool elt)
     | "list" -> Obj.magic (to_list convert elt)
+    | "option" -> Obj.magic (to_option convert elt)
+    | "pair" -> Obj.magic (to_pair convert convert elt)
     | _ -> raise Marshal_error
     end
   | _ -> raise Marshal_error
@@ -306,6 +322,7 @@ let pr_call = function
     "INTERP"^raw^verb^" ["^s^"]"
   | Rewind i -> "REWIND "^(string_of_int i)
   | Goal -> "GOALS"
+  | Hints -> "HINTS"
   | Status -> "STATUS"
   | InLoadPath s -> "INLOADPATH "^s
   | MkCases s -> "MKCASES "^s
@@ -351,6 +368,7 @@ let pr_full_value call value =
     | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value)
     | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value)
     | Goal -> pr_value_gen pr_goals (Obj.magic value : goals value)
+    | Hints -> pr_value value
     | Status -> pr_value_gen pr_status (Obj.magic value : status value)
     | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value)
     | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value)
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 7533ff3a4c..cdd86f7946 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -27,6 +27,8 @@ type goals =
   | Uninstantiated_evars of string list
   | Goals of goal list
 
+type hint = (string * string) list
+
 type 'a call
 
 type raw = bool
@@ -54,6 +56,10 @@ val rewind : int -> int call
 (** Fetching the list of current goals *)
 val goals : goals call
 
+(** Retrieving the tactics applicable to the current goal. [None] if there is 
+    no proof in progress. *)
+val hints : (hint list * hint) option call
+
 (** The status, for instance "Ready in SomeSection, proving Foo" *)
 val status : status call
 
@@ -80,6 +86,7 @@ type handler = {
   interp : raw * verbose * string -> string;
   rewind : int -> int;
   goals : unit -> goals;
+  hints : unit -> (hint list * hint) option;
   status : unit -> status;
   inloadpath : string -> bool;
   mkcases : string -> string list list;
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index b24ded0f25..102c92237d 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -435,6 +435,20 @@ let goals () =
     Ide_intf.Goals (List.map (process_goal sigma) all_goals)
   with Proof_global.NoCurrentProof -> Ide_intf.No_current_proof
 
+let hints () =
+  try
+    let pfts = Proof_global.give_me_the_proof () in
+    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
+    match all_goals with
+    | [] -> None
+    | g :: _ ->
+      let env = Goal.V82.env sigma g in
+      let hint_goal = concl_next_tac sigma g in
+      let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in
+      let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
+      Some (hint_hyps, hint_goal)
+  with Proof_global.NoCurrentProof -> None
+
 (** Other API calls *)
 
 let inloadpath dir =
@@ -483,6 +497,7 @@ let eval_call c =
     Ide_intf.interp = interruptible interp;
     Ide_intf.rewind = interruptible rewind;
     Ide_intf.goals = interruptible goals;
+    Ide_intf.hints = interruptible hints;
     Ide_intf.status = interruptible status;
     Ide_intf.inloadpath = interruptible inloadpath;
     Ide_intf.mkcases = interruptible Vernacentries.make_cases;