Module EConstr

type t = Evd.econstr

Type of incomplete terms. Essentially a wrapper around Constr.t ensuring that Constr.kind does not observe defined evars.

Universe variables
module ERelevance : sig ... end
module ESorts : sig ... end
module EInstance : sig ... end
type types = t
type constr = t
type existential = t Constr.pexistential
type case_return = (t, ERelevance.t) Constr.pcase_return
type case_branch = (t, ERelevance.t) Constr.pcase_branch
type rec_declaration = (t, t, ERelevance.t) Constr.prec_declaration
type fixpoint = (t, t, ERelevance.t) Constr.pfixpoint
type cofixpoint = (t, t, ERelevance.t) Constr.pcofixpoint
type unsafe_judgment = (constr, types) Environ.punsafe_judgment
type unsafe_type_judgment = (types, Evd.esorts) Environ.punsafe_type_judgment
type named_context = (constr, types, ERelevance.t) Context.Named.pt
type rel_context = (constr, types, ERelevance.t) Context.Rel.pt
type 'a binder_annot = ('a, ERelevance.t) Context.pbinder_annot
val annotR : 'a -> 'a binder_annot
type case_invert = t Constr.pcase_invert
type 'a puniverses = 'a * EInstance.t
Destructors

Same as Constr.kind except that it expands evars and normalizes universes on the fly.

val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t

Returns the evar-normal form of the argument. Note that this function is supposed to be called when the original term has not more free-evars anymore. If you need compatibility with the old semantics, set abort_on_undefined_evars to false.

For getting the evar-normal form of a term with evars see Evarutil.nf_evar.

val to_constr_opt : Evd.evar_map -> t -> Constr.t option

Same as to_constr, but returns None if some unresolved evars remain

type kind_of_type =
  1. | SortType of ESorts.t
  2. | CastType of types * t
  3. | ProdType of Names.Name.t binder_annot * t * t
  4. | LetInType of Names.Name.t binder_annot * t * t * t
  5. | AtomicType of t * t array
val kind_of_type : Evd.evar_map -> t -> kind_of_type
Constructors

Construct a term from a view.

val of_constr : Constr.t -> t

Translate a kernel term into an incomplete term in O(1).

Insensitive primitives

Evar-insensitive versions of the corresponding functions. See the Constr module for more information.

Constructors
val mkRel : int -> t
val mkVar : Names.Id.t -> t
val mkMeta : Constr.metavariable -> t
val mkEvar : t Constr.pexistential -> t
val mkSort : ESorts.t -> t
val mkSProp : t
val mkProp : t
val mkSet : t
val mkType : Univ.Universe.t -> t
val mkCast : (t * Constr.cast_kind * t) -> t
val mkProd : (Names.Name.t binder_annot * t * t) -> t
val mkLambda : (Names.Name.t binder_annot * t * t) -> t
val mkLetIn : (Names.Name.t binder_annot * t * t * t) -> t
val mkApp : (t * t array) -> t
val mkConstU : (Names.Constant.t * EInstance.t) -> t
val mkProj : (Names.Projection.t * ERelevance.t * t) -> t
val mkIndU : (Names.inductive * EInstance.t) -> t
val mkConstructU : (Names.constructor * EInstance.t) -> t
val mkConstructUi : ((Names.inductive * EInstance.t) * int) -> t
val mkCase : case -> t
val mkFix : (t, t, ERelevance.t) Constr.pfixpoint -> t
val mkCoFix : (t, t, ERelevance.t) Constr.pcofixpoint -> t
val mkArrow : t -> ERelevance.t -> t -> t
val mkArrowR : t -> t -> t
val mkInt : Uint63.t -> t
val mkFloat : Float64.t -> t
val mkString : Pstring.t -> t
val mkArray : (EInstance.t * t array * t * t) -> t
module UnsafeMonomorphic : sig ... end
val mkRef : (Names.GlobRef.t * EInstance.t) -> t
val type1 : t
val applist : (t * t list) -> t
val applistc : t -> t list -> t

Abstracting/generalizing over binders

it = iterated or_LetIn = turn a local definition into a LetIn wo_LetIn = inlines local definitions (i.e. substitute them in the body) Named = binding is by name and the combinators turn it into a binding by index (complexity is nb(binders) * size(term))

val it_mkProd : t -> (Names.Name.t binder_annot * t) list -> t
val it_mkLambda : t -> (Names.Name.t binder_annot * t) list -> t
val mkProd_or_LetIn : rel_declaration -> t -> t
val mkLambda_or_LetIn : rel_declaration -> t -> t
val it_mkProd_or_LetIn : t -> rel_context -> t
val it_mkLambda_or_LetIn : t -> rel_context -> t
val mkProd_wo_LetIn : rel_declaration -> t -> t
val mkLambda_wo_LetIn : rel_declaration -> t -> t
val it_mkProd_wo_LetIn : t -> rel_context -> t
val it_mkLambda_wo_LetIn : t -> rel_context -> t
val mkNamedProd : Evd.evar_map -> Names.Id.t binder_annot -> types -> types -> types
val mkNamedLambda : Evd.evar_map -> Names.Id.t binder_annot -> types -> constr -> constr
val mkNamedLetIn : Evd.evar_map -> Names.Id.t binder_annot -> constr -> types -> constr -> constr
val mkNamedProd_or_LetIn : Evd.evar_map -> named_declaration -> types -> types
val mkNamedLambda_or_LetIn : Evd.evar_map -> named_declaration -> types -> types
val it_mkNamedProd_or_LetIn : Evd.evar_map -> t -> named_context -> t
val it_mkNamedLambda_or_LetIn : Evd.evar_map -> t -> named_context -> t
val mkNamedProd_wo_LetIn : Evd.evar_map -> named_declaration -> t -> t
val it_mkNamedProd_wo_LetIn : Evd.evar_map -> t -> named_context -> t
val mkLEvar : Evd.evar_map -> (Evar.t * t list) -> t

Variant of mkEvar that removes identity variable instances from its argument.

Simple case analysis
val isRel : Evd.evar_map -> t -> bool
val isVar : Evd.evar_map -> t -> bool
val isInd : Evd.evar_map -> t -> bool
val isRef : Evd.evar_map -> t -> bool
val isEvar : Evd.evar_map -> t -> bool
val isMeta : Evd.evar_map -> t -> bool
val isSort : Evd.evar_map -> t -> bool
val isCast : Evd.evar_map -> t -> bool
val isApp : Evd.evar_map -> t -> bool
val isLambda : Evd.evar_map -> t -> bool
val isLetIn : Evd.evar_map -> t -> bool
val isProd : Evd.evar_map -> t -> bool
val isConst : Evd.evar_map -> t -> bool
val isConstruct : Evd.evar_map -> t -> bool
val isFix : Evd.evar_map -> t -> bool
val isCoFix : Evd.evar_map -> t -> bool
val isCase : Evd.evar_map -> t -> bool
val isProj : Evd.evar_map -> t -> bool
val isType : Evd.evar_map -> constr -> bool
type arity = rel_context * ESorts.t
val mkArity : arity -> types
val destArity : Evd.evar_map -> types -> arity
val isArity : Evd.evar_map -> t -> bool
val isVarId : Evd.evar_map -> Names.Id.t -> t -> bool
val isRelN : Evd.evar_map -> int -> t -> bool
val isRefX : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> t -> bool
val is_lib_ref : Environ.env -> Evd.evar_map -> string -> t -> bool

The string is interpreted by Rocqlib.lib_ref. If it is not registered, return false.

val destRel : Evd.evar_map -> t -> int
val destMeta : Evd.evar_map -> t -> Constr.metavariable
val destVar : Evd.evar_map -> t -> Names.Id.t
val destSort : Evd.evar_map -> t -> ESorts.t
val destCast : Evd.evar_map -> t -> t * Constr.cast_kind * t
val destLambda : Evd.evar_map -> t -> Names.Name.t binder_annot * types * t
val destLetIn : Evd.evar_map -> t -> Names.Name.t binder_annot * t * types * t
val destApp : Evd.evar_map -> t -> t * t array
val destConst : Evd.evar_map -> t -> Names.Constant.t * EInstance.t
val destEvar : Evd.evar_map -> t -> t Constr.pexistential
val destConstruct : Evd.evar_map -> t -> Names.constructor * EInstance.t
val destCase : Evd.evar_map -> t -> case
val destFix : Evd.evar_map -> t -> (t, t, ERelevance.t) Constr.pfixpoint
val destCoFix : Evd.evar_map -> t -> (t, t, ERelevance.t) Constr.pcofixpoint
val decompose_app : Evd.evar_map -> t -> t * t array
val decompose_app_list : Evd.evar_map -> t -> t * t list
val decompose_lambda : Evd.evar_map -> t -> (Names.Name.t binder_annot * t) list * t

Pops lambda abstractions until there are no more, skipping casts.

val decompose_lambda_decls : Evd.evar_map -> t -> rel_context * t

Pops lambda abstractions and letins until there are no more, skipping casts.

val decompose_lambda_n : Evd.evar_map -> int -> t -> (Names.Name.t binder_annot * t) list * t

Pops n lambda abstractions, skipping casts.

  • raises UserError

    if the term doesn't have enough lambdas.

val decompose_lambda_n_assum : Evd.evar_map -> int -> t -> rel_context * t

Pops n lambda abstractions, and pop letins only if needed to expose enough lambdas, skipping casts.

  • raises UserError

    if the term doesn't have enough lambdas.

