diff options
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 10 | ||||
| -rw-r--r-- | kernel/genOpcodeFiles.ml | 1 | ||||
| -rw-r--r-- | kernel/vmbytecodes.ml | 2 | ||||
| -rw-r--r-- | kernel/vmbytecodes.mli | 1 | ||||
| -rw-r--r-- | kernel/vmbytegen.ml | 2 | ||||
| -rw-r--r-- | kernel/vmemitcodes.ml | 2 |
7 files changed, 2 insertions, 18 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 51ac290ad0..4bc6848ba7 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -43,7 +43,7 @@ void init_arity () { arity[GETFIELD0]=arity[GETFIELD1]= arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= - arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= + arity[ACCUMULATE]=arity[STOP]= 0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a1537cd963..a9ea6d9f46 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1270,16 +1270,6 @@ value coq_interprete Next; } - Instruct(MAKEPROD) { - print_instr("MAKEPROD"); - *--sp=accu; - Alloc_small(accu,2,0); - Field(accu, 0) = sp[0]; - Field(accu, 1) = sp[1]; - sp += 2; - Next; - } - Instruct(BRANCH) { /* unconditional branching */ print_instr("BRANCH"); diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 6e79b431a5..0e1cd0c56a 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -98,7 +98,6 @@ let opcodes = "ACCUMULATE"; "MAKESWITCHBLOCK"; "MAKEACCU"; - "MAKEPROD"; "BRANCH"; "CHECKADDINT63"; "CHECKADDCINT63"; diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml index 4977aec00a..c2b087f061 100644 --- a/kernel/vmbytecodes.ml +++ b/kernel/vmbytecodes.ml @@ -49,7 +49,6 @@ type instruction = | Kgetglobal of Constant.t | Kconst of structured_constant | Kmakeblock of int * tag - | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int | Kswitch of Label.t array * Label.t array | Kpushfields of int @@ -123,7 +122,6 @@ let rec pp_instr i = str "const " ++ pp_struct_const sc | Kmakeblock(n, m) -> str "makeblock " ++ int n ++ str ", " ++ int m - | Kmakeprod -> str "makeprod" | Kmakeswitchblock(lblt,lbls,_,sz) -> str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++ pp_lbl lbls ++ str ", " ++ int sz diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli index 003a77ab78..eeca0d2ad1 100644 --- a/kernel/vmbytecodes.mli +++ b/kernel/vmbytecodes.mli @@ -47,7 +47,6 @@ type instruction = | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0 ** is accu, all others are popped from ** the top of the stack *) - | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int | Kswitch of Label.t array * Label.t array (** consts,blocks *) | Kpushfields of int diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 70c92fd8f0..20de4bc81b 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -569,7 +569,7 @@ let rec compile_lam env cenv lam sz cont = | Lprod (dom,codom) -> let cont1 = - Kpush :: compile_lam env cenv dom (sz+1) (Kmakeprod :: cont) in + Kpush :: compile_lam env cenv dom (sz+1) (Kmakeblock (2,0) :: cont) in compile_lam env cenv codom sz cont1 | Llam (ids,body) -> diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index 85b5ca03e5..d3af8bf09b 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -337,8 +337,6 @@ let emit_instr env = function if Int.equal n 0 then invalid_arg "emit_instr : block size = 0" else if n < 4 then (out env(opMAKEBLOCK1 + n - 1); out_int env t) else (out env opMAKEBLOCK; out_int env n; out_int env t) - | Kmakeprod -> - out env opMAKEPROD | Kmakeswitchblock(typlbl,swlbl,annot,sz) -> out env opMAKESWITCHBLOCK; out_label env typlbl; out_label env swlbl; |