diff options
Diffstat (limited to 'tactics/hipattern.mli')
| -rw-r--r-- | tactics/hipattern.mli | 79 |
1 files changed, 53 insertions, 26 deletions
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 3c423202..d98d2a2b 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: hipattern.mli 11739 2009-01-02 19:33:19Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Util @@ -16,6 +16,7 @@ open Sign open Evd open Pattern open Proof_trees +open Coqlib (*i*) (*s Given a term with second-order variables in it, @@ -41,8 +42,8 @@ open Proof_trees is an inductive but non-recursive type, a general conjuction, a general disjunction, or a type with no constructors. - They are more general than matching with [or_term], [and_term], etc, - since they do not depend on the name of the type. Hence, they + They are more general than matching with [or_term], [and_term], etc, + since they do not depend on the name of the type. Hence, they also work on ad-hoc disjunctions introduced by the user. (Eduardo, 6/8/97). *) @@ -50,41 +51,50 @@ type 'a matching_function = constr -> 'a option type testing_function = constr -> bool val match_with_non_recursive_type : (constr * constr list) matching_function -val is_non_recursive_type : testing_function +val is_non_recursive_type : testing_function +(* Non recursive type with no indices and exactly one argument for each + constructor; canonical definition of n-ary disjunction if strict *) val match_with_disjunction : ?strict:bool -> (constr * constr list) matching_function -val is_disjunction : ?strict:bool -> testing_function +val is_disjunction : ?strict:bool -> testing_function +(* Non recursive tuple (one constructor and no indices) with no inner + dependencies; canonical definition of n-ary conjunction if strict *) val match_with_conjunction : ?strict:bool -> (constr * constr list) matching_function -val is_conjunction : ?strict:bool -> testing_function +val is_conjunction : ?strict:bool -> testing_function +(* Non recursive tuple, possibly with inner dependencies *) val match_with_record : (constr * constr list) matching_function -val is_record : testing_function +val is_record : testing_function + +(* Like record but supports and tells if recursive (e.g. Acc) *) +val match_with_tuple : (constr * constr list * bool) matching_function +val is_tuple : testing_function +(* No constructor, possibly with indices *) val match_with_empty_type : constr matching_function -val is_empty_type : testing_function +val is_empty_type : testing_function (* type with only one constructor and no arguments, possibly with indices *) val match_with_unit_or_eq_type : constr matching_function -val is_unit_or_eq_type : testing_function +val is_unit_or_eq_type : testing_function (* type with only one constructor and no arguments, no indices *) -val is_unit_type : testing_function - -val match_with_equation : (constr * constr list) matching_function -val is_equation : testing_function +val is_unit_type : testing_function (* type with only one constructor, no arguments and at least one dependency *) +val is_inductive_equality : inductive -> bool val match_with_equality_type : (constr * constr list) matching_function +val is_equality_type : testing_function val match_with_nottype : (constr * constr) matching_function -val is_nottype : testing_function +val is_nottype : testing_function val match_with_forall_term : (name * constr * constr) matching_function -val is_forall_term : testing_function +val is_forall_term : testing_function val match_with_imp_term : (constr * constr) matching_function -val is_imp_term : testing_function +val is_imp_term : testing_function (* I added these functions to test whether a type contains dependent products or not, and if an inductive has constructors with dependent types @@ -94,24 +104,41 @@ val is_imp_term : testing_function val has_nodep_prod_after : int -> testing_function val has_nodep_prod : testing_function -val match_with_nodep_ind : (constr * constr list * int) matching_function -val is_nodep_ind : testing_function +val match_with_nodep_ind : (constr * constr list * int) matching_function +val is_nodep_ind : testing_function + +val match_with_sigma_type : (constr * constr list) matching_function +val is_sigma_type : testing_function + +(* Recongnize inductive relation defined by reflexivity *) -val match_with_sigma_type : (constr * constr list) matching_function -val is_sigma_type : testing_function +type equation_kind = + | MonomorphicLeibnizEq of constr * constr + | PolymorphicLeibnizEq of constr * constr * constr + | HeterogenousEq of constr * constr * constr * constr + +exception NoEquationFound + +val match_with_equation: + constr -> coq_eq_data option * constr * equation_kind (***** Destructing patterns bound to some theory *) -open Coqlib +(* Match terms [eq A t u], [identity A t u] or [JMeq A t A u] *) +(* Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) +val find_eq_data_decompose : Proof_type.goal sigma -> constr -> + coq_eq_data * (types * constr * constr) + +(* Idem but fails with an error message instead of PatternMatchingFailure *) +val find_this_eq_data_decompose : Proof_type.goal sigma -> constr -> + coq_eq_data * (types * constr * constr) -(* Match terms [(eq A t u)] or [(identity A t u)] *) -(* Returns associated lemmas and [A,t,u] *) -val find_eq_data_decompose : constr -> - coq_leibniz_eq_data * (constr * constr * constr) +(* A variant that returns more informative structure on the equality found *) +val find_eq_data : constr -> coq_eq_data * equation_kind (* Match a term of the form [(existT A P t p)] *) (* Returns associated lemmas and [A,P,t,p] *) -val find_sigma_data_decompose : constr -> +val find_sigma_data_decompose : constr -> coq_sigma_data * (constr * constr * constr * constr) (* Match a term of the form [{x:A|P}], returns [A] and [P] *) |