diff options
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 68 |
1 files changed, 22 insertions, 46 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 3a7f77d521..c2d53eed47 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -15,7 +15,6 @@ open Esubst (** Flags for profiling reductions. *) val stats : bool ref -val share : bool ref val with_stats: 'a Lazy.t -> 'a @@ -25,14 +24,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 *) - - -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.t -> bool - (** Sets of reduction kinds. *) module type RedFlagsSig = sig type reds @@ -61,10 +52,10 @@ module type RedFlagsSig = sig val red_sub : reds -> red_kind -> reds (** Adds a reduction kind to a set *) - val red_add_transparent : reds -> transparent_state -> reds + val red_add_transparent : reds -> TransparentState.t -> reds (** Retrieve the transparent state of the reduction flags *) - val red_transparent : reds -> transparent_state + val red_transparent : reds -> TransparentState.t (** Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds @@ -74,7 +65,7 @@ module type RedFlagsSig = sig (** This tests if the projection is in unfolded state already or is unfodable due to delta. *) - val red_projection : reds -> projection -> bool + val red_projection : reds -> Projection.t -> bool end module RedFlags : RedFlagsSig @@ -99,20 +90,7 @@ val unfold_red : evaluable_global_reference -> reds (***********************************************************************) type table_key = Constant.t Univ.puniverses tableKey -type 'a infos_cache -type 'a infos_tab -type 'a infos = { - i_flags : reds; - i_cache : 'a infos_cache } - -val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option -val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env -> - (existential -> constr option) -> 'a infos -val create_tab : unit -> 'a infos_tab -val evar_value : 'a infos_cache -> existential -> constr option - -val info_env : 'a infos -> env -val info_flags: 'a infos -> reds +module KeyTable : Hashtbl.S with type key = table_key (*********************************************************************** s Lazy reduction. *) @@ -127,17 +105,16 @@ type fconstr type fterm = | FRel of int | FAtom of constr (** Metas and Sorts *) - | FCast of fconstr * cast_kind * fconstr | FFlex of table_key | FInd of inductive Univ.puniverses | FConstruct of constructor Univ.puniverses | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | 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 + | FProd of Name.t * fconstr * constr * fconstr subs | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FLIFT of int * fconstr @@ -152,7 +129,7 @@ type fterm = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * Constant.t + | Zproj of Projection.Repr.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -170,7 +147,6 @@ val stack_tail : int -> stack -> stack val stack_nth : stack -> int -> fconstr val zip_term : (fconstr -> constr) -> constr -> stack -> constr val eta_expand_stack : stack -> stack -val unfold_projection : 'a infos -> Projection.t -> stack_member option (** To lazy reduce a constr, create a [clos_infos] with [create_clos_infos], inject the term to reduce with [inject]; then use @@ -190,27 +166,32 @@ val destFLambda : (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr (** Global and local constant cache *) -type clos_infos = fconstr infos +type clos_infos +type clos_tab 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 : 'a infos -> env +val create_tab : unit -> clos_tab + +val info_env : clos_infos -> env +val info_flags: clos_infos -> reds +val unfold_projection : clos_infos -> Projection.t -> stack_member option val infos_with_reds : clos_infos -> reds -> clos_infos (** Reduction function *) (** [norm_val] is for strong normalization *) -val norm_val : clos_infos -> fconstr infos_tab -> fconstr -> constr +val norm_val : clos_infos -> clos_tab -> fconstr -> constr (** [whd_val] is for weak head normalization *) -val whd_val : clos_infos -> fconstr infos_tab -> fconstr -> constr +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 -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack + clos_infos -> clos_tab -> 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 @@ -227,9 +208,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** Conversion auxiliary functions to do step by step normalisation *) (** [unfold_reference] unfolds references in a [fconstr] *) -val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option - -val eq_table_key : table_key -> table_key -> bool +val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr option (*********************************************************************** i This is for lazy debug *) @@ -239,14 +218,11 @@ val lift_fconstr_vect : int -> fconstr array -> fconstr array val mk_clos : fconstr subs -> constr -> fconstr val mk_clos_vect : fconstr subs -> constr array -> fconstr array -val mk_clos_deep : - (fconstr subs -> constr -> fconstr) -> - fconstr subs -> constr -> fconstr -val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack -val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack -val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr +val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack +val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack +val kl : clos_infos -> clos_tab -> fconstr -> constr -val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr +val to_constr : lift -> fconstr -> constr (** End of cbn debug section i*) |