Module `EConstr`Source

Sourcetype t = Evd.econstr

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

Universe variables

Sourcemodule ERelevance : sig ... end

Sourcemodule ESorts : sig ... end

Sourcemodule EInstance : sig ... end

Sourcetype types = t

Sourcetype constr = t

Sourcetype existential = t Constr.pexistential

Sourcetype case_return = (t, ERelevance.t) Constr.pcase_return

Sourcetype case_branch = (t, ERelevance.t) Constr.pcase_branch

Sourcetype rec_declaration = (t, t, ERelevance.t) Constr.prec_declaration

Sourcetype fixpoint = (t, t, ERelevance.t) Constr.pfixpoint

Sourcetype cofixpoint = (t, t, ERelevance.t) Constr.pcofixpoint

Sourcetype unsafe_judgment = (constr, types) Environ.punsafe_judgment

Sourcetype unsafe_type_judgment = (types, Evd.esorts) Environ.punsafe_type_judgment

Source

type named_declaration =
  (constr, types, ERelevance.t) Context.Named.Declaration.pt

Sourcetype rel_declaration = (constr, types, ERelevance.t) Context.Rel.Declaration.pt

Source

type compacted_declaration =
  (constr, types, ERelevance.t) Context.Compacted.Declaration.pt

Sourcetype named_context = (constr, types, ERelevance.t) Context.Named.pt

Sourcetype compacted_context = compacted_declaration list

Sourcetype rel_context = (constr, types, ERelevance.t) Context.Rel.pt

Sourcetype 'a binder_annot = ('a, ERelevance.t) Context.pbinder_annot

Sourceval annotR : 'a -> 'a binder_annot

Sourceval nameR : Names.Id.t -> Names.Name.t binder_annot

Sourceval anonR : Names.Name.t binder_annot

Sourcetype case_invert = t Constr.pcase_invert

Sourcetype case = (t, t, EInstance.t, ERelevance.t) Constr.pcase

Sourcetype 'a puniverses = 'a * EInstance.t

Destructors

Source

val kind : 
  Evd.evar_map ->
  t ->
  (t, t, ESorts.t, EInstance.t, ERelevance.t) Constr.kind_of_term

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

Source

val kind_upto : 
  Evd.evar_map ->
  Constr.t ->
  (Constr.t, Constr.t, Sorts.t, UVars.Instance.t, Sorts.relevance)
    Constr.kind_of_term

Sourceval 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.

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

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

Sourcetype kind_of_type =

| SortType of ESorts.t
| CastType of types * t
| ProdType of Names.Name.t binder_annot * t * t
| LetInType of Names.Name.t binder_annot * t * t * t
| AtomicType of t * t array

Sourceval kind_of_type : Evd.evar_map -> t -> kind_of_type

Constructors

Source

val of_kind : 
  (t, t, ESorts.t, EInstance.t, ERelevance.t) Constr.kind_of_term ->
  t

Construct a term from a view.

Sourceval 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

Sourceval mkRel : int -> t

Sourceval mkVar : Names.Id.t -> t

Sourceval mkMeta : Constr.metavariable -> t

Sourceval mkEvar : t Constr.pexistential -> t

Sourceval mkSort : ESorts.t -> t

Sourceval mkSProp : t

Sourceval mkProp : t

Sourceval mkSet : t

Sourceval mkType : Univ.Universe.t -> t

Sourceval mkCast : (t * Constr.cast_kind * t) -> t

Sourceval mkProd : (Names.Name.t binder_annot * t * t) -> t

Sourceval mkLambda : (Names.Name.t binder_annot * t * t) -> t

Sourceval mkLetIn : (Names.Name.t binder_annot * t * t * t) -> t

Sourceval mkApp : (t * t array) -> t

Sourceval mkConstU : (Names.Constant.t * EInstance.t) -> t

Sourceval mkProj : (Names.Projection.t * ERelevance.t * t) -> t

Sourceval mkIndU : (Names.inductive * EInstance.t) -> t

Sourceval mkConstructU : (Names.constructor * EInstance.t) -> t

Sourceval mkConstructUi : ((Names.inductive * EInstance.t) * int) -> t

Sourceval mkCase : case -> t

Sourceval mkFix : (t, t, ERelevance.t) Constr.pfixpoint -> t

Sourceval mkCoFix : (t, t, ERelevance.t) Constr.pcofixpoint -> t

Sourceval mkArrow : t -> ERelevance.t -> t -> t

Sourceval mkArrowR : t -> t -> t

Sourceval mkInt : Uint63.t -> t

Sourceval mkFloat : Float64.t -> t

Sourceval mkString : Pstring.t -> t

Sourceval mkArray : (EInstance.t * t array * t * t) -> t

