Module `CClosure`Source

...

Delta implies all consts (both global (= by kernel_name) and local (= by Rel or Var)), all evars, and letin's. Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction

Sourcemodule RedFlags : sig ... end

Sets of reduction kinds.

Sourceval all : RedFlags.reds

Sourceval allnolet : RedFlags.reds

Sourceval beta : RedFlags.reds

Sourceval betadeltazeta : RedFlags.reds

Sourceval betaiota : RedFlags.reds

Sourceval betaiotazeta : RedFlags.reds

Sourceval betazeta : RedFlags.reds

Sourceval delta : RedFlags.reds

Sourceval zeta : RedFlags.reds

Sourceval nored : RedFlags.reds

Sourcetype table_key = Names.Constant.t Univ.puniverses Names.tableKey

Sourcemodule KeyTable : Hashtbl.S with type key = table_key

fconstr is the type of frozen constr

Sourcetype fconstr

fconstr can be accessed by using the function fterm_of and by matching on type fterm

Sourcetype finvert

Sourcetype 'a usubs = 'a Esubst.subs Univ.puniverses

Sourcetype evar_repack

Sourcetype fterm =

| FRel of int
| FAtom of Constr.constr
(*
Metas and Sorts
*)
| FFlex of table_key
| FInd of Constr.pinductive
| FConstruct of Constr.pconstructor
| FApp of fconstr * fconstr array
| FProj of Names.Projection.t * fconstr
| FFix of Constr.fixpoint * fconstr usubs
| FCoFix of Constr.cofixpoint * fconstr usubs
| FCaseT of Constr.case_info * Univ.Instance.t * Constr.constr array * Constr.case_return * fconstr * Constr.case_branch array * fconstr usubs
| FCaseInvert of Constr.case_info * Univ.Instance.t * Constr.constr array * Constr.case_return * finvert * fconstr * Constr.case_branch array * fconstr usubs
| FLambda of int * (Names.Name.t Context.binder_annot * Constr.constr) list * Constr.constr * fconstr usubs
| FProd of Names.Name.t Context.binder_annot * fconstr * Constr.constr * fconstr usubs
| FLetIn of Names.Name.t Context.binder_annot * fconstr * fconstr * Constr.constr * fconstr usubs
| FEvar of Evar.t * Constr.constr list * fconstr usubs * evar_repack
| FInt of Uint63.t
| FFloat of Float64.t
| FArray of Univ.Instance.t * fconstr Parray.t * fconstr
| FLIFT of int * fconstr
| FCLOS of Constr.constr * fconstr usubs
| FIrrelevant
| FLOCKED

Sourcetype 'a next_native_args = (CPrimitives.arg_kind * 'a) list

Sourcetype stack_member =

| Zapp of fconstr array
| ZcaseT of Constr.case_info * Univ.Instance.t * Constr.constr array * Constr.case_return * Constr.case_branch array * fconstr usubs
| Zproj of Names.Projection.Repr.t
| Zfix of fconstr * stack
| Zprimitive of CPrimitives.t * Constr.pconstant * fconstr list * fconstr next_native_args
| Zshift of int
| Zupdate of fconstr

Sourceand stack = stack_member list

Sourceval empty_stack : stack

Sourceval append_stack : fconstr array -> stack -> stack

Sourceval check_native_args : CPrimitives.t -> stack -> bool

Source

val get_native_args1 : 
  CPrimitives.t ->
  Constr.pconstant ->
  stack ->
  fconstr list * fconstr * fconstr next_native_args * stack

Sourceval stack_args_size : stack -> int

Source

val inductive_subst : 
  Declarations.mutual_inductive_body ->
  Univ.Instance.t ->
  fconstr array ->
  fconstr usubs

Sourceval usubs_lift : 'a usubs -> 'a usubs

Sourceval usubs_liftn : int -> 'a usubs -> 'a usubs

Sourceval usubs_cons : 'a -> 'a usubs -> 'a usubs

Sourceval usubst_instance : 'a Univ.puniverses -> Univ.Instance.t -> Univ.Instance.t

identity if the first instance is empty

To lazy reduce a constr, create a clos_infos with create_clos_infos, inject the term to reduce with inject; then use a reduction function

Sourceval inject : Constr.constr -> fconstr

Sourceval mk_atom : Constr.constr -> fconstr

mk_atom: prevents a term from being evaluated

