package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3
doc/coq-core.kernel/Constr/index.html
Module ConstrSource
This file defines the most important datatype of Coq, namely kernel terms, as well as a handful of generic manipulation functions.
Simply type aliases
Existential variables
Case annotation
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;
}The type of constructions
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)
Functions for dealing with constr terms.
The following functions are intended to simplify and to uniform the manipulation of terms. Some of these functions may be overlapped with previous ones.
Term constructors.
Constructs a Variable
Constructs an patvar named "?n"
This defines the strategy to use for verifiying a Cast
Constructs the term t1::t2, i.e. the term t1 casted with the type t2 (that means t2 is declared as the type of t1).
Constructs the product (x:t1)t2
Constructs the abstraction [x:t1]t2
Constructs the product let x = t1 : t2 in t3
mkApp (f, [|t1; ...; tN|] constructs the application (f t1 ... tn) .
Constructs a Constant.t
Constructs a projection application
Inductive types
Constructs the ith (co)inductive type of the block named kn
Constructs the jth constructor of the ith (co)inductive type of the block named kn.
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"
acith element is ith constructor case presented as construct_args |- case_term
Names of the indices + name of self
Names of the branches
type ('constr, 'types, 'univs) pcase =
case_info
* 'univs
* 'constr array
* 'types pcase_return
* 'constr pcase_invert
* 'constr
* 'constr pcase_branch arraytype ('constr, 'types) prec_declaration =
Names.Name.t Context.binder_annot array * 'types array * 'constr arrayIf 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 $ .
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
The component int tells which component of the block of cofixpoint is returned
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.
Concrete type for making pattern-matching.
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(*Gallina-variable introduced by
*)forall,fun,let-in,fix, orcofix.| Var of Names.Id.t(*Gallina-variable that was introduced by Vernacular-command that extends the local context of the currently open section (i.e.
*)VariableorLet).| 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
*)"forall A:B,C"is represented asProd (A,B,C).| Lambda of Names.Name.t Context.binder_annot * 'types * 'constr(*Concrete syntax
*)"fun A:B => C"is represented asLambda (A,B,C).| LetIn of Names.Name.t Context.binder_annot * 'constr * 'types * 'constr(*Concrete syntax
*)"let A:C := B in D"is represented asLetIn (A,B,C,D).| App of 'constr * 'constr array| Const of Names.Constant.t * 'univs(*Gallina-variable that was introduced by Vernacular-command that extends the global environment (i.e.
*)Parameter, orAxiom, orDefinition, orTheoremetc.)| Ind of Names.inductive * 'univs(*A name of an inductive type defined by
*)Variant,InductiveorRecordVernacular-commands.| Construct of Names.constructor * 'univs(*A constructor of an inductive type defined by
*)Variant,InductiveorRecordVernacular-commands.| Case of case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array(*Case (ci,u,params,p,iv,c,brs)is amatch c return p with brsexpression.clives in inductiveci.ci_indat universe instanceuand parametersparams. If this match has case inversion (ie match on a 1 constructor SProp inductive with proof relevant return type) the indices are iniv.The names in
pare the names of the bound indices and inductive value (ie theinandasclauses).The names in the
*)brsare the names of the variables bound in the respective branch.| 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(*
*)Array (u,vals,def,t)is an array ofvalsin typetwith default valuedef.uis a universe containingt.
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_nocast_gen :
('v -> ('v, 'v, 'sort, 'univs) kind_of_term) ->
'v ->
('v, 'v, 'sort, 'univs) kind_of_termTerm destructors
Destructor operations are partial functions and
Destructs an existential variable
Destructs a variable
Destructs a sort. is_Prop recognizes the sort Prop, whether isprop recognizes both Prop and Set.
Destructs the product $ (x:t_1)t_2 $
Destructs the abstraction $ x:t_1t_2 $
Destructs the let $ x:=b:t_1t_2 $
Decompose any term as an applicative term; the list of args can be empty
Same as decompose_app, but returns an array.
Destructs a constant
Destructs an existential variable
Destructs a (co)inductive type
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)
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 $ .
Equality
equal a b is true if a equals b modulo alpha, casts, and application grouping
eq_constr_univs u a b is true if a equals b modulo alpha, casts, application grouping and the universe equalities in u.
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 u a b is true if a equals b modulo alpha, casts, application grouping and the universe equalities in u.
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.
Extension of Context with declarations on constr
Relocation and substitution
exliftn el c lifts c with lifting el
liftn n k c lifts by n indexes above or equal to k in c
Functionals working on expressions canonically abstracted over a local context (possibly with let-ins)
map_branches f br maps f on the immediate subterms of an array of "match" branches br in canonical eta-let-expanded 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
map_return_predicate f p maps f on the immediate subterms of a return predicate of a "match" in canonical eta-let-expanded 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
map_branches_with_binders f br maps f on the immediate subterms of an array of "match" branches br in canonical eta-let-expanded 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 arraymap_return_predicate_with_binders f p maps f on the immediate subterms of a return predicate of a "match" in canonical eta-let-expanded 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_returnFunctionals working on the immediate subterm of a construction
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
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
Like map, but also has an additional accumulator.
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
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
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) ->
constr constr_compare_fn ->
constr constr_compare_fnval 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 constr_compare_fn ->
'v constr_compare_fn ->
'v constr_compare_fnval 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 constr_compare_fn ->
'v constr_compare_fncompare_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) ->
constr constr_compare_fn ->
constr constr_compare_fn ->
constr constr_compare_fnHashconsing
- The type of constructions
- Functions for dealing with constr terms.
- Term constructors.
- Concrete type for making pattern-matching.
- Term destructors
- Equality
- Extension of Context with declarations on constr
- Relocation and substitution
- Functionals working on expressions canonically abstracted over a local context (possibly with let-ins)
- Functionals working on the immediate subterm of a construction
- Hashconsing