From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- kernel/pre_env.ml | 88 +++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 59 insertions(+), 29 deletions(-) (limited to 'kernel/pre_env.ml') diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index e1fe0259..7be8606e 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -15,17 +15,16 @@ open Util open Names -open Context -open Univ open Term open Declarations +open Context.Named.Declaration (* The type of environments. *) (* The key attached to each constant is used by the VM to retrieve previous *) (* evaluations of the constant. It is essentially an index in the symbols table *) (* used by the VM. *) -type key = int Ephemeron.key option ref +type key = int CEphemeron.key option ref (** Linking information for the native compiler. *) @@ -45,41 +44,45 @@ type globals = { env_modtypes : module_type_body MPmap.t} type stratification = { - env_universes : universes; + env_universes : UGraph.t; env_engagement : engagement } type val_kind = - | VKvalue of (values * Id.Set.t) Ephemeron.key + | VKvalue of (values * Id.Set.t) CEphemeron.key | VKnone type lazy_val = val_kind ref let force_lazy_val vk = match !vk with | VKnone -> None -| VKvalue v -> try Some (Ephemeron.get v) with Ephemeron.InvalidKey -> None +| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None let dummy_lazy_val () = ref VKnone -let build_lazy_val vk key = vk := VKvalue (Ephemeron.create key) +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 : named_context; - env_named_vals : named_vals; - env_rel_context : rel_context; + env_named_context : named_context_val; + env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; env_stratification : stratification; + env_typing_flags : typing_flags; env_conv_oracle : Conv_oracle.oracle; retroknowledge : Retroknowledge.retroknowledge; indirect_pterms : Opaqueproof.opaquetab; } -type named_context_val = named_context * 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,14 +90,14 @@ let empty_env = { env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; - env_named_context = empty_named_context; - env_named_vals = []; - env_rel_context = empty_rel_context; + env_named_context = empty_named_context_val; + env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0; env_stratification = { - env_universes = initial_universes; - env_engagement = (PredicativeSet,StratifiedType) }; + env_universes = UGraph.initial_universes; + env_engagement = PredicativeSet }; + env_typing_flags = Declareops.safe_flags; env_conv_oracle = Conv_oracle.empty; retroknowledge = Retroknowledge.initial_retroknowledge; indirect_pterms = Opaqueproof.empty_opaquetab } @@ -107,7 +110,7 @@ let nb_rel env = env.env_nb_rel let push_rel d env = let rval = ref VKnone in { env with - env_rel_context = add_rel_decl d env.env_rel_context; + env_rel_context = Context.Rel.add d env.env_rel_context; env_rel_val = rval :: env.env_rel_val; env_nb_rel = env.env_nb_rel + 1 } @@ -124,30 +127,57 @@ let env_of_rel n env = (* Named context *) -let push_named_context_val d (ctxt,vals) = - let id,_,_ = d in - let rval = ref VKnone in - add_named_decl d ctxt, (id,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 id,body,_ = d in - let rval = ref VKnone in { env_globals = env.env_globals; - env_named_context = Context.add_named_decl d env.env_named_context; - env_named_vals = (id, 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; env_stratification = env.env_stratification; + env_typing_flags = env.env_typing_flags; env_conv_oracle = env.env_conv_oracle; retroknowledge = env.retroknowledge; 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 -- cgit v1.2.3