Sourcemodule UnsafeMonomorphic : sig ... end

Sourceval mkConst : Names.Constant.t -> t

deprecated (8.18) Use [mkConstU] or if truly needed [UnsafeMonomorphic.mkConst]

Sourceval mkInd : Names.inductive -> t

deprecated (8.18) Use [mkIndU] or if truly needed [UnsafeMonomorphic.mkInd]

Sourceval mkConstruct : Names.constructor -> t

deprecated (8.18) Use [mkConstructU] or if truly needed [UnsafeMonomorphic.mkConstruct]

Sourceval mkRef : (Names.GlobRef.t * EInstance.t) -> t

Sourceval type1 : t

Sourceval applist : (t * t list) -> t

Sourceval 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))

Sourceval it_mkProd : t -> (Names.Name.t binder_annot * t) list -> t

Sourceval it_mkLambda : t -> (Names.Name.t binder_annot * t) list -> t

Sourceval mkProd_or_LetIn : rel_declaration -> t -> t

Sourceval mkLambda_or_LetIn : rel_declaration -> t -> t

Sourceval it_mkProd_or_LetIn : t -> rel_context -> t

Sourceval it_mkLambda_or_LetIn : t -> rel_context -> t

Sourceval mkProd_wo_LetIn : rel_declaration -> t -> t

Sourceval mkLambda_wo_LetIn : rel_declaration -> t -> t

Sourceval it_mkProd_wo_LetIn : t -> rel_context -> t

Sourceval it_mkLambda_wo_LetIn : t -> rel_context -> t

Source

val mkNamedProd : 
  Evd.evar_map ->
  Names.Id.t binder_annot ->
  types ->
  types ->
  types

Source

val mkNamedLambda : 
  Evd.evar_map ->
  Names.Id.t binder_annot ->
  types ->
  constr ->
  constr

Source

val mkNamedLetIn : 
  Evd.evar_map ->
  Names.Id.t binder_annot ->
  constr ->
  types ->
  constr ->
  constr

Sourceval mkNamedProd_or_LetIn : Evd.evar_map -> named_declaration -> types -> types

Source

val mkNamedLambda_or_LetIn : 
  Evd.evar_map ->
  named_declaration ->
  types ->
  types

Sourceval it_mkNamedProd_or_LetIn : Evd.evar_map -> t -> named_context -> t

Sourceval it_mkNamedLambda_or_LetIn : Evd.evar_map -> t -> named_context -> t

Sourceval mkNamedProd_wo_LetIn : Evd.evar_map -> named_declaration -> t -> t

Sourceval it_mkNamedProd_wo_LetIn : Evd.evar_map -> t -> named_context -> t

Sourceval mkLEvar : Evd.evar_map -> (Evar.t * t list) -> t

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

Simple case analysis

Sourceval isRel : Evd.evar_map -> t -> bool

Sourceval isVar : Evd.evar_map -> t -> bool

Sourceval isInd : Evd.evar_map -> t -> bool

Sourceval isRef : Evd.evar_map -> t -> bool

Sourceval isEvar : Evd.evar_map -> t -> bool

Sourceval isMeta : Evd.evar_map -> t -> bool

Sourceval isSort : Evd.evar_map -> t -> bool

Sourceval isCast : Evd.evar_map -> t -> bool

Sourceval isApp : Evd.evar_map -> t -> bool

Sourceval isLambda : Evd.evar_map -> t -> bool

Sourceval isLetIn : Evd.evar_map -> t -> bool

Sourceval isProd : Evd.evar_map -> t -> bool

Sourceval isConst : Evd.evar_map -> t -> bool

Sourceval isConstruct : Evd.evar_map -> t -> bool

Sourceval isFix : Evd.evar_map -> t -> bool

Sourceval isCoFix : Evd.evar_map -> t -> bool

Sourceval isCase : Evd.evar_map -> t -> bool

Sourceval isProj : Evd.evar_map -> t -> bool

Sourceval isType : Evd.evar_map -> constr -> bool

Sourcetype arity = rel_context * ESorts.t

Sourceval mkArity : arity -> types

Sourceval destArity : Evd.evar_map -> types -> arity

Sourceval isArity : Evd.evar_map -> t -> bool

Sourceval isVarId : Evd.evar_map -> Names.Id.t -> t -> bool

Sourceval isRelN : Evd.evar_map -> int -> t -> bool

Sourceval isRefX : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> t -> bool

Sourceval 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.

Sourceval destRel : Evd.evar_map -> t -> int

Sourceval destMeta : Evd.evar_map -> t -> Constr.metavariable

Sourceval destVar : Evd.evar_map -> t -> Names.Id.t

