diff options
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 148 |
1 files changed, 36 insertions, 112 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 8167bfb2..75fd6d3d 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -1,23 +1,19 @@ (************************************************************************) (* 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 *) (************************************************************************) -(*i $Id: refiner.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Term open Sign open Evd -open Proof_trees open Proof_type open Tacexpr -(*i*) +open Logic -(* The refiner (handles primitive rules and high-level tactics). *) +(** The refiner (handles primitive rules and high-level tactics). *) val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map @@ -28,14 +24,14 @@ val pf_hyps : goal sigma -> named_context val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma val apply_sig_tac : - evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation - -type transformation_tactic = proof_tree -> (goal list * validation) + evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list -(*s Hiding the implementation of tactics. *) +(** {6 Hiding the implementation of tactics. } *) -(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under +(** [abstract_tactic tac] hides the (partial) proof produced by [tac] under a single proof node. The boolean tells if the default tactic is used. *) +(* spiwack: currently here for compatibility, abstract_operation + is a second projection *) val abstract_operation : compound_rule -> tactic -> tactic val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic @@ -43,100 +39,84 @@ val abstract_extended_tactic : ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic val refiner : rule -> tactic -val frontier : transformation_tactic -val list_pf : proof_tree -> goal list -val unTAC : tactic -> goal sigma -> proof_tree sigma - - -(* Install a hook frontier_map and frontier_mapi call on the new node they create *) -val set_solve_hook : (Proof_type.proof_tree -> unit) -> unit -(* [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. *) +(** {6 Tacticals. } *) -(* [tclNORMEVAR] forces propagation of evar constraints *) +(** [tclNORMEVAR] forces propagation of evar constraints *) val tclNORMEVAR : tactic -(* [tclIDTAC] is the identity tactic without message printing*) +(** [tclIDTAC] is the identity tactic without message printing*) val tclIDTAC : tactic val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic -(* [tclEVARS sigma] changes the current evar map *) +(** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies +(** [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 +(** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More convenient than [tclTHEN] when [n] is large *) val tclTHENLIST : tactic list -> tactic -(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) +(** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) val tclMAP : ('a -> tactic) -> 'a 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) *) +(** [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] +(** [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] +(** [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 +(** [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 *) +(** Same with a list of tactics *) val tclTHENS : tactic -> tactic list -> tactic -(* [tclTHENST] is renamed [tclTHENSFIRSTn] +(** [tclTHENST] is renamed [tclTHENSFIRSTn] val tclTHENST : tactic -> tactic array -> tactic -> tactic *) -(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] +(** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] subgoals and [tac2] to the rest of the subgoals in the middle. Raises an error if the number of resulting subgoals is strictly less than [n+m] *) val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic -(* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the +(** [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 +(** [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, +(** [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, +(** [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 *) +(** A special exception for levels for the Fail tactic *) exception FailError of int * Pp.std_ppcmds Lazy.t -(* Takes an exception and either raise it at the next +(** Takes an exception and either raise it at the next level or do nothing. *) val catch_failerror : exn -> unit @@ -153,29 +133,28 @@ val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> Pp.std_ppcmds -> tactic val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic -val tclPROGRESS : tactic -> tactic +val tclTIMEOUT : int -> tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic +val tclPROGRESS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic val tclINFO : tactic -> tactic -(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, +(** [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 -(* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] +(** [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. Equivalent to [(tac1;try tac2)||tac2] *) val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic -(*s Tactics handling a list of goals. *) +(** {6 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 +type tactic_list = goal list sigma -> goal list sigma val tclFIRSTLIST : tactic_list list -> tactic_list val tclIDTAC_list : tactic_list @@ -185,63 +164,8 @@ 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 -(* [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which +(** [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which may have unresolved holes; if [solve_holes] these holes must be resolved after application of the tactic; [sigma] must be an extension of the sigma of the goal *) val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic - -(*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 match_rule : (rule -> bool) -> 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 map_pftreestate : - (evar_map ref -> proof_tree -> proof_tree) -> 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_proof : evar_map -> proof_tree -> constr * (int * types) list -val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map -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 match_rule : (rule -> bool) -> pftreestate -> bool -val up_until_matching_rule : (rule -> bool) -> - pftreestate -> pftreestate -val up_to_matching_rule : (rule -> bool) -> - pftreestate -> pftreestate -val change_rule : (rule -> rule) -> pftreestate -> pftreestate -val change_constraints_pftreestate - : evar_map -> pftreestate -> pftreestate - - -(*s Pretty-printers. *) - -(*i*) -open Pp -(*i*) -val set_info_printer : - (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit -val set_proof_printer : - (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit -val print_pftreestate : pftreestate -> Pp.std_ppcmds |