Constr
This file defines the most important datatype of Coq, namely kernel terms, as well as a handful of generic manipulation functions.
type pconstant = Names.Constant.t Univ.puniverses
Simply type aliases
type pinductive = Names.inductive Univ.puniverses
type pconstructor = Names.constructor Univ.puniverses
type case_style =
 LetStyle  
 IfStyle  
 LetPatternStyle  
 MatchStyle  
 RegularStyle  (* infer printing form from number of constructor *) 
Case annotation
type case_printing = {
ind_tags : bool list;  (* tell whether letin or lambda in the arity of the inductive type *) 
cstr_tags : bool list array;  (* tell whether letin or lambda in the signature of each constructor *) 
style : case_style; 
}
type case_info = {
ci_ind : Names.inductive; 
ci_npar : int; 
ci_cstr_ndecls : int array; 
ci_cstr_nargs : int array; 
ci_relevance : Sorts.relevance; 
ci_pp_info : case_printing; 
}
type constr = t
types
is the same as constr
but is intended to be used for documentation to indicate that such or such function specifically works with types (i.e. terms of type a sort). (Rem:plurial form since type
is a reserved ML keyword)
type types = constr
The following functions are intended to simplify and to uniform the manipulation of terms. Some of these functions may be overlapped with previous ones.
val mkRel : int > constr
Constructs a de Bruijn index (DB indices begin at 1)
val mkVar : Names.Id.t > constr
Constructs a Variable
val mkArray : (Univ.Instance.t * constr array * constr * types) > constr
Constructs an array
val mkMeta : metavariable > constr
Constructs an patvar named "?n"
val mkEvar : existential > constr
val mkSProp : types
val mkProp : types
val mkSet : types
val mkType : Univ.Universe.t > types
This defines the strategy to use for verifiying a Cast
Constructs the term t1::t2
, i.e. the term t_{1} casted with the type t_{2} (that means t2 is declared as the type of t1).
val mkProd : (Names.Name.t Context.binder_annot * types * types) > types
Constructs the product (x:t1)t2
val mkLambda : (Names.Name.t Context.binder_annot * types * constr) > constr
Constructs the abstraction [x:t_{1}]t_{2}
val mkLetIn :
(Names.Name.t Context.binder_annot * constr * types * constr) >
constr
Constructs the product let x = t1 : t2 in t3
mkApp (f, [t1; ...; tN]
constructs the application (f t_{1} ... t_{n}) .
val map_puniverses : ( 'a > 'b ) > 'a Univ.puniverses > 'b Univ.puniverses
val mkConst : Names.Constant.t > constr
Constructs a Constant.t
val mkProj : (Names.Projection.t * constr) > constr
Constructs a projection application
Inductive types
val mkInd : Names.inductive > constr
Constructs the ith (co)inductive type of the block named kn
val mkIndU : pinductive > constr
val mkConstruct : Names.constructor > constr
Constructs the jth constructor of the ith (co)inductive type of the block named kn.
val mkConstructU : pconstructor > constr
val mkConstructUi : (pinductive * int) > constr
val mkRef : Names.GlobRef.t Univ.puniverses > constr
Make a constant, inductive, constructor or variable.
Constructs a destructor of inductive type.
mkCase ci params p c ac
stand for match c
as x
in I args
return p
with ac
presented as describe in ci
.
p
structure is args x  "return clause"
ac
^{ith} element is ith constructor case presented as construct_args  case_term
type 'constr pcase_branch = Names.Name.t Context.binder_annot array * 'constr
Names of the indices + name of self
type 'types pcase_return = Names.Name.t Context.binder_annot array * 'types
Names of the branches
type ('constr, 'types, 'univs) pcase =
case_info
* 'univs
* 'constr array
* 'types pcase_return
* 'constr pcase_invert
* 'constr
* 'constr pcase_branch array
type case_invert = constr pcase_invert
type case_return = types pcase_return
type case_branch = constr pcase_branch
type case = ( constr, types, Univ.Instance.t ) pcase
type ('constr, 'types) prec_declaration =
Names.Name.t Context.binder_annot array * 'types array * 'constr array
If recindxs = [i1,...in]
funnames = [f1,.....fn]
typarray = [t1,...tn]
bodies = [b1,.....bn]
then mkFix ((recindxs,i), funnames, typarray, bodies)
constructs the $
i $
th function of the block (counting from 0)
Fixpoint f1 [ctx1] = b1
with f2 [ctx2] = b2
...
with fn [ctxn] = bn.
where the length of the $
j $
th context is $
ij $
.
type ('constr, 'types) pfixpoint =
(int array * int) * ( 'constr, 'types ) prec_declaration
The array of int
's tells for each component of the array of mutual fixpoints the number of lambdas to skip before finding the recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) (v:=u) (w:I) struct w
"), telling to skip x and z and that w is the recursive argument); The second component int
tells which component of the block is returned
type ('constr, 'types) pcofixpoint = int * ( 'constr, 'types ) prec_declaration
The component int
tells which component of the block of cofixpoint is returned
type rec_declaration = ( constr, types ) prec_declaration
type cofixpoint = ( constr, types ) pcofixpoint
If funnames = [f1,.....fn]
typarray = [t1,...tn]
bodies = [b1,.....bn]
then mkCoFix (i, (funnames, typarray, bodies))
constructs the ith function of the block
CoFixpoint f1 = b1
with f2 = b2
...
with fn = bn.
val mkCoFix : cofixpoint > constr
constr list
is an instance matching definitional named_context
in the same order (i.e. last argument first)
type ('constr, 'types, 'sort, 'univs) kind_of_term =
 Rel of int  (* Gallinavariable introduced by 
 Var of Names.Id.t  (* Gallinavariable that was introduced by Vernacularcommand that extends the local context of the currently open section (i.e. 
 Meta of metavariable  
 Evar of 'constr pexistential  
 Sort of 'sort  
 Cast of 'constr * cast_kind * 'types  
 Prod of Names.Name.t Context.binder_annot * 'types * 'types  (* Concrete syntax 
 Lambda of Names.Name.t Context.binder_annot * 'types * 'constr  (* Concrete syntax 
 LetIn of Names.Name.t Context.binder_annot * 'constr * 'types * 'constr  (* Concrete syntax 
 App of 'constr * 'constr array  (* Concrete syntax

 Const of Names.Constant.t * 'univs  (* Gallinavariable that was introduced by Vernacularcommand that extends the global environment (i.e. 
 Ind of Names.inductive * 'univs  (* A name of an inductive type defined by 
 Construct of Names.constructor * 'univs  (* A constructor of an inductive type defined by 
 Case of case_info
* 'univs
* 'constr array
* 'types pcase_return
* 'constr pcase_invert
* 'constr
* 'constr pcase_branch array  (*
The names in The names in the 
 Fix of ( 'constr, 'types ) pfixpoint  
 CoFix of ( 'constr, 'types ) pcofixpoint  
 Proj of Names.Projection.t * 'constr  
 Int of Uint63.t  
 Float of Float64.t  
 Array of 'univs * 'constr array * 'constr * 'types  (*

User view of constr
. For App
, it is ensured there is at least one argument and the function is not itself an applicative term
val kind : constr > ( constr, types, Sorts.t, Univ.Instance.t ) kind_of_term
val of_kind :
( constr, types, Sorts.t, Univ.Instance.t ) kind_of_term >
constr
val kind_nocast_gen :
( 'v > ( 'v, 'v, 'sort, 'univs ) kind_of_term ) >
'v >
( 'v, 'v, 'sort, 'univs ) kind_of_term
val kind_nocast :
constr >
( constr, types, Sorts.t, Univ.Instance.t ) kind_of_term
val isRel : constr > bool
Simple case analysis
val isRelN : int > constr > bool
val isVar : constr > bool
val isVarId : Names.Id.t > constr > bool
val isRef : constr > bool
val isRefX : Names.GlobRef.t > constr > bool
val isInd : constr > bool
val isEvar : constr > bool
val isMeta : constr > bool
val isEvar_or_Meta : constr > bool
val isSort : constr > bool
val isCast : constr > bool
val isApp : constr > bool
val isLambda : constr > bool
val isLetIn : constr > bool
val isProd : constr > bool
val isConst : constr > bool
val isConstruct : constr > bool
val isFix : constr > bool
val isCoFix : constr > bool
val isCase : constr > bool
val isProj : constr > bool
val is_Prop : constr > bool
val is_Set : constr > bool
val isprop : constr > bool
val is_Type : constr > bool
val iskind : constr > bool
val is_small : Sorts.t > bool
Destructor operations are partial functions and
val destRel : constr > int
Destructs a de Bruijn index
val destMeta : constr > metavariable
Destructs an existential variable
val destVar : constr > Names.Id.t
Destructs a variable
Destructs a sort. is_Prop
recognizes the sort Prop
, whether isprop
recognizes both Prop
and Set
.
val destProd : types > Names.Name.t Context.binder_annot * types * types
Destructs the product $
(x:t_1)t_2 $
val destLambda : constr > Names.Name.t Context.binder_annot * types * constr
Destructs the abstraction $
x:t_1
t_2 $
val destLetIn :
constr >
Names.Name.t Context.binder_annot * constr * types * constr
Destructs the let $
x:=b:t_1
t_2 $
Decompose any term as an applicative term; the list of args can be empty
val destConst : constr > Names.Constant.t Univ.puniverses
Destructs a constant
val destEvar : constr > existential
Destructs an existential variable
val destInd : constr > Names.inductive Univ.puniverses
Destructs a (co)inductive type
val destConstruct : constr > Names.constructor Univ.puniverses
Destructs a constructor
Destructs a match c as x in I args return P with ... 
Ci(...yij...) => ti  ... end
(or let (..y1i..) := c as x in I args
return P in t1
, or if c then t1 else t2
)
val destProj : constr > Names.Projection.t * constr
Destructs a projection
Destructs the $
i $
th function of the block Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
with f{_ 2} ctx{_ 2} = b{_ 2}
...
with f{_ n} ctx{_ n} = b{_ n}
, where the length of the $
j $
th context is $
ij $
.
val destCoFix : constr > cofixpoint
val destRef : constr > Names.GlobRef.t Univ.puniverses
equal a b
is true if a
equals b
modulo alpha, casts, and application grouping
val eq_constr_univs : constr UGraph.check_function
eq_constr_univs u a b
is true
if a
equals b
modulo alpha, casts, application grouping and the universe equalities in u
.
val leq_constr_univs : constr UGraph.check_function
leq_constr_univs u a b
is true
if a
is convertible to b
modulo alpha, casts, application grouping and the universe inequalities in u
.
eq_constr_univs a b
true, c
if a
equals b
modulo alpha, casts, application grouping and ignoring universe instances.
type rel_declaration = ( constr, types ) Context.Rel.Declaration.pt
type named_declaration = ( constr, types ) Context.Named.Declaration.pt
type compacted_declaration = ( constr, types ) Context.Compacted.Declaration.pt
type rel_context = rel_declaration list
type named_context = named_declaration list
type compacted_context = compacted_declaration list
val exliftn : Esubst.lift > constr > constr
exliftn el c
lifts c
with lifting el
map_branches f br
maps f
on the immediate subterms of an array of "match" branches br
in canonical etaletexpanded form; it is not recursive and the order with which subterms are processed is not specified; it preserves sharing; the immediate subterms are the types and possibly terms occurring in the context of each branch as well as the body of each branch
val map_branches :
( constr > constr ) >
case_branch array >
case_branch array
map_return_predicate f p
maps f
on the immediate subterms of a return predicate of a "match" in canonical etaletexpanded form; it is not recursive and the order with which subterms are processed is not specified; it preserves sharing; the immediate subterms are the types and possibly terms occurring in the context of each branch as well as the body of the predicate
val map_return_predicate : ( constr > constr ) > case_return > case_return
map_branches_with_binders f br
maps f
on the immediate subterms of an array of "match" branches br
in canonical etaletexpanded form; it carries an extra data n
(typically a lift index) which is processed by g
(which typically adds 1 to n
) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified; it preserves sharing; the immediate subterms are the types and possibly terms occurring in the context of the branch as well as the body of the branch
val map_branches_with_binders :
( 'a > 'a ) >
( 'a > constr > constr ) >
'a >
case_branch array >
case_branch array
map_return_predicate_with_binders f p
maps f
on the immediate subterms of a return predicate of a "match" in canonical etaletexpanded form; it carries an extra data n
(typically a lift index) which is processed by g
(which typically adds 1 to n
) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified; it preserves sharing; the immediate subterms are the types and possibly terms occurring in the context of each branch as well as the body of the predicate
val map_return_predicate_with_binders :
( 'a > 'a ) >
( 'a > constr > constr ) >
'a >
case_return >
case_return
fold f acc c
folds f
on the immediate subterms of c
starting from acc
and proceeding from left to right according to the usual representation of the constructions; it is not recursive
val fold_invert : ( 'a > 'b > 'a ) > 'a > 'b pcase_invert > 'a
map f c
maps f
on the immediate subterms of c
; it is not recursive and the order with which subterms are processed is not specified
val map_invert : ( 'a > 'a ) > 'a pcase_invert > 'a pcase_invert
Like map
, but also has an additional accumulator.
val fold_map_invert :
( 'a > 'b > 'a * 'b ) >
'a >
'b pcase_invert >
'a * 'b pcase_invert
map_with_binders g f n c
maps f n
on the immediate subterms of c
; it carries an extra data n
(typically a lift index) which is processed by g
(which typically add 1 to n
) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified
iter f c
iters f
on the immediate subterms of c
; it is not recursive and the order with which subterms are processed is not specified
val iter_invert : ( 'a > unit ) > 'a pcase_invert > unit
iter_with_binders g f n c
iters f n
on the immediate subterms of c
; it carries an extra data n
(typically a lift index) which is processed by g
(which typically add 1 to n
) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified
iter_with_binders g f n c
iters f n
on the immediate subterms of c
; it carries an extra data n
(typically a lift index) which is processed by g
(which typically add 1 to n
) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified
compare_head f c1 c2
compare c1
and c2
using f
to compare the immediate subterms of c1
of c2
if needed; Cast's, binders name and Cases annotations are not taken into account
val compare_head :
( existential > existential > bool ) >
constr constr_compare_fn >
constr constr_compare_fn
type 'univs instance_compare_fn =
(Names.GlobRef.t * int) option >
'univs >
'univs >
bool
Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .
compare_head_gen u s f c1 c2
compare c1
and c2
using f
to compare the immediate subterms of c1
of c2
if needed, u
to compare universe instances, s
to compare sorts; Cast's, binders name and Cases annotations are not taken into account
val compare_head_gen :
Univ.Instance.t instance_compare_fn >
( Sorts.t > Sorts.t > bool ) >
( existential > existential > bool ) >
constr constr_compare_fn >
constr constr_compare_fn
val compare_head_gen_leq_with :
( 'v > ( 'v, 'v, 'sort, 'univs ) kind_of_term ) >
( 'v > ( 'v, 'v, 'sort, 'univs ) kind_of_term ) >
'univs instance_compare_fn >
( 'sort > 'sort > bool ) >
( 'v pexistential > 'v pexistential > bool ) >
'v constr_compare_fn >
'v constr_compare_fn >
'v constr_compare_fn
val compare_head_gen_with :
( 'v > ( 'v, 'v, 'sort, 'univs ) kind_of_term ) >
( 'v > ( 'v, 'v, 'sort, 'univs ) kind_of_term ) >
'univs instance_compare_fn >
( 'sort > 'sort > bool ) >
( 'v pexistential > 'v pexistential > bool ) >
'v constr_compare_fn >
'v constr_compare_fn
compare_head_gen_with k1 k2 u s f c1 c2
compares c1
and c2
like compare_head_gen u s f c1 c2
, except that k1
(resp. k2
) is used,rather than kind
, to expose the immediate subterms of c1
(resp. c2
).
compare_head_gen_leq u s f fle c1 c2
compare c1
and c2
using f
to compare the immediate subterms of c1
of c2
for conversion, fle
for cumulativity, u
to compare universe instances (the first boolean tells if they belong to a Constant.t), s
to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account
val compare_head_gen_leq :
Univ.Instance.t instance_compare_fn >
( Sorts.t > Sorts.t > bool ) >
( existential > existential > bool ) >
constr constr_compare_fn >
constr constr_compare_fn >
constr constr_compare_fn
val eq_invert :
( 'a > 'a > bool ) >
'a pcase_invert >
'a pcase_invert >
bool
type 'constr evar_handler = {
evar_expand : 'constr pexistential > 'constr evar_expansion; 
evar_repack : (Evar.t * 'constr list) > 'constr; 
evar_relevant : 'constr pexistential > bool; 
qvar_relevant : Sorts.QVar.t > bool; 
}
val default_evar_handler : 'constr evar_handler
val hash : constr > int
val case_info_hash : case_info > int