aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.ml142
-rw-r--r--ide/coq.mli8
-rw-r--r--ide/coqide.ml211
-rw-r--r--ide/ide.mllib1
-rw-r--r--ide/proofBrowser.ml80
5 files changed, 168 insertions, 274 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 3dc3e1431..c58b158f0 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -679,76 +679,84 @@ let print_no_goal () =
(* Fall back on standard coq goal printer for completed goal printing *)
msg (pr_open_subgoals ())
-let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
- [("clear "^ident),("clear "^ident^".");
-
- ("apply "^ident),
- ("apply "^ident^".");
-
- ("exact "^ident),
- ("exact "^ident^".");
-
- ("generalize "^ident),
- ("generalize "^ident^".");
-
- ("absurd <"^ident^">"),
- ("absurd "^
- 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
- []) @
-
- [("elim "^ident),
- ("elim "^ident^".");
-
- ("inversion "^ident),
- ("inversion "^ident^".");
-
- ("inversion clear "^ident),
- ("inversion_clear "^ident^".")]
-
-let concl_menu (_,_,concl,_) =
- let is_eq = is_equality_type concl in
- ["intro", "intro.";
- "intros", "intros.";
- "intuition","intuition." ] @
+(**)
+(** renvoi des buts **)
+(**)
- (if is_eq then
- ["reflexivity", "reflexivity.";
- "discriminate", "discriminate.";
- "symmetry", "symmetry." ]
- else
- []) @
-
- ["assumption" ,"assumption.";
- "omega", "omega.";
- "ring", "ring.";
- "auto with *", "auto with *.";
- "eauto with *", "eauto with *.";
- "tauto", "tauto.";
- "trivial", "trivial.";
- "decide equality", "decide equality.";
-
- "simpl", "simpl.";
- "subst", "subst.";
-
- "red", "red.";
- "split", "split.";
- "left", "left.";
- "right", "right.";
+type context_menu = (string * string) list
+
+let string_of_ppcmds c =
+ Pp.msg_with Format.str_formatter c;
+ Format.flush_str_formatter ()
+
+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
+ 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
+ let goals_strings = List.map process_goal all_goals in
+ goals_strings
+
+let no_goal_message () =
+ string_of_ppcmds (pr_open_subgoals ())
+
+(** **)
let id_of_name = function
| Names.Anonymous -> id_of_string "x"
diff --git a/ide/coq.mli b/ide/coq.mli
index 83e6ea93b..dff178bc2 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -84,12 +84,12 @@ val get_current_goals : unit -> goal list
val get_current_pm_goal : unit -> goal
-val print_no_goal : unit -> string
+type context_menu = (string * string) list
-val process_exn : exn -> string*(Util.loc option)
+val goals : unit -> ((string * context_menu) list * string * context_menu) list
+val no_goal_message : unit -> string
-val hyp_menu : hyp -> (string * string) list
-val concl_menu : concl -> (string * string) list
+val process_exn : exn -> string*(Util.loc option)
val is_in_coq_lib : string -> bool
val is_in_coq_path : string -> bool
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 6e3d86787..308291da5 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -86,9 +86,7 @@ object('self)
bool -> bool -> bool ->
(bool*reset_info) option
method set_message : string -> unit
- method show_pm_goal : unit
method show_goals : unit
- method show_goals_full : unit
method undo_last_step : unit
method help_for_keyword : unit -> unit
method complete_at_offset : int -> bool
@@ -723,203 +721,21 @@ object(self)
(String.make previous_line_spaces ' ')
end
- method show_pm_goal =
- proof_buffer#insert
- (Printf.sprintf " *** Declarative Mode ***\n");
- try
- let (hyps,concl) = get_current_pm_goal () in
- List.iter
- (fun ((_,_,_,(s,_)) as _hyp) ->
- proof_buffer#insert (s^"\n"))
- hyps;
- proof_buffer#insert
- (String.make 38 '_' ^ "\n");
- let (_,_,_,s) = concl in
- proof_buffer#insert ("thesis := \n "^s^"\n");
- let my_mark = `NAME "end_of_conclusion" in
- proof_buffer#move_mark
- ~where:((proof_buffer#get_iter_at_mark `INSERT))
- my_mark;
- ignore (proof_view#scroll_to_mark my_mark)
- with Not_found ->
- match Decl_mode.get_end_command (Pfedit.get_pftreestate ()) with
- Some endc ->
- proof_buffer#insert
- ("Subproof completed, now type "^endc^".")
- | None ->
- proof_buffer#insert "Proof completed."
-
method show_goals =
try
proof_buffer#set_text "";
match Decl_mode.get_current_mode () with
Decl_mode.Mode_none -> ()
- | Decl_mode.Mode_tactic ->
- begin
- let s = Coq.get_current_goals () in
- match s with
- | [] -> proof_buffer#insert (Coq.print_no_goal ())
- | (hyps,concl)::r ->
- let goal_nb = List.length s in
- proof_buffer#insert
- (Printf.sprintf "%d subgoal%s\n"
- goal_nb
- (if goal_nb<=1 then "" else "s"));
- List.iter
- (fun ((_,_,_,(s,_)) as _hyp) ->
- proof_buffer#insert (s^"\n"))
- hyps;
- proof_buffer#insert
- (String.make 38 '_' ^ "(1/"^
- (string_of_int goal_nb)^
- ")\n") ;
- let _,_,_,sconcl = concl in
- proof_buffer#insert sconcl;
- proof_buffer#insert "\n";
- let my_mark = `NAME "end_of_conclusion" in
- proof_buffer#move_mark
- ~where:((proof_buffer#get_iter_at_mark `INSERT))
- my_mark;
- proof_buffer#insert "\n\n";
- let i = ref 1 in
- List.iter
- (function (_,(_,_,_,concl)) ->
- incr i;
- proof_buffer#insert
- (String.make 38 '_' ^"("^
- (string_of_int !i)^
- "/"^
- (string_of_int goal_nb)^
- ")\n");
- proof_buffer#insert concl;
- proof_buffer#insert "\n\n";
- )
- r;
- ignore (proof_view#scroll_to_mark my_mark)
- end
+ | Decl_mode.Mode_tactic
| Decl_mode.Mode_proof ->
- self#show_pm_goal
- with e ->
- prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
-
-
- val mutable full_goal_done = true
-
- method show_goals_full =
- if not full_goal_done then
- begin
- try
- proof_buffer#set_text "";
- match Decl_mode.get_current_mode () with
- Decl_mode.Mode_none -> ()
- | Decl_mode.Mode_tactic ->
- begin
- match Coq.get_current_goals () with
- [] -> Util.anomaly "show_goals_full"
- | ((hyps,concl)::r) as s ->
- let last_shown_area = Tags.Proof.highlight
- in
- let goal_nb = List.length s in
- proof_buffer#insert (Printf.sprintf "%d subgoal%s\n"
- goal_nb
- (if goal_nb<=1 then "" else "s"));
- let coq_menu commands =
- let tag = proof_buffer#create_tag []
- in
- ignore
- (tag#connect#event ~callback:
- (fun ~origin ev it ->
- match GdkEvent.get_type ev with
- | `BUTTON_PRESS ->
- let ev = (GdkEvent.Button.cast ev) in
- if (GdkEvent.Button.button ev) = 3
- then (
- let loc_menu = GMenu.menu () in
- let factory =
- new GMenu.factory loc_menu in
- let add_coq_command (cp,ip) =
- ignore
- (factory#add_item cp
- ~callback:
- (fun () -> ignore
- (self#insert_this_phrase_on_success
- true
- true
- false
- ("progress "^ip^"\n")
- (ip^"\n"))
- )
- )
- in
- List.iter add_coq_command commands;
- loc_menu#popup
- ~button:3
- ~time:(GdkEvent.Button.time ev);
- true)
- else false
- | `MOTION_NOTIFY ->
- proof_buffer#remove_tag
- ~start:proof_buffer#start_iter
- ~stop:proof_buffer#end_iter
- last_shown_area;
- prerr_endline "Before find_tag_limits";
-
- let s,e = find_tag_limits tag
- (new GText.iter it)
- in
- prerr_endline "After find_tag_limits";
- proof_buffer#apply_tag
- ~start:s
- ~stop:e
- last_shown_area;
-
- prerr_endline "Applied tag";
- false
- | _ ->
- false
- )
- );
- tag
- in
- List.iter
- (fun ((_,_,_,(s,_)) as hyp) ->
- let tag = coq_menu (hyp_menu hyp) in
- proof_buffer#insert ~tags:[tag] (s^"\n"))
- hyps;
- proof_buffer#insert
- (String.make 38 '_' ^"(1/"^
- (string_of_int goal_nb)^
- ")\n")
- ;
- let tag = coq_menu (concl_menu concl) in
- let _,_,_,sconcl = concl in
- proof_buffer#insert ~tags:[tag] sconcl;
- proof_buffer#insert "\n";
- let my_mark = `NAME "end_of_conclusion" in
- proof_buffer#move_mark
- ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
- proof_buffer#insert "\n\n";
- let i = ref 1 in
- List.iter
- (function (_,(_,_,_,concl)) ->
- incr i;
- proof_buffer#insert
- (String.make 38 '_' ^"("^
- (string_of_int !i)^
- "/"^
- (string_of_int goal_nb)^
- ")\n");
- proof_buffer#insert concl;
- proof_buffer#insert "\n\n";
- )
- r;
- ignore (proof_view#scroll_to_mark my_mark) ;
- full_goal_done <- true
- end
- | Decl_mode.Mode_proof ->
- self#show_pm_goal
+ match Coq.goals () with
+ | [] -> proof_buffer#insert (Coq.no_goal_message ())
+ | ((hyps,concl,ccl_menu)::r) as s ->
+ let on_sel ip () =
+ ignore (self#insert_this_phrase_on_success true true false
+ ("progress" ^ ip ^ "\n") (ip^"\n")) in
+ ProofBrowser.display_proof proof_view on_sel s
with e -> prerr_endline (Printexc.to_string e)
- end
method send_to_coq verbosely replace phrase show_output show_error localize =
let display_output msg =
@@ -944,7 +760,6 @@ object(self)
~stop:stopi;
input_buffer#place_cursor starti) in
try
- full_goal_done <- false;
prerr_endline "Send_to_coq starting now";
Decl_mode.clear_daimon_flag ();
if replace then begin
@@ -1556,16 +1371,6 @@ let create_session () =
ignore (GtkText.Tag.event t#as_tag proof#as_widget e it#as_iter))
tags;
false) in
- let _ =
- proof#event#connect#enter_notify
- (fun _ -> if !current.contextual_menus_on_goal then
- begin
- push_info "Computing advanced goal menus";
- prerr_endline "Entering Goal Window. Computing Menus...";
- on_active_view (function {analyzed_view = av} -> av#show_goals_full);
- prerr_endline "...Done with Goal menu.";
- pop_info();
- end; false) in
script#misc#set_name "ScriptWindow";
script#buffer#place_cursor ~where:(script#buffer#start_iter);
proof#misc#set_can_focus true;
diff --git a/ide/ide.mllib b/ide/ide.mllib
index a235039b9..af620fd09 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -16,6 +16,7 @@ Ideutils
CoqLex
Gtk_parsing
Undo
+ProofBrowser
Coq
Coq_commands
Coq_tactics
diff --git a/ide/proofBrowser.ml b/ide/proofBrowser.ml
new file mode 100644
index 000000000..d2f89a617
--- /dev/null
+++ b/ide/proofBrowser.ml
@@ -0,0 +1,80 @@
+(************************************************************************)
+(* 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: coqide.ml 11952 2009-03-02 15:29:08Z vgross $ *)
+
+(* 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 display_proof (proof:GText.view) sel_cb = function
+ | [] -> ()
+ | (hyps,cur_goal,cur_goal_menu)::rem_goals ->
+ let on_hover sel_start sel_stop =
+ proof#buffer#remove_tag
+ ~start:proof#buffer#start_iter
+ ~stop:sel_start
+ Tags.Proof.highlight;
+ proof#buffer#apply_tag
+ ~start:sel_start
+ ~stop:sel_stop
+ Tags.Proof.highlight;
+ proof#buffer#remove_tag
+ ~start:sel_stop
+ ~stop:proof#buffer#end_iter
+ Tags.Proof.highlight;
+ 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)))
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-18 05:16:17 +0000