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, 274 insertions, 168 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index c58b158f0..3dc3e1431 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -679,84 +679,76 @@ let print_no_goal () =
(* Fall back on standard coq goal printer for completed goal printing *)
msg (pr_open_subgoals ())
-(**)
-(** renvoi des buts **)
-(**)
+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
+ []) @
-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 _,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." ] @
+
+ (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.";
]
-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 dff178bc2..83e6ea93b 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -84,13 +84,13 @@ val get_current_goals : unit -> goal list
val get_current_pm_goal : unit -> goal
-type context_menu = (string * string) list
-
-val goals : unit -> ((string * context_menu) list * string * context_menu) list
-val no_goal_message : unit -> string
+val print_no_goal : unit -> string
val process_exn : exn -> string*(Util.loc option)
+val hyp_menu : hyp -> (string * string) list
+val concl_menu : concl -> (string * string) list
+
val is_in_coq_lib : string -> bool
val is_in_coq_path : string -> bool
val is_in_loadpath : string -> bool
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 308291da5..6e3d86787 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -86,7 +86,9 @@ 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
@@ -721,21 +723,203 @@ 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
+ | 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_proof ->
- 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
+ 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
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 =
@@ -760,6 +944,7 @@ 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
@@ -1371,6 +1556,16 @@ 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 af620fd09..a235039b9 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -16,7 +16,6 @@ Ideutils
CoqLex
Gtk_parsing
Undo
-ProofBrowser
Coq
Coq_commands
Coq_tactics
diff --git a/ide/proofBrowser.ml b/ide/proofBrowser.ml
deleted file mode 100644
index d2f89a617..000000000
--- a/ide/proofBrowser.ml
+++ /dev/null
@@ -1,80 +0,0 @@
-(************************************************************************)
-(* 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-20 10:33:07 +0000