Hipattern (coq-core.Hipattern)

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 of Dale Miller.

ALGORITHM:

Given a pattern, we decompose it, flattening casts and apply's, recursing on all operators, and pushing the name of the binder each time we descend a binder.

When we reach a first-order variable, we ask that the corresponding term's free-rels all be higher than the depth of the current stack.

When we reach a second-order application, we ask that the intersection of the free-rels of the term and the current stack be contained in the arguments of the application

I implemented the following functions which test whether a term t is an inductive but non-recursive type, a general conjunction, 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 also work on ad-hoc disjunctions introduced by the user. (Eduardo, 6/8/97).

type 'a matching_function =
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  'a option

type testing_function = Environ.env -> Evd.evar_map -> EConstr.constr -> bool

val match_with_non_recursive_type : 
  (EConstr.constr * EConstr.constr list) matching_function

val is_non_recursive_type : testing_function

val match_with_disjunction : 
  ?strict:bool ->
  ?onlybinary:bool ->
  (EConstr.constr * EConstr.constr list) matching_function

Non recursive type with no indices and exactly one argument for each constructor; canonical definition of n-ary disjunction if strict

val is_disjunction : ?strict:bool -> ?onlybinary:bool -> testing_function

val match_with_conjunction : 
  ?strict:bool ->
  ?onlybinary:bool ->
  (EConstr.constr * EConstr.constr list) matching_function

Non recursive tuple (one constructor and no indices) with no inner dependencies; canonical definition of n-ary conjunction if strict

val is_conjunction : ?strict:bool -> ?onlybinary:bool -> testing_function

val match_with_record : 
  (EConstr.constr * EConstr.constr list) matching_function

Non recursive tuple, possibly with inner dependencies

val is_record : testing_function

val match_with_tuple : 
  (EConstr.constr * EConstr.constr list * bool) matching_function

Like record but supports and tells if recursive (e.g. Acc)

val is_tuple : testing_function

val match_with_empty_type : EConstr.constr matching_function

No constructor, possibly with indices

val is_empty_type : testing_function

val match_with_unit_or_eq_type : EConstr.constr matching_function

type with only one constructor and no arguments, possibly with indices

val is_unit_or_eq_type : testing_function

val is_unit_type : testing_function

type with only one constructor and no arguments, no indices

val is_inductive_equality : Environ.env -> Names.inductive -> bool

type with only one constructor, no arguments and at least one dependency

val match_with_equality_type : 
  (EConstr.constr * EConstr.constr list) matching_function

val is_equality_type : testing_function

val match_with_nottype : (EConstr.constr * EConstr.constr) matching_function

val is_nottype : testing_function

val match_with_forall_term : 
  (Names.Name.t Context.binder_annot * EConstr.constr * EConstr.constr)
    matching_function

val is_forall_term : testing_function

val match_with_imp_term : (EConstr.constr * EConstr.constr) matching_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 (excluding parameters). this is useful to check whether a conjunction is a real conjunction and not a dependent tuple. (Pierre Corbineau, 13/5/2002)

val has_nodep_prod_after : int -> testing_function

val has_nodep_prod : testing_function

val match_with_nodep_ind : 
  (EConstr.constr * EConstr.constr list * int) matching_function

val is_nodep_ind : testing_function

val match_with_sigma_type : 
  (EConstr.constr * EConstr.constr list) matching_function

val is_sigma_type : testing_function

Recongnize inductive relation defined by reflexivity

type equation_kind =

| MonomorphicLeibnizEq of EConstr.constr * EConstr.constr

| PolymorphicLeibnizEq of EConstr.constr * EConstr.constr * EConstr.constr

| HeterogenousEq of EConstr.constr
  * EConstr.constr
  * EConstr.constr
  * EConstr.constr

exception NoEquationFound

val match_with_equation : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Coqlib.coq_eq_data option * EConstr.constr * equation_kind

val find_eq_data_decompose : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Coqlib.coq_eq_data
  * EConstr.EInstance.t
  * (EConstr.types * EConstr.constr * EConstr.constr)

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_this_eq_data_decompose : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Coqlib.coq_eq_data
  * EConstr.EInstance.t
  * (EConstr.types * EConstr.constr * EConstr.constr)

Idem but fails with an error message instead of PatternMatchingFailure

val find_eq_data : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Coqlib.coq_eq_data * EConstr.EInstance.t * equation_kind

A variant that returns more informative structure on the equality found

val find_sigma_data_decompose : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Coqlib.coq_sigma_data
  * (EConstr.EInstance.t
     * EConstr.constr
     * EConstr.constr
     * EConstr.constr
     * EConstr.constr)

Match a term of the form (existT A P t p) Returns associated lemmas and A,P,t,p

val match_sigma : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr * EConstr.constr

Match a term of the form {x:A|P}, returns A and P

val is_matching_sigma : Environ.env -> Evd.evar_map -> EConstr.constr -> bool

val match_eqdec : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  bool * Names.GlobRef.t * EConstr.constr * EConstr.constr * EConstr.constr

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 is_matching_not : Environ.env -> Evd.evar_map -> EConstr.constr -> bool

Match a negation

val is_matching_imp_False : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  bool