Rename VM-related kernel/cfoo files to kernel/vmfoo

1 files changed, 226 insertions, 0 deletions

diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
new file mode 100644
index 0000000000..85f7369654
--- /dev/null
+++ b/kernel/vmsymtable.ml
@@ -0,0 +1,226 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    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
+   bytecode-based reduction machine, Oct 2004 *)
+(* Bug fix #1419 by Jean-Marc Notin, Mar 2007 *)
+
+(* This file manages the table of global symbols for the bytecode machine *)
+
+open Util
+open Names
+open Vmvalues
+open Vmemitcodes
+open Vmbytecodes
+open Declarations
+open Environ
+open Vmbytegen
+
+module NamedDecl = Context.Named.Declaration
+module RelDecl = Context.Rel.Declaration
+
+external eval_tcode : tcode -> atom array -> vm_global -> values array -> values = "coq_eval_tcode"
+
+type global_data = { mutable glob_len : int; mutable glob_val : values array }
+
+(*******************)
+(* Linkage du code *)
+(*******************)
+
+(* Table des globaux *)
+
+(* [global_data] contient les valeurs des constantes globales
+   (axiomes,definitions), les annotations des switch et les structured
+   constant *)
+let global_data = {
+  glob_len = 0;
+  glob_val = Array.make 4096 crazy_val;
+}
+
+let get_global_data () = Vmvalues.vm_global global_data.glob_val
+
+let realloc_global_data n =
+  let n = min (2 * n + 0x100) Sys.max_array_length in
+  let ans = Array.make n crazy_val in
+  let src = global_data.glob_val in
+  let () = Array.blit src 0 ans 0 (Array.length src) in
+  global_data.glob_val <- ans
+
+let check_global_data n =
+  if n >= Array.length global_data.glob_val then realloc_global_data n
+
+let set_global v =
+  let n = global_data.glob_len in
+  check_global_data n;
+  global_data.glob_val.(n) <- v;
+  global_data.glob_len <- global_data.glob_len + 1;
+  n
+
+(* Initialization of OCaml primitives *)
+let parray_make = set_global Vmvalues.parray_make
+let parray_get = set_global Vmvalues.parray_get
+let parray_get_default = set_global Vmvalues.parray_get_default
+let parray_set = set_global Vmvalues.parray_set
+let parray_copy = set_global Vmvalues.parray_copy
+let parray_reroot = set_global Vmvalues.parray_reroot
+let parray_length = set_global Vmvalues.parray_length
+
+(* table pour les structured_constant et les annotations des switchs *)
+
+module SConstTable = Hashtbl.Make (struct
+  type t = structured_constant
+  let equal = eq_structured_constant
+  let hash = hash_structured_constant
+end)
+
+module AnnotTable = Hashtbl.Make (struct
+  type t = annot_switch
+  let equal = eq_annot_switch
+  let hash = hash_annot_switch
+end)
+
+module ProjNameTable = Hashtbl.Make (Projection.Repr)
+
+let str_cst_tbl : int SConstTable.t = SConstTable.create 31
+
+let annot_tbl : int AnnotTable.t = AnnotTable.create 31
+    (* (annot_switch * int) Hashtbl.t  *)
+
+let proj_name_tbl : int ProjNameTable.t = ProjNameTable.create 31
+
+(*************************************************************)
+(*** Mise a jour des valeurs des variables et des constantes *)
+(*************************************************************)
+
+exception NotEvaluated
+
+let key rk =
+  match !rk with
+  | None -> raise NotEvaluated
+  | Some k ->
+      try CEphemeron.get k
+      with CEphemeron.InvalidKey -> raise NotEvaluated
+
+(************************)
+(* traduction des patch *)
+
+(* slot_for_*, calcul la valeur de l'objet, la place
+   dans la table global, rend sa position dans la table *)
+
+let slot_for_str_cst key =
+  try SConstTable.find str_cst_tbl key
+  with Not_found ->
+    let n = set_global (val_of_str_const key) in
+    SConstTable.add str_cst_tbl key n;
+    n
+
+let slot_for_annot key =
+  try AnnotTable.find annot_tbl key
+  with Not_found ->
+    let n =  set_global (val_of_annot_switch key) in
+    AnnotTable.add annot_tbl key n;
+    n
+
+let slot_for_caml_prim =
+  let open CPrimitives in function
+  | Arraymake -> parray_make
+  | Arrayget -> parray_get
+  | Arraydefault -> parray_get_default
+  | Arrayset -> parray_set
+  | Arraycopy -> parray_copy
+  | Arrayreroot -> parray_reroot
+  | Arraylength -> parray_length
+  | _ -> assert false
+
+let slot_for_proj_name key =
+  try ProjNameTable.find proj_name_tbl key
+  with Not_found ->
+    let n =  set_global (val_of_proj_name key) in
+    ProjNameTable.add proj_name_tbl key n;
+    n
+
+let rec slot_for_getglobal env kn =
+  let (cb,(_,rk)) = lookup_constant_key kn env in
+  try key rk
+  with NotEvaluated ->
+(*    Pp.msgnl(str"not yet evaluated");*)
+    let pos =
+      match cb.const_body_code with
+      | None -> set_global (val_of_constant kn)
+      | Some code ->
+         match Vmemitcodes.force code with
+         | BCdefined(code,pl,fv) ->
+           let v = eval_to_patch env (code,pl,fv) in
+           set_global v
+         | BCalias kn' -> slot_for_getglobal env kn'
+         | BCconstant -> set_global (val_of_constant kn)
+    in
+(*Pp.msgnl(str"value stored at: "++int pos);*)
+    rk := Some (CEphemeron.create pos);
+    pos
+
+and slot_for_fv env fv =
+  let fill_fv_cache cache id v_of_id env_of_id b =
+    let v,d =
+      match b with
+      | None -> v_of_id id, Id.Set.empty
+      | Some c ->
+          val_of_constr (env_of_id id env) c,
+          Environ.global_vars_set env c in
+    build_lazy_val cache (v, d); v in
+  let val_of_rel i = val_of_rel (nb_rel env - i) in
+  let idfun _ x = x in
+  match fv with
+  | FVnamed id ->
+      let nv = lookup_named_val id env in
+      begin match force_lazy_val nv with
+      | None ->
+         env |> lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun
+      | Some (v, _) -> v
+      end
+  | FVrel i ->
+      let rv = lookup_rel_val i env in
+      begin match force_lazy_val rv with
+      | None ->
+        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 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
+    | Reloc_proj_name p -> slot_for_proj_name p
+    | Reloc_caml_prim op -> slot_for_caml_prim op
+  in
+  let tc = patch buff pl slots in
+  let vm_env =
+    (* Beware, this may look like a call to [Array.map], but it's not.
+       Calling [Array.map f] when the first argument returned by [f]
+       is a float would lead to [vm_env] being an unboxed Double_array
+       (Tag_val = Double_array_tag) whereas eval_tcode expects a
+       regular array (Tag_val = 0).
+       See test-suite/primitive/float/coq_env_double_array.v
+       for an actual instance. *)
+    let a = Array.make (Array.length fv) crazy_val in
+    Array.iteri (fun i v -> a.(i) <- slot_for_fv env v) fv; a in
+  eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
+
+and val_of_constr env c =
+  match compile ~fail_on_error: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 = () (* !?! *)