diff options
Diffstat (limited to 'checker/closure.mli')
| -rw-r--r-- | checker/closure.mli | 33 |
1 files changed, 21 insertions, 12 deletions
diff --git a/checker/closure.mli b/checker/closure.mli index e072a106..e6b39250 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -1,15 +1,14 @@ (************************************************************************) (* 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 *) (************************************************************************) (*i*) -open Pp open Names -open Term +open Cic open Esubst open Environ (*i*) @@ -25,7 +24,7 @@ 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 = Idpred.t * Cpred.t +type transparent_state = Id.Pred.t * Cpred.t val all_opaque : transparent_state val all_transparent : transparent_state @@ -44,7 +43,7 @@ module type RedFlagsSig = sig 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 @@ -67,11 +66,13 @@ val betaiotazeta : reds val betadeltaiotanolet : reds (***********************************************************************) -type table_key = - | ConstKey of constant - | VarKey of identifier +type 'a tableKey = + | ConstKey of 'a + | VarKey of Id.t | RelKey of int +type table_key = constant puniverses tableKey + type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos @@ -91,12 +92,14 @@ 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 pinductive + | FConstruct of pconstructor | FApp of fconstr * fconstr array + | FProj of constant * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCases of case_info * fconstr * fconstr * fconstr array + | 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 @@ -113,6 +116,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 @@ -121,6 +126,9 @@ and stack = stack_member list val append_stack : fconstr array -> stack -> stack val eta_expand_stack : stack -> stack + +val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> + (fconstr * 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 @@ -136,6 +144,8 @@ val destFLambda : (* 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 (* Reduction function *) @@ -172,6 +182,5 @@ val kni: clos_infos -> fconstr -> stack -> fconstr * stack val knr: clos_infos -> fconstr -> stack -> fconstr * stack val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr -val optimise_closure : fconstr subs -> constr -> fconstr subs * constr (* End of cbn debug section i*) |