diff options
Diffstat (limited to 'kernel/pre_env.ml')
| -rw-r--r-- | kernel/pre_env.ml | 52 |
1 files changed, 23 insertions, 29 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index dd4d430a..b58951e9 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pre_env.ml 10664 2008-03-14 11:27:37Z soubiran $ *) +(* $Id$ *) open Util open Names @@ -18,23 +18,22 @@ open Declarations (* The type of environments. *) -type key = int option ref +type key = int option ref type constant_key = constant_body * key - + type globals = { - env_constants : constant_key Cmap.t; - env_inductives : mutual_inductive_body KNmap.t; + env_constants : constant_key Cmap_env.t; + env_inductives : mutual_inductive_body Mindmap_env.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t; - env_alias : module_path MPmap.t } + env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : universes; env_engagement : engagement option } -type val_kind = +type val_kind = | VKvalue of values * Idset.t | VKnone @@ -56,13 +55,12 @@ type named_context_val = named_context * named_vals let empty_named_context_val = [],[] -let empty_env = { +let empty_env = { env_globals = { - env_constants = Cmap.empty; - env_inductives = KNmap.empty; + env_constants = Cmap_env.empty; + env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; - env_modtypes = MPmap.empty; - env_alias = MPmap.empty }; + env_modtypes = MPmap.empty}; env_named_context = empty_named_context; env_named_vals = []; env_rel_context = empty_rel_context; @@ -77,25 +75,25 @@ let empty_env = { (* Rel context *) 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_val = rval :: env.env_rel_val; env_nb_rel = env.env_nb_rel + 1 } - + let lookup_rel_val n env = try List.nth env.env_rel_val (n - 1) with _ -> 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_nb_rel = env.env_nb_rel - n } - + (* Named context *) let push_named_context_val d (ctxt,vals) = @@ -103,36 +101,32 @@ let push_named_context_val d (ctxt,vals) = let rval = ref VKnone in Sign.add_named_decl d ctxt, (id,rval)::vals -exception ASSERT of Sign.rel_context +exception ASSERT of rel_context -let push_named d env = +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 with env_named_context = Sign.add_named_decl d env.env_named_context; env_named_vals = (id,rval):: env.env_named_vals } let lookup_named_val id env = snd(List.find (fun (id',_) -> id = id') env.env_named_vals) - + (* Warning all the names should be different *) let env_of_named id env = env - + (* Global constants *) let lookup_constant_key kn env = - Cmap.find kn env.env_globals.env_constants + Cmap_env.find kn env.env_globals.env_constants let lookup_constant kn env = - fst (Cmap.find kn env.env_globals.env_constants) + fst (Cmap_env.find kn env.env_globals.env_constants) (* Mutual Inductives *) let lookup_mind kn env = - KNmap.find kn env.env_globals.env_inductives + Mindmap_env.find kn env.env_globals.env_inductives -let rec scrape_mind env kn = - match (lookup_mind kn env).mind_equiv with - | None -> kn - | Some kn' -> scrape_mind env kn' |