From 375a47bab8395695a4f74e19691854d2d0248045 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 23 Feb 2018 23:28:44 +0100 Subject: [VM] Remove projection names from structured constants. It was actually a hack since those names are never used to represent values, only to be passed as arguments to bytecode instructions. So instead of reusing the structured_constant type, we follow the same pattern as switch annotations. --- kernel/cbytecodes.ml | 11 +++-------- kernel/cbytecodes.mli | 1 - kernel/cemitcodes.ml | 11 +++++++++-- kernel/cemitcodes.mli | 1 + kernel/csymtable.ml | 16 ++++++++++++++++ kernel/vmvalues.ml | 2 +- kernel/vmvalues.mli | 1 + 7 files changed, 31 insertions(+), 12 deletions(-) (limited to 'kernel') 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 *) -- cgit v1.2.3