New functions for goals fetching.

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

3 files changed, 203 insertions, 12 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 4c5179edd..1f9e396b7 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -567,6 +567,97 @@ let print_no_goal () =
   (* Fall back on standard coq goal printer for completed goal printing *)
   msg (pr_open_subgoals ())
 
+let string_of_ppcmds c =
+  Pp.msg_with Format.str_formatter c;
+  Format.flush_str_formatter ()
+
+type 'a menu = 'a * (string * string) list
+
+type goals =
+  | Message of string
+  | Goals of ((string menu) list * string menu) list
+
+module Goals =
+struct
+  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")
+    ] @ (if Hipattern.is_equality_type ast then [
+      ("discriminate "^id_s),("discriminate "^id_s^".\n");
+      ("injection "^id_s),("injection "^id_s^".\n")
+    ] else []) @ (if Hipattern.is_equality_type (snd (Reductionops.splay_prod env sigma ast)) then [
+      ("rewrite "^id_s),("rewrite "^id_s^".\n");
+      ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n")
+    ] else []) @ [
+      ("elim "^id_s), ("elim "^id_s^".\n");
+      ("inversion "^id_s), ("inversion "^id_s^".\n");
+      ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n")
+    ]
+
+  let concl_next_tac concl =
+    let expand s = (s,s^".\n") in
+    List.map expand ([
+      "intro";
+      "intros";
+      "intuition"
+    ] @ (if Hipattern.is_equality_type concl.Evd.evar_concl then [
+      "reflexivity";
+      "discriminate";
+      "symmetry"
+    ] else []) @ [
+      "assumption";
+      "omega";
+      "ring";
+      "auto";
+      "eauto";
+      "tauto";
+      "trivial";
+      "decide equality";
+      "simpl";
+      "subst";
+      "red";
+      "split";
+      "left";
+      "right"
+    ])
+
+  let goals () =
+    let pfts = Pfedit.get_pftreestate () in
+    let sigma = Tacmach.evc_of_pftreestate pfts in
+    let (all_goals,_) = Refiner.frontier (Refiner.proof_of_pftreestate pfts) in
+    if all_goals = [] then
+      begin
+        Message (
+          match Decl_mode.get_end_command pfts with
+            | Some c -> "Subproof completed, now type "^c^".\n"
+            | None ->
+                let exl = Evarutil.non_instantiated sigma in
+                if exl = [] then "Proof Completed.\n" else
+                  ("No more subgoals but non-instantiated existential variables:\n"^
+                   string_of_ppcmds (pr_evars_int 1 exl)))
+      end
+    else
+      begin
+        let process_goal g =
+          let env = Evd.evar_env g in
+          let ccl =
+            string_of_ppcmds (pr_ltype_env_at_top env g.Evd.evar_concl) in
+          let process_hyp h_env d acc =
+            (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in
+          let hyps =
+            List.rev (Environ.fold_named_context process_hyp env ~init:[]) in
+          (hyps,(ccl,concl_next_tac g))
+        in
+        Goals (List.map process_goal all_goals)
+      end
+end
+
 let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
   [("clear "^ident),("clear "^ident^".");
 
@@ -584,18 +675,18 @@ let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
     pr_ast
     ^".") ] @
 
