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/refiner.mli | 210 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 210 insertions(+) create mode 100644 proofs/refiner.mli (limited to 'proofs/refiner.mli') diff --git a/proofs/refiner.mli b/proofs/refiner.mli new file mode 100644 index 00000000..bed1158d --- /dev/null +++ b/proofs/refiner.mli @@ -0,0 +1,210 @@ + +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a +val sig_sig : 'a sigma -> evar_map + +val project_with_focus : goal sigma -> named_context sigma + +val unpackage : 'a sigma -> evar_map ref * 'a +val repackage : evar_map ref -> 'a -> 'a sigma +val apply_sig_tac : + evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c + +type transformation_tactic = proof_tree -> (goal list * validation) + +val add_tactic : string -> (closed_generic_argument list -> tactic) -> unit +val overwriting_add_tactic : string -> (closed_generic_argument list -> tactic) -> unit +val lookup_tactic : string -> (closed_generic_argument list) -> tactic + +(*s Hiding the implementation of tactics. *) + +(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under + a single proof node *) +val abstract_tactic : atomic_tactic_expr -> tactic -> tactic +val abstract_tactic_expr : tactic_expr -> tactic -> tactic +val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic + +val refiner : rule -> tactic +val vernac_tactic : string * closed_generic_argument list -> tactic +val frontier : transformation_tactic +val list_pf : proof_tree -> goal list +val unTAC : tactic -> goal sigma -> proof_tree sigma + +val local_Constraints : tactic + +(* [frontier_map f n p] applies f on the n-th open subgoal of p and + rebuilds proof-tree. + n=1 for first goal, n negative counts from the right *) +val frontier_map : + (proof_tree -> proof_tree) -> int -> proof_tree -> proof_tree + +(* [frontier_mapi f p] applies (f i) on the i-th open subgoal of p. *) +val frontier_mapi : + (int -> proof_tree -> proof_tree) -> proof_tree -> proof_tree + +(*s Tacticals. *) + +(* [tclIDTAC] is the identity tactic without message printing*) +val tclIDTAC : tactic +val tclIDTAC_MESSAGE : string -> tactic + + +(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [tac2] to every resulting subgoals *) +val tclTHEN : tactic -> tactic -> tactic + +(* [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More + convenient than [tclTHEN] when [n] is large *) +val tclTHENLIST : tactic list -> tactic + +(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *) +val tclTHEN_i : tactic -> (int -> tactic) -> tactic + +(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the last resulting subgoal (previously called [tclTHENL]) *) +val tclTHENLAST : tactic -> tactic -> tactic + +(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the first resulting subgoal *) +val tclTHENFIRST : tactic -> tactic -> tactic + +(* [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to + [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises + an error if the number of resulting subgoals is not [n] *) +val tclTHENSV : tactic -> tactic array -> tactic + +(* Same with a list of tactics *) +val tclTHENS : tactic -> tactic list -> tactic + +(* [tclTHENST] is renamed [tclTHENSFIRSTn] +val tclTHENST : tactic -> tactic array -> tactic -> tactic +*) + +(* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the + last [n] resulting subgoals and [tac2] on the remaining first subgoals *) +val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic + +(* [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then + applies [t1],...,[tn] on the first [n] resulting subgoals and + [tac2] for the remaining last subgoals (previously called tclTHENST) *) +val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic + +(* [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, + applies [t1],...,[tn] on the last [n] resulting subgoals and leaves + unchanged the other subgoals *) +val tclTHENLASTn : tactic -> tactic array -> tactic + +(* [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, + applies [t1],...,[tn] on the first [n] resulting subgoals and leaves + unchanged the other subgoals (previously called [tclTHENSI]) *) +val tclTHENFIRSTn : tactic -> tactic array -> tactic + +(* A special exception for levels for the Fail tactic *) +exception FailError of int * string + +val tclORELSE : tactic -> tactic -> tactic +val tclREPEAT : tactic -> tactic +val tclREPEAT_MAIN : tactic -> tactic +val tclFIRST : tactic list -> tactic +val tclSOLVE : tactic list -> tactic +val tclTRY : tactic -> tactic +val tclTHENTRY : tactic -> tactic -> tactic +val tclCOMPLETE : tactic -> tactic +val tclAT_LEAST_ONCE : tactic -> tactic +val tclFAIL : int -> string -> tactic +val tclDO : int -> tactic -> tactic +val tclPROGRESS : tactic -> tactic +val tclWEAK_PROGRESS : tactic -> tactic +val tclNOTSAMEGOAL : tactic -> tactic +val tclINFO : tactic -> tactic + +(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, + if it succeeds, applies [tac2] to the resulting subgoals, + and if not applies [tac3] to the initial goal [gls] *) +val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic +val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic +val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic + +(*s Tactics handling a list of goals. *) + +type validation_list = proof_tree list -> proof_tree list + +type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list + +val tclFIRSTLIST : tactic_list list -> tactic_list +val tclIDTAC_list : tactic_list +val first_goal : 'a list sigma -> 'a sigma +val apply_tac_list : tactic -> tactic_list +val then_tactic_list : tactic_list -> tactic_list -> tactic_list +val tactic_list_tactic : tactic_list -> tactic +val goal_goal_list : 'a sigma -> 'a list sigma + + +(*s Functions for handling the state of the proof editor. *) + +type pftreestate + +val proof_of_pftreestate : pftreestate -> proof_tree +val cursor_of_pftreestate : pftreestate -> int list +val is_top_pftreestate : pftreestate -> bool +val evc_of_pftreestate : pftreestate -> evar_map +val top_goal_of_pftreestate : pftreestate -> goal sigma +val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma + +val traverse : int -> pftreestate -> pftreestate +val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate +val solve_pftreestate : tactic -> pftreestate -> pftreestate + +(* a weak version of logical undoing, that is really correct only *) +(* if there are no existential variables. *) +val weak_undo_pftreestate : pftreestate -> pftreestate + +val mk_pftreestate : goal -> pftreestate +val extract_open_pftreestate : pftreestate -> constr * Termops.metamap +val extract_pftreestate : pftreestate -> constr +val first_unproven : pftreestate -> pftreestate +val last_unproven : pftreestate -> pftreestate +val nth_unproven : int -> pftreestate -> pftreestate +val node_prev_unproven : int -> pftreestate -> pftreestate +val node_next_unproven : int -> pftreestate -> pftreestate +val next_unproven : pftreestate -> pftreestate +val prev_unproven : pftreestate -> pftreestate +val top_of_tree : pftreestate -> pftreestate +val change_constraints_pftreestate + : evar_map -> pftreestate -> pftreestate + + +(*s Pretty-printers. *) + +(*i*) +open Pp +(*i*) + +val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds +val pr_rule : rule -> std_ppcmds +val pr_tactic : tactic_expr -> std_ppcmds +val print_script : + bool -> evar_map -> named_context -> proof_tree -> std_ppcmds +val print_treescript : + bool -> evar_map -> named_context -> proof_tree -> std_ppcmds -- cgit v1.2.3