From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- kernel/byterun/coq_fix_code.c | 16 ++++---------- kernel/byterun/coq_fix_code.h | 1 - kernel/byterun/coq_instruct.h | 3 ++- kernel/byterun/coq_interp.c | 50 ++++++++++++++++++++++--------------------- kernel/byterun/coq_memory.c | 34 ----------------------------- kernel/byterun/coq_memory.h | 3 --- 6 files changed, 32 insertions(+), 75 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 5d302660..3fded663 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -46,7 +46,8 @@ void init_arity () { arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]= arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]= arity[HEAD0INT31]=arity[TAIL0INT31]= - arity[COMPINT31]=arity[DECOMPINT31]=0; + arity[COMPINT31]=arity[DECOMPINT31]= + arity[ORINT31]=arity[ANDINT31]=arity[XORINT31]=0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= @@ -54,7 +55,7 @@ void init_arity () { arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= - arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=arity[ACCUMULATECOND]= + arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]= arity[BRANCH]=arity[ISCONST]= 1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= @@ -84,15 +85,6 @@ value coq_makeaccu (value i) { return (value)res; } -value coq_accucond (value i) { - code_t q; - code_t res = coq_stat_alloc(8); - q = res; - *q++ = VALINSTR(ACCUMULATECOND); - *q = (opcode_t)Int_val(i); - return (value)res; -} - value coq_pushpop (value i) { code_t res; int n; @@ -117,7 +109,7 @@ value coq_is_accumulate_code(value code){ code_t q; int res; q = (code_t)code; - res = Is_instruction(q,ACCUMULATECOND) || Is_instruction(q,ACCUMULATE); + res = Is_instruction(q,ACCUMULATE); return Val_bool(res); } diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index c1a4e0ae..5c85389d 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -29,7 +29,6 @@ void init_arity(); value coq_tcode_of_code(value code, value len); value coq_makeaccu (value i); value coq_pushpop (value i); -value coq_accucond (value i); value coq_is_accumulate_code(value code); #endif /* _COQ_FIX_CODE_ */ diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index e224a108..9cbf4077 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -38,7 +38,7 @@ enum instructions { SETFIELD0, SETFIELD1, SETFIELD, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, - ACCUMULATE, ACCUMULATECOND, + ACCUMULATE, MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, /* spiwack: */ BRANCH, @@ -49,6 +49,7 @@ enum instructions { HEAD0INT31, TAIL0INT31, ISCONST, ARECONST, COMPINT31, DECOMPINT31, + ORINT31, ANDINT31, XORINT31, /* /spiwack */ STOP }; diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index aab08d89..f9e0dc7f 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -543,21 +543,21 @@ value coq_interprete coq_extra_args = Long_val(sp[2]); sp += 3; } else { - /* L'argument recursif est un accumulateur */ + /* The recursif argument is an accumulator */ mlsize_t num_args, i; - /* Construction du PF partiellement appliqué */ + /* Construction of partially applied PF */ Alloc_small(accu, rec_pos + 2, Closure_tag); Field(accu, 1) = coq_env; for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; Code_val(accu) = pc; sp += rec_pos; *--sp = accu; - /* Construction de l'atom */ + /* Construction of the atom */ Alloc_small(accu, 2, ATOM_FIX_TAG); Field(accu,1) = sp[0]; Field(accu,0) = sp[1]; sp++; sp[0] = accu; - /* Construction de l'accumulateur */ + /* Construction of the accumulator */ num_args = coq_extra_args - rec_pos; Alloc_small(accu, 2+num_args, Accu_tag); Code_val(accu) = accumulate; @@ -922,26 +922,6 @@ value coq_interprete } /* Special operations for reduction of open term */ - Instruct(ACCUMULATECOND) { - int i, num; - print_instr("ACCUMULATECOND"); - num = *pc; - pc++; - if (Field(coq_global_boxed, num) == Val_false || coq_all_transp) { - /* printf ("false\n"); - printf ("tag = %d", Tag_val(Field(accu,1))); */ - num = Wosize_val(coq_env); - for(i = 2; i < num; i++) *--sp = Field(accu,i); - coq_extra_args = coq_extra_args + (num - 2); - coq_env = Field(Field(accu,1),1); - pc = Code_val(coq_env); - accu = coq_env; - /* printf ("end\n"); */ - Next; - }; - /* printf ("true\n"); */ - } - Instruct(ACCUMULATE) { mlsize_t i, size; print_instr("ACCUMULATE"); @@ -1373,7 +1353,29 @@ value coq_interprete Next; } + Instruct (ORINT31) { + /* returns the bitwise or */ + print_instr("ORINT31"); + accu = + value_of_uint32((uint32_of_value(accu)) | (uint32_of_value(*sp++))); + Next; + } + Instruct (ANDINT31) { + /* returns the bitwise and */ + print_instr("ANDINT31"); + accu = + value_of_uint32((uint32_of_value(accu)) & (uint32_of_value(*sp++))); + Next; + } + + Instruct (XORINT31) { + /* returns the bitwise xor */ + print_instr("XORINT31"); + accu = + value_of_uint32((uint32_of_value(accu)) ^ (uint32_of_value(*sp++))); + Next; + } /* /spiwack */ diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 00f5eb3b..8d03829a 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size; value coq_global_data; -value coq_global_boxed; int coq_all_transp; value coq_atom_tbl; @@ -62,7 +61,6 @@ static void coq_scan_roots(scanning_action action) register value * i; /* Scan the global variables */ (*action)(coq_global_data, &coq_global_data); - (*action)(coq_global_boxed, &coq_global_boxed); (*action)(coq_atom_tbl, &coq_atom_tbl); /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { @@ -90,14 +88,6 @@ void init_coq_global_data(long requested_size) Field (coq_global_data, i) = Val_unit; } -void init_coq_global_boxed(long requested_size) -{ - int i; - coq_global_boxed = alloc_shr(requested_size, 0); - for (i = 0; i < requested_size; i++) - Field (coq_global_boxed, i) = Val_true; -} - void init_coq_atom_tbl(long requested_size){ int i; coq_atom_tbl = alloc_shr(requested_size, 0); @@ -125,7 +115,6 @@ value init_coq_vm(value unit) /* ML */ /* Allocate the table of global and the stack */ init_coq_stack(); init_coq_global_data(Coq_global_data_Size); - init_coq_global_boxed(40); init_coq_atom_tbl(40); /* Initialing the interpreter */ coq_all_transp = 0; @@ -181,11 +170,6 @@ value get_coq_atom_tbl(value unit) /* ML */ return coq_atom_tbl; } -value get_coq_global_boxed(value unit) /* ML */ -{ - return coq_global_boxed; -} - value realloc_coq_global_data(value size) /* ML */ { mlsize_t requested_size, actual_size, i; @@ -205,24 +189,6 @@ value realloc_coq_global_data(value size) /* ML */ return Val_unit; } -value realloc_coq_global_boxed(value size) /* ML */ -{ - mlsize_t requested_size, actual_size, i; - value new_global_boxed; - requested_size = Long_val(size); - actual_size = Wosize_val(coq_global_boxed); - if (requested_size >= actual_size) { - requested_size = (requested_size + 0x100) & 0xFFFFFF00; - new_global_boxed = alloc_shr(requested_size, 0); - for (i = 0; i < actual_size; i++) - initialize(&Field(new_global_boxed, i), Field(coq_global_boxed, i)); - for (i = actual_size; i < requested_size; i++) - Field (new_global_boxed, i) = Val_long (0); - coq_global_boxed = new_global_boxed; - } - return Val_unit; -} - value realloc_coq_atom_tbl(value size) /* ML */ { mlsize_t requested_size, actual_size, i; diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index 79e4d0fe..cec34f56 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -35,7 +35,6 @@ extern value * coq_stack_threshold; /* global_data */ extern value coq_global_data; -extern value coq_global_boxed; extern int coq_all_transp; extern value coq_atom_tbl; @@ -56,8 +55,6 @@ value re_init_coq_vm(value unit); /* ML */ void realloc_coq_stack(asize_t required_space); value get_coq_global_data(value unit); /* ML */ value realloc_coq_global_data(value size); /* ML */ -value get_coq_global_boxed(value unit); -value realloc_coq_global_boxed(value size); /* ML */ value get_coq_atom_tbl(value unit); /* ML */ value realloc_coq_atom_tbl(value size); /* ML */ value coq_set_transp_value(value transp); /* ML */ -- cgit v1.2.3