aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-10-03 15:26:17 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-10-03 15:26:17 +0200
commit6cc37a67e4be8e20cd3da46077ab8f3458e22394 (patch)
tree7baf96eaccf037a94d7e525ccaec898955b465bd /kernel
parent4a2e0798cf24c9edf4e96bd6ad62bdbde7a7cdf7 (diff)
parentd55818c7da468ce1c7c9644cb63f68f7561a17bc (diff)
Merge remote-tracking branch 'github/pr/263' into v8.6
Was PR#263: Fast lookup in named contexts
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml10
-rw-r--r--kernel/csymtable.ml2
-rw-r--r--kernel/environ.ml102
-rw-r--r--kernel/environ.mli5
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--kernel/pre_env.ml60
-rw-r--r--kernel/pre_env.mli18
7 files changed, 104 insertions, 95 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index d475f097c..fe9ec5794 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -270,11 +270,9 @@ let info_env info = info.i_cache.i_env
open Context.Named.Declaration
-let rec assoc_defined id = function
-| [] -> raise Not_found
-| LocalAssum _ :: ctxt -> assoc_defined id ctxt
-| LocalDef (id', c, _) :: ctxt ->
- if Id.equal id id' then c else assoc_defined id ctxt
+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) ref =
try
@@ -291,7 +289,7 @@ let ref_value_cache ({i_cache = cache} as infos) ref =
| None -> raise Not_found
| Some t -> lift n t
end
- | VarKey id -> assoc_defined id (named_context cache.i_env)
+ | VarKey id -> assoc_defined id cache.i_env
| ConstKey cst -> constant_value_in cache.i_env cst
in
let v = cache.i_repr infos body in
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index e195618b6..6f1ace25a 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -191,7 +191,7 @@ and slot_for_fv env fv =
| None ->
let open Context.Named in
let open Declaration in
- env.env_named_context |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun
+ env.env_named_context.env_named_ctx |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun
| Some (v, _) -> v
end
| FVrel i ->
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7351a87d4..54898320d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -56,14 +56,14 @@ let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
let universes env = env.env_stratification.env_universes
-let named_context env = env.env_named_context
-let named_context_val env = env.env_named_context,env.env_named_vals
+let named_context env = env.env_named_context.env_named_ctx
+let named_context_val env = env.env_named_context
let rel_context env = env.env_rel_context
let opaque_tables env = env.indirect_pterms
let set_opaque_tables env indirect_pterms = { env with indirect_pterms }
let empty_context env =
- match env.env_rel_context, env.env_named_context with
+ match env.env_rel_context, env.env_named_context.env_named_ctx with
| [], [] -> true
| _ -> false
@@ -99,14 +99,12 @@ let fold_rel_context f env ~init =
(* Named context *)
-let named_context_of_val = fst
-let named_vals_of_val = snd
+let named_context_of_val c = c.env_named_ctx
(* [map_named_val f ctxt] apply [f] to the body and the type of
each declarations.
*** /!\ *** [f t] should be convertible with t *)
-let map_named_val f =
- on_fst (Context.Named.map f)
+let map_named_val = map_named_val
let empty_named_context = Context.Named.empty
@@ -118,8 +116,8 @@ let val_of_named_context ctxt =
List.fold_right push_named_context_val ctxt empty_named_context_val
-let lookup_named id env = Context.Named.lookup id env.env_named_context
-let lookup_named_val id (ctxt,_) = Context.Named.lookup id ctxt
+let lookup_named = lookup_named
+let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map)
let eq_named_context_val c1 c2 =
c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2)
@@ -139,10 +137,9 @@ let evaluable_named id env =
| Some _ -> true
| _ -> false
-let reset_with_named_context (ctxt,ctxtv) env =
+let reset_with_named_context ctxt env =
{ env with
env_named_context = ctxt;
- env_named_vals = ctxtv;
env_rel_context = Context.Rel.empty;
env_rel_val = [];
env_nb_rel = 0 }
@@ -157,11 +154,11 @@ let pop_rel_context n env =
let fold_named_context f env ~init =
let rec fold_right env =
- match env.env_named_context with
- | [] -> init
- | d::ctxt ->
+ match match_named_context_val env.env_named_context with
+ | None -> init
+ | Some (d, v, rem) ->
let env =
- reset_with_named_context (ctxt,List.tl env.env_named_vals) env in
+ reset_with_named_context rem env in
f env d (fold_right env)
in fold_right env
@@ -493,66 +490,47 @@ let compile_constant_body = Cbytegen.compile_constant_body false
exception Hyp_not_found
-let apply_to_hyp (ctxt,vals) id f =
- let rec aux rtail ctxt vals =
- match ctxt, vals with
- | d::ctxt, v::vals ->
+let apply_to_hyp ctxt id f =
+ let rec aux rtail ctxt =
+ match match_named_context_val ctxt with
+ | Some (d, v, ctxt) ->
if Id.equal (get_id d) id then
- (f ctxt d rtail)::ctxt, v::vals
+ push_named_context_val_val (f ctxt.env_named_ctx d rtail) v ctxt
else
- let ctxt',vals' = aux (d::rtail) ctxt vals in
- d::ctxt', v::vals'
- | [],[] -> raise Hyp_not_found
- | _, _ -> assert false
- in aux [] ctxt vals
-
-let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
- let rec aux ctxt vals =
- match ctxt,vals with
- | d::ctxt, v::vals ->
+ let ctxt' = aux (d::rtail) ctxt in
+ push_named_context_val_val d v ctxt'
+ | None -> raise Hyp_not_found
+ in aux [] ctxt
+
+let apply_to_hyp_and_dependent_on ctxt id f g =
+ let rec aux sign =
+ match match_named_context_val sign with
+ | Some (d, v, sign) ->
if Id.equal (get_id d) id then
- let sign = ctxt,vals in
push_named_context_val (f d sign) sign
else
- let (ctxt,vals as sign) = aux ctxt vals in
+ let sign = aux sign in
push_named_context_val (g d sign) sign
- | [],[] -> raise Hyp_not_found
- | _,_ -> assert false
- in aux ctxt vals
-
-let insert_after_hyp (ctxt,vals) id d check =
- let rec aux ctxt vals =
- match ctxt, vals with
- | decl::ctxt', v::vals' ->
- if Id.equal (get_id decl) id then begin
- check ctxt;
- push_named_context_val d (ctxt,vals)
- end else
- let ctxt,vals = aux ctxt vals in
- d::ctxt, v::vals
- | [],[] -> raise Hyp_not_found
- | _, _ -> assert false
- in aux ctxt vals
-
+ | None -> raise Hyp_not_found
+ in aux ctxt
(* To be used in Logic.clear_hyps *)
-let remove_hyps ids check_context check_value (ctxt, vals) =
- let rec remove_hyps ctxt vals = match ctxt, vals with
- | [], [] -> ([], []), false
- | d :: rctxt, (nid, v) :: rvals ->
- let (ans, seen) = remove_hyps rctxt rvals in
+let remove_hyps ids check_context check_value ctxt =
+ let rec remove_hyps ctxt = match match_named_context_val ctxt with
+ | None -> empty_named_context_val, false
+ | Some (d, v, rctxt) ->
+ let (ans, seen) = remove_hyps rctxt in
if Id.Set.mem (get_id d) ids then (ans, true)
- else if not seen then (ctxt, vals), false
+ else if not seen then ctxt, false
else
- let (rctxt', rvals') = ans in
+ let rctxt' = ans in
let d' = check_context d in
let v' = check_value v in
- if d == d' && v == v' && rctxt == rctxt' && rvals == rvals' then
- (ctxt, vals), true
- else (d' :: rctxt', (nid, v') :: rvals'), true
- | _ -> assert false
+ if d == d' && v == v' && rctxt == rctxt' then
+ ctxt, true
+ else push_named_context_val_val d' v' rctxt', true
in
- fst (remove_hyps ctxt vals)
+ fst (remove_hyps ctxt)
(*spiwack: the following functions assemble the pieces of the retroknowledge
note that the "consistent" register function is available in the module
diff --git a/kernel/environ.mli b/kernel/environ.mli
index b5e576435..235ba2fd1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -78,7 +78,6 @@ val fold_rel_context :
(** {5 Context of variables (section variables and goal assumptions) } *)
val named_context_of_val : named_context_val -> Context.Named.t
-val named_vals_of_val : named_context_val -> Pre_env.named_vals
val val_of_named_context : Context.Named.t -> named_context_val
val empty_named_context_val : named_context_val
@@ -273,10 +272,6 @@ val apply_to_hyp_and_dependent_on : named_context_val -> variable ->
(Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) ->
named_context_val
-val insert_after_hyp : named_context_val -> variable ->
- Context.Named.Declaration.t ->
- (Context.Named.t -> unit) -> named_context_val
-
val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ad5b04f3d..eaddace4b 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1861,7 +1861,7 @@ and compile_rel env sigma univ auxdefs n =
and compile_named env sigma univ auxdefs id =
let open Context.Named.Declaration in
- match Context.Named.lookup id env.env_named_context with
+ match lookup_named id env with
| LocalDef (_,t,_) ->
let code = lambda_of_constr env sigma t in
let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 5afefeebd..7be8606ef 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -61,12 +61,14 @@ let force_lazy_val vk = match !vk with
let dummy_lazy_val () = ref VKnone
let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
-type named_vals = (Id.t * lazy_val) list
+type named_context_val = {
+ env_named_ctx : Context.Named.t;
+ env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
+}
type env = {
env_globals : globals;
- env_named_context : Context.Named.t;
- env_named_vals : named_vals;
+ env_named_context : named_context_val;
env_rel_context : Context.Rel.t;
env_rel_val : lazy_val list;
env_nb_rel : int;
@@ -77,9 +79,10 @@ type env = {
indirect_pterms : Opaqueproof.opaquetab;
}
-type named_context_val = Context.Named.t * named_vals
-
-let empty_named_context_val = [],[]
+let empty_named_context_val = {
+ env_named_ctx = [];
+ env_named_map = Id.Map.empty;
+}
let empty_env = {
env_globals = {
@@ -87,8 +90,7 @@ let empty_env = {
env_inductives = Mindmap_env.empty;
env_modules = MPmap.empty;
env_modtypes = MPmap.empty};
- env_named_context = Context.Named.empty;
- env_named_vals = [];
+ env_named_context = empty_named_context_val;
env_rel_context = Context.Rel.empty;
env_rel_val = [];
env_nb_rel = 0;
@@ -125,17 +127,42 @@ let env_of_rel n env =
(* Named context *)
-let push_named_context_val d (ctxt,vals) =
- let rval = ref VKnone in
- Context.Named.add d ctxt, (get_id d,rval)::vals
+let push_named_context_val_val d rval ctxt =
+(* assert (not (Id.Map.mem (get_id d) ctxt.env_named_map)); *)
+ {
+ env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
+ env_named_map = Id.Map.add (get_id d) (d, rval) ctxt.env_named_map;
+ }
+
+let push_named_context_val d ctxt =
+ push_named_context_val_val d (ref VKnone) ctxt
+
+let match_named_context_val c = match c.env_named_ctx with
+| [] -> None
+| decl :: ctx ->
+ let (_, v) = Id.Map.find (get_id decl) c.env_named_map in
+ let map = Id.Map.remove (get_id decl) c.env_named_map in
+ let cval = { env_named_ctx = ctx; env_named_map = map } in
+ Some (decl, v, cval)
+
+let map_named_val f ctxt =
+ let open Context.Named.Declaration in
+ let fold accu d =
+ let d' = map_constr f d in
+ let accu =
+ if d == d' then accu
+ else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu
+ in
+ (accu, d')
+ in
+ let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in
+ { env_named_ctx = ctx; env_named_map = map }
let push_named d env =
(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
assert (env.env_rel_context = []); *)
- let rval = ref VKnone in
{ env_globals = env.env_globals;
- env_named_context = Context.Named.add d env.env_named_context;
- env_named_vals = (get_id d, rval) :: env.env_named_vals;
+ env_named_context = push_named_context_val d env.env_named_context;
env_rel_context = env.env_rel_context;
env_rel_val = env.env_rel_val;
env_nb_rel = env.env_nb_rel;
@@ -146,8 +173,11 @@ let push_named d env =
indirect_pterms = env.indirect_pterms;
}
+let lookup_named id env =
+ fst (Id.Map.find id env.env_named_context.env_named_map)
+
let lookup_named_val id env =
- snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals)
+ snd(Id.Map.find id env.env_named_context.env_named_map)
(* Warning all the names should be different *)
let env_of_named id env = env
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index e551d22c8..866790367 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -40,12 +40,14 @@ val force_lazy_val : lazy_val -> (values * Id.Set.t) option
val dummy_lazy_val : unit -> lazy_val
val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit
-type named_vals = (Id.t * lazy_val) list
+type named_context_val = private {
+ env_named_ctx : Context.Named.t;
+ env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
+}
type env = {
env_globals : globals;
- env_named_context : Context.Named.t;
- env_named_vals : named_vals;
+ env_named_context : named_context_val;
env_rel_context : Context.Rel.t;
env_rel_val : lazy_val list;
env_nb_rel : int;
@@ -56,8 +58,6 @@ type env = {
indirect_pterms : Opaqueproof.opaquetab;
}
-type named_context_val = Context.Named.t * named_vals
-
val empty_named_context_val : named_context_val
val empty_env : env
@@ -73,7 +73,15 @@ val env_of_rel : int -> env -> env
val push_named_context_val :
Context.Named.Declaration.t -> named_context_val -> named_context_val
+val push_named_context_val_val :
+ Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val
+val match_named_context_val :
+ named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option
+val map_named_val :
+ (constr -> constr) -> named_context_val -> named_context_val
+
val push_named : Context.Named.Declaration.t -> env -> env
+val lookup_named : Id.t -> env -> Context.Named.Declaration.t
val lookup_named_val : Id.t -> env -> lazy_val
val env_of_named : Id.t -> env -> env