diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/cbytecodes.ml | 11 | ||||
-rw-r--r-- | kernel/cbytecodes.mli | 1 | ||||
-rw-r--r-- | kernel/cbytegen.ml | 168 | ||||
-rw-r--r-- | kernel/cemitcodes.ml | 11 | ||||
-rw-r--r-- | kernel/cemitcodes.mli | 1 | ||||
-rw-r--r-- | kernel/csymtable.ml | 16 | ||||
-rw-r--r-- | kernel/names.ml | 6 | ||||
-rw-r--r-- | kernel/names.mli | 6 | ||||
-rw-r--r-- | kernel/vmvalues.ml | 2 | ||||
-rw-r--r-- | kernel/vmvalues.mli | 1 |
10 files changed, 127 insertions, 96 deletions
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/cbytegen.ml b/kernel/cbytegen.ml index df5b17da3..7a27a3d20 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -399,55 +399,55 @@ let code_makeblock ~stack_size ~arity ~tag cont = Kpush :: nest_block tag arity cont end -let compile_structured_constant reloc sc sz cont = +let compile_structured_constant cenv sc sz cont = set_max_stack_size sz; Kconst sc :: cont (* compiling application *) -let comp_args comp_expr reloc args sz cont = +let comp_args comp_expr cenv args sz cont = let nargs_m_1 = Array.length args - 1 in - let c = ref (comp_expr reloc args.(0) (sz + nargs_m_1) cont) in + let c = ref (comp_expr cenv args.(0) (sz + nargs_m_1) cont) in for i = 1 to nargs_m_1 do - c := comp_expr reloc args.(i) (sz + nargs_m_1 - i) (Kpush :: !c) + c := comp_expr cenv args.(i) (sz + nargs_m_1 - i) (Kpush :: !c) done; !c -let comp_app comp_fun comp_arg reloc f args sz cont = +let comp_app comp_fun comp_arg cenv f args sz cont = let nargs = Array.length args in - if Int.equal nargs 0 then comp_fun reloc f sz cont + if Int.equal nargs 0 then comp_fun cenv f sz cont else match is_tailcall cont with | Some k -> - comp_args comp_arg reloc args sz + comp_args comp_arg cenv args sz (Kpush :: - comp_fun reloc f (sz + nargs) + comp_fun cenv f (sz + nargs) (Kappterm(nargs, k + nargs) :: (discard_dead_code cont))) | None -> if nargs < 4 then - comp_args comp_arg reloc args sz - (Kpush :: (comp_fun reloc f (sz+nargs) (Kapply nargs :: cont))) + comp_args comp_arg cenv args sz + (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont))) else let lbl,cont1 = label_code cont in Kpush_retaddr lbl :: - (comp_args comp_arg reloc args (sz + 3) - (Kpush :: (comp_fun reloc f (sz+3+nargs) (Kapply nargs :: cont1)))) + (comp_args comp_arg cenv args (sz + 3) + (Kpush :: (comp_fun cenv f (sz+3+nargs) (Kapply nargs :: cont1)))) (* Compiling free variables *) -let compile_fv_elem reloc fv sz cont = +let compile_fv_elem cenv fv sz cont = match fv with - | FVrel i -> pos_rel i reloc sz :: cont - | FVnamed id -> pos_named id reloc :: cont - | FVuniv_var i -> pos_universe_var i reloc sz :: cont - | FVevar evk -> pos_evar evk reloc :: cont + | FVrel i -> pos_rel i cenv sz :: cont + | FVnamed id -> pos_named id cenv :: cont + | FVuniv_var i -> pos_universe_var i cenv sz :: cont + | FVevar evk -> pos_evar evk cenv :: cont -let rec compile_fv reloc l sz cont = +let rec compile_fv cenv l sz cont = match l with | [] -> cont - | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem reloc fvn sz cont + | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem cenv fvn sz cont | fvn :: tl -> - compile_fv_elem reloc fvn sz - (Kpush :: compile_fv reloc tl (sz + 1) cont) + compile_fv_elem cenv fvn sz + (Kpush :: compile_fv cenv tl (sz + 1) cont) (* Compiling constants *) @@ -472,58 +472,58 @@ let make_areconst n else_lbl cont = Kareconst (n, else_lbl)::cont (* sz is the size of the local stack *) -let rec compile_lam env reloc lam sz cont = +let rec compile_lam env cenv lam sz cont = set_max_stack_size sz; match lam with - | Lrel(_, i) -> pos_rel i reloc sz :: cont + | Lrel(_, i) -> pos_rel i cenv sz :: cont - | Lval v -> compile_structured_constant reloc v sz cont + | Lval v -> compile_structured_constant cenv v sz cont | Lproj (n,kn,arg) -> - compile_lam env reloc arg sz (Kproj (n,kn) :: cont) + compile_lam env cenv arg sz (Kproj (n,kn) :: cont) - | Lvar id -> pos_named id reloc :: cont + | Lvar id -> pos_named id cenv :: cont | Levar (evk, args) -> if Array.is_empty args then - compile_fv_elem reloc (FVevar evk) sz cont + compile_fv_elem cenv (FVevar evk) sz cont else - comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz cont + comp_app compile_fv_elem (compile_lam env) cenv (FVevar evk) args sz cont - | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont + | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont | Lind (ind,u) -> if Univ.Instance.is_empty u then - compile_structured_constant reloc (Const_ind ind) sz cont - else comp_app compile_structured_constant compile_universe reloc + compile_structured_constant cenv (Const_ind ind) sz cont + else comp_app compile_structured_constant compile_universe cenv (Const_ind ind) (Univ.Instance.to_array u) sz cont | Lsort (Sorts.Prop _ as s) -> - compile_structured_constant reloc (Const_sort s) sz cont + compile_structured_constant cenv (Const_sort s) sz cont | Lsort (Sorts.Type u) -> (* We represent universes as a global constant with local universes "compacted", i.e. as [u arg0 ... argn] where we will substitute (after evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *) let u,s = Univ.compact_univ u in - let compile_get_univ reloc idx sz cont = + let compile_get_univ cenv idx sz cont = set_max_stack_size sz; - compile_fv_elem reloc (FVuniv_var idx) sz cont + compile_fv_elem cenv (FVuniv_var idx) sz cont in if List.is_empty s then - compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont + compile_structured_constant cenv (Const_sort (Sorts.Type u)) sz cont else - comp_app compile_structured_constant compile_get_univ reloc + comp_app compile_structured_constant compile_get_univ cenv (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont | Llet (id,def,body) -> - compile_lam env reloc def sz + compile_lam env cenv def sz (Kpush :: - compile_lam env (push_local sz reloc) body (sz+1) (add_pop 1 cont)) + compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont)) | Lprod (dom,codom) -> let cont1 = - Kpush :: compile_lam env reloc dom (sz+1) (Kmakeprod :: cont) in - compile_lam env reloc codom sz cont1 + Kpush :: compile_lam env cenv dom (sz+1) (Kmakeprod :: cont) in + compile_lam env cenv codom sz cont1 | Llam (ids,body) -> let arity = Array.length ids in @@ -534,12 +534,12 @@ let rec compile_lam env reloc lam sz cont = in fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; let fv = fv r_fun in - compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) + compile_fv cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) | Lapp (f, args) -> begin match f with - | Lconst (kn,u) -> compile_constant env reloc kn u args sz cont - | _ -> comp_app (compile_lam env) (compile_lam env) reloc f args sz cont + | Lconst (kn,u) -> compile_constant env cenv kn u args sz cont + | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont end | Lfix ((rec_args, init), (decl, types, bodies)) -> @@ -571,7 +571,7 @@ let rec compile_lam env reloc lam sz cont = fun_code := [Ksequence(fcode,!fun_code)] done; let fv = !rfv in - compile_fv reloc fv.fv_rev sz + compile_fv cenv fv.fv_rev sz (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) @@ -607,7 +607,7 @@ let rec compile_lam env reloc lam sz cont = done; let fv = !rfv in set_max_stack_size (sz + fv.size + ndef + 2); - compile_fv reloc fv.fv_rev sz + compile_fv cenv fv.fv_rev sz (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) @@ -625,7 +625,7 @@ let rec compile_lam env reloc lam sz cont = let branch1, cont = make_branch cont in (* Compilation of the return type *) let fcode = - ensure_stack_capacity (compile_lam env reloc t sz) [Kpop sz; Kstop] + ensure_stack_capacity (compile_lam env cenv t sz) [Kpop sz; Kstop] in let lbl_typ,fcode = label_code fcode in fun_code := [Ksequence(fcode,!fun_code)]; @@ -653,7 +653,7 @@ let rec compile_lam env reloc lam sz cont = (* Compilation of constant branches *) for i = nconst - 1 downto 0 do let aux = - compile_lam env reloc branches.constant_branches.(i) sz_b (branch::!c) + compile_lam env cenv branches.constant_branches.(i) sz_b (branch::!c) in let lbl_b,code_b = label_code aux in lbl_consts.(i) <- lbl_b; @@ -665,7 +665,7 @@ let rec compile_lam env reloc lam sz cont = let (ids, body) = branches.nonconstant_branches.(i) in let arity = Array.length ids in let code_b = - compile_lam env (push_param arity sz_b reloc) + compile_lam env (push_param arity sz_b cenv) body (sz_b+arity) (add_pop arity (branch::!c)) in let code_b = if tag < last_variant_tag then begin @@ -703,25 +703,25 @@ let rec compile_lam env reloc lam sz cont = | Kbranch lbl -> Kpush_retaddr lbl :: !c | _ -> !c in - compile_lam env reloc a sz code_sw + compile_lam env cenv a sz code_sw | Lmakeblock (tag,args) -> let arity = Array.length args in let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in - comp_args (compile_lam env) reloc args sz cont + comp_args (compile_lam env) cenv args sz cont | Lprim (kn, ar, op, args) -> - op_compilation env ar op kn reloc args sz cont + op_compilation env ar op kn cenv args sz cont | Luint v -> (match v with - | UintVal i -> compile_structured_constant reloc (Const_b0 (Uint31.to_int i)) sz cont + | UintVal i -> compile_structured_constant cenv (Const_b0 (Uint31.to_int i)) sz cont | UintDigits ds -> let nargs = Array.length ds in if Int.equal nargs 31 then let (escape,labeled_cont) = make_branch cont in let else_lbl = Label.create() in - comp_args (compile_lam env) reloc ds sz + comp_args (compile_lam env) cenv ds sz ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont) else let code_construct cont = (* spiwack: variant of the global code_construct @@ -737,40 +737,40 @@ let rec compile_lam env reloc lam sz cont = Kclosure(lbl,0) :: cont in comp_app (fun _ _ _ cont -> code_construct cont) - (compile_lam env) reloc () ds sz cont + (compile_lam env) cenv () ds sz cont | UintDecomp t -> let escape_lbl, labeled_cont = label_code cont in - compile_lam env reloc t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont)) + compile_lam env cenv t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont)) (* spiwack : compilation of constants with their arguments. Makes a special treatment with 31-bit integer addition *) -and compile_get_global reloc (kn,u) sz cont = +and compile_get_global cenv (kn,u) sz cont = set_max_stack_size sz; if Univ.Instance.is_empty u then Kgetglobal kn :: cont else comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) - compile_universe reloc () (Univ.Instance.to_array u) sz cont + compile_universe cenv () (Univ.Instance.to_array u) sz cont -and compile_universe reloc uni sz cont = +and compile_universe cenv uni sz cont = set_max_stack_size sz; match Univ.Level.var_index uni with - | None -> compile_structured_constant reloc (Const_univ_level uni) sz cont - | Some idx -> pos_universe_var idx reloc sz :: cont + | None -> compile_structured_constant cenv (Const_univ_level uni) sz cont + | Some idx -> pos_universe_var idx cenv sz :: cont -and compile_constant env reloc kn u args sz cont = +and compile_constant env cenv kn u args sz cont = set_max_stack_size sz; if Univ.Instance.is_empty u then (* normal compilation *) comp_app (fun _ _ sz cont -> - compile_get_global reloc (kn,u) sz cont) - (compile_lam env) reloc () args sz cont + compile_get_global cenv (kn,u) sz cont) + (compile_lam env) cenv () args sz cont else - let compile_arg reloc constr_or_uni sz cont = + let compile_arg cenv constr_or_uni sz cont = match constr_or_uni with - | ArgLambda t -> compile_lam env reloc t sz cont - | ArgUniv uni -> compile_universe reloc uni sz cont + | ArgLambda t -> compile_lam env cenv t sz cont + | ArgUniv uni -> compile_universe cenv uni sz cont in let u = Univ.Instance.to_array u in let lu = Array.length u in @@ -779,7 +779,7 @@ and compile_constant env reloc kn u args sz cont = (fun i -> if i < lu then ArgUniv u.(i) else ArgLambda args.(i-lu)) in comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) - compile_arg reloc () all sz cont + compile_arg cenv () all sz cont (*template for n-ary operation, invariant: n>=1, the operations does the following : @@ -788,34 +788,34 @@ and compile_constant env reloc kn u args sz cont = 3/ if at least one is not, branches to the normal behavior: Kgetglobal (get_alias !global_env kn) *) and op_compilation env n op = - let code_construct reloc kn sz cont = + let code_construct cenv kn sz cont = let f_cont = let else_lbl = Label.create () in Kareconst(n, else_lbl):: Kacc 0:: Kpop 1:: op:: Kreturn 0:: Klabel else_lbl:: (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*) - compile_get_global reloc kn sz ( + compile_get_global cenv kn sz ( Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *) in let lbl = Label.create () in fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)]; Kclosure(lbl, 0)::cont in - fun kn reloc args sz cont -> + fun kn cenv args sz cont -> let nargs = Array.length args in if Int.equal nargs n then (*if it is a fully applied addition*) let (escape, labeled_cont) = make_branch cont in let else_lbl = Label.create () in assert (n < 4); - comp_args (compile_lam env) reloc args sz + comp_args (compile_lam env) cenv args sz (Kisconst else_lbl::(make_areconst (n-1) else_lbl (*Kaddint31::escape::Klabel else_lbl::Kpush::*) (op::escape::Klabel else_lbl::Kpush:: (* works as comp_app with nargs < 4 and non-tailcall cont*) - compile_get_global reloc kn (sz+n) (Kapply n::labeled_cont)))) + compile_get_global cenv kn (sz+n) (Kapply n::labeled_cont)))) else - comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont) - (compile_lam env) reloc () args sz cont + comp_app (fun cenv _ sz cont -> code_construct cenv kn sz cont) + (compile_lam env) cenv () args sz cont let is_univ_copy max u = @@ -846,11 +846,11 @@ let compile ~fail_on_error ?universes:(universes=0) env c = Label.reset_label_counter (); let cont = [Kstop] in try - let reloc, init_code = + let cenv, init_code = if Int.equal universes 0 then let lam = lambda_of_constr ~optimize:true env c in - let reloc = empty_comp_env () in - reloc, ensure_stack_capacity (compile_lam env reloc lam 0) cont + let cenv = empty_comp_env () in + cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont else (* We are going to generate a lambda, but merge the universe closure * with the function closure if it exists. @@ -858,7 +858,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = let lam = lambda_of_constr ~optimize:true env c in let params, body = decompose_Llam lam in let arity = Array.length params in - let reloc = empty_comp_env () in + let cenv = empty_comp_env () in let full_arity = arity + universes in let r_fun = comp_env_fun ~univs:universes arity in let lbl_fun = Label.create () in @@ -869,12 +869,12 @@ let compile ~fail_on_error ?universes:(universes=0) env c = fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; let fv = fv r_fun in let init_code = - ensure_stack_capacity (compile_fv reloc fv.fv_rev 0) + ensure_stack_capacity (compile_fv cenv fv.fv_rev 0) (Kclosure(lbl_fun,fv.size) :: cont) in - reloc, init_code + cenv, init_code in - let fv = List.rev (!(reloc.in_env).fv_rev) in + let fv = List.rev (!(cenv.in_env).fv_rev) in (if !dump_bytecode then Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) @@ -922,13 +922,13 @@ let op2_compilation op = fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)]; Kclosure(lbl, 0)::cont in - fun normal fc _ reloc args sz cont -> + fun normal fc _ cenv args sz cont -> if not fc then raise Not_found else let nargs = Array.length args in if nargs=2 then (*if it is a fully applied addition*) let (escape, labeled_cont) = make_branch cont in let else_lbl = Label.create () in - comp_args compile_constr reloc args sz + comp_args compile_constr cenv args sz (Kisconst else_lbl::(make_areconst 1 else_lbl (*Kaddint31::escape::Klabel else_lbl::Kpush::*) (op::escape::Klabel else_lbl::Kpush:: @@ -940,5 +940,5 @@ let op2_compilation op = code_construct normal cont else comp_app (fun _ _ _ cont -> code_construct normal cont) - compile_constr reloc () args sz cont *) + compile_constr cenv () args sz cont *) 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/names.ml b/kernel/names.ml index 54f089e60..597061278 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -852,3 +852,9 @@ let eq_egr e1 e2 = match e1, e2 with EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 | _, _ -> false + +(** Located identifiers and objects with syntax. *) + +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t diff --git a/kernel/names.mli b/kernel/names.mli index f988b559a..4eb5adb62 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -605,3 +605,9 @@ type evaluable_global_reference = | EvalConstRef of Constant.t val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool + +(** Located identifiers and objects with syntax. *) + +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t 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 *) |