diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 5 | ||||
| -rw-r--r-- | proofs/refiner.mli | 3 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 6 |
4 files changed, 15 insertions, 4 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 7a66067cd7..9dd35a8c23 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -448,8 +448,9 @@ let rec tclTHENLIST = function [] -> tclIDTAC | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl) - - +(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) +let tclMAP tacfun l = + List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC (* various progress criterions *) let same_goal gl subgoal = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 1823514270..5cbc2bde8f 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -80,6 +80,9 @@ val tclTHEN : tactic -> tactic -> tactic convenient than [tclTHEN] when [n] is large *) val tclTHENLIST : tactic list -> tactic +(* [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) *) val tclTHEN_i : tactic -> (int -> tactic) -> tactic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index f9b7b8677d..fa22de7bb2 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -111,11 +111,14 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) +let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) +let pf_is_matching = pf_apply Matching.is_matching_conv +let pf_matches = pf_apply Matching.matches_conv + (************************************) (* Tactics handling a list of goals *) (************************************) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f57b121dba..826337cc8d 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -21,6 +21,7 @@ open Refiner open Redexpr open Tacexpr open Rawterm +open Pattern (*i*) (* Operations for handling terms under a local typing context. *) @@ -51,7 +52,7 @@ val pf_global : goal sigma -> identifier -> constr val pf_parse_const : goal sigma -> string -> constr val pf_type_of : goal sigma -> constr -> types val pf_check_type : goal sigma -> constr -> types -> unit -val hnf_type_of : goal sigma -> constr -> types +val pf_hnf_type_of : goal sigma -> constr -> types val pf_interp_constr : goal sigma -> Topconstr.constr_expr -> constr val pf_interp_type : goal sigma -> Topconstr.constr_expr -> types @@ -86,6 +87,9 @@ val pf_const_value : goal sigma -> constant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool +val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map +val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool + type transformation_tactic = proof_tree -> (goal list * validation) val frontier : transformation_tactic |