From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 kernel/csymtable.ml | 47 +++++++++++++++++------------------------------
 1 file changed, 17 insertions(+), 30 deletions(-)

(limited to 'kernel/csymtable.ml')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index fc7e1b93..c27cb048 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -15,7 +15,6 @@
 open Util
 open Names
 open Term
-open Context
 open Vm
 open Cemitcodes
 open Cbytecodes
@@ -131,8 +130,8 @@ let key rk =
   match !rk with
   | None -> raise NotEvaluated
   | Some k ->
-      try Ephemeron.get k
-      with Ephemeron.InvalidKey -> raise NotEvaluated
+      try CEphemeron.get k
+      with CEphemeron.InvalidKey -> raise NotEvaluated
 
 (************************)
 (* traduction des patch *)
@@ -171,7 +170,7 @@ let rec slot_for_getglobal env kn =
 	 | BCconstant -> set_global (val_of_constant kn)
     in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
-    rk := Some (Ephemeron.create pos);
+    rk := Some (CEphemeron.create pos);
     pos
 
 and slot_for_fv env fv =
@@ -190,51 +189,39 @@ and slot_for_fv env fv =
       let nv = Pre_env.lookup_named_val id env in
       begin match force_lazy_val nv with
       | None ->
-          let _, b, _ = Context.lookup_named id env.env_named_context in
-          fill_fv_cache nv id val_of_named idfun b
+         let open Context.Named in
+         let open Declaration in
+	 env |> Pre_env.lookup_named id |> get_value |> fill_fv_cache nv id val_of_named idfun
       | Some (v, _) -> v
       end
   | FVrel i ->
       let rv = Pre_env.lookup_rel_val i env in
       begin match force_lazy_val rv with
       | None ->
-          let _, b, _ = lookup_rel i env.env_rel_context in
-          fill_fv_cache rv i val_of_rel env_of_rel b
+         let open Context.Rel in
+         let open Declaration in
+	 env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel
       | Some (v, _) -> v
       end
   | FVuniv_var idu ->
     assert false
 
 and eval_to_patch env (buff,pl,fv) =
-  (* copy code *before* patching because of nested evaluations:
-     the code we are patching might be called (and thus "concurrently" patched)
-     and results in wrong results. Side-effects... *)
-  let buff = Cemitcodes.copy buff in
   let patch = function
-    | Reloc_annot a, pos -> patch_int buff pos (slot_for_annot a)
-    | Reloc_const sc, pos -> patch_int buff pos (slot_for_str_cst sc)
-    | Reloc_getglobal kn, pos ->
-(*      Pp.msgnl (str"patching global: "++str(debug_string_of_con kn));*)
-	patch_int buff pos (slot_for_getglobal env kn);
-(*      Pp.msgnl (str"patch done: "++str(debug_string_of_con kn))*)
+    | Reloc_annot a, pos -> (pos, slot_for_annot a)
+    | Reloc_const sc, pos -> (pos, slot_for_str_cst sc)
+    | Reloc_getglobal kn, pos -> (pos, slot_for_getglobal env kn)
   in
-  List.iter patch pl;
+  let patches = List.map_left patch pl in
+  let buff = patch_int buff patches in
   let vm_env = Array.map (slot_for_fv env) fv in
   let tc = tcode_of_code buff (length buff) in
   eval_tcode tc vm_env
 
 and val_of_constr env c =
-  let (_,fun_code,_ as ccfv) =
-    try match compile true env c with
-	| Some v -> v
-	| None -> assert false
-    with reraise ->
-      let reraise = Errors.push reraise in
-      let () = print_string "can not compile \n" in
-      let () = Format.print_flush () in
-      iraise reraise
-  in
-  eval_to_patch env (to_memory ccfv)
+  match compile true env c with
+  | Some v -> eval_to_patch env (to_memory v)
+  | None -> assert false
 
 let set_transparent_const kn = () (* !?! *)
 let set_opaque_const kn = () (* !?! *)
-- 
cgit v1.2.3