diff options
Diffstat (limited to 'tactics/hipattern.mli')
| -rw-r--r-- | tactics/hipattern.mli | 53 |
1 files changed, 25 insertions, 28 deletions
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 15d7bfc6..aa386364 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -1,25 +1,22 @@ (************************************************************************) (* 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: hipattern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Term open Sign open Evd open Pattern -open Proof_trees open Coqlib -(*i*) -(*s Given a term with second-order variables in it, +(** High-order patterns *) + +(** Given a term with second-order variables in it, represented by Meta's, and possibly applied using SoApp terms, this function will perform second-order, binding-preserving, matching, in the case where the pattern is a pattern in the sense @@ -38,7 +35,7 @@ open Coqlib intersection of the free-rels of the term and the current stack be contained in the arguments of the application *) -(*s I implemented the following functions which test whether a term [t] +(** I implemented the following functions which test whether a term [t] is an inductive but non-recursive type, a general conjuction, a general disjunction, or a type with no constructors. @@ -53,36 +50,36 @@ type testing_function = constr -> bool val match_with_non_recursive_type : (constr * constr list) matching_function val is_non_recursive_type : testing_function -(* Non recursive type with no indices and exactly one argument for each +(** 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 -(* Non recursive tuple (one constructor and no indices) with no inner +(** 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 -(* Non recursive tuple, possibly with inner dependencies *) +(** Non recursive tuple, possibly with inner dependencies *) val match_with_record : (constr * constr list) matching_function val is_record : testing_function -(* Like record but supports and tells if recursive (e.g. Acc) *) +(** 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 *) +(** No constructor, possibly with indices *) val match_with_empty_type : constr matching_function val is_empty_type : testing_function -(* type with only one constructor and no arguments, possibly with indices *) +(** 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 -(* type with only one constructor and no arguments, no indices *) +(** type with only one constructor and no arguments, no indices *) val is_unit_type : testing_function -(* type with only one constructor, no arguments and at least one dependency *) +(** 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 @@ -96,7 +93,7 @@ val is_forall_term : testing_function val match_with_imp_term : (constr * constr) matching_function val is_imp_term : testing_function -(* I added these functions to test whether a type contains dependent +(** I added these functions to test whether a type contains dependent products or not, and if an inductive has constructors with dependent types (excluding parameters). this is useful to check whether a conjunction is a real conjunction and not a dependent tuple. (Pierre Corbineau, 13/5/2002) *) @@ -110,7 +107,7 @@ 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 *) +(** Recongnize inductive relation defined by reflexivity *) type equation_kind = | MonomorphicLeibnizEq of constr * constr @@ -124,37 +121,37 @@ val match_with_equation: (***** Destructing patterns bound to some theory *) -(* 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 *) +(** 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 *) +(** 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) -(* A variant that returns more informative structure on the equality found *) +(** 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] *) +(** 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 -> coq_sigma_data * (constr * constr * constr * constr) -(* Match a term of the form [{x:A|P}], returns [A] and [P] *) +(** Match a term of the form [{x:A|P}], returns [A] and [P] *) val match_sigma : constr -> constr * constr val is_matching_sigma : constr -> bool -(* Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns +(** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns [t,u,T] and a boolean telling if equality is on the left side *) val match_eqdec : constr -> bool * constr * constr * constr * constr -(* Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) +(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) open Proof_type open Tacmach val dest_nf_eq : goal sigma -> constr -> (constr * constr * constr) -(* Match a negation *) +(** Match a negation *) val is_matching_not : constr -> bool val is_matching_imp_False : constr -> bool |