Module Hipattern

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 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 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

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

Idem but fails with an error message instead of PatternMatchingFailure

A variant that returns more informative structure on the equality found

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 {x:A|P}, returns A and P

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

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
val is_homogeneous_relation : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types

Test if a homogeneous relation (in Prop) and, if so, returns the domain