From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- proofs/pfedit.ml | 333 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 333 insertions(+) create mode 100644 proofs/pfedit.ml (limited to 'proofs/pfedit.ml') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml new file mode 100644 index 00000000..f53ea870 --- /dev/null +++ b/proofs/pfedit.ml @@ -0,0 +1,333 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (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 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_topstate () = snd(get_state()) +let get_pftreestate () = fst(get_state()) + +let get_end_tac () = let ts = get_topstate () in ts.top_end_tac + +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 get_current_goal_context () = get_goal_context 1 + +let set_current_proof = Edit.focus proof_edits + +let resume_proof (loc,id) = + 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 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 init_proofs () = Edit.clear proof_edits + +let mutate f = + try + Edit.mutate proof_edits (fun _ pfs -> f pfs) + with Invalid_argument "Edit.mutate" -> + errorlabstrm "Pfedit.mutate" + (str"No focused proof" ++ msg_proofs true) + +let start (na,ts) = + let pfs = mk_pftreestate ts.top_goal in + add_proof(na,pfs,ts) + +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) + +(*********************************************************************) +(* 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) + +(*********************************************************************) +(* Proof cooking *) +(*********************************************************************) + +let xml_cook_proof = ref (fun _ -> ()) +let set_xml_cook_proof f = xml_cook_proof := f + +let cook_proof () = + 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); + (ident, + ({ const_entry_body = pfterm; + const_entry_type = Some concl; + const_entry_opaque = true }, + 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 refining () = [] <> (Edit.dom proof_edits) + +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 delete_current_proof () = delete_proof_gen (get_current_proof_name ()) + +let delete_all_proofs = init_proofs + +(*********************************************************************) +(* 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 hook = + let top_goal = mk_goal sign concl in + let ts = { + top_end_tac = None; + top_hyps = (sign,empty_named_context); + 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 -> Tacmach.traverse 0 (traverse_up (n - 1) pf)) + +let rec traverse_down = function + | [] -> (function pf -> pf) + | n::l -> (function pf -> Tacmach.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 () = + let pts = get_pftreestate () in + if not (is_top_pftreestate pts) then mutate top_of_tree + +(** Printers *) + +let pr_subgoals_of_pfts pfts = + let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in + let sigma = project (top_goal_of_pftreestate pfts) in + pr_subgoals_existential sigma gls + +let pr_open_subgoals () = + let pfts = get_pftreestate () in + match focus() with + | 0 -> + pr_subgoals_of_pfts pfts + | n -> + let pf = proof_of_pftreestate pfts in + let gls = fst (frontier pf) in + assert (n > List.length gls); + if List.length gls < 2 then + pr_subgoal n gls + else + v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++ + pr_subgoal n gls) + +let pr_nth_open_subgoal n = + let pf = proof_of_pftreestate (get_pftreestate ()) in + pr_subgoal n (fst (frontier pf)) -- cgit v1.2.3