From f4586d1e8b1116340574d9660117f93e7a1e4e3b Mon Sep 17 00:00:00 2001
From: bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 20 Jun 2007 09:43:36 +0000
Subject: ajout de head0 et tail0 en natif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/byterun/coq_fix_code.c |  1 +
 kernel/byterun/coq_instruct.h |  1 +
 kernel/byterun/coq_interp.c   | 30 ++++++++++++++++++++++++++++++
 3 files changed, 32 insertions(+)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 961c49785..55b907adf 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -45,6 +45,7 @@ void init_arity () {
     arity[SUBINT31]=arity[SUBCINT31]=arity[SUBCARRYCINT31]=
     arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]=
     arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]=
+    arity[HEAD0INT31]=arity[TAIL0INT31]=
     arity[COMPINT31]=arity[DECOMPINT31]=0;
   /* instruction with one operand */
   arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 00156ebe8..8a45e9739 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -42,6 +42,7 @@ enum instructions {
   SUBINT31, SUBCINT31, SUBCARRYCINT31,
   MULCINT31, MULINT31, DIV21INT31, DIVINT31,
   ADDMULDIVINT31, COMPAREINT31, 
+  HEAD0INT31, TAIL0INT31,
   ISCONST, ARECONST,
   COMPINT31, DECOMPINT31,
 /* /spiwack  */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index e7eb1bc8d..ccfb2515a 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1255,6 +1255,36 @@ value coq_interprete
         Next;
       }
  
+      Instruct (HEAD0INT31) {
+	int r = 0;
+        uint32 x;
+        print_instr("HEAD0INT31");
+	x = (uint32) accu;
+        if (!(x & 0xFFFF0000)) { x <<= 16; r += 16; }
+        if (!(x & 0xFF000000)) { x <<= 8;  r += 8; }
+        if (!(x & 0xF0000000)) { x <<= 4;  r += 4; }
+        if (!(x & 0xC0000000)) { x <<= 2;  r += 2; }
+        if (!(x & 0x80000000)) { x <<=1;   r += 1; }
+        if (!(x & 0x80000000)) {           r += 1; }
+        accu = value_of_uint32(r);
+        Next;
+      }
+        
+      Instruct (TAIL0INT31) {
+	int r = 0;
+        uint32 x;
+        print_instr("TAIL0INT31");
+	x = (((uint32) accu >> 1) | 0x80000000);
+        if (!(x & 0xFFFF)) { x >>= 16; r += 16; }
+        if (!(x & 0x00FF)) { x >>= 8;  r += 8; }
+        if (!(x & 0x000F)) { x >>= 4;  r += 4; }
+        if (!(x & 0x0003)) { x >>= 2;  r += 2; }
+        if (!(x & 0x0001)) { x >>=1;   r += 1; }
+        if (!(x & 0x0001)) {           r += 1; }
+        accu = value_of_uint32(r);
+        Next;
+      }
+
       Instruct (ISCONST) {
         /* Branches if the accu does not contain a constant
            (i.e., a non-block value) */
-- 
cgit v1.2.3