aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml131
-rw-r--r--kernel/cClosure.mli46
-rw-r--r--kernel/reduction.ml6
3 files changed, 73 insertions, 110 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 819a66c190..c558689595 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -224,11 +224,6 @@ let unfold_red kn =
* abstractions, storing a representation (of type 'a) of the body of
* this constant or abstraction.
* * i_tab is the cache table of the results
- * * i_repr is the function to get the representation from the current
- * state of the cache and the body of the constant. The result
- * is stored in the table.
- * * i_rels is the array of free rel variables together with their optional
- * body
*
* ref_value_cache searchs in the tab, otherwise uses i_repr to
* compute the result and store it in the table. If the constant can't
@@ -256,74 +251,12 @@ end
module KeyTable = Hashtbl.Make(IdKeyHash)
-let eq_table_key = IdKeyHash.equal
-
-type 'a infos_tab = 'a KeyTable.t
-
-type 'a infos_cache = {
- i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
- i_env : env;
- i_sigma : existential -> constr option;
- i_rels : (Constr.rel_declaration * lazy_val) Range.t;
- i_share : bool;
-}
-
-and 'a infos = {
- i_flags : reds;
- i_cache : 'a infos_cache }
-
-let info_flags info = info.i_flags
-let info_env info = info.i_cache.i_env
-
open Context.Named.Declaration
let assoc_defined id env = match Environ.lookup_named id env with
| LocalDef (_, c, _) -> c
| _ -> raise Not_found
-let ref_value_cache ({i_cache = cache;_} as infos) tab ref =
- try
- Some (KeyTable.find tab ref)
- with Not_found ->
- try
- let body =
- match ref with
- | RelKey n ->
- let open! Context.Rel.Declaration in
- let i = n - 1 in
- let (d, _) =
- try Range.get cache.i_rels i
- with Invalid_argument _ -> raise Not_found
- in
- begin match d with
- | LocalAssum _ -> raise Not_found
- | LocalDef (_, t, _) -> lift n t
- end
- | VarKey id -> assoc_defined id cache.i_env
- | ConstKey cst -> constant_value_in cache.i_env cst
- in
- let v = cache.i_repr infos tab body in
- KeyTable.add tab ref v;
- Some v
- with
- | Not_found (* List.assoc *)
- | 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 *)
@@ -391,6 +324,23 @@ let update ~share v1 no t =
v1)
else {norm=no;term=t}
+(** Reduction cache *)
+
+type infos_cache = {
+ i_env : env;
+ i_sigma : existential -> constr option;
+ i_share : bool;
+}
+
+type clos_infos = {
+ i_flags : reds;
+ i_cache : infos_cache }
+
+type clos_tab = fconstr KeyTable.t
+
+let info_flags info = info.i_flags
+let info_env info = info.i_cache.i_env
+
(**********************************************************************)
(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
@@ -539,6 +489,8 @@ let mk_clos e t =
| (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
{norm = Red; term = FCLOS(t,e)}
+let inject c = mk_clos (subs_id 0) c
+
(** Hand-unrolling of the map function to bypass the call to the generic array
allocation *)
let mk_clos_vect env v = match v with
@@ -550,6 +502,35 @@ let mk_clos_vect env v = match v with
[|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|]
| v -> Array.Fun1.map mk_clos env v
+let ref_value_cache ({ i_cache = cache; _ }) tab ref =
+ try
+ Some (KeyTable.find tab ref)
+ with Not_found ->
+ try
+ let body =
+ match ref with
+ | RelKey n ->
+ let open! Context.Rel.Declaration in
+ let i = n - 1 in
+ let (d, _) =
+ try Range.get cache.i_env.env_rel_context.env_rel_map i
+ with Invalid_argument _ -> raise Not_found
+ in
+ begin match d with
+ | LocalAssum _ -> raise Not_found
+ | LocalDef (_, t, _) -> lift n t
+ end
+ | VarKey id -> assoc_defined id cache.i_env
+ | ConstKey cst -> constant_value_in cache.i_env cst
+ in
+ let v = inject body in
+ KeyTable.add tab ref v;
+ Some v
+ with
+ | Not_found (* List.assoc *)
+ | NotEvaluableConst _ (* Const *)
+ -> None
+
(* The inverse of mk_clos: move back to constr *)
let rec to_constr lfts v =
match v.term with
@@ -944,7 +925,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 _
@@ -1040,8 +1021,6 @@ let whd_val info tab v =
let norm_val info tab v =
with_stats (lazy (kl info tab v))
-let inject c = mk_clos (subs_id 0) c
-
let whd_stack infos tab m stk = match m.norm with
| Whnf | Norm ->
(** No need to perform [kni] nor to unlock updates because
@@ -1052,19 +1031,19 @@ let whd_stack infos tab m stk = match m.norm with
let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
k
-(* cache of constants: the body is computed only when needed. *)
-type clos_infos = fconstr infos
-
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_env = env;
+ i_sigma = evars;
+ 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..1ee4bccc25 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,9 +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 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 *)
@@ -243,9 +227,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 18:32:57 +0000