diff options
| -rw-r--r-- | ide/coq.ml | 275 | ||||
| -rw-r--r-- | ide/coq.mli | 18 | ||||
| -rw-r--r-- | ide/coqide.ml | 184 | ||||
| -rw-r--r-- | ide/ide.mllib | 1 | ||||
| -rw-r--r-- | ide/proof.ml | 17 |
5 files changed, 96 insertions, 399 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 1f9e396b7..954fbfa02 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -518,55 +518,6 @@ type tried_tactic = | Success of int (* nb of goals after *) | Failed -type hyp = env * evar_map * - ((identifier * string) * constr option * constr) * - (string * string) -type concl = env * evar_map * constr * string -type meta = env * evar_map * string -type goal = hyp list * concl - -let prepare_hyp sigma env ((i,c,d) as a) = - env, sigma, - ((i,string_of_id i),c,d), - (msg (pr_var_decl env a), msg (pr_ltype_env env d)) - -let prepare_hyps sigma env = - assert (rel_context env = []); - let hyps = - fold_named_context - (fun env d acc -> let hyp = prepare_hyp sigma env d in hyp :: acc) - env ~init:[] - in - List.rev hyps - -let prepare_goal_main sigma g = - let env = evar_env g in - (prepare_hyps sigma env, - (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl))) - -let prepare_goal sigma g = - let x = prepare_goal_main sigma g in - x - -let get_current_pm_goal () = - PrintOpt.enforce_hack (); - let pfts = get_pftreestate () in - let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in - let sigma= sig_sig gls in - let gl = sig_it gls in - prepare_goal sigma gl - -let get_current_goals () = - PrintOpt.enforce_hack (); - let pfts = get_pftreestate () in - let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in - let sigma = Tacmach.evc_of_pftreestate pfts in - List.map (prepare_goal sigma) gls - -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 () @@ -577,157 +528,85 @@ 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^"."); - - ("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." ] @ - - (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 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 () = + PrintOpt.enforce_hack (); + 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 + let id_of_name = function | Names.Anonymous -> id_of_string "x" diff --git a/ide/coq.mli b/ide/coq.mli index 5b76fa98a..173bd75f7 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -47,30 +47,14 @@ val is_vernac_proof_ending_command : Vernacexpr.vernac_expr -> bool (* type hyp = (identifier * constr option * constr) * string *) -type hyp = env * evar_map * - ((identifier*string) * constr option * constr) * (string * string) -type meta = env * evar_map * string -type concl = env * evar_map * constr * string -type goal = hyp list * concl - -val get_current_goals : unit -> goal list - -val get_current_pm_goal : unit -> goal - -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 val make_cases : string -> string list list - type tried_tactic = | Interrupted | Success of int (* nb of goals after *) @@ -85,3 +69,5 @@ type 'a menu = 'a * (string * string) list type goals = | Message of string | Goals of ((string menu) list * string menu) list + +val goals : unit -> goals diff --git a/ide/coqide.ml b/ide/coqide.ml index f9101cf8a..7f878646e 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -87,7 +87,6 @@ object('self) bool -> bool -> bool -> (bool*int) 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 @@ -731,201 +730,32 @@ 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 + Proof.display (Proof.mode_tactic (fun _ _ -> ())) proof_view (Coq.goals ()) | Decl_mode.Mode_proof -> - self#show_pm_goal + Proof.display Proof.mode_cesar proof_view (Coq.goals ()) 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 + Proof.display + (Proof.mode_tactic (fun s () -> ignore (self#insert_this_phrase_on_success + true true false ("progress "^s) s))) + proof_view (Coq.goals ()) | Decl_mode.Mode_proof -> - self#show_pm_goal + Proof.display Proof.mode_cesar proof_view (Coq.goals ()) with e -> prerr_endline (Printexc.to_string e) end diff --git a/ide/ide.mllib b/ide/ide.mllib index 63935db38..fe91cf339 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -13,6 +13,7 @@ Config_lexer Utf8_convert Preferences Ideutils +Proof Coq_lex Gtk_parsing Undo diff --git a/ide/proof.ml b/ide/proof.ml index b91233e29..700b5a729 100644 --- a/ide/proof.ml +++ b/ide/proof.ml @@ -38,16 +38,17 @@ let hook_tag_cb tag menu_content sel_cb hover_cb = let mode_tactic sel_cb (proof:GText.view) = function | [] -> assert false - | (hyps,cur_goal,cur_goal_menu)::rem_goals -> + | (hyps,(cur_goal,cur_goal_menu))::rem_goals -> let on_hover sel_start sel_stop = - proof#buffer#remove_tag_by_name - "highlight" + proof#buffer#remove_tag ~start:proof#buffer#start_iter - ~stop:sel_start; - proof#buffer#remove_tag_by_name - "highlight" + ~stop:sel_start + Tags.Proof.highlight; + proof#buffer#remove_tag ~start:sel_stop ~stop:proof#buffer#end_iter + Tags.Proof.highlight; + proof#buffer#apply_tag ~start:sel_start ~stop:sel_stop 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 @@ -70,7 +71,7 @@ let mode_tactic sel_cb (proof:GText.view) = function 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; + 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))) @@ -85,7 +86,7 @@ let mode_cesar (proof:GText.view) = function 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 = +let display mode (view:GText.view) goals = view#buffer#set_text ""; match goals with | Coq.Message msg -> |