From 27c93465dcf0d5233c1195d1649f5e699ed54a90 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 21 Aug 2016 20:55:23 +0200 Subject: Packing the named_context_val in a proper record and marking it private. --- kernel/environ.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'kernel/environ.mli') diff --git a/kernel/environ.mli b/kernel/environ.mli index b5e576435..cb4a94d45 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -273,10 +273,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 -- cgit v1.2.3 From 1888527bb43d6a8c801565af3e6376c91769fbc1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 9 Sep 2016 11:51:51 +0200 Subject: Removing the now useless field env_named_val from named_context_val. This field was only used by the VM before, but since the previous patches, this part of the code relies on the map instead. --- kernel/environ.ml | 1 - kernel/environ.mli | 1 - kernel/pre_env.ml | 17 ++++++----------- kernel/pre_env.mli | 3 --- 4 files changed, 6 insertions(+), 16 deletions(-) (limited to 'kernel/environ.mli') diff --git a/kernel/environ.ml b/kernel/environ.ml index f4a3312ef..96e35610c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -100,7 +100,6 @@ let fold_rel_context f env ~init = (* Named context *) let named_context_of_val c = c.env_named_ctx -let named_vals_of_val c = c.env_named_val (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. diff --git a/kernel/environ.mli b/kernel/environ.mli index cb4a94d45..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 diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index defc0afc8..104fe59d1 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -61,11 +61,8 @@ 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_val : named_vals; env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; } @@ -84,7 +81,6 @@ type env = { let empty_named_context_val = { env_named_ctx = []; - env_named_val = []; env_named_map = Id.Map.empty; } @@ -135,20 +131,19 @@ 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_val = (get_id d, rval) :: ctxt.env_named_val; 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, c.env_named_val with -| [], [] -> None -| decl :: ctx, (_, v) :: vls -> +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_val = vls; env_named_map = map } in + let cval = { env_named_ctx = ctx; env_named_map = map } in Some (decl, v, cval) -| _ -> assert false let map_named_val f ctxt = let open Context.Named.Declaration in @@ -161,7 +156,7 @@ let map_named_val f ctxt = (accu, d') in let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in - { ctxt with env_named_ctx = ctx; env_named_map = map } + { 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); diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 4390177da..1e4eff3d5 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -40,11 +40,8 @@ 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_val : named_vals; env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; } -- cgit v1.2.3