package coq

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

Module CClosureSource

Sourceval stats : bool ref

Flags for profiling reductions.

Sourceval with_stats : 'a Lazy.t -> 'a
...

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

Sourcemodule RedFlags : sig ... end

Sets of reduction kinds.

Sourceval allnolet : RedFlags.reds
Sourceval betadeltazeta : RedFlags.reds
Sourceval betaiota : RedFlags.reds
Sourceval betaiotazeta : RedFlags.reds
Sourceval betazeta : RedFlags.reds
Sourcemodule KeyTable : Hashtbl.S with type key = table_key

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 'a next_native_args = (CPrimitives.arg_kind * 'a) list
Sourcetype 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 Esubst.subs
  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
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 eta_expand_stack : Names.Name.t Context.binder_annot -> stack -> stack
Sourceval skip_irrelevant_stack : stack -> stack

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
Sourceval create_conv_infos : ?univs:UGraph.t -> ?evars:(Constr.existential -> Constr.constr option) -> RedFlags.reds -> Environ.env -> clos_infos
Sourceval create_clos_infos : ?univs:UGraph.t -> ?evars:(Constr.existential -> Constr.constr option) -> 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 -> 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 infos_with_reds : clos_infos -> RedFlags.reds -> clos_infos

Reduction function

norm_val is for strong normalization

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

unfold_reference unfolds references in a fconstr. Produces a FIrrelevant when the reference is irrelevant.

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_vect : fconstr Esubst.subs -> 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