package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module CClosureSource

Lazy reduction.

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 evar_repack
Sourcetype fterm =
  1. | FRel of int
  2. | FAtom of Constr.constr
    (*

    Metas and Sorts

    *)
  3. | FFlex of table_key
  4. | FInd of Constr.pinductive
  5. | FConstruct of Constr.pconstructor
  6. | FApp of fconstr * fconstr array
  7. | FProj of Names.Projection.t * Sorts.relevance * fconstr
  8. | FFix of Constr.fixpoint * usubs
  9. | FCoFix of Constr.cofixpoint * usubs
  10. | FCaseT of Constr.case_info * UVars.Instance.t * Constr.constr array * Constr.case_return * fconstr * Constr.case_branch array * usubs
  11. | FCaseInvert of Constr.case_info * UVars.Instance.t * Constr.constr array * Constr.case_return * finvert * fconstr * Constr.case_branch array * usubs
  12. | FLambda of int * (Names.Name.t Context.binder_annot * Constr.constr) list * Constr.constr * usubs
  13. | FProd of Names.Name.t Context.binder_annot * fconstr * Constr.constr * usubs
  14. | FLetIn of Names.Name.t Context.binder_annot * fconstr * fconstr * Constr.constr * usubs
  15. | FEvar of Evar.t * Constr.constr list * usubs * evar_repack
  16. | FInt of Uint63.t
  17. | FFloat of Float64.t
  18. | FArray of UVars.Instance.t * fconstr Parray.t * fconstr
  19. | FLIFT of int * fconstr
  20. | FCLOS of Constr.constr * usubs
  21. | FIrrelevant
  22. | FLOCKED

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

Sourcetype 'a next_native_args = (CPrimitives.arg_kind * 'a) list
Sourcetype stack_member =
  1. | Zapp of fconstr array
  2. | ZcaseT of Constr.case_info * UVars.Instance.t * Constr.constr array * Constr.case_return * Constr.case_branch array * usubs
  3. | Zproj of Names.Projection.Repr.t * Sorts.relevance
  4. | Zfix of fconstr * stack
  5. | Zprimitive of CPrimitives.t * Constr.pconstant * fconstr list * fconstr next_native_args
  6. | Zshift of int
  7. | 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
Sourceval stack_args_size : stack -> int
Sourceval usubs_lift : usubs -> usubs
Sourceval usubs_liftn : int -> usubs -> usubs
Sourceval usubs_cons : fconstr -> usubs -> usubs

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 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
Sourcetype clos_infos

Global and local constant cache

Sourcetype clos_tab
Sourcetype 'a evar_expansion =
  1. | EvarDefined of 'a
  2. | EvarUndefined of Evar.t * 'a list
Sourcetype 'constr evar_handler = {
  1. evar_expand : 'constr Constr.pexistential -> 'constr evar_expansion;
  2. evar_repack : (Evar.t * 'constr list) -> 'constr;
  3. evar_irrelevant : 'constr Constr.pexistential -> bool;
  4. qvar_irrelevant : Sorts.QVar.t -> bool;
}
Sourceval default_evar_handler : Environ.env -> 'constr evar_handler
Sourceval create_conv_infos : ?univs:UGraph.t -> ?evars:Constr.constr evar_handler -> RedFlags.reds -> Environ.env -> clos_infos
Sourceval create_clos_infos : ?univs:UGraph.t -> ?evars: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 -> Sorts.relevance -> 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 is_irrelevant : clos_infos -> Sorts.relevance -> bool
Sourceval infos_with_reds : clos_infos -> RedFlags.reds -> clos_infos

Reduction function

norm_val is for strong normalization

Same as norm_val but for terms

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
Sourceval eta_expand_ind_stack : Environ.env -> Constr.pinductive -> 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

Sourceval 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 : usubs -> Constr.constr -> fconstr
Sourceval mk_clos_vect : usubs -> Constr.constr array -> fconstr array
Sourceval zip : fconstr -> stack -> fconstr
Sourceval term_of_process : fconstr -> stack -> Constr.constr

End of cbn debug section i

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct