package coq-core

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

Lazy reduction.

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 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 Constr.binder_annot * Constr.constr) list * Constr.constr * usubs
  13. | FProd of Names.Name.t Constr.binder_annot * fconstr * Constr.constr * usubs
  14. | FLetIn of Names.Name.t Constr.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. | FString of Pstring.t
  19. | FArray of UVars.Instance.t * fconstr Parray.t * fconstr
  20. | FLIFT of int * fconstr
  21. | FCLOS of Constr.constr * usubs
  22. | FIrrelevant
  23. | 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 =
  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
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_invert : finvert -> fconstr array
val stack_args_size : stack -> int
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 mk_atom : Constr.constr -> fconstr

mk_atom: prevents a term from being evaluated

val mk_red : fterm -> fconstr

mk_red: makes a reducible term (used in ring)

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

Global and local constant cache

type clos_tab
type 'a evar_expansion =
  1. | EvarDefined of 'a
  2. | EvarUndefined of Evar.t * 'a list
type evar_handler = {
  1. evar_expand : Constr.constr Constr.pexistential -> Constr.constr evar_expansion;
  2. evar_repack : (Evar.t * Constr.constr list) -> Constr.constr;
  3. evar_irrelevant : Constr.constr Constr.pexistential -> bool;
  4. qvar_irrelevant : Sorts.QVar.t -> bool;
}
val default_evar_handler : Environ.env -> evar_handler
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 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

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

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 set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit

Hook for Reduction

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