val decompose_lambda_n_decls : Evd.evar_map -> int -> t -> rel_context * t

Pops n lambda abstractions and letins, skipping casts.

  • raises UserError

    if the term doesn't have enough lambdas/letins.

val decompose_lambda_n_decls_opt : Evd.evar_map -> int -> t -> (rel_context * t) option

Like decompose_lambda_n_decls but returns None instead of raising an anomaly when there are not enough abstractions.

val prod_decls : Evd.evar_map -> t -> rel_context
val to_lambda : Evd.evar_map -> int -> t -> t
val decompose_prod : Evd.evar_map -> t -> (Names.Name.t binder_annot * t) list * t
val decompose_prod_n : Evd.evar_map -> int -> t -> (Names.Name.t binder_annot * t) list * t
val decompose_prod_decls : Evd.evar_map -> t -> rel_context * t
val decompose_prod_n_decls : Evd.evar_map -> int -> t -> rel_context * t
val existential_type : Evd.evar_map -> existential -> types
val whd_evar : Evd.evar_map -> constr -> constr
Equality
val eq_constr : Evd.evar_map -> t -> t -> bool
val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
val eq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option

Does not produce QLeq nor QElimTo constraints

val leq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
val eq_existential : Evd.evar_map -> (t -> t -> bool) -> existential -> existential -> bool
val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option

eq_constr_universes_proj can equate projections and their eta-expanded constant form.

val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
Iterators
val map : Evd.evar_map -> (t -> t) -> t -> t
val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
val map_branches : (t -> t) -> case_branch array -> case_branch array
val map_return_predicate : (t -> t) -> case_return -> case_return
val map_existential : Evd.evar_map -> (t -> t) -> existential -> existential
val iter : Evd.evar_map -> (t -> unit) -> t -> unit
val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
val iter_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
val fold_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> t -> 'b) -> 'a -> 'b -> t -> 'b

Gather the universes transitively used in the term, including in the type of evars appearing in it.

Substitutions
module Vars : sig ... end

See vars.mli for the documentation of the functions below

Environment handling
val push_rel_context : rel_context -> Environ.env -> Environ.env
val push_rec_types : rec_declaration -> Environ.env -> Environ.env
val push_named_context : (Environ.var_status * named_declaration) list -> Environ.env -> Environ.env
val rel_context : Environ.env -> rel_context
val named_context : Environ.env -> named_context
val val_of_named_context : (Environ.var_status * named_declaration) list -> Environ.named_context_val
val named_context_of_val : Environ.named_context_val -> named_context
val named_context_of_val_with_status : Environ.named_context_val -> (Environ.var_status * named_declaration) list
val fold_named_context_val : (Environ.named_context_val -> Environ.var_status -> named_declaration -> 'a -> 'a) -> Environ.named_context_val -> init:'a -> 'a
val fold_named_context : (Environ.env -> Environ.var_status -> named_declaration -> 'a -> 'a) -> Environ.env -> init:'a -> 'a
val lookup_rel : int -> Environ.env -> rel_declaration
val check_hyps_inclusion : Environ.env -> Names.GlobRef.t -> Constr.named_context -> unit

check_hyps_inclusion env gr hyps Check that hyps are included in env and fails with error otherwise.

val constant_value_in : Environ.env -> Evd.evar_map -> (Names.Constant.t * EInstance.t) -> constr
val map_rel_context_in_env : (Environ.env -> constr -> constr) -> Environ.env -> rel_context -> rel_context

map_named_val f ctxt apply f to the body and the type of each declarations. *** /!\ *** f t must preserve the name

val identity_subst_val : Environ.named_context_val -> t SList.t
val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:EInstance.t -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Evd.evar_map * t
val annotate_case : Environ.env -> Evd.evar_map -> case -> Constr.case_info * EInstance.t * t array * ((rel_context * t) * ERelevance.t) * case_invert * t * (rel_context * t) array

Same as above, but doesn't turn contexts into binders

val expand_branch : Environ.env -> Evd.evar_map -> EInstance.t -> t array -> Names.constructor -> case_branch -> rel_context

Given a universe instance and parameters for the inductive type, constructs the typed context in which the branch lives.

Extra
val of_existential : Constr.existential -> existential
val of_named_context : Constr.named_context -> named_context
val of_rel_context : Constr.rel_context -> rel_context
val to_named_context : Evd.evar_map -> named_context -> Constr.named_context
val to_rel_context : Evd.evar_map -> rel_context -> Constr.rel_context
val of_case_invert : Constr.case_invert -> case_invert
val of_constr_array : Constr.t array -> t array
val of_binder_annot : 'a Constr.binder_annot -> 'a binder_annot
val to_binder_annot : Evd.evar_map -> 'a binder_annot -> 'a Constr.binder_annot
Unsafe operations
module Unsafe : sig ... end
Delayed evar expansion
module Expand : sig ... end