Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Namesopen Constropen Environopen Esubstopen RedFlags
(** 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 subs_contenttype usubs = subs_content subs UVars.puniverses
type table_key = Constant.t UVars.puniverses tableKey
(** Relevances (eg in binder_annot or case_info) have NOT been substituted when there is a usubs field *)type fterm = | FRel of int | FAtom of constr (** Metas and Sorts *) | FFlex of table_key | FInd of pinductive | FConstruct of pconstructor * fconstr array | FApp of fconstr * fconstr array | FProj of Projection.t * Sorts.relevance * fconstr | FFix of fixpoint * usubs | FCoFix of cofixpoint * usubs | FCaseT of case_info * UVars.Instance.t * constr array * case_return * fconstr * case_branch array * usubs (* predicate and branches are closures *) | FCaseInvert of case_info * UVars.Instance.t * constr array * case_return * finvert * fconstr * case_branch array * usubs | FLambda of int * (Name.t binder_annot * constr) list * constr * usubs | FProd of Name.t binder_annot * fconstr * constr * usubs | FLetIn of Name.t binder_annot * fconstr * fconstr * constr * usubs | FEvar of Evar.t * constr list * usubs * evar_repack | FInt of Uint63.t | FFloat of Float64.t | FString of Pstring.t | FArray of UVars.Instance.t * fconstr Parray.t * fconstr | FLIFT of int * fconstr | FCLOS of constr * usubs | FIrrelevant | FLOCKED
(*********************************************************************** s A [stack] is a context of arguments, arguments are pushed by [append_stack] one array at a time *)type 'a next_native_args = (CPrimitives.arg_kind * 'a) list
type stack_member = | Zapp of fconstr array | ZcaseT of case_info * UVars.Instance.t * constr array * case_return * case_branch array * usubs | Zproj of Projection.Repr.t * Sorts.relevance | Zfix of fconstr * stack | Zprimitive of CPrimitives.t * pconstant * fconstr list * fconstr next_native_args (* operator, constr def, arguments already seen (in rev order), next arguments *) | Zshift of int | Zupdate of fconstr
and stack = stack_member list
val empty_stack : stackval append_stack : fconstr array -> stack -> stack
val check_native_args : CPrimitives.t -> stack -> boolval get_native_args1 : CPrimitives.t -> pconstant -> stack -> fconstr list * fconstr * fconstr next_native_args * stack
val get_invert : finvert -> fconstr array
val stack_args_size : stack -> int
val inductive_subst : Declarations.mutual_inductive_body -> UVars.Instance.t -> fconstr array -> usubs
val usubs_lift : usubs -> usubsval usubs_liftn : int -> usubs -> usubsval usubs_cons : fconstr -> usubs -> usubs
(** identity if the first instance is empty *)val usubst_instance : 'a UVars.puniverses -> UVars.Instance.t -> UVars.Instance.t
val usubst_binder : _ UVars.puniverses -> 'a binder_annot -> 'a 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 -> fconstr
val mk_clos : usubs -> constr -> fconstrval mk_clos_vect : usubs -> constr array -> fconstr array
val zip : fconstr -> stack -> fconstr
val fterm_of : fconstr -> ftermval term_of_fconstr : fconstr -> constrval term_of_process : fconstr -> stack -> constrval destFLambda : (usubs -> constr -> fconstr) -> fconstr -> Name.t binder_annot * fconstr * fconstr
(** Global and local constant cache *)type clos_infostype clos_tab
type 'a evar_expansion =| EvarDefined of 'a| EvarUndefined of Evar.t * 'a list
type evar_handler = { evar_expand : constr pexistential -> constr evar_expansion; evar_repack : Evar.t * constr list -> constr; evar_irrelevant : constr pexistential -> bool; qvar_irrelevant : Sorts.QVar.t -> bool; qual_equal : Sorts.Quality.t -> Sorts.Quality.t -> bool; abstr_const : Constant.t -> (unit, (unit -> Vmemitcodes.to_patch) Vmemitcodes.pbody_code) Declarations.pconstant_body;}
val default_evar_handler : env -> evar_handlerval lookup_constant_handler : env -> evar_handler -> Constant.t -> (unit, (unit -> Vmemitcodes.to_patch) Vmemitcodes.pbody_code) Declarations.pconstant_body
val create_conv_infos : ?univs:UGraph.t -> ?evars:evar_handler -> reds -> env -> clos_infosval create_clos_infos : ?univs:UGraph.t -> ?evars:evar_handler -> reds -> env -> clos_infosval oracle_of_infos : clos_infos -> Conv_oracle.oracle
val create_tab : unit -> clos_tab
val info_env : clos_infos -> envval info_flags: clos_infos -> redsval info_univs : clos_infos -> UGraph.tval unfold_projection : clos_infos -> Projection.t -> Sorts.relevance -> stack_member option
val push_relevance : clos_infos -> 'b binder_annot -> clos_infosval push_relevances : clos_infos -> 'b binder_annot array -> clos_infosval 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 -> boolval eq_quality : clos_infos -> Sorts.Quality.t -> Sorts.Quality.t -> bool
val infos_with_reds : clos_infos -> reds -> clos_infos
(** Reduction function *)
(** [norm_val] is for strong normalization *)val norm_val : clos_infos -> clos_tab -> fconstr -> constr
(** Same as [norm_val] but for terms *)val norm_term : clos_infos -> clos_tab -> usubs -> Constr.constr -> Constr.constr
(** [whd_val] is for weak head normalization *)val whd_val : clos_infos -> clos_tab -> fconstr -> constr
(** [whd_stack] performs weak head normalization in a given stack. It stops whenever a reduction is blocked. *)val whd_stack : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val skip_irrelevant_stack : clos_infos -> stack -> stack
val eta_expand_stack : clos_infos -> Name.t binder_annot -> stack -> stack
(** [eta_expand_ind_stack env ind args t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the constructor of this inductive type applied to arguments args. @assumes [t] is a rigid term, and not a constructor; that [args] are valid arguments for the constructor of inductive [ind]. @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *)val eta_expand_ind_stack : env -> pinductive -> fconstr array -> (fconstr * stack) -> stack * stack
val esubst_of_context : constr option list -> usubs -> usubs -> int * usubs
(** Conversion auxiliary functions to do step by step normalisation *)
(** 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 unfold_ref_with_args : clos_infos -> clos_tab -> table_key -> stack -> (fconstr * stack) option
val get_ref_mask : clos_infos -> clos_tab -> table_key -> bool array
(** Hook for Reduction *)val set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit