diff options
Diffstat (limited to 'kernel/byterun/coq_interp.c')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 50 |
1 files changed, 26 insertions, 24 deletions
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 */ |