Changement dans les boxed values .

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 41 insertions, 1 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 55ad3aa5e..446c76498 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -39,6 +39,26 @@ 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++ = (opcode_t)(coq_instr_table[ACCUMULATECOND] - coq_instr_base);
+  *q = (opcode_t)Int_val(i);
+  return (value)res;
+}
+
+value coq_is_accumulate_code(value code){
+  code_t q;
+  int res;
+  q = (code_t)code;
+  res = 
+    (*q == (opcode_t)(coq_instr_table[ACCUMULATECOND] - coq_instr_base))
+    || 
+    (*q == (opcode_t)(coq_instr_table[ACCUMULATE] - coq_instr_base));
+  return Val_bool(res);
+}
+
 value coq_pushpop (value i) {
   code_t res;
   int n;
@@ -91,9 +111,10 @@ code_t coq_thread_code (code_t code, asize_t len){
     case GRAB: case COGRAB: 
     case OFFSETCLOSURE: case PUSHOFFSETCLOSURE: 
     case GETGLOBAL: case PUSHGETGLOBAL: 
-    case GETGLOBALBOXED: case PUSHGETGLOBALBOXED: 
+      /*    case GETGLOBALBOXED: case PUSHGETGLOBALBOXED: */
     case MAKEBLOCK1: case MAKEBLOCK2: case MAKEBLOCK3: case MAKEACCU:
     case CONSTINT: case PUSHCONSTINT: case GRABREC: case PUSHFIELD:
+    case ACCUMULATECOND:
     *q++ = *p++;
     break;
     
@@ -148,6 +169,25 @@ 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++ = (opcode_t)ACCUMULATECOND;
+  *q = (opcode_t)Int_val(i);
+  return (value)res;
+}
+
+value coq_is_accumulate_code(value code){
+  code_t q;
+  int res;
+  q = (code_t)code;
+  res = 
+    (*q == ACCUMULATECOND) || 
+    (*q == ACCUMULATE);
+  return Val_bool(res);
+}
+
 value coq_pushpop (value i) {
   code_t res;
   int n;