package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 : 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 =
  1. | MonomorphicLeibnizEq of EConstr.constr * EConstr.constr
  2. | PolymorphicLeibnizEq of EConstr.constr * EConstr.constr * EConstr.constr
  3. | 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct