From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/cemitcodes.ml | 35 ++++++++++++++++------------------- 1 file changed, 16 insertions(+), 19 deletions(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 2535a64d..ef0c9af4 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -19,7 +19,7 @@ open Mod_subst type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of pconstant + | Reloc_getglobal of Names.constant type patch = reloc_info * int @@ -127,11 +127,11 @@ let slot_for_const c = enter (Reloc_const c); out_int 0 -and slot_for_annot a = +let slot_for_annot a = enter (Reloc_annot a); out_int 0 -and slot_for_getglobal p = +let slot_for_getglobal p = enter (Reloc_getglobal p); out_int 0 @@ -190,7 +190,7 @@ let emit_instr = function Array.iter (out_label_with_orig org) lbl_bodies | Kgetglobal q -> out opGETGLOBAL; slot_for_getglobal q - | Kconst((Const_b0 i)) -> + | Kconst (Const_b0 i) -> if i >= 0 && i <= 3 then out (opCONST0 + i) else (out opCONSTINT; out_int i) @@ -225,6 +225,7 @@ let emit_instr = function if n <= 1 then out (opSETFIELD0+n) else (out opSETFIELD;out_int n) | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" + | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p) (* spiwack *) | Kbranch lbl -> out opBRANCH; out_label lbl | Kaddint31 -> out opADDINT31 @@ -306,9 +307,10 @@ type to_patch = emitcodes * (patch list) * fv (* Substitution *) let rec subst_strcst s sc = match sc with - | Const_sorts _ | Const_b0 _ -> sc + | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> 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,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u) + | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) let subst_patch s (ri,pos) = match ri with @@ -317,7 +319,7 @@ let subst_patch s (ri,pos) = let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in (Reloc_annot {a with ci = ci},pos) | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv @@ -326,36 +328,36 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u) type body_code = | BCdefined of to_patch - | BCallias of pconstant + | BCalias of Names.constant | BCconstant type to_patch_substituted = | PBCdefined of to_patch substituted -| PBCallias of pconstant substituted +| PBCalias of Names.constant substituted | PBCconstant let from_val = function | BCdefined tp -> PBCdefined (from_val tp) -| BCallias cu -> PBCallias (from_val cu) +| BCalias cu -> PBCalias (from_val cu) | BCconstant -> PBCconstant let force = function | PBCdefined tp -> BCdefined (force subst_to_patch tp) -| PBCallias cu -> BCallias (force subst_pconstant cu) +| PBCalias cu -> BCalias (force subst_constant cu) | PBCconstant -> BCconstant let subst_to_patch_subst s = function | PBCdefined tp -> PBCdefined (subst_substituted s tp) -| PBCallias cu -> PBCallias (subst_substituted s cu) +| PBCalias cu -> PBCalias (subst_substituted s cu) | PBCconstant -> PBCconstant let repr_body_code = function | PBCdefined tp -> let (s, tp) = repr_substituted tp in (s, BCdefined tp) -| PBCallias cu -> +| PBCalias cu -> let (s, cu) = repr_substituted cu in - (s, BCallias cu) + (s, BCalias cu) | PBCconstant -> (None, BCconstant) let to_memory (init_code, fun_code, fv) = @@ -371,8 +373,3 @@ let to_memory (init_code, fun_code, fv) = | Label_undefined patchlist -> assert (patchlist = []))) !label_table; (code, reloc, fv) - - - - - -- cgit v1.2.3