1 files changed, 215 insertions, 161 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 89ba6f65..778c9a24 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -28,26 +28,208 @@ open Names
 open Constr
 open Vars
 open Declarations
-open Pre_env
 open Context.Rel.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 (* The type of environments. *)
 
-type named_context_val = Pre_env.named_context_val
+(* 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 CEphemeron.key option ref
+
+(** Linking information for the native compiler. *)
+
+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 : mind_key Mindmap_env.t;
+  env_modules : module_body MPmap.t;
+  env_modtypes : module_type_body MPmap.t;
+}
+
+type stratification = {
+  env_universes : UGraph.t;
+  env_engagement : engagement
+}
+
+type val_kind =
+    | VKvalue of (Vmvalues.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 (CEphemeron.get v) with CEphemeron.InvalidKey -> None
+
+let dummy_lazy_val () = ref VKnone
+let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
+
+type named_context_val = {
+  env_named_ctx : Constr.named_context;
+  env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
+}
+
+type rel_context_val = {
+  env_rel_ctx : Constr.rel_context;
+  env_rel_map : (Constr.rel_declaration * lazy_val) Range.t;
+}
+
+type env = {
+  env_globals       : globals;
+  env_named_context : named_context_val; (* section variables *)
+  env_rel_context   : rel_context_val;
+  env_nb_rel        : int;
+  env_stratification : stratification;
+  env_typing_flags  : typing_flags;
+  retroknowledge : Retroknowledge.retroknowledge;
+  indirect_pterms : Opaqueproof.opaquetab;
+}
+
+let empty_named_context_val = {
+  env_named_ctx = [];
+  env_named_map = Id.Map.empty;
+}
+
+let empty_rel_context_val = {
+  env_rel_ctx = [];
+  env_rel_map = Range.empty;
+}
+
+let empty_env = {
+  env_globals = {
+    env_constants = Cmap_env.empty;
+    env_inductives = Mindmap_env.empty;
+    env_modules = MPmap.empty;
+    env_modtypes = MPmap.empty};
+  env_named_context = empty_named_context_val;
+  env_rel_context = empty_rel_context_val;
+  env_nb_rel = 0;
+  env_stratification = {
+    env_universes = UGraph.initial_universes;
+    env_engagement = PredicativeSet };
+  env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
+  retroknowledge = Retroknowledge.initial_retroknowledge;
+  indirect_pterms = Opaqueproof.empty_opaquetab }
+
+
+(* Rel context *)
+
+let push_rel_context_val d ctx = {
+  env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx;
+  env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map;
+}
+
+let match_rel_context_val ctx = match ctx.env_rel_ctx with
+| [] -> None
+| decl :: rem ->
+  let (_, lval) = Range.hd ctx.env_rel_map in
+  let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in
+  Some (decl, lval, ctx)
+
+let push_rel d env =
+    { env with
+      env_rel_context = push_rel_context_val d env.env_rel_context;
+      env_nb_rel = env.env_nb_rel + 1 }
+
+let lookup_rel n env =
+  try fst (Range.get env.env_rel_context.env_rel_map (n - 1))
+  with Invalid_argument _ -> raise Not_found
+
+let lookup_rel_val n env =
+  try snd (Range.get env.env_rel_context.env_rel_map (n - 1))
+  with Invalid_argument _ -> raise Not_found
+
+let rel_skipn n ctx = {
+  env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx;
+  env_rel_map = Range.skipn n ctx.env_rel_map;
+}
+
+let env_of_rel n env =
+  { env with
+    env_rel_context = rel_skipn n env.env_rel_context;
+    env_nb_rel = env.env_nb_rel - n
+  }
+
+(* Named context *)
+
+let push_named_context_val_val d rval ctxt =
+(*   assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *)
+  {
+    env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
+    env_named_map = Id.Map.add (NamedDecl.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 (NamedDecl.get_id decl) c.env_named_map in
+  let map = Id.Map.remove (NamedDecl.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_left_map fold ctxt.env_named_map ctxt.env_named_ctx in
+  if map == ctxt.env_named_map then ctxt
+  else { env_named_ctx = ctx; env_named_map = map }
+
+let push_named d env =
+  {env with env_named_context = push_named_context_val d env.env_named_context}
 
-type env = Pre_env.env
+let lookup_named id env =
+  fst (Id.Map.find id env.env_named_context.env_named_map)
+
+let lookup_named_val id env =
+  snd(Id.Map.find id env.env_named_context.env_named_map)
+
+let lookup_named_ctxt id ctxt =
+  fst (Id.Map.find id ctxt.env_named_map)
+
+let fold_constants f env acc =
+  Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc
+
+(* Global constants *)
+
+let lookup_constant_key kn env =
+  Cmap_env.find kn env.env_globals.env_constants
+
+let lookup_constant kn env =
+  fst (Cmap_env.find kn env.env_globals.env_constants)
+
+(* Mutual Inductives *)
+let lookup_mind kn env =
+  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
 
-let pre_env env = env
-let env_of_pre_env env = env
 let oracle env = env.env_typing_flags.conv_oracle
 let set_oracle env o =
   let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in
   { env with env_typing_flags }
 
-let empty_named_context_val = empty_named_context_val
-
-let empty_env = empty_env
-
 let engagement env = env.env_stratification.env_engagement
 let typing_flags env = env.env_typing_flags
 
@@ -72,15 +254,11 @@ let empty_context env =
   | _ -> false
 
 (* Rel context *)
-let lookup_rel = lookup_rel
-
 let evaluable_rel n env =
   is_local_def (lookup_rel n env)
 
 let nb_rel env = env.env_nb_rel
 
-let push_rel = push_rel
-
 let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
@@ -105,24 +283,14 @@ let named_context_of_val c = c.env_named_ctx
 
 let ids_of_named_context_val c = Id.Map.domain c.env_named_map
 
-(* [map_named_val f ctxt] apply [f] to the body and the type of
-   each declarations.
-   *** /!\ ***   [f t] should be convertible with t *)
-let map_named_val = map_named_val
-
 let empty_named_context = Context.Named.empty
 
-let push_named = push_named
 let push_named_context = List.fold_right push_named
-let push_named_context_val = push_named_context_val
 
 let val_of_named_context ctxt =
   List.fold_right push_named_context_val ctxt empty_named_context_val
 
 
-let lookup_named = lookup_named
-let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map)
-
 let eq_named_context_val c1 c2 =
    c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2)
 
@@ -181,7 +349,10 @@ let map_universes f env =
   let s = env.env_stratification in
     { env with env_stratification =
 	 { s with env_universes = f s.env_universes } }
-				     
+
+let set_universes env u =
+  { env with env_stratification = { env.env_stratification with env_universes = u } }
+
 let add_constraints c env =
   if Univ.Constraint.is_empty c then env
   else map_universes (UGraph.merge_constraints c) env
@@ -221,8 +392,6 @@ let set_typing_flags c env = (* Unsafe *)
 
 (* Global constants *)
 
-let lookup_constant = lookup_constant
-
 let no_link_info = NotLinked
 
 let add_constant_key kn cb linkinfo env =
@@ -319,19 +488,26 @@ let polymorphic_pconstant (cst,u) env =
 let type_in_type_constant cst env =
   not (lookup_constant cst env).const_typing_flags.check_universes
 
-let lookup_projection cst env =
-  match (lookup_constant (Projection.constant cst) env).const_proj with 
-  | Some pb -> pb
-  | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.")
-
-let is_projection cst env =
-  match (lookup_constant cst env).const_proj with 
-  | Some _ -> true
-  | None -> false
+let lookup_projection p env =
+  let mind,i = Projection.inductive p in
+  let mib = lookup_mind mind env in
+  (if not (Int.equal mib.mind_nparams (Projection.npars p))
+   then anomaly ~label:"lookup_projection" Pp.(str "Bad number of parameters on projection."));
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> anomaly ~label:"lookup_projection" Pp.(str "not a projection")
+  | PrimRecord infos ->
+    let _,_,typs = infos.(i) in
+    typs.(Projection.arg p)
+
+let get_projection env ind ~proj_arg =
+  let mib = lookup_mind (fst ind) env in
+  Declareops.inductive_make_projection ind mib ~proj_arg
+
+let get_projections env ind =
+  let mib = lookup_mind (fst ind) env in
+  Declareops.inductive_make_projections ind mib
 
 (* Mutual Inductives *)
-let lookup_mind = lookup_mind
-
 let polymorphic_ind (mind,i) env =
   Declareops.inductive_is_polymorphic (lookup_mind mind env)
 
@@ -351,11 +527,11 @@ let template_polymorphic_pind (ind,u) env =
   if not (Univ.Instance.is_empty u) then false
   else template_polymorphic_ind ind env
   
-let add_mind_key kn mind_key env =
+let add_mind_key kn (mind, _ as mind_key) env =
   let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
   let new_globals =
     { env.env_globals with
-	env_inductives = new_inds } in
+        env_inductives = new_inds; } in
   { env with env_globals = new_globals }
 
 let add_mind kn mib env =
@@ -468,10 +644,6 @@ type 'types punsafe_type_judgment = {
 
 type unsafe_type_judgment = types punsafe_type_judgment
 
-(*s Compilation of global declaration *)
-
-let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false
-
 exception Hyp_not_found
 
 let apply_to_hyp ctxt id f =
@@ -530,121 +702,3 @@ let register env field entry =
 	in
         register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry
     | field -> register_one env field entry
-
-(* the Environ.register function syncrhonizes the proactive and reactive
-   retroknowledge. *)
-let dispatch =
-
-  (* subfunction used for static decompilation of int31 (after a vm_compute,
-     see pretyping/vnorm.ml for more information) *)
-  let constr_of_int31 =
-    let nth_digit_plus_one i n = (* calculates the nth (starting with 0)
-                                    digit of i and adds 1 to it
-                                    (nth_digit_plus_one 1 3 = 2) *)
-      if Int.equal (i land (1 lsl n)) 0 then
-        1
-      else
-        2
-    in
-      fun ind -> fun digit_ind -> fun tag ->
-	let array_of_int i =
-	  Array.init 31 (fun n -> mkConstruct
-			   (digit_ind, nth_digit_plus_one i (30-n)))
-	in
-	(* We check that no bit above 31 is set to one. This assertion used to
-	fail in the VM, and led to conversion tests failing at Qed. *)
-        assert (Int.equal (tag lsr 31) 0);
-	mkApp(mkConstruct(ind, 1), array_of_int tag)
-  in
-
-  (* subfunction which dispatches the compiling information of an
-     int31 operation which has a specific vm instruction (associates
-     it to the name of the coq definition in the reactive retroknowledge) *)
-  let int31_op n op prim kn =
-    { empty_reactive_info with
-      vm_compiling = Some (Clambda.compile_prim n op kn);
-      native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
-    }
-  in
-
-fun rk value field ->
-  (* subfunction which shortens the (very common) dispatch of operations *)
-  let int31_op_from_const n op prim =
-    match kind value with
-      | Const kn ->  int31_op n op prim kn
-      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.")
-  in
-  let int31_binop_from_const op prim = int31_op_from_const 2 op prim in
-  let int31_unop_from_const op prim = int31_op_from_const 1 op prim in
-  match field with
-    | KInt31 (grp, Int31Type) ->
-        let int31bit =
-          (* invariant : the type of bits is registered, otherwise the function
-             would raise Not_found. The invariant is enforced in safe_typing.ml *)
-          match field with
-          | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits))
-          | _ -> anomaly ~label:"Environ.register"
-              (Pp.str "add_int31_decompilation_from_type called with an abnormal field.")
-        in
-        let i31bit_type =
-          match kind int31bit with
-          | Ind (i31bit_type,_) -> i31bit_type
-          |  _ -> anomaly ~label:"Environ.register"
-              (Pp.str "Int31Bits should be an inductive type.")
-        in
-        let int31_decompilation =
-          match kind value with
-          | Ind (i31t,_) ->
-              constr_of_int31 i31t i31bit_type
-          | _ -> anomaly ~label:"Environ.register"
-              (Pp.str "should be an inductive type.")
-        in
-        { empty_reactive_info with
-          vm_decompile_const = Some int31_decompilation;
-          vm_before_match = Some Clambda.int31_escape_before_match;
-          native_before_match = Some (Nativelambda.before_match_int31 i31bit_type);
-        }
-    | KInt31 (_, Int31Constructor) ->
-        { empty_reactive_info with
-          vm_constant_static = Some Clambda.compile_structured_int31;
-          vm_constant_dynamic = Some Clambda.dynamic_int31_compilation;
-          native_constant_static = Some Nativelambda.compile_static_int31;
-          native_constant_dynamic = Some Nativelambda.compile_dynamic_int31;
-        }
-    | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31
-							  CPrimitives.Int31add
-    | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31
-							   CPrimitives.Int31addc
-    | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31
-								CPrimitives.Int31addcarryc
-    | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31
-							   CPrimitives.Int31sub
-    | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31
-							    CPrimitives.Int31subc
-    | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const
-	                                Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc
-    | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31
-							   CPrimitives.Int31mul
-    | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31
-							   CPrimitives.Int31mulc
-    | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31
-                                                           CPrimitives.Int31div21
-    | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31
-							 CPrimitives.Int31diveucl
-    | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31
-                                                         CPrimitives.Int31addmuldiv
-    | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31
-							     CPrimitives.Int31compare
-    | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31
-							  CPrimitives.Int31head0
-    | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31
-							  CPrimitives.Int31tail0
-    | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31
-							 CPrimitives.Int31lor
-    | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31
-							  CPrimitives.Int31land
-    | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31
-							  CPrimitives.Int31lxor
-    | _ -> empty_reactive_info
-
-let _ = Hook.set Retroknowledge.dispatch_hook dispatch