diff options
Diffstat (limited to 'checker/closure.mli')
| -rw-r--r-- | checker/closure.mli | 48 |
1 files changed, 20 insertions, 28 deletions
diff --git a/checker/closure.mli b/checker/closure.mli index 8b1f246c..49b07f73 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (*i*) @@ -24,14 +26,6 @@ val with_stats: 'a Lazy.t -> 'a Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *) -type transparent_state = Id.Pred.t * Cpred.t - -val all_opaque : transparent_state -val all_transparent : transparent_state - -val is_transparent_variable : transparent_state -> variable -> bool -val is_transparent_constant : transparent_state -> constant -> bool - (* Sets of reduction kinds. *) module type RedFlagsSig = sig type reds @@ -42,8 +36,6 @@ module type RedFlagsSig = sig val fDELTA : red_kind val fIOTA : red_kind val fZETA : red_kind - val fCONST : constant -> red_kind - val fVAR : Id.t -> red_kind (* No reduction at all *) val no_red : reds @@ -66,12 +58,8 @@ val betaiotazeta : reds val betadeltaiotanolet : reds (***********************************************************************) -type 'a tableKey = - | ConstKey of 'a - | VarKey of Id.t - | RelKey of int -type table_key = constant puniverses tableKey +type table_key = Constant.t puniverses tableKey type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option @@ -95,14 +83,13 @@ type fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * 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 * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | 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_key * fconstr array | FLIFT of int * fconstr | FCLOS of constr * fconstr subs @@ -115,9 +102,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 * projection + | Zproj of int * int * Projection.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -125,11 +111,16 @@ type stack_member = and stack = stack_member list val append_stack : fconstr array -> stack -> stack + +val stack_args_size : stack -> int + val eta_expand_stack : stack -> stack val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (fconstr * stack) -> stack * stack +val unfold_projection : env -> Projection.t -> stack_member + (* 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 *) @@ -139,13 +130,15 @@ val inject : 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 val create_clos_infos : reds -> env -> clos_infos val infos_env : clos_infos -> env val infos_flags : clos_infos -> reds +val oracle_of_infos : clos_infos -> oracle + (* Reduction function *) @@ -165,7 +158,6 @@ val unfold_reference : clos_infos -> table_key -> fconstr option (* [mind_equiv] checks whether two inductive types are intentionally equal *) val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool -val eq_table_key : table_key -> table_key -> bool (************************************************************************) (*i This is for lazy debug *) |