-   (if is_equality_type ast then
-      [ "discriminate "^ident, "discriminate "^ident^".";
-	"injection "^ident, "injection "^ident^"." ]
-    else
-      []) @
-
-   (let _,t = splay_prod env sigma ast in
-    if is_equality_type t then
-      [ "rewrite "^ident, "rewrite "^ident^".";
-	"rewrite <- "^ident, "rewrite <- "^ident^"." ]
-    else
-      []) @
+  (if is_equality_type ast then
+     [ "discriminate "^ident, "discriminate "^ident^".";
+       "injection "^ident, "injection "^ident^"." ]
+   else
+     []) @
+
+  (let _,t = splay_prod env sigma ast in
+   if is_equality_type t then
+     [ "rewrite "^ident, "rewrite "^ident^".";
+       "rewrite <- "^ident, "rewrite <- "^ident^"." ]
+   else
+     []) @
 
   [("elim "^ident),
    ("elim "^ident^".");
diff --git a/ide/coq.mli b/ide/coq.mli
index ffa05b00a..5b76fa98a 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -79,3 +79,9 @@ type tried_tactic =
 (* Message to display in lower status bar. *)
 
 val current_status : unit -> string
+
+type 'a menu = 'a * (string * string) list
+
+type goals =
+  | Message of string
+  | Goals of ((string menu) list * string menu) list
diff --git a/ide/proof.ml b/ide/proof.ml
new file mode 100644
index 000000000..b91233e29
--- /dev/null
+++ b/ide/proof.ml
@@ -0,0 +1,94 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+
+(* $Id$ *)
+
+(* tag is the tag to be hooked, item is the item covered by this tag, make_menu
+ *  * is the template for building menu if needed, sel_cb is the callback if
+ *  there
+ *   * is a selection o said menu, hover_cb is the callback when there is only
+ *    * hovering *)
+let hook_tag_cb tag menu_content sel_cb hover_cb =
+  ignore (tag#connect#event ~callback:
+            (fun ~origin evt it ->
+               let iter = new GText.iter it in
+               let start = iter#backward_to_tag_toggle (Some tag) in
+               let stop = iter#forward_to_tag_toggle (Some tag) in
+               match GdkEvent.get_type evt with
+                 | `BUTTON_PRESS ->
+                     let ev = GdkEvent.Button.cast evt in
+                     if (GdkEvent.Button.button ev) <> 3 then false else begin
+                       let ctxt_menu = GMenu.menu () in
+                       let factory = new GMenu.factory ctxt_menu in
+                       List.iter
+                         (fun (text,cmd) -> ignore (factory#add_item text ~callback:(sel_cb cmd)))
+                         menu_content;
+                       ctxt_menu#popup ~button:3 ~time:(GdkEvent.Button.time ev);
+                       true
+                     end
+                 | `MOTION_NOTIFY ->
+                     hover_cb start stop; false
+                 | _ -> false))
+
+let mode_tactic sel_cb (proof:GText.view) = function
+  | [] -> assert false
+  | (hyps,cur_goal,cur_goal_menu)::rem_goals ->
+      let on_hover sel_start sel_stop =
+        proof#buffer#remove_tag_by_name
+          "highlight"
+          ~start:proof#buffer#start_iter
+          ~stop:sel_start;
+        proof#buffer#remove_tag_by_name
+          "highlight"
+          ~start:sel_stop
+          ~stop:proof#buffer#end_iter
+      in
+      let goals_cnt = List.length rem_goals + 1 in
+      let head_str = Printf.sprintf "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "" else "s") in
+      let insert_hyp (h,menu) =
+        let tag = proof#buffer#create_tag [] in
+        hook_tag_cb tag menu sel_cb on_hover;
+        proof#buffer#insert ~tags:[tag] (h^"\n")
+      in
+      let insert_goal g menu index total =
+        let tags = if menu <> [] then
+          let tag = proof#buffer#create_tag [] in
+          hook_tag_cb tag menu sel_cb on_hover;
+          [tag]
+          else []
+        in
+        proof#buffer#insert (Printf.sprintf
+                               "\n______________________________________(%d/%d)\n" index total);
+        proof#buffer#insert ~tags (g^"\n")
+      in
+      proof#buffer#insert head_str;
+      List.iter insert_hyp hyps;
+      insert_goal cur_goal cur_goal_menu 1 goals_cnt;
+      Util.list_fold_left_i (fun i _ (_,g,_) -> insert_goal g [] i goals_cnt) 2 () rem_goals;
+      ignore (proof#scroll_to_iter
+                ((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2)))
+
+let mode_cesar (proof:GText.view) = function
+  | [] -> assert false
+  | (hyps,(cur_goal,cur_goal_menu))::_ ->
+      proof#buffer#insert "    *** Declarative Mode ***\n";
+      List.iter
+        (fun (hyp,_) -> proof#buffer#insert (hyp^"\n"))
+        hyps;
+      proof#buffer#insert "______________________________________\n";
+      proof#buffer#insert ("thesis := \n "^cur_goal^"\n");
+      ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
+
+let display mode view goals =
+  view#buffer#set_text "";
+  match goals with
+    | Coq.Message msg ->
+        view#buffer#insert msg
+    | Coq.Goals g ->
+        mode view g