Sourceval mk_red : fterm -> fconstr

mk_red: makes a reducible term (used in ring)

Sourceval fterm_of : fconstr -> fterm

Sourceval term_of_fconstr : fconstr -> Constr.constr

Source

val destFLambda : 
  (fconstr usubs -> Constr.constr -> fconstr) ->
  fconstr ->
  Names.Name.t Context.binder_annot * fconstr * fconstr

Sourcetype clos_infos

Global and local constant cache

Sourcetype clos_tab

Source

val create_conv_infos : 
  ?univs:UGraph.t ->
  ?evars:Constr.constr Constr.evar_handler ->
  RedFlags.reds ->
  Environ.env ->
  clos_infos

Source

val create_clos_infos : 
  ?univs:UGraph.t ->
  ?evars:Constr.constr Constr.evar_handler ->
  RedFlags.reds ->
  Environ.env ->
  clos_infos

Sourceval oracle_of_infos : clos_infos -> Conv_oracle.oracle

Sourceval create_tab : unit -> clos_tab

Sourceval info_env : clos_infos -> Environ.env

Sourceval info_flags : clos_infos -> RedFlags.reds

Sourceval info_univs : clos_infos -> UGraph.t

Sourceval unfold_projection : clos_infos -> Names.Projection.t -> stack_member option

Sourceval push_relevance : clos_infos -> 'b Context.binder_annot -> clos_infos

Sourceval push_relevances : clos_infos -> 'b Context.binder_annot array -> clos_infos

Sourceval set_info_relevances : clos_infos -> Sorts.relevance Range.t -> clos_infos

Sourceval info_relevances : clos_infos -> Sorts.relevance Range.t

Sourceval infos_with_reds : clos_infos -> RedFlags.reds -> clos_infos

Reduction function

Sourceval norm_val : clos_infos -> clos_tab -> fconstr -> Constr.constr

norm_val is for strong normalization

Source

val norm_term : 
  clos_infos ->
  clos_tab ->
  fconstr usubs ->
  Constr.constr ->
  Constr.constr

Same as norm_val but for terms

Sourceval whd_val : clos_infos -> clos_tab -> fconstr -> Constr.constr

whd_val is for weak head normalization

Sourceval whd_stack : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack

whd_stack performs weak head normalization in a given stack. It stops whenever a reduction is blocked.

Sourceval skip_irrelevant_stack : clos_infos -> stack -> stack

Source

val eta_expand_stack : 
  clos_infos ->
  Names.Name.t Context.binder_annot ->
  stack ->
  stack

Source

val eta_expand_ind_stack : 
  Environ.env ->
  Names.inductive ->
  fconstr ->
  stack ->
  (fconstr * stack) ->
  stack * stack

eta_expand_ind_stack env ind c s t computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. Assumes t is a rigid term, and not a constructor. ind is the inductive of the constructor term c

raises Not_found
if the inductive is not a primitive record, or if the constructor is partially applied.

Conversion auxiliary functions to do step by step normalisation

Source

val unfold_ref_with_args : 
  clos_infos ->
  clos_tab ->
  table_key ->
  stack ->
  (fconstr * stack) option

Like unfold_reference, but handles primitives: if there are not enough arguments, return None. Otherwise return Some with ZPrimitive added to the stack. Produces a FIrrelevant when the reference is irrelevant and the infos was created with create_conv_infos.

Sourceval set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit

Hook for Reduction

Sourceval lift_fconstr : int -> fconstr -> fconstr

Sourceval lift_fconstr_vect : int -> fconstr array -> fconstr array

Sourceval mk_clos : fconstr usubs -> Constr.constr -> fconstr

Sourceval mk_clos_vect : fconstr usubs -> Constr.constr array -> fconstr array

Sourceval kni : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack

Sourceval knr : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack

Sourceval kl : clos_infos -> clos_tab -> fconstr -> Constr.constr

Sourceval zip : fconstr -> stack -> fconstr

Sourceval term_of_process : fconstr -> stack -> Constr.constr

Sourceval to_constr : Esubst.lift Univ.puniverses -> fconstr -> Constr.constr

End of cbn debug section i

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/CClosure/index.html

Module `CClosure`Source

...

package coq-core

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/CClosure/index.html

Module CClosureSource

...

dune-project
Dependency

Module `CClosure`Source