From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 kernel/csymtable.ml | 88 +++++++++++------------------------------------------
 1 file changed, 18 insertions(+), 70 deletions(-)

(limited to 'kernel/csymtable.ml')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index c27cb048..01294895 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Created by Bruno Barras for Benjamin Grégoire as part of the
@@ -14,16 +16,16 @@
 
 open Util
 open Names
-open Term
-open Vm
+open Vmvalues
 open Cemitcodes
 open Cbytecodes
 open Declarations
 open Pre_env
 open Cbytegen
 
+module NamedDecl = Context.Named.Declaration
+module RelDecl = Context.Rel.Declaration
 
-external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
 external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
 
 (*******************)
@@ -54,61 +56,12 @@ let set_global v =
 
 (* table pour les structured_constant et les annotations des switchs *)
 
-let rec eq_structured_constant c1 c2 = match c1, c2 with
-| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
-| Const_sorts _, _ -> false
-| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
-| Const_ind _, _ -> false
-| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
-| Const_proj _, _ -> false
-| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
-| Const_b0 _, _ -> false
-| Const_bn (t1, a1), Const_bn (t2, a2) ->
-  Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
-| Const_bn _, _ -> false
-| Const_univ_level l1 , Const_univ_level l2 -> Univ.eq_levels l1 l2
-| Const_univ_level _ , _ -> false
-| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
-| Const_type _ , _ -> false
-
-let rec hash_structured_constant c =
-  let open Hashset.Combine in
-  match c with
-  | Const_sorts s -> combinesmall 1 (Sorts.hash s)
-  | Const_ind i -> combinesmall 2 (ind_hash i)
-  | Const_proj p -> combinesmall 3 (Constant.hash p)
-  | Const_b0 t -> combinesmall 4 (Int.hash t)
-  | Const_bn (t, a) ->
-    let fold h c = combine h (hash_structured_constant c) in
-    let h = Array.fold_left fold 0 a in
-    combinesmall 5 (combine (Int.hash t) h)
-  | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
-  | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
-
 module SConstTable = Hashtbl.Make (struct
   type t = structured_constant
   let equal = eq_structured_constant
   let hash = hash_structured_constant
 end)
 
-let eq_annot_switch asw1 asw2 =
-  let eq_ci ci1 ci2 =
-    eq_ind ci1.ci_ind ci2.ci_ind &&
-    Int.equal ci1.ci_npar ci2.ci_npar &&
-    Array.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
-  in
-  let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
-  eq_ci asw1.ci asw2.ci &&
-  Array.equal eq_rlc asw1.rtbl asw2.rtbl &&
-  (asw1.tailcall : bool) == asw2.tailcall
-
-let hash_annot_switch asw =
-  let open Hashset.Combine in
-  let h1 = Constr.case_info_hash asw.ci in
-  let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
-  let h3 = if asw.tailcall then 1 else 0 in
-  combine3 h1 h2 h3
-
 module AnnotTable = Hashtbl.Make (struct
   type t = annot_switch
   let equal = eq_annot_switch
@@ -189,37 +142,32 @@ 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 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
+	 env |> Pre_env.lookup_named id |> NamedDecl.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 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
+        env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel
       | Some (v, _) -> v
       end
+  | FVevar evk -> val_of_evar evk
   | FVuniv_var idu ->
     assert false
 
 and eval_to_patch env (buff,pl,fv) =
-  let patch = function
-    | 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)
+  let slots = function
+    | Reloc_annot a -> slot_for_annot a
+    | Reloc_const sc -> slot_for_str_cst sc
+    | Reloc_getglobal kn -> slot_for_getglobal env kn
   in
-  let patches = List.map_left patch pl in
-  let buff = patch_int buff patches in
+  let tc = patch buff pl slots 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 =
-  match compile true env c with
+  match compile ~fail_on_error:true env c with
   | Some v -> eval_to_patch env (to_memory v)
   | None -> assert false
 
-- 
cgit v1.2.3