package coq-core

  1. Overview
  2. Docs
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.