Module 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).

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)

Recongnize inductive relation defined by reflexivity