diff options
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r-- | proofs/pfedit.ml | 424 |
1 files changed, 129 insertions, 295 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a9799f38..3d507f35 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pfedit.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -20,322 +18,139 @@ open Environ open Evd open Typing open Refiner -open Proof_trees open Tacexpr open Proof_type open Lib open Safe_typing -(*********************************************************************) -(* Managing the proofs state *) -(* Mainly contributed by C. Murthy *) -(*********************************************************************) - -type lemma_possible_guards = int list list - -type proof_topstate = { - mutable top_end_tac : tactic option; - top_init_tac : tactic option; - top_compute_guard : lemma_possible_guards; - top_goal : goal; - top_strength : Decl_kinds.goal_kind; - top_hook : declaration_hook } - -let proof_edits = - (Edit.empty() : (identifier,pftreestate,proof_topstate) Edit.t) - -let get_all_proof_names () = Edit.dom proof_edits - -let msg_proofs use_resume = - match Edit.dom proof_edits with - | [] -> (spc () ++ str"(No proof-editing in progress).") - | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++ - (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ++ - str"." ++ - (if use_resume then (fnl () ++ str"Use \"Resume\" first.") - else (mt ())) -) - -let undo_default = 50 -let undo_limit = ref undo_default - -(*********************************************************************) -(* Functions for decomposing and modifying the proof state *) -(*********************************************************************) +let refining = Proof_global.there_are_pending_proofs +let check_no_pending_proofs = Proof_global.check_no_pending_proof -let get_state () = - match Edit.read proof_edits with - | None -> errorlabstrm "Pfedit.get_state" - (str"No focused proof" ++ msg_proofs true) - | Some(_,pfs,ts) -> (pfs,ts) +let get_current_proof_name = Proof_global.get_current_proof_name +let get_all_proof_names = Proof_global.get_all_proof_names -let get_topstate () = snd(get_state()) -let get_pftreestate () = fst(get_state()) +type lemma_possible_guards = Proof_global.lemma_possible_guards -let get_end_tac () = let ts = get_topstate () in ts.top_end_tac +let delete_proof = Proof_global.discard +let delete_current_proof = Proof_global.discard_current +let delete_all_proofs = Proof_global.discard_all -let get_goal_context n = - let pftree = get_pftreestate () in - let goal = nth_goal_of_pftreestate n pftree in - (project goal, pf_env goal) +let undo n = + let p = Proof_global.give_me_the_proof () in + for i = 1 to n do + Proof.undo p + done -let get_current_goal_context () = get_goal_context 1 - -let set_current_proof = Edit.focus proof_edits - -let resume_proof (loc,id) = +let current_proof_depth () = try - Edit.focus proof_edits id - with Invalid_argument "Edit.focus" -> - user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false) + let p = Proof_global.give_me_the_proof () in + Proof.V82.depth p + with Proof_global.NoCurrentProof -> -1 -let suspend_proof () = - try - Edit.unfocus proof_edits - with Invalid_argument "Edit.unfocus" -> - errorlabstrm "Pfedit.suspend_current_proof" - (str"No active proof" ++ (msg_proofs true)) - -let resume_last_proof () = - match (Edit.last_focused proof_edits) with - | None -> - errorlabstrm "resume_last" (str"No proof-editing in progress.") - | Some p -> - Edit.focus proof_edits p - -let get_current_proof_name () = - match Edit.read proof_edits with - | None -> - errorlabstrm "Pfedit.get_proof" - (str"No focused proof" ++ msg_proofs true) - | Some(na,_,_) -> na - -let add_proof (na,pfs,ts) = - Edit.create proof_edits (na,pfs,ts,!undo_limit+1) - -let delete_proof_gen = Edit.delete proof_edits - -let delete_proof (loc,id) = - try - delete_proof_gen id - with (UserError ("Edit.delete",_)) -> - user_err_loc - (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false) - -let mutate f = +(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d + is the depth of the focus stack). *) +let undo_todepth n = try - Edit.mutate proof_edits (fun _ pfs -> f pfs) - with Invalid_argument "Edit.mutate" -> - errorlabstrm "Pfedit.mutate" - (str"No focused proof" ++ msg_proofs true) + undo ((current_proof_depth ()) - n ) + with Proof_global.NoCurrentProof when n=0 -> () -let start (na,ts) = - let pfs = mk_pftreestate ts.top_goal in - let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in - add_proof(na,pfs,ts) +let set_undo _ = () +let get_undo _ = None -let restart_proof () = - match Edit.read proof_edits with - | None -> - errorlabstrm "Pfedit.restart" - (str"No focused proof to restart" ++ msg_proofs true) - | Some(na,_,ts) -> - delete_proof_gen na; - start (na,ts); - set_current_proof na - -let proof_term () = - extract_pftreestate (get_pftreestate()) - -(* Detect is one has completed a subtree of the initial goal *) -let subtree_solved () = - let pts = get_pftreestate () in - is_complete_proof (proof_of_pftreestate pts) & - not (is_top_pftreestate pts) - -let tree_solved () = - let pts = get_pftreestate () in - is_complete_proof (proof_of_pftreestate pts) - -let top_tree_solved () = - let pts = get_pftreestate () in - is_complete_proof (proof_of_pftreestate (top_of_tree pts)) - -(*********************************************************************) -(* Undo functions *) -(*********************************************************************) - -let set_undo = function - | None -> undo_limit := undo_default - | Some n -> - if n>=0 then - undo_limit := n - else - error "Cannot set a negative undo limit" - -let get_undo () = Some !undo_limit - -let undo n = - try - Edit.undo proof_edits n; - (* needed because the resolution of a subtree is done in 2 steps - then a sequence of undo can lead to a focus on a completely solved - subtree - this solution only works properly if undoing one step *) - if subtree_solved() then Edit.undo proof_edits 1 - with (Invalid_argument "Edit.undo") -> - errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true) - -(* Undo current focused proof to reach depth [n]. This is used in - [vernac_backtrack]. *) -let undo_todepth n = - try - Edit.undo_todepth proof_edits n - with (Invalid_argument "Edit.undo") -> - errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true) -(* Return the depth of the current focused proof stack, this is used - to put informations in coq prompt (in emacs mode). *) -let current_proof_depth() = - try - Edit.depth proof_edits - with (Invalid_argument "Edit.depth") -> -1 +let start_proof id str hyps c ?init_tac ?compute_guard hook = + let goals = [ (Global.env_of_context hyps , c) ] in + let init_tac = Option.map Proofview.V82.tactic init_tac in + Proof_global.start_proof id str goals ?compute_guard hook; + Option.iter Proof_global.run_tactic init_tac -(*********************************************************************) -(* Proof cooking *) -(*********************************************************************) +let restart_proof () = + let p = Proof_global.give_me_the_proof () in + try while true do + Proof.undo p + done with Proof.EmptyUndoStack -> () + +let resume_last_proof () = Proof_global.resume_last () +let resume_proof (_,id) = Proof_global.resume id +let suspend_proof () = Proof_global.suspend () + +let cook_proof hook = + let prf = Proof_global.give_me_the_proof () in + hook prf; + match Proof_global.close_proof () with + | (i,([e],cg,str,h)) -> (i,(e,cg,str,h)) + | _ -> Util.anomaly "Pfedit.cook_proof: more than one proof term." let xml_cook_proof = ref (fun _ -> ()) let set_xml_cook_proof f = xml_cook_proof := f -let cook_proof k = - let (pfs,ts) = get_state() - and ident = get_current_proof_name () in - let {evar_concl=concl} = ts.top_goal - and strength = ts.top_strength in - let pfterm = extract_pftreestate pfs in - !xml_cook_proof (strength,pfs); - k pfs; - (ident, - ({ const_entry_body = pfterm; - const_entry_type = Some concl; - const_entry_opaque = true; - const_entry_boxed = false}, - ts.top_compute_guard, strength, ts.top_hook)) - -let current_proof_statement () = - let ts = get_topstate() in - (get_current_proof_name (), ts.top_strength, - ts.top_goal.evar_concl, ts.top_hook) - -(*********************************************************************) -(* Abort functions *) -(*********************************************************************) +let get_pftreestate () = + Proof_global.give_me_the_proof () -let refining () = [] <> (Edit.dom proof_edits) +let set_end_tac tac = + let tac = Proofview.V82.tactic tac in + Proof_global.set_endline_tactic tac + +let set_used_variables l = + Proof_global.set_used_variables l +let get_used_variables () = + Proof_global.get_used_variables () + +exception NoSuchGoal +let _ = Errors.register_handler begin function + | NoSuchGoal -> Util.error "No such goal." + | _ -> raise Errors.Unhandled +end +let get_nth_V82_goal i = + let p = Proof_global.give_me_the_proof () in + let { it=goals ; sigma = sigma } = Proof.V82.subgoals p in + try + { it=(List.nth goals (i-1)) ; sigma=sigma } + with Failure _ -> raise NoSuchGoal + +let get_goal_context_gen i = + try + let { it=goal ; sigma=sigma } = get_nth_V82_goal i in + (sigma, Refiner.pf_env { it=goal ; sigma=sigma }) + with Proof_global.NoCurrentProof -> Util.error "No focused proof." -let check_no_pending_proofs () = - if refining () then - errorlabstrm "check_no_pending_proofs" - (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++ - str"Use \"Abort All\" first or complete proof(s).") +let get_goal_context i = + try get_goal_context_gen i + with NoSuchGoal -> Util.error "No such goal." -let delete_current_proof () = delete_proof_gen (get_current_proof_name ()) +let get_current_goal_context () = + try get_goal_context_gen 1 + with NoSuchGoal -> + (* spiwack: returning empty evar_map, since if there is no goal, under focus, + there is no accessible evar either *) + (Evd.empty, Global.env ()) -let delete_all_proofs () = Edit.clear proof_edits +let current_proof_statement () = + match Proof_global.V82.get_current_initial_conclusions () with + | (id,([concl],strength,hook)) -> id,strength,concl,hook + | _ -> Util.anomaly "Pfedit.current_proof_statement: more than one statement" + +let solve_nth ?(with_end_tac=false) gi tac = + try + let tac = Proofview.V82.tactic tac in + let tac = if with_end_tac then + Proof_global.with_end_tac tac + else + tac + in + Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac) + with + | Proof_global.NoCurrentProof -> Util.error "No focused proof" + | Proofview.IndexOutOfRange | Failure "list_chop" -> + let msg = str "No such goal: " ++ int gi ++ str "." in + Util.errorlabstrm "" msg + +let by = solve_nth 1 + +let instantiate_nth_evar_com n com = + let pf = Proof_global.give_me_the_proof () in + Proof.V82.instantiate_evar n com pf -(*********************************************************************) -(* Modifying the end tactic of the current profftree *) -(*********************************************************************) -let set_end_tac tac = - let top = get_topstate () in - top.top_end_tac <- Some tac - -(*********************************************************************) -(* Modifying the current prooftree *) -(*********************************************************************) - -let start_proof na str sign concl ?init_tac ?(compute_guard=[]) hook = - let top_goal = mk_goal sign concl None in - let ts = { - top_end_tac = None; - top_init_tac = init_tac; - top_compute_guard = compute_guard; - top_goal = top_goal; - top_strength = str; - top_hook = hook} - in - start(na,ts); - set_current_proof na - -let solve_nth k tac = - let pft = get_pftreestate () in - if not (List.mem (-1) (cursor_of_pftreestate pft)) then - mutate (solve_nth_pftreestate k tac) - else - error "cannot apply a tactic when we are descended behind a tactic-node" - -let by tac = mutate (solve_pftreestate tac) - -let instantiate_nth_evar_com n c = - mutate (Evar_refiner.instantiate_pf_com n c) - -let traverse n = mutate (traverse n) - -(* [traverse_to path] - - Traverses the current proof to get to the location specified by - [path]. - - ALGORITHM: The algorithm works on reversed paths. One just has to remove - the common part on the reversed paths. - -*) - -let common_ancestor l1 l2 = - let rec common_aux l1 l2 = - match l1, l2 with - | a1::l1', a2::l2' when a1 = a2 -> common_aux l1' l2' - | _, _ -> List.rev l1, List.length l2 - in - common_aux (List.rev l1) (List.rev l2) - -let rec traverse_up = function - | 0 -> (function pf -> pf) - | n -> (function pf -> Refiner.traverse 0 (traverse_up (n - 1) pf)) - -let rec traverse_down = function - | [] -> (function pf -> pf) - | n::l -> (function pf -> Refiner.traverse n (traverse_down l pf)) - -let traverse_to path = - let up_and_down path pfs = - let cursor = cursor_of_pftreestate pfs in - let down_list, up_count = common_ancestor path cursor in - traverse_down down_list (traverse_up up_count pfs) - in - mutate (up_and_down path) - -(* traverse the proof tree until it reach the nth subgoal *) -let traverse_nth_goal n = mutate (nth_unproven n) - -let traverse_prev_unproven () = mutate prev_unproven - -let traverse_next_unproven () = mutate next_unproven - -(* The goal focused on *) -let focus_n = ref 0 -let make_focus n = focus_n := n -let focus () = !focus_n -let focused_goal () = let n = !focus_n in if n=0 then 1 else n - -let reset_top_of_tree () = - mutate top_of_tree - -let reset_top_of_script () = - mutate (fun pts -> - try - up_until_matching_rule is_proof_instr pts - with Not_found -> top_of_tree pts) (**********************************************************************) (* Shortcut to build a term using tactics *) @@ -355,7 +170,26 @@ let build_constant_by_tactic id sign typ tac = delete_current_proof (); raise e -let build_by_tactic typ tac = +let build_by_tactic env typ tac = let id = id_of_string ("temporary_proof"^string_of_int (next())) in - let sign = Decls.clear_proofs (Global.named_context ()) in + let sign = val_of_named_context (named_context env) in (build_constant_by_tactic id sign typ tac).const_entry_body + +(**********************************************************************) +(* Support for resolution of evars in tactic interpretation, including + resolution by application of tactics *) + +let implicit_tactic = ref None + +let declare_implicit_tactic tac = implicit_tactic := Some tac + +let solve_by_implicit_tactic env sigma (evk,args) = + let evi = Evd.find_undefined sigma evk in + match (!implicit_tactic, snd (evar_source evk sigma)) with + | Some tac, (ImplicitArg _ | QuestionMark _) + when + Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + (Environ.named_context env) -> + (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac) + with e when Logic.catchable_exception e -> raise Exit) + | _ -> raise Exit |