Module `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 metavariable = int: Existential variables

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 pcase_invert = | NoInvert Normal reduction: match when the scrutinee is a constructor. | CaseInvert of { indices : 'constr array; } Reduce when the indices match those of the unique constructor. (SProp to non SProp only)

The type of constructions

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

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.

val mkRel : int -> constr: Constructs a de Bruijn index (DB indices begin at 1)

val mkVar : Names.Id.t -> constr: Constructs a Variable

val mkInt : Uint63.t -> constr: Constructs a machine integer

val mkArray : (Univ.Instance.t * constr array * constr * types) -> constr: Constructs an array

val mkFloat : Float64.t -> constr: Constructs a machine float number

val mkMeta : metavariable -> constr: Constructs an patvar named "?n"

type existential = Evar.t * constr list: Constructs an existential variable

val mkEvar : existential -> constr
val mkSort : Sorts.t -> types: Construct a sort

val mkSProp : types
val mkProp : types
val mkSet : types
val mkType : Univ.Universe.t -> types

type cast_kind = | VMcast | NATIVEcast | DEFAULTcast: This defines the strategy to use for verifiying a Cast

val mkCast : (constr * cast_kind * constr) -> constr: Constructs the term t1::t2, i.e. the term t₁ casted with the type t₂ (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₁]t₂

val mkLetIn : (Names.Name.t Context.binder_annot * constr * types * constr) -> constr: Constructs the product let x = t1 : t2 in t3

val mkApp : (constr * constr array) -> constr: mkApp (f, [|t1; ...; tN|] constructs the application (f t₁ ... t_n) $(f~t_1\dots f_n)$ .

val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses
val mkConst : Names.Constant.t -> constr: Constructs a Constant.t

val mkConstU : pconstant -> constr
val mkProj : (Names.Projection.t * constr) -> constr: Constructs a projection application

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.

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

val mkCase : case -> constr

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 fixpoint = (constr, types) pfixpoint

val mkFix : fixpoint -> constr

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

Concrete type for making pattern-matching.

type 'constr pexistential = Evar.t * 'constr list: 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, or cofix. | 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. Variable or Let). | 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 as Prod (A,B,C). | Lambda of Names.Name.t Context.binder_annot * 'types * 'constr Concrete syntax "fun A:B => C" is represented as Lambda (A,B,C). | LetIn of Names.Name.t Context.binder_annot * 'constr * 'types * 'constr Concrete syntax "let A:C := B in D" is represented as LetIn (A,B,C,D). | App of 'constr * 'constr array Concrete syntax "(F P1 P2 ... Pn)" is represented as App (F, [|P1; P2; ...; Pn|]). The mkApp constructor also enforces the following invariant: F itself is not App and [|P1;..;Pn|] is not empty. | Const of Names.Constant.t * 'univs Gallina-variable that was introduced by Vernacular-command that extends the global environment (i.e. Parameter, or Axiom, or Definition, or Theorem etc.) | Ind of Names.inductive * 'univs A name of an inductive type defined by Variant, Inductive or Record Vernacular-commands. | Construct of Names.constructor * 'univs A constructor of an inductive type defined by Variant, Inductive or Record Vernacular-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 a match c return p with brs expression. c lives in inductive ci.ci_ind at universe instance u and parameters params. If this match has case inversion (ie match on a 1 constructor SProp inductive with proof relevant return type) the indices are in iv. The names in p are the names of the bound indices and inductive value (ie the in and as clauses). The names in the brs are 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 of vals in type t with default value def. u is a universe containing t.

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

Term destructors

exception DestKO

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

val destSort : constr -> Sorts.t: Destructs a sort. is_Prop recognizes the sort Prop, whether isprop recognizes both Prop and Set.

val destCast : constr -> constr * cast_kind * constr: Destructs a casted term

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

val destLetIn : constr -> Names.Name.t Context.binder_annot * constr * types * constr: Destructs the let $ x:=b:t_1t_2 $

val destApp : constr -> constr * constr array: Destructs an application

val decompose_app : constr -> constr * constr list: Decompose any term as an applicative term; the list of args can be empty

val decompose_appvect : constr -> constr * constr array: Same as decompose_app, but returns an array.

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

val destCase : constr -> case

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)

returns: (info,c,fun args x => P,[|...|fun yij => ti| ...|]) where info is pretty-printing information

val destProj : constr -> Names.Projection.t * constr: Destructs a projection

val destFix : constr -> fixpoint: 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

Equality

val equal : constr -> constr -> bool: 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.

val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained: 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_infer : UGraph.t -> constr -> constr -> bool Univ.constrained: 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.

val eq_constr_nounivs : constr -> constr -> bool: eq_constr_univs a b true, c if a equals b modulo alpha, casts, application grouping and ignoring universe instances.

val compare : constr -> constr -> int: Total ordering compatible with equal

Extension of Context with declarations on constr

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

Relocation and substitution

val exliftn : Esubst.lift -> constr -> constr: exliftn el c lifts c with lifting el

val liftn : int -> int -> constr -> constr: liftn n k c lifts by n indexes above or equal to k in c

val lift : int -> constr -> constr: lift n c lifts by n the positive indexes in c

Functionals working on expressions canonically abstracted over a local context (possibly with let-ins)

val map_branches : (constr -> constr) -> case_branch array -> case_branch array

val map_return_predicate : (constr -> constr) -> case_return -> case_return

val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_branch array -> case_branch array

val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_return -> case_return

Functionals working on the immediate subterm of a construction

val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
val fold_invert : ('a -> 'b -> 'a) -> 'a -> 'b pcase_invert -> 'a

val map : (constr -> constr) -> constr -> constr
val map_invert : ('a -> 'a) -> 'a pcase_invert -> 'a pcase_invert

val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
val fold_map_invert : ('a -> 'b -> 'a * 'b) -> 'a -> 'b pcase_invert -> 'a * 'b pcase_invert

val map_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr

val iter : (constr -> unit) -> constr -> unit
val iter_invert : ('a -> unit) -> 'a pcase_invert -> unit

val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit

val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b

type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool

val compare_head : 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) .

val compare_head_gen : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> 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 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 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).

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_fn
val eq_invert : ('a -> 'a -> bool) -> 'a pcase_invert -> 'a pcase_invert -> bool

Hashconsing

val hash : constr -> int
val case_info_hash : case_info -> int
val hcons : constr -> constr
val debug_print : constr -> Pp.t
val debug_print_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t

`\|` `LetStyle`
`\|` `IfStyle`
`\|` `LetPatternStyle`
`\|` `MatchStyle`
`\|` `RegularStyle`	infer printing form from number of constructor

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

`\|` `Rel of int`	Gallina-variable introduced by `forall`, `fun`, `let-in`, `fix`, or `cofix`.
`\|` `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. `Variable` or `Let`).
`\|` `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 as `Prod (A,B,C)`.
`\|` `Lambda of Names.Name.t Context.binder_annot * 'types * 'constr`	Concrete syntax `"fun A:B => C"` is represented as `Lambda (A,B,C)`.
`\|` `LetIn of Names.Name.t Context.binder_annot * 'constr * 'types * 'constr`	Concrete syntax `"let A:C := B in D"` is represented as `LetIn (A,B,C,D)`.
`\|` `App of 'constr * 'constr array`	Concrete syntax `"(F P1 P2 ... Pn)"` is represented as `App (F, [\|P1; P2; ...; Pn\|])`. The `mkApp` constructor also enforces the following invariant: `F` itself is not `App` and `[\|P1;..;Pn\|]` is not empty.
`\|` `Const of Names.Constant.t * 'univs`	Gallina-variable that was introduced by Vernacular-command that extends the global environment (i.e. `Parameter`, or `Axiom`, or `Definition`, or `Theorem` etc.)
`\|` `Ind of Names.inductive * 'univs`	A name of an inductive type defined by `Variant`, `Inductive` or `Record` Vernacular-commands.
`\|` `Construct of Names.constructor * 'univs`	A constructor of an inductive type defined by `Variant`, `Inductive` or `Record` Vernacular-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 a `match c return p with brs` expression. `c` lives in inductive `ci.ci_ind` at universe instance `u` and parameters `params`. If this match has case inversion (ie match on a 1 constructor SProp inductive with proof relevant return type) the indices are in `iv`. The names in `p` are the names of the bound indices and inductive value (ie the `in` and `as` clauses). The names in the `brs` are 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 of `vals` in type `t` with default value `def`. `u` is a universe containing `t`.

Simply type aliases

Existential variables

Case annotation

Simple case analysis