diff options
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 67 |
1 files changed, 49 insertions, 18 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 0818d42f..a3b0e0f3 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open Environ @@ -37,13 +36,16 @@ module type RedFlagsSig = sig type reds type red_kind - (** The different kinds of reduction *) + (** {7 The different kinds of reduction } *) + val fBETA : red_kind val fDELTA : red_kind + val fETA : red_kind + (** This flag is never used by the kernel reduction but pretyping does *) val fIOTA : red_kind val fZETA : red_kind val fCONST : constant -> red_kind - val fVAR : identifier -> red_kind + val fVAR : Id.t -> red_kind (** No reduction at all *) val no_red : reds @@ -62,7 +64,10 @@ module type RedFlagsSig = sig (** Tests if a reduction kind is set *) val red_set : reds -> red_kind -> bool - + + (** This tests if the projection is in unfolded state already or + is unfodable due to delta. *) + val red_projection : reds -> projection -> bool end module RedFlags : RedFlagsSig @@ -78,14 +83,20 @@ val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds (***********************************************************************) -type table_key = id_key +type table_key = constant puniverses tableKey + +type 'a infos_cache +type 'a infos = { + i_flags : reds; + i_cache : 'a infos_cache } -type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option -val info_flags: 'a infos -> reds val create: ('a infos -> constr -> 'a) -> reds -> env -> (existential -> constr option) -> 'a infos -val evar_value : 'a infos -> existential -> constr option +val evar_value : 'a infos_cache -> existential -> constr option + +val info_env : 'a infos -> env +val info_flags: 'a infos -> reds (*********************************************************************** s Lazy reduction. *) @@ -102,15 +113,17 @@ type fterm = | FAtom of constr (** Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive - | FConstruct of constructor + | FInd of inductive puniverses + | FConstruct of constructor puniverses | FApp of fconstr * fconstr array + | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCases of case_info * fconstr * fconstr * fconstr array - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FCase of case_info * fconstr * fconstr * fconstr array + | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) + | FLambda of int * (Name.t * constr) list * constr * fconstr subs + | FProd of Name.t * fconstr * fconstr + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FLIFT of int * fconstr | FCLOS of constr * fconstr subs @@ -124,6 +137,8 @@ type fterm = type stack_member = | Zapp of fconstr array | Zcase of case_info * fconstr * fconstr array + | ZcaseT of case_info * constr * constr array * fconstr subs + | Zproj of int * int * constant | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -154,12 +169,17 @@ val mk_atom : constr -> fconstr val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : - (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr + (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr (** Global and local constant cache *) -type clos_infos +type clos_infos = fconstr infos val create_clos_infos : ?evars:(existential->constr option) -> reds -> env -> clos_infos +val oracle_of_infos : clos_infos -> Conv_oracle.oracle + +val env_of_infos : clos_infos -> env + +val infos_with_reds : clos_infos -> reds -> clos_infos (** Reduction function *) @@ -174,6 +194,18 @@ val whd_val : clos_infos -> fconstr -> constr val whd_stack : clos_infos -> fconstr -> stack -> fconstr * stack +(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding + 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. + *) +val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> + (fconstr * stack) -> stack * stack + (** Conversion auxiliary functions to do step by step normalisation *) (** [unfold_reference] unfolds references in a [fconstr] *) @@ -198,6 +230,5 @@ val knr: clos_infos -> fconstr -> stack -> fconstr * stack val kl : clos_infos -> fconstr -> constr val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr -val optimise_closure : fconstr subs -> constr -> fconstr subs * constr (** End of cbn debug section i*) |