aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml28
-rw-r--r--kernel/cClosure.mli44
-rw-r--r--kernel/reduction.ml6
3 files changed, 28 insertions, 50 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 819a66c190..af50623429 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -310,20 +310,6 @@ let ref_value_cache ({i_cache = cache;_} as infos) tab ref =
| NotEvaluableConst _ (* Const *)
-> None
-let evar_value cache ev =
- cache.i_sigma ev
-
-let create ~repr ~share flgs env evars =
- let cache =
- { i_repr = repr;
- i_env = env;
- i_sigma = evars;
- i_rels = env.env_rel_context.env_rel_map;
- i_share = share;
- }
- in { i_flags = flgs; i_cache = cache }
-
-
(**********************************************************************)
(* Lazy reduction: the one used in kernel operations *)
@@ -944,7 +930,7 @@ let rec knr info tab m stk =
| FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
knit info tab (subs_cons([|v|],e)) bd stk
| FEvar(ev,env) ->
- (match evar_value info.i_cache ev with
+ (match info.i_cache.i_sigma ev with
Some c -> knit info tab env c stk
| None -> (m,stk))
| FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _
@@ -1054,17 +1040,23 @@ let whd_stack infos tab m stk = match m.norm with
(* cache of constants: the body is computed only when needed. *)
type clos_infos = fconstr infos
+type clos_tab = fconstr infos_tab
let create_clos_infos ?(evars=fun _ -> None) flgs env =
let share = (Environ.typing_flags env).Declarations.share_reduction in
- create ~share ~repr:(fun _ _ c -> inject c) flgs env evars
+ let cache = {
+ i_repr = (fun _ _ c -> inject c);
+ i_env = env;
+ i_sigma = evars;
+ i_rels = env.env_rel_context.env_rel_map;
+ i_share = share;
+ } in
+ { i_flags = flgs; i_cache = cache }
let create_tab () = KeyTable.create 17
let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
-let env_of_infos infos = infos.i_cache.i_env
-
let infos_with_reds infos reds =
{ infos with i_flags = reds }
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 2a018d172a..22c82f6d36 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -98,25 +98,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:
- repr:('a infos -> 'a infos_tab -> constr -> 'a) ->
- share:bool ->
- 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. *)
@@ -173,7 +155,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
@@ -193,27 +174,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
@@ -230,7 +216,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 unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr option
val eq_table_key : table_key -> table_key -> bool
@@ -243,9 +229,9 @@ 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 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
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 00576476ab..18697d07e5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -316,8 +316,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
type conv_tab = {
cnv_inf : clos_infos;
- lft_tab : fconstr infos_tab;
- rgt_tab : fconstr infos_tab;
+ lft_tab : clos_tab;
+ rgt_tab : clos_tab;
}
(** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory
location contained both in tl and in tr. *)
@@ -346,7 +346,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| (Sort s1, Sort s2) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
- sort_cmp_universes (env_of_infos infos.cnv_inf) cv_pb s1 s2 cuniv
+ sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
if Int.equal n m
then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:00:36 +0000