aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/vm_printers.ml5
-rw-r--r--kernel/cbytecodes.ml11
-rw-r--r--kernel/cbytecodes.mli1
-rw-r--r--kernel/cemitcodes.ml11
-rw-r--r--kernel/cemitcodes.mli1
-rw-r--r--kernel/csymtable.ml16
-rw-r--r--kernel/vmvalues.ml2
-rw-r--r--kernel/vmvalues.mli1
8 files changed, 35 insertions, 13 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 16917586f..7589e5348 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -15,7 +15,10 @@ let ppripos (ri,pos) =
| Reloc_const _ ->
print_string "structured constant\n"
| Reloc_getglobal kn ->
- print_string ("getglob "^(Constant.to_string kn)^"\n"));
+ print_string ("getglob "^(Constant.to_string kn)^"\n")
+ | Reloc_proj_name p ->
+ print_string ("proj "^(Constant.to_string p)^"\n")
+ );
print_flush ()
let print_vfix () = print_string "vfix"
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 599856b64..521f540d2 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -36,7 +36,6 @@ let last_variant_tag = 245
type structured_constant =
| Const_sort of Sorts.t
| Const_ind of inductive
- | Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
| Const_univ_level of Univ.Level.t
@@ -51,8 +50,6 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
| Const_sort _, _ -> 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) ->
@@ -66,13 +63,12 @@ let rec hash_structured_constant c =
match c with
| Const_sort 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_b0 t -> combinesmall 3 (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)
+ combinesmall 4 (combine (Int.hash t) h)
+ | Const_univ_level l -> combinesmall 5 (Univ.Level.hash l)
let eq_annot_switch asw1 asw2 =
let eq_ci ci1 ci2 =
@@ -246,7 +242,6 @@ let pp_sort s =
let rec pp_struct_const = function
| Const_sort s -> pp_sort s
| Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i
- | Const_proj p -> Constant.print p
| Const_b0 i -> int i
| Const_bn (i,t) ->
int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 03b6bc619..238edc0af 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -30,7 +30,6 @@ val last_variant_tag : tag
type structured_constant =
| Const_sort of Sorts.t
| Const_ind of inductive
- | Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
| Const_univ_level of Univ.Level.t
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index f4e6d45c2..2426255e4 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -27,6 +27,7 @@ type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
| Reloc_getglobal of Names.Constant.t
+ | Reloc_proj_name of Constant.t
let eq_reloc_info r1 r2 = match r1, r2 with
| Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2
@@ -35,6 +36,8 @@ let eq_reloc_info r1 r2 = match r1, r2 with
| Reloc_const _, _ -> false
| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2
| Reloc_getglobal _, _ -> false
+| Reloc_proj_name p1, Reloc_proj_name p2 -> Constant.equal p1 p2
+| Reloc_proj_name _, _ -> false
let hash_reloc_info r =
let open Hashset.Combine in
@@ -42,6 +45,7 @@ let hash_reloc_info r =
| Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
| Reloc_const c -> combinesmall 2 (hash_structured_constant c)
| Reloc_getglobal c -> combinesmall 3 (Constant.hash c)
+ | Reloc_proj_name p -> combinesmall 4 (Constant.hash p)
module RelocTable = Hashtbl.Make(struct
type t = reloc_info
@@ -187,6 +191,9 @@ let slot_for_getglobal env p =
enter env (Reloc_getglobal p);
out_int env 0
+let slot_for_proj_name env p =
+ enter env (Reloc_proj_name p);
+ out_int env 0
(* Emission of one instruction *)
@@ -277,7 +284,7 @@ let emit_instr env = function
if n <= 1 then out env (opSETFIELD0+n)
else (out env opSETFIELD;out_int env n)
| Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
- | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_const env (Const_proj p)
+ | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_proj_name env p
| Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
(* spiwack *)
| Kbranch lbl -> out env opBRANCH; out_label env lbl
@@ -353,7 +360,6 @@ type to_patch = emitcodes * patches * fv
let rec subst_strcst s sc =
match sc with
| Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc
- | Const_proj p -> Const_proj (subst_constant s p)
| Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
| Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
@@ -365,6 +371,7 @@ let subst_reloc s ri =
Reloc_annot {a with ci = ci}
| Reloc_const sc -> Reloc_const (subst_strcst s sc)
| Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
+ | Reloc_proj_name p -> Reloc_proj_name (subst_constant s p)
let subst_patches subst p =
let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 03920dc1a..696721c37 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -5,6 +5,7 @@ type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
| Reloc_getglobal of Constant.t
+ | Reloc_proj_name of Constant.t
type patches
type emitcodes
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 9bacdb65f..bbe093782 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -77,11 +77,19 @@ module AnnotTable = Hashtbl.Make (struct
let hash = hash_annot_switch
end)
+module ProjNameTable = Hashtbl.Make (struct
+ type t = Constant.t
+ let equal = Constant.equal
+ let hash = Constant.hash
+end)
+
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 *)
(*************************************************************)
@@ -115,6 +123,13 @@ let slot_for_annot key =
AnnotTable.add annot_tbl key n;
n
+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
@@ -170,6 +185,7 @@ and eval_to_patch env (buff,pl,fv) =
| 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
in
let tc = patch buff pl slots in
let vm_env = Array.map (slot_for_fv env) fv in
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 7a703e653..8524c44d2 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -297,7 +297,6 @@ let rec obj_of_str_const str =
match str with
| Const_sort s -> obj_of_atom (Asort s)
| Const_ind ind -> obj_of_atom (Aind ind)
- | Const_proj p -> Obj.repr p
| Const_b0 tag -> Obj.repr tag
| Const_bn(tag, args) ->
let len = Array.length args in
@@ -355,6 +354,7 @@ let val_of_constant c = val_of_idkey (ConstKey c)
let val_of_evar evk = val_of_idkey (EvarKey evk)
external val_of_annot_switch : annot_switch -> values = "%identity"
+external val_of_proj_name : Constant.t -> values = "%identity"
(*************************************************)
(** Operations manipulating data types ***********)
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 550791b2c..08d05a038 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -112,6 +112,7 @@ val val_of_proj : Constant.t -> values -> values
val val_of_atom : atom -> values
external val_of_annot_switch : annot_switch -> values = "%identity"
+external val_of_proj_name : Constant.t -> values = "%identity"
(** Destructors *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 05:05:43 +0000