Sourceval destSort : Evd.evar_map -> t -> ESorts.t

Sourceval destCast : Evd.evar_map -> t -> t * Constr.cast_kind * t

Sourceval destProd : Evd.evar_map -> t -> Names.Name.t binder_annot * types * types

Sourceval destLambda : Evd.evar_map -> t -> Names.Name.t binder_annot * types * t

Sourceval destLetIn : Evd.evar_map -> t -> Names.Name.t binder_annot * t * types * t

Sourceval destApp : Evd.evar_map -> t -> t * t array

Sourceval destConst : Evd.evar_map -> t -> Names.Constant.t * EInstance.t

Sourceval destEvar : Evd.evar_map -> t -> t Constr.pexistential

Sourceval destInd : Evd.evar_map -> t -> Names.inductive * EInstance.t

Sourceval destConstruct : Evd.evar_map -> t -> Names.constructor * EInstance.t

Sourceval destCase : Evd.evar_map -> t -> case

Sourceval destProj : Evd.evar_map -> t -> Names.Projection.t * ERelevance.t * t

Sourceval destFix : Evd.evar_map -> t -> (t, t, ERelevance.t) Constr.pfixpoint

Sourceval destCoFix : Evd.evar_map -> t -> (t, t, ERelevance.t) Constr.pcofixpoint

Sourceval destRef : Evd.evar_map -> t -> Names.GlobRef.t * EInstance.t

Sourceval decompose_app : Evd.evar_map -> t -> t * t array

Sourceval decompose_app_list : Evd.evar_map -> t -> t * t list

Source

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.

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

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

Source

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.

Sourceval 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.

Sourceval 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.

Sourceval prod_decls : Evd.evar_map -> t -> rel_context

Sourceval compose_lam : (Names.Name.t binder_annot * t) list -> t -> t

deprecated (8.17) Use [it_mkLambda] instead.

Sourceval to_lambda : Evd.evar_map -> int -> t -> t

Source

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

Source

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

Sourceval decompose_prod_decls : Evd.evar_map -> t -> rel_context * t

Sourceval decompose_prod_n_decls : Evd.evar_map -> int -> t -> rel_context * t

Sourceval existential_type : Evd.evar_map -> existential -> types

Sourceval whd_evar : Evd.evar_map -> constr -> constr

Equality

Sourceval eq_constr : Evd.evar_map -> t -> t -> bool

Sourceval eq_constr_nounivs : Evd.evar_map -> t -> t -> bool

Source

val eq_constr_universes : 
  Environ.env ->
  Evd.evar_map ->
  ?nargs:int ->
  t ->
  t ->
  UnivProblem.Set.t option

Source

val leq_constr_universes : 
  Environ.env ->
  Evd.evar_map ->
  ?nargs:int ->
  t ->
  t ->
  UnivProblem.Set.t option

Source

val eq_existential : 
  Evd.evar_map ->
  (t -> t -> bool) ->
  existential ->
  existential ->
  bool

Source

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.

Sourceval compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool

Iterators

Sourceval map : Evd.evar_map -> (t -> t) -> t -> t

Source

