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.mli | 183 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 183 insertions(+) create mode 100644 proofs/pfedit.mli (limited to 'proofs/pfedit.mli') diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli new file mode 100644 index 00000000..e95881ba --- /dev/null +++ b/proofs/pfedit.mli @@ -0,0 +1,183 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool + +(* [check_no_pending_proofs ()] fails if there is still some proof in + progress *) + +val check_no_pending_proofs : unit -> unit + +(*s [delete_proof name] deletes proof of name [name] or fails if no proof + has this name *) + +val delete_proof : identifier located -> unit + +(* [delete_current_proof ()] deletes current focused proof or fails if + no proof is focused *) + +val delete_current_proof : unit -> unit + +(* [delete_all_proofs ()] deletes all open proofs if any *) + +val delete_all_proofs : unit -> unit + +(*s [undo n] undoes the effect of the last [n] tactics applied to the + current proof; it fails if no proof is focused or if the ``undo'' + stack is exhausted *) + +val undo : int -> unit + +(* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None] + sets the size to the default value (12) *) + +val set_undo : int option -> unit +val get_undo : unit -> int option + +(*s [start_proof s str env t hook] starts a proof of name [s] and conclusion + [t]; [hook] is optionally a function to be applied at proof end (e.g. to + declare the built constructions as a coercion or a setoid morphism) *) + +val start_proof : + identifier -> goal_kind -> named_context -> constr + -> declaration_hook -> unit + +(* [restart_proof ()] restarts the current focused proof from the beginning + or fails if no proof is focused *) + +val restart_proof : unit -> unit + +(*s [resume_last_proof ()] focus on the last unfocused proof or fails + if there is no suspended proofs *) + +val resume_last_proof : unit -> unit + +(* [resume_proof name] focuses on the proof of name [name] or + raises [UserError] if no proof has name [name] *) + +val resume_proof : identifier located -> unit + +(* [suspend_proof ()] unfocuses the current focused proof or + failed with [UserError] if no proof is currently focused *) + +val suspend_proof : unit -> unit + +(*s [cook_proof opacity] turns the current proof (assumed completed) into + a constant with its name, kind and possible hook (see [start_proof]); + it fails if there is no current proof of if it is not completed *) + +val cook_proof : unit -> + identifier * (Entries.definition_entry * goal_kind * declaration_hook) + +(* To export completed proofs to xml *) +val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit + +(*s [get_pftreestate ()] returns the current focused pending proof or + raises [UserError "no focused proof"] *) + +val get_pftreestate : unit -> pftreestate + +(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *) + +val get_end_tac : unit -> tactic option + +(* [get_goal_context n] returns the context of the [n]th subgoal of + the current focused proof or raises a [UserError] if there is no + focused proof or if there is no more subgoals *) + +val get_goal_context : int -> Evd.evar_map * env + +(* [get_current_goal_context ()] works as [get_goal_context 1] *) + +val get_current_goal_context : unit -> Evd.evar_map * env + +(* [current_proof_statement] *) + +val current_proof_statement : + unit -> identifier * goal_kind * types * declaration_hook + +(*s [get_current_proof_name ()] return the name of the current focused + proof or failed if no proof is focused *) + +val get_current_proof_name : unit -> identifier + +(* [get_all_proof_names ()] returns the list of all pending proof names *) + +val get_all_proof_names : unit -> identifier list + +(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate + by [solve_nth] *) + +val set_end_tac : tactic -> unit + +(*s [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the + current focused proof or raises a UserError if no proof is focused or + if there is no [n]th subgoal *) + +val solve_nth : int -> tactic -> unit + +(* [by tac] applies tactic [tac] to the 1st subgoal of the current + focused proof or raises a UserError if there is no focused proof or + if there is no more subgoals *) + +val by : tactic -> unit + +(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined + existential variable of the current focused proof by [c] or raises a + UserError if no proof is focused or if there is no such [n]th + existential variable *) + +val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit + +(*s To deal with subgoal focus *) + +val make_focus : int -> unit +val focus : unit -> int +val focused_goal : unit -> int +val subtree_solved : unit -> bool + +val reset_top_of_tree : unit -> unit +val traverse : int -> unit +val traverse_nth_goal : int -> unit +val traverse_next_unproven : unit -> unit +val traverse_prev_unproven : unit -> unit + + +(* These two functions make it possible to implement more elaborate + proof and goal management, as it is done, for instance in pcoq *) +val traverse_to : int list -> unit +val mutate : (pftreestate -> pftreestate) -> unit + +(** Printers *) + +val pr_open_subgoals : unit -> std_ppcmds +val pr_nth_open_subgoal : int -> std_ppcmds -- cgit v1.2.3