CClosure (rocq-runtime.CClosure)

fconstr is the type of frozen constr

type fconstr

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

type finvert

type evar_repack

type usubs = fconstr Esubst.subs UVars.puniverses

type table_key = Names.Constant.t UVars.puniverses Names.tableKey

type fterm =

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

Relevances (eg in binder_annot or case_info) have NOT been substituted when there is a usubs field

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

type stack_member =

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

and stack = stack_member list

val empty_stack : stack

val append_stack : fconstr array -> stack -> stack

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

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

val get_invert : finvert -> fconstr array

val stack_args_size : stack -> int

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

val usubs_lift : usubs -> usubs

val usubs_liftn : int -> usubs -> usubs

val usubs_cons : fconstr -> usubs -> usubs

val usubst_instance : 
  'a UVars.puniverses ->
  UVars.Instance.t ->
  UVars.Instance.t

identity if the first instance is empty

val usubst_binder : 
  _ UVars.puniverses ->
  'a Constr.binder_annot ->
  'a Constr.binder_annot

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

val inject : Constr.constr -> fconstr

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

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

val zip : fconstr -> stack -> fconstr

val fterm_of : fconstr -> fterm

val term_of_fconstr : fconstr -> Constr.constr

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

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

type clos_infos

Global and local constant cache

type clos_tab

type 'a evar_expansion =

| EvarDefined of 'a
| EvarUndefined of Evar.t * 'a list

type evar_handler = {

evar_expand : Constr.constr Constr.pexistential -> Constr.constr evar_expansion;
evar_repack : (Evar.t * Constr.constr list) -> Constr.constr;
evar_irrelevant : Constr.constr Constr.pexistential -> bool;
qvar_irrelevant : Sorts.QVar.t -> bool;
qual_equal : Sorts.Quality.t -> Sorts.Quality.t -> bool;
abstr_const : Names.Constant.t -> (unit, (unit -> Vmemitcodes.to_patch) Vmemitcodes.pbody_code) Declarations.pconstant_body;

}

val default_evar_handler : Environ.env -> evar_handler

val lookup_constant_handler : 
  Environ.env ->
  evar_handler ->
  Names.Constant.t ->
  (unit, (unit -> Vmemitcodes.to_patch) Vmemitcodes.pbody_code)
    Declarations.pconstant_body

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

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

val oracle_of_infos : clos_infos -> Conv_oracle.oracle

val create_tab : unit -> clos_tab

val info_env : clos_infos -> Environ.env

val info_flags : clos_infos -> RedFlags.reds

val info_univs : clos_infos -> UGraph.t

val unfold_projection : 
  clos_infos ->
  Names.Projection.t ->
  Sorts.relevance ->
  stack_member option

val push_relevance : clos_infos -> 'b Constr.binder_annot -> clos_infos

val push_relevances : clos_infos -> 'b Constr.binder_annot array -> clos_infos

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

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

val is_irrelevant : clos_infos -> Sorts.relevance -> bool

val eq_quality : clos_infos -> Sorts.Quality.t -> Sorts.Quality.t -> bool

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

Reduction function

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

norm_val is for strong normalization

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

Same as norm_val but for terms

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

whd_val is for weak head normalization

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

val skip_irrelevant_stack : clos_infos -> stack -> stack

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

val eta_expand_ind_stack : 
  Environ.env ->
  Constr.pinductive ->
  fconstr array ->
  (fconstr * stack) ->
  stack * stack

eta_expand_ind_stack env ind args t computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the constructor of this inductive type applied to arguments args. @assumes t is a rigid term, and not a constructor; that args are valid arguments for the constructor of inductive ind.

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

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.

val get_ref_mask : clos_infos -> clos_tab -> table_key -> bool array

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

Hook for Reduction