diff options
Diffstat (limited to 'kernel/pre_env.ml')
| -rw-r--r-- | kernel/pre_env.ml | 77 |
1 files changed, 55 insertions, 22 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 6ef1039e..557ed3d7 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,36 +15,55 @@ open Util open Names -open Sign +open Context open Univ open Term open Declarations (* 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 option ref +(** Linking information for the native compiler. *) -type constant_key = constant_body * key +type link_info = + | Linked of string + | LinkedInteractive of string + | NotLinked + +type constant_key = constant_body * (link_info ref * key) + +type mind_key = mutual_inductive_body * link_info ref type globals = { env_constants : constant_key Cmap_env.t; - env_inductives : mutual_inductive_body Mindmap_env.t; + env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : universes; - env_engagement : engagement option + env_engagement : engagement option; + env_type_in_type : bool } type val_kind = - | VKvalue of values * Idset.t + | VKvalue of (values * Id.Set.t) Ephemeron.key | VKnone type lazy_val = val_kind ref -type named_vals = (identifier * lazy_val) list +let force_lazy_val vk = match !vk with +| VKnone -> None +| VKvalue v -> try Some (Ephemeron.get v) with Ephemeron.InvalidKey -> None + +let dummy_lazy_val () = ref VKnone +let build_lazy_val vk key = vk := VKvalue (Ephemeron.create key) + +type named_vals = (Id.t * lazy_val) list type env = { env_globals : globals; @@ -54,7 +73,10 @@ type env = { env_rel_val : lazy_val list; env_nb_rel : int; env_stratification : stratification; - retroknowledge : Retroknowledge.retroknowledge } + env_conv_oracle : Conv_oracle.oracle; + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} type named_context_val = named_context * named_vals @@ -73,8 +95,11 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = initial_universes; - env_engagement = None }; - retroknowledge = Retroknowledge.initial_retroknowledge } + env_engagement = None; + env_type_in_type = false}; + env_conv_oracle = Conv_oracle.empty; + retroknowledge = Retroknowledge.initial_retroknowledge; + indirect_pterms = Opaqueproof.empty_opaquetab } (* Rel context *) @@ -90,12 +115,12 @@ let push_rel d env = let lookup_rel_val n env = try List.nth env.env_rel_val (n - 1) - with e when Errors.noncritical e -> raise Not_found + with Failure _ -> raise Not_found let env_of_rel n env = { env with - env_rel_context = Util.list_skipn n env.env_rel_context; - env_rel_val = Util.list_skipn n env.env_rel_val; + env_rel_context = Util.List.skipn n env.env_rel_context; + env_rel_val = Util.List.skipn n env.env_rel_val; env_nb_rel = env.env_nb_rel - n } @@ -104,21 +129,27 @@ let env_of_rel n env = let push_named_context_val d (ctxt,vals) = let id,_,_ = d in let rval = ref VKnone in - Sign.add_named_decl d ctxt, (id,rval)::vals - -exception ASSERT of rel_context + add_named_decl d ctxt, (id,rval)::vals 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 with - env_named_context = Sign.add_named_decl d env.env_named_context; - env_named_vals = (id,rval):: env.env_named_vals } + { 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_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_conv_oracle = env.env_conv_oracle; + retroknowledge = env.retroknowledge; + indirect_pterms = env.indirect_pterms; + } let lookup_named_val id env = - snd(List.find (fun (id',_) -> id = id') env.env_named_vals) + snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals) (* Warning all the names should be different *) let env_of_named id env = env @@ -133,5 +164,7 @@ let lookup_constant kn env = (* Mutual Inductives *) let lookup_mind kn env = - Mindmap_env.find kn env.env_globals.env_inductives + fst (Mindmap_env.find kn env.env_globals.env_inductives) +let lookup_mind_key kn env = + Mindmap_env.find kn env.env_globals.env_inductives |