Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 146 insertions, 0 deletions

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
new file mode 100644
index 00000000..5a45c167
--- /dev/null
+++ b/kernel/pre_env.ml
@@ -0,0 +1,146 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: pre_env.ml 7642 2005-12-06 08:56:29Z gregoire $ *)
+
+open Util
+open Names
+open Sign
+open Univ
+open Term
+open Declarations
+
+(* The type of environments. *)
+
+
+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_modules : module_body MPmap.t;
+  env_modtypes : module_type_body KNmap.t }
+
+type stratification = {
+  env_universes : universes;
+  env_engagement : engagement option
+}
+
+type 'a val_kind =   
+  | VKvalue of values
+  | VKaxiom of 'a
+  | VKdef of constr
+
+type 'a lazy_val = 'a 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 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_nb_rel        : int;
+  env_stratification : stratification }
+
+type named_context_val = named_context * named_vals
+
+let empty_named_context_val = [],[]
+
+let empty_env = { 
+  env_globals = {
+    env_constants = Cmap.empty;
+    env_inductives = KNmap.empty;
+    env_modules = MPmap.empty;
+    env_modtypes = KNmap.empty };
+  env_named_context = empty_named_context;
+  env_named_vals = [];
+  env_rel_context = empty_rel_context;
+  env_rel_val = [];
+  env_nb_rel = 0;
+  env_stratification = {
+    env_universes = initial_universes;
+    env_engagement = None } }
+
+
+(* 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 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) =
+  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
+
+exception ASSERT of Sign.rel_context
+
+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 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
+
+let lookup_constant kn env =
+  fst (Cmap.find kn env.env_globals.env_constants)
+
+(* Mutual Inductives *)
+let lookup_mind kn env =
+  KNmap.find kn env.env_globals.env_inductives