package coq-core

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

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

module RedFlags : sig ... end

Sets of reduction kinds.

val all : RedFlags.reds
val allnolet : RedFlags.reds
val beta : RedFlags.reds
val betadeltazeta : RedFlags.reds
val betaiota : RedFlags.reds
val betaiotazeta : RedFlags.reds
val betazeta : RedFlags.reds
val delta : RedFlags.reds
val zeta : RedFlags.reds
val nored : RedFlags.reds
module KeyTable : Hashtbl.S with type key = table_key

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 'a usubs = 'a Esubst.subs Univ.puniverses
type evar_repack
type 'a next_native_args = (CPrimitives.arg_kind * 'a) list
type stack_member =
  1. | Zapp of fconstr array
  2. | ZcaseT of Constr.case_info * Univ.Instance.t * Constr.constr array * Constr.case_return * Constr.case_branch array * fconstr usubs
  3. | Zproj of Names.Projection.Repr.t
  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 stack_args_size : stack -> int
val usubs_lift : 'a usubs -> 'a usubs
val usubs_liftn : int -> 'a usubs -> 'a usubs
val usubs_cons : 'a -> 'a usubs -> 'a usubs
val 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

val inject : Constr.constr -> fconstr
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 fterm_of : fconstr -> fterm
val term_of_fconstr : fconstr -> Constr.constr
type clos_infos

Global and local constant cache

type clos_tab
val create_conv_infos : ?univs:UGraph.t -> ?evars:Constr.constr Constr.evar_handler -> RedFlags.reds -> Environ.env -> clos_infos
val create_clos_infos : ?univs:UGraph.t -> ?evars:Constr.constr Constr.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 -> stack_member option
val push_relevance : clos_infos -> 'b Context.binder_annot -> clos_infos
val push_relevances : clos_infos -> 'b Context.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 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 Context.binder_annot -> stack -> stack
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

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

val lift_fconstr : int -> fconstr -> fconstr
val lift_fconstr_vect : int -> fconstr array -> fconstr array
val mk_clos : fconstr usubs -> Constr.constr -> fconstr
val mk_clos_vect : fconstr usubs -> Constr.constr array -> fconstr array
val kni : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val knr : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val zip : fconstr -> stack -> fconstr
val 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