diff options
Diffstat (limited to 'kernel/pre_env.ml')
| -rw-r--r-- | kernel/pre_env.ml | 75 |
1 files changed, 31 insertions, 44 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 947e4675..dd4d430a 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 8810 2006-05-12 18:50:21Z barras $ *) +(* $Id: pre_env.ml 10664 2008-03-14 11:27:37Z soubiran $ *) open Util open Names @@ -26,34 +26,31 @@ type globals = { env_constants : constant_key Cmap.t; env_inductives : mutual_inductive_body KNmap.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body KNmap.t } + env_modtypes : module_type_body MPmap.t; + env_alias : module_path MPmap.t } type stratification = { env_universes : universes; env_engagement : engagement option } -type 'a val_kind = - | VKvalue of values - | VKaxiom of 'a - | VKdef of constr +type val_kind = + | VKvalue of values * Idset.t + | VKnone -type 'a lazy_val = 'a val_kind ref +type lazy_val = val_kind ref -type rel_val = inv_rel_key lazy_val - -type named_val = identifier lazy_val - -type named_vals = (identifier * named_val) list +type named_vals = (identifier * lazy_val) list type env = { env_globals : globals; env_named_context : named_context; env_named_vals : named_vals; env_rel_context : rel_context; - env_rel_val : rel_val list; + env_rel_val : lazy_val list; env_nb_rel : int; - env_stratification : stratification } + env_stratification : stratification; + retroknowledge : Retroknowledge.retroknowledge } type named_context_val = named_context * named_vals @@ -64,7 +61,8 @@ let empty_env = { env_constants = Cmap.empty; env_inductives = KNmap.empty; env_modules = MPmap.empty; - env_modtypes = KNmap.empty }; + env_modtypes = MPmap.empty; + env_alias = MPmap.empty }; env_named_context = empty_named_context; env_named_vals = []; env_rel_context = empty_rel_context; @@ -72,24 +70,20 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = initial_universes; - env_engagement = None } } + env_engagement = None }; + retroknowledge = Retroknowledge.initial_retroknowledge } (* Rel context *) let nb_rel env = env.env_nb_rel - + let push_rel d env = - let _,body,_ = d in - let rval = - match body with - | None -> ref (VKaxiom env.env_nb_rel) - | Some c -> ref (VKdef c) - 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 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) @@ -101,16 +95,13 @@ let env_of_rel n env = 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) = - let id,body,_ = d in - let rval = - match body with - | None -> ref (VKaxiom id) - | Some c -> ref (VKdef c) - in Sign.add_named_decl d ctxt, (id,rval)::vals + let id,_,_ = d in + let rval = ref VKnone in + Sign.add_named_decl d ctxt, (id,rval)::vals exception ASSERT of Sign.rel_context @@ -118,18 +109,14 @@ 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 = - match body with - | None -> ref (VKaxiom id) - | Some c -> ref (VKdef c) - in - { env with - env_named_context = Sign.add_named_decl d env.env_named_context; - env_named_vals = (id,rval):: env.env_named_vals } + 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 } let lookup_named_val id env = - snd(List.find (fun (id',_) -> id = id') env.env_named_vals) - + 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 |