val map_with_binders : 
  Evd.evar_map ->
  ('a -> 'a) ->
  ('a -> t -> t) ->
  'a ->
  t ->
  t

Sourceval map_branches : (t -> t) -> case_branch array -> case_branch array

Sourceval map_return_predicate : (t -> t) -> case_return -> case_return

Sourceval map_existential : Evd.evar_map -> (t -> t) -> existential -> existential

Sourceval iter : Evd.evar_map -> (t -> unit) -> t -> unit

Source

val iter_with_binders : 
  Evd.evar_map ->
  ('a -> 'a) ->
  ('a -> t -> unit) ->
  'a ->
  t ->
  unit

Source

val iter_with_full_binders : 
  Environ.env ->
  Evd.evar_map ->
  (rel_declaration -> 'a -> 'a) ->
  ('a -> t -> unit) ->
  'a ->
  t ->
  unit

Sourceval fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a

Source

val fold_with_binders : 
  Evd.evar_map ->
  ('a -> 'a) ->
  ('a -> 'b -> t -> 'b) ->
  'a ->
  'b ->
  t ->
  'b

Source

val universes_of_constr : 
  ?init:(Sorts.QVar.Set.t * Univ.Level.Set.t) ->
  Evd.evar_map ->
  t ->
  Sorts.QVar.Set.t * Univ.Level.Set.t

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

Substitutions

Sourcemodule Vars : sig ... end

See vars.mli for the documentation of the functions below

Environment handling

Sourceval push_rel : rel_declaration -> Environ.env -> Environ.env

Sourceval push_rel_context : rel_context -> Environ.env -> Environ.env

Sourceval push_rec_types : rec_declaration -> Environ.env -> Environ.env

Sourceval push_named : named_declaration -> Environ.env -> Environ.env

Sourceval push_named_context : named_context -> Environ.env -> Environ.env

Source

val push_named_context_val : 
  named_declaration ->
  Environ.named_context_val ->
  Environ.named_context_val

Sourceval rel_context : Environ.env -> rel_context

Sourceval named_context : Environ.env -> named_context

Sourceval val_of_named_context : named_context -> Environ.named_context_val

Sourceval named_context_of_val : Environ.named_context_val -> named_context

Sourceval lookup_rel : int -> Environ.env -> rel_declaration

Sourceval lookup_named : Names.variable -> Environ.env -> named_declaration

Source

val lookup_named_val : 
  Names.variable ->
  Environ.named_context_val ->
  named_declaration

Source

val map_rel_context_in_env : 
  (Environ.env -> constr -> constr) ->
  Environ.env ->
  rel_context ->
  rel_context

Source

val match_named_context_val : 
  Environ.named_context_val ->
  (named_declaration * Environ.named_context_val) option

Sourceval identity_subst_val : Environ.named_context_val -> t SList.t

Source

val fresh_global : 
  ?loc:Loc.t ->
  ?rigid:Evd.rigid ->
  ?names:UVars.Instance.t ->
  Environ.env ->
  Evd.evar_map ->
  Names.GlobRef.t ->
  Evd.evar_map * t

Sourceval is_global : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> t -> bool

deprecated (8.12) Use [EConstr.isRefX] instead.

Source

val expand_case : 
  Environ.env ->
  Evd.evar_map ->
  case ->
  (t, t, ERelevance.t) Inductive.pexpanded_case

Source

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

Source

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.

Source

val contract_case : 
  Environ.env ->
  Evd.evar_map ->
  (t, t, ERelevance.t) Inductive.pexpanded_case ->
  case

Extra

Sourceval of_existential : Constr.existential -> existential

Sourceval of_named_decl : Constr.named_declaration -> named_declaration

Sourceval of_rel_decl : Constr.rel_declaration -> rel_declaration

Sourceval to_rel_decl : Evd.evar_map -> rel_declaration -> Constr.rel_declaration

Source

val to_named_decl : 
  Evd.evar_map ->
  named_declaration ->
  Constr.named_declaration

Sourceval of_named_context : Constr.named_context -> named_context

Sourceval of_rel_context : Constr.rel_context -> rel_context

Sourceval to_named_context : Evd.evar_map -> named_context -> Constr.named_context

Sourceval to_rel_context : Evd.evar_map -> rel_context -> Constr.rel_context

Sourceval of_case_invert : Constr.case_invert -> case_invert

Sourceval of_constr_array : Constr.t array -> t array

Sourceval of_binder_annot : 'a Constr.binder_annot -> 'a binder_annot

Sourceval to_binder_annot : Evd.evar_map -> 'a binder_annot -> 'a Constr.binder_annot

Unsafe operations

Sourcemodule Unsafe : sig ... end

Delayed evar expansion

Sourcemodule Expand : sig ... end

Deprecated

Sourceval decompose_lambda_assum : Evd.evar_map -> t -> rel_context * t

deprecated (8.18) Use [decompose_lambda_decls] instead.

Sourceval decompose_prod_assum : Evd.evar_map -> t -> rel_context * t

deprecated (8.18) Use [decompose_prod_decls] instead.

Sourceval decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t

deprecated (8.18) Use [decompose_prod_n_decls] instead.

Sourceval prod_assum : Evd.evar_map -> t -> rel_context

deprecated (8.18) Use [prod_decls] instead.

Source

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

deprecated (8.18) Use [decompose_lambda] instead.

Sourceval decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t

deprecated (8.18) Use [decompose_lambda_n_assum] instead.

Sourceval decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t

deprecated (8.18) Use [decompose_lambda_n_decls] instead.

Sourceval decompose_lam_assum : Evd.evar_map -> t -> rel_context * t

deprecated (8.18) Use [decompose_lambda_assum] instead.

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.engine/EConstr/index.html

Module `EConstr`Source

Universe variables

Destructors

Constructors

Insensitive primitives

Constructors

Simple case analysis

Equality

Iterators

Substitutions

Environment handling

Extra

Unsafe operations

Delayed evar expansion

package rocq-runtime

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.engine/EConstr/index.html

Module EConstrSource

Universe variables

Destructors

Constructors

Insensitive primitives

Constructors

Simple case analysis

Equality

Iterators

Substitutions

Environment handling

Extra

Unsafe operations

Delayed evar expansion

dune-project
Dependency

Module `EConstr`Source