summaryrefslogtreecommitdiff
path: root/kernel/csymtable.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /kernel/csymtable.ml
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'kernel/csymtable.ml')
-rw-r--r--kernel/csymtable.ml179
1 files changed, 179 insertions, 0 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
new file mode 100644
index 00000000..fc2d0925
--- /dev/null
+++ b/kernel/csymtable.ml
@@ -0,0 +1,179 @@
+open Names
+open Term
+open Vm
+open Cemitcodes
+open Cbytecodes
+open Declarations
+open Pre_env
+open Cbytegen
+
+
+external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
+external free_tcode : tcode -> unit = "coq_static_free"
+external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
+
+(*******************)
+(* Linkage du code *)
+(*******************)
+
+(* Table des globaux *)
+
+(* [global_data] contient les valeurs des constantes globales
+ (axiomes,definitions), les annotations des switch et les structured
+ constant *)
+external global_data : unit -> values array = "get_coq_global_data"
+
+(* [realloc_global_data n] augmente de n la taille de [global_data] *)
+external realloc_global_data : int -> unit = "realloc_coq_global_data"
+
+let check_global_data n =
+ if n >= Array.length (global_data()) then realloc_global_data n
+
+let num_global = ref 0
+
+let set_global v =
+ let n = !num_global in
+ check_global_data n;
+ (global_data()).(n) <- v;
+ incr num_global;
+ n
+
+(* [global_transp],[global_boxed] contiennent les valeurs des
+ definitions gelees. Les deux versions sont maintenues en //.
+ [global_transp] contient la version transparente.
+ [global_boxed] contient la version gelees. *)
+
+external global_boxed : unit -> bool array = "get_coq_global_boxed"
+
+(* [realloc_global_data n] augmente de n la taille de [global_data] *)
+external realloc_global_boxed : int -> unit = "realloc_coq_global_boxed"
+
+let check_global_boxed n =
+ if n >= Array.length (global_boxed()) then realloc_global_boxed n
+
+let num_boxed = ref 0
+
+let boxed_tbl = Hashtbl.create 53
+
+let cst_opaque = ref Cpred.full
+
+let is_opaque kn = Cpred.mem kn !cst_opaque
+
+let set_global_boxed kn v =
+ let n = !num_boxed in
+ check_global_boxed n;
+ (global_boxed()).(n) <- (is_opaque kn);
+ Hashtbl.add boxed_tbl kn n ;
+ incr num_boxed;
+ set_global (val_of_constant_def n kn v)
+
+(* table pour les structured_constant et les annotations des switchs *)
+
+let str_cst_tbl = Hashtbl.create 31
+ (* (structured_constant * int) Hashtbl.t*)
+
+let annot_tbl = Hashtbl.create 31
+ (* (annot_switch * int) Hashtbl.t *)
+
+(*************************************************************)
+(*** Mise a jour des valeurs des variables et des constantes *)
+(*************************************************************)
+
+exception NotEvaluated
+
+let key rk =
+ match !rk with
+ | Some k -> k
+ | _ -> 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 Hashtbl.find str_cst_tbl key
+ with Not_found ->
+ let n = set_global (val_of_str_const key) in
+ Hashtbl.add str_cst_tbl key n;
+ n
+
+let slot_for_annot key =
+ try Hashtbl.find annot_tbl key
+ with Not_found ->
+ let n = set_global (Obj.magic key) in
+ Hashtbl.add annot_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 ->
+ let pos =
+ match Cemitcodes.force cb.const_body_code with
+ | BCdefined(boxed,(code,pl,fv)) ->
+ let v = eval_to_patch env (code,pl,fv) in
+ if boxed then set_global_boxed kn v
+ else set_global v
+ | BCallias kn' -> slot_for_getglobal env kn'
+ | BCconstant -> set_global (val_of_constant kn) in
+ rk := Some pos;
+ pos
+
+and slot_for_fv env fv=
+ match fv with
+ | FVnamed id ->
+ let nv = lookup_named_val id env in
+ begin
+ match !nv with
+ | VKvalue v -> v
+ | VKaxiom id ->
+ let v = val_of_named id in
+ nv := VKvalue v; v
+ | VKdef c ->
+ let v = val_of_constr (env_of_named id env) c in
+ nv := VKvalue v; v
+ end
+ | FVrel i ->
+ let rv = lookup_rel_val i env in
+ begin
+ match !rv with
+ | VKvalue v -> v
+ | VKaxiom k ->
+ let v = val_of_rel k in
+ rv := VKvalue v; v
+ | VKdef c ->
+ let v = val_of_constr (env_of_rel i env) c in
+ rv := VKvalue v; v
+ end
+
+and eval_to_patch env (buff,pl,fv) =
+ 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 ->
+ patch_int buff pos (slot_for_getglobal env kn)
+ in
+ List.iter patch pl;
+ 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 compile env c
+ with e -> print_string "can not compile \n";Format.print_flush();raise e in
+ eval_to_patch env (to_memory ccfv)
+
+let set_transparent_const kn =
+ cst_opaque := Cpred.remove kn !cst_opaque;
+ List.iter (fun n -> (global_boxed()).(n) <- false)
+ (Hashtbl.find_all boxed_tbl kn)
+
+let set_opaque_const kn =
+ cst_opaque := Cpred.add kn !cst_opaque;
+ List.iter (fun n -> (global_boxed()).(n) <- true)
+ (Hashtbl.find_all boxed_tbl kn)
+
+