Processor integers + Print assumption (see coqdev mailing list for the

details).




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

30 files changed, 2108 insertions, 101 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index affcccb3a..961c49785 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -8,6 +8,9 @@
 /*                                                                     */
 /***********************************************************************/
 
+/* Arnaud Spiwack: expanded the virtual machine with operators used
+   for fast computation of bounded (31bits) integers */
+
 #include <stdio.h>
 #include <stdlib.h> 
 #include <config.h>
@@ -37,7 +40,12 @@ void init_arity () {
     arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
     arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
     arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
-    arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 0;
+    arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 
+    arity[ADDINT31]=arity[ADDCINT31]=arity[ADDCARRYCINT31]=
+    arity[SUBINT31]=arity[SUBCINT31]=arity[SUBCARRYCINT31]=
+    arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]=
+    arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]=
+    arity[COMPINT31]=arity[DECOMPINT31]=0;
   /* instruction with one operand */
   arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
     arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
@@ -45,9 +53,11 @@ 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]= 1;
+    arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=arity[ACCUMULATECOND]=
+    arity[BRANCH]=arity[ISCONST]= 1;
   /* instruction with two operands */
-  arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=2;
+  arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
+  arity[ARECONST]=2;
   /* instruction with four operands */ 
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index d1dac80fb..003453183 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -31,4 +31,5 @@ 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 89616c5f3..00156ebe8 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -35,7 +35,17 @@ enum instructions {
   CONST0, CONST1, CONST2, CONST3, CONSTINT,
   PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
   ACCUMULATE, ACCUMULATECOND, 
-  MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, STOP
+  MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, 
+/* spiwack: */
+  BRANCH,
+  ADDINT31, ADDCINT31, ADDCARRYCINT31,
+  SUBINT31, SUBCINT31, SUBCARRYCINT31,
+  MULCINT31, MULINT31, DIV21INT31, DIVINT31,
+  ADDMULDIVINT31, COMPAREINT31, 
+  ISCONST, ARECONST,
+  COMPINT31, DECOMPINT31,
+/* /spiwack  */
+  STOP
 };
 
 #endif /* _COQ_INSTRUCT_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 8f9c10e68..c3072dc72 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -10,12 +10,31 @@
 
 /* The bytecode interpreter */
 
+/* Spiwack: expanded the virtual machine with operators used
+   for fast computation of bounded (31bits) integers */
+
 #include <stdio.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
-#include "coq_memory.h"  
-#include "coq_values.h"
+#include "coq_memory.h" 
+#include "coq_values.h" 
+
+/*spiwack : imports support functions for 64-bit integers */
+#include "config.h"
+#ifdef ARCH_INT64_TYPE
+#include "int64_native.h"
+#else
+#include "int64_emul.h"
+#endif
+
+/* spiwack: I append here a few macros for value/number manipulation */
+#define uint32_of_value(val) (((uint32)val >> 1))
+#define value_of_uint32(i)   ((value)(((uint32)i << 1) | 1))
+#define UI64_of_uint32(i)  ((uint64)I64_literal(0,i))
+#define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
+/* /spiwack */
+
 
 
 /* Registers for the abstract machine:
@@ -61,13 +80,6 @@ sp is a local copy of the global variable extern_sp. */
 #   define print_int(i) 
 #endif
 
-/* Wrapper pour caml_modify */
-#ifdef OCAML_307
-#define CAML_MODIFY(a,b) modify(a,b)
-#else
-#define CAML_MODIFY(a,b) caml_modify(a,b)
-#endif
-
 /* GC interface */
 #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
 #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
@@ -640,7 +652,7 @@ value coq_interprete
 	  Field(accu, 0) = sp[0];
 	  *sp = accu;
 	  /* mise a jour du block accumulate */
-	  CAML_MODIFY(&Field(p[i], 1),*sp);
+	  caml_modify(&Field(p[i], 1),*sp);
 	  sp++;
 	}
 	pc += nfunc;
@@ -811,7 +823,7 @@ value coq_interprete
       
       Instruct(SETFIELD0){
 	print_instr("SETFIELD0");
-	CAML_MODIFY(&Field(accu, 0),*sp);
+	caml_modify(&Field(accu, 0),*sp);
 	sp++;
 	Next;
       }
@@ -819,7 +831,7 @@ value coq_interprete
       Instruct(SETFIELD1){
         int i, j, size, size_aux;
 	print_instr("SETFIELD1");
-	CAML_MODIFY(&Field(accu, 1),*sp);
+	caml_modify(&Field(accu, 1),*sp);
        	sp++;
 	Next; 
       }
@@ -848,7 +860,7 @@ value coq_interprete
       
       Instruct(SETFIELD){
 	print_instr("SETFIELD");
-	CAML_MODIFY(&Field(accu, *pc),*sp);
+	caml_modify(&Field(accu, *pc),*sp);
 	sp++; pc++;
 	Next;
       }	
@@ -1035,7 +1047,285 @@ value coq_interprete
 	sp += 2;
 	Next;
       }
-      
+
+      /* spiwack: code for interpreting compiled integers */
+      Instruct(BRANCH) {
+	/* unconditional branching */
+        print_instr("BRANCH");
+        pc += *pc;
+        /* pc = (code_t)(pc+*pc); */
+        Next;
+      }
+
+      Instruct(ADDINT31) {
+        /* Adds the integer in the accumulator with 
+           the one ontop of the stack (which is poped)*/
+        print_instr("ADDINT31");
+        accu = 
+           (value)((uint32) accu + (uint32) *sp++ - 1); 
+        /* nota,unlike CaML we don't want
+           to have a different behavior depending on the 
+           architecture. Thus we cast the operand to uint32 */
+        Next;
+      }
+
+      Instruct (ADDCINT31) {
+	print_instr("ADDCINT31");
+	/* returns the sum with a carry */
+	uint32 s;
+	s = (uint32)accu + (uint32)*sp++ - 1;
+        if( (uint32)s < (uint32)accu ) {
+          /* carry */
+	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
+	}
+	else {
+	  /*no carry */
+	  Alloc_small(accu, 1, 1);
+	}
+	Field(accu, 0)=(value)s;
+	Next;
+      }
+
+      Instruct (ADDCARRYCINT31) {
+	print_instr("ADDCARRYCINT31");
+	/* returns the sum plus one with a carry */
+	uint32 s;
+	s = (uint32)accu + (uint32)*sp++ + 1;
+	value block;
+        if( (uint32)s <= (uint32)accu ) {
+          /* carry */
+	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
+	}
+	else {
+	  /*no carry */
+	  Alloc_small(accu, 1, 1);
+	}
+	Field(accu, 0)=(value)s;
+	Next;
+      }
+
+      Instruct (SUBINT31) {
+	print_instr("SUBINT31");
+	/* returns the subtraction */
+	accu = 
+	  (value)((uint32) accu - (uint32) *sp++ + 1); 
+        Next;
+      }
+
+      Instruct (SUBCINT31) {
+	print_instr("SUBCINT31");
+	/* returns the subtraction with a carry */
+	uint32 b;
+	uint32 s;
+	b = (uint32)*sp++;
+	s = (uint32)accu - b + 1;
+        if( (uint32)accu < b ) {
+          /* carry */
+	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
+	}
+	else {
+	  /*no carry */
+	  Alloc_small(accu, 1, 1);
+	}
+	Field(accu, 0)=(value)s;
+	Next;
+      }
+
+      Instruct (SUBCARRYCINT31) {
+	print_instr("SUBCARRYCINT31");
+	/* returns the subtraction minus one with a carry */
+	uint32 b;
+	uint32 s;
+	b = (uint32)*sp++;
+	s = (value)((uint32)accu - b - 1);
+        if( (uint32)accu <= b ) {
+          /* carry */
+	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
+	}
+	else {
+	  /*no carry */
+	  Alloc_small(accu, 1, 1);
+	}
+	Field(accu, 0)=(value)s;
+	Next;
+      }
+
+      Instruct (MULINT31) {
+	/* returns the multiplication */
+	print_instr("MULINT31");
+        accu = 
+	  value_of_uint32((uint32_of_value(accu)) * (uint32_of_value(*sp++)));
+	Next;
+      }
+
+      Instruct (MULCINT31) {
+        /*returns the multiplication on a double size word
+          (special case for 0) */
+        print_instr("MULCINT31");
+	uint64 p;
+        /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
+        p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
+	if ( I64_is_zero(p) ) {
+	  accu = (value)1;
+	}
+	else {
+          /* the output type is supposed to have a constant constructor
+	     and a non-constant constructor (in that order), the tag
+	     of the non-constant constructor is then 1 */
+	  Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
+	  /*unsigned shift*/
+	  Field(accu, 0) = (value)(I64_lsr(p,31)|1) ;  /*higher part*/
+	  Field(accu, 1) = (value)(I64_to_int32(p)|1); /*lower part*/
+	}
+	Next;
+      }
+
+      Instruct (DIV21INT31) {
+	print_instr("DIV21INT31");
+	/* spiwack: takes three int31 (the two first ones represent an
+                    int62) and perfoms the euclidian division of the
+                    int62 by the int31 */
+        uint64 bigint;
+        bigint = UI64_of_value(accu);
+        bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
+        uint64 divisor;
+        divisor = UI64_of_value(*sp++);
+        Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
+        if (I64_is_zero (divisor)) {
+          Field(accu, 0) = 1; /* 2*0+1 */
+          Field(accu, 1) = 1; /* 2*0+1 */
+	}
+	else {
+	  uint64 quo, mod;
+          I64_udivmod(bigint, divisor, &quo, &mod);
+          Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
+	  Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
+	}
+	Next;
+      }
+
+      Instruct (DIVINT31) {
+	print_instr("DIVINT31");
+        /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
+                    since it probably only concerns negative number.
+                    needs to be checked at this point */
+        uint32 divisor;
+        divisor = uint32_of_value(*sp++);
+        if (divisor == 0) { 
+          Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
+	  Field(accu, 0) = 1; /* 2*0+1 */
+          Field(accu, 1) = 1; /* 2*0+1 */
+        }
+        else {
+          uint32 modulus;
+          modulus = uint32_of_value(accu);
+          Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
+	  Field(accu, 0) = value_of_uint32(modulus/divisor);
+          Field(accu, 1) = value_of_uint32(modulus%divisor);
+        }
+	Next;
+      }
+
+      Instruct (ADDMULDIVINT31) {
+        print_instr("ADDMULDIVINT31");
+        /* higher level shift (does shifts and cycles and such) */
+        uint32 shiftby;
+        shiftby = uint32_of_value(accu);
+        /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
+        accu = (value)(((*sp++)^1) << shiftby);
+        /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */
+        accu = (value)((accu | ((*sp++) >> (31-shiftby)))|1);
+        Next;
+      }
+
+      Instruct (COMPAREINT31) {
+	/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
+	/* assumes Inudctive _ : _ := Eq | Lt | Gt */
+	print_instr("COMPAREINT31");
+	if ((uint32)accu == (uint32)*sp) {
+	  accu = 1;  /* 2*0+1 */
+	  sp++;
+	}
+	else{if ((uint32)accu < (uint32)(*sp++)) {
+	  accu = 3;  /* 2*1+1 */
+	}
+	else{
+	  accu = 5;   /* 2*2+1 */
+	}}
+        Next;
+      }
+ 
+      Instruct (ISCONST) {
+        /* Branches if the accu does not contain a constant
+           (i.e., a non-block value) */
+        print_instr("ISCONST");
+        if ((accu & 1) == 0) /* last bit is 0 -> it is a block */
+	  pc +=  *pc;
+        else
+	  pc++;
+        Next;
+
+      }
+
+      Instruct (ARECONST) {
+        /* Branches if the n first values on the stack are not
+           all constansts */
+        print_instr("ARECONST");
+        int i, n, ok;
+        ok = 1;
+        n = *pc++;
+        for(i=0; i < n; i++) {
+          if ((sp[i] & 1) == 0) {
+	    ok = 0;
+            break;
+          }
+        }
+        if(ok) pc++; else pc += *pc;
+        Next;
+      }
+
+      Instruct (COMPINT31) {
+        /* makes an 31-bit integer out of the accumulator and
+           the 30 first values of the stack 
+           and put it in the accumulator (the accumulator then the 
+           topmost get to be the heavier bits) */
+        print_instr("COMPINT31");
+        int i;
+        /*accu=accu or accu = (value)((unsigned long)1-accu) if bool
+	               is used for the bits */
+        for(i=0; i < 30; i++) {
+	  accu = (value) ((((uint32)accu-1) << 1) | *sp++);
+          /* -1 removes the tag bit, << 1 multiplies the value by 2, 
+              | *sp++ pops the last value and add it (no carry involved)
+	      not that it reintroduces a tag bit */
+          /* alternative, if bool is used for the bits :
+	     accu = (value) ((((unsigned long)accu) << 1) & !*sp++); */
+        }
+        Next;
+      }
+
+      Instruct (DECOMPINT31) {
+        /* builds a block out of a 31-bit integer (from the accumulator), 
+           used before cases */
+        int i;
+	value block;
+	print_instr("DECOMPINT31");
+        Alloc_small(block, 31, 1); // Alloc_small(*, size, tag)
+        for(i = 30; i >= 0; i--) {
+          Field(block, i) = (value)(accu & 3); /* two last bits of the accumulator */
+          //Field(block, i) = 3;
+          accu = (value) ((uint32)accu >> 1) | 1;  /* last bit must be a one */
+        };
+	accu = block;
+        Next;
+      }
+
+
+
+      /*  /spiwack   */
+
+
+
 /* Debugging and machine control */
 
       Instruct(STOP){
diff --git a/kernel/byterun/int64_emul.h b/kernel/byterun/int64_emul.h
new file mode 100644
index 000000000..ba8a60149
--- /dev/null
+++ b/kernel/byterun/int64_emul.h
@@ -0,0 +1,272 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Objective Caml                            */
+/*                                                                     */
+/*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         */
+/*                                                                     */
+/*  Copyright 2002 Institut National de Recherche en Informatique et   */
+/*  en Automatique.  All rights reserved.  This file is distributed    */
+/*  under the terms of the GNU Library General Public License, with    */
+/*  the special exception on linking described in file ../LICENSE.     */
+/*                                                                     */
+/***********************************************************************/
+
+/* $Id: int64_emul.h,v 1.5 2005/09/22 14:21:50 xleroy Exp $ */
+
+/* Software emulation of 64-bit integer arithmetic, for C compilers
+   that do not support it.  */
+
+#ifndef CAML_INT64_EMUL_H
+#define CAML_INT64_EMUL_H
+
+#include <math.h>
+
+#ifdef ARCH_BIG_ENDIAN
+#define I64_literal(hi,lo) { hi, lo }
+#else
+#define I64_literal(hi,lo) { lo, hi }
+#endif
+
+/* Unsigned comparison */
+static int I64_ucompare(uint64 x, uint64 y)
+{
+  if (x.h > y.h) return 1;
+  if (x.h < y.h) return -1;
+  if (x.l > y.l) return 1;
+  if (x.l < y.l) return -1;
+  return 0;
+}
+
+#define I64_ult(x, y) (I64_ucompare(x, y) < 0)
+
+/* Signed comparison */
+static int I64_compare(int64 x, int64 y)
+{
+  if ((int32)x.h > (int32)y.h) return 1;
+  if ((int32)x.h < (int32)y.h) return -1;
+  if (x.l > y.l) return 1;
+  if (x.l < y.l) return -1;
+  return 0;
+}
+
+/* Negation */
+static int64 I64_neg(int64 x)
+{
+  int64 res;
+  res.l = -x.l;
+  res.h = ~x.h;
+  if (res.l == 0) res.h++;
+  return res;
+}
+
+/* Addition */
+static int64 I64_add(int64 x, int64 y)
+{
+  int64 res;
+  res.l = x.l + y.l;
+  res.h = x.h + y.h;
+  if (res.l < x.l) res.h++;
+  return res;
+}
+
+/* Subtraction */
+static int64 I64_sub(int64 x, int64 y)
+{
+  int64 res;
+  res.l = x.l - y.l;
+  res.h = x.h - y.h;
+  if (x.l < y.l) res.h--;
+  return res;
+}
+
+/* Multiplication */
+static int64 I64_mul(int64 x, int64 y)
+{
+  int64 res;
+  uint32 prod00 = (x.l & 0xFFFF) * (y.l & 0xFFFF);
+  uint32 prod10 = (x.l >> 16) * (y.l & 0xFFFF);
+  uint32 prod01 = (x.l & 0xFFFF) * (y.l >> 16);
+  uint32 prod11 = (x.l >> 16) * (y.l >> 16);
+  res.l = prod00;
+  res.h = prod11 + (prod01 >> 16) + (prod10 >> 16);
+  prod01 = prod01 << 16; res.l += prod01; if (res.l < prod01) res.h++;
+  prod10 = prod10 << 16; res.l += prod10; if (res.l < prod10) res.h++;
+  res.h += x.l * y.h + x.h * y.l;
+  return res;
+}
+
+#define I64_is_zero(x) (((x).l | (x).h) == 0)
+
+#define I64_is_negative(x) ((int32) (x).h < 0)
+
+/* Bitwise operations */
+static int64 I64_and(int64 x, int64 y)
+{
+  int64 res;
+  res.l = x.l & y.l;
+  res.h = x.h & y.h;
+  return res;
+}
+
+static int64 I64_or(int64 x, int64 y)
+{
+  int64 res;
+  res.l = x.l | y.l;
+  res.h = x.h | y.h;
+  return res;
+}
+
+static int64 I64_xor(int64 x, int64 y)
+{
+  int64 res;
+  res.l = x.l ^ y.l;
+  res.h = x.h ^ y.h;
+  return res;
+}
+
+/* Shifts */
+static int64 I64_lsl(int64 x, int s)
+{
+  int64 res;
+  s = s & 63;
+  if (s == 0) return x;
+  if (s < 32) {
+    res.l = x.l << s;
+    res.h = (x.h << s) | (x.l >> (32 - s));
+  } else {
+    res.l = 0;
+    res.h = x.l << (s - 32);
+  }
+  return res;
+}
+
+static int64 I64_lsr(int64 x, int s)
+{
+  int64 res;
+  s = s & 63;
+  if (s == 0) return x;
+  if (s < 32) {
+    res.l = (x.l >> s) | (x.h << (32 - s));
+    res.h = x.h >> s;
+  } else {
+    res.l = x.h >> (s - 32);
+    res.h = 0;
+  }
+  return res;
+}
+
+static int64 I64_asr(int64 x, int s)
+{
+  int64 res;
+  s = s & 63;
+  if (s == 0) return x;
+  if (s < 32) {
+    res.l = (x.l >> s) | (x.h << (32 - s));
+    res.h = (int32) x.h >> s;
+  } else {
+    res.l = (int32) x.h >> (s - 32);
+    res.h = (int32) x.h >> 31;
+  }
+  return res;
+}
+
+/* Division and modulus */
+
+#define I64_SHL1(x) x.h = (x.h << 1) | (x.l >> 31); x.l <<= 1
+#define I64_SHR1(x) x.l = (x.l >> 1) | (x.h << 31); x.h >>= 1
+
+static void I64_udivmod(uint64 modulus, uint64 divisor,
+                        uint64 * quo, uint64 * mod)
+{
+  int64 quotient, mask;
+  int cmp;
+
+  quotient.h = 0; quotient.l = 0;
+  mask.h = 0; mask.l = 1;
+  while ((int32) divisor.h >= 0) {
+    cmp = I64_ucompare(divisor, modulus);
+    I64_SHL1(divisor);
+    I64_SHL1(mask);
+    if (cmp >= 0) break;
+  }
+  while (mask.l | mask.h) {
+    if (I64_ucompare(modulus, divisor) >= 0) {
+      quotient.h |= mask.h; quotient.l |= mask.l;
+      modulus = I64_sub(modulus, divisor);
+    }
+    I64_SHR1(mask);
+    I64_SHR1(divisor);
+  }
+  *quo = quotient;
+  *mod = modulus;
+}
+
+static int64 I64_div(int64 x, int64 y)
+{
+  int64 q, r;
+  int32 sign;
+
+  sign = x.h ^ y.h;
+  if ((int32) x.h < 0) x = I64_neg(x);
+  if ((int32) y.h < 0) y = I64_neg(y);
+  I64_udivmod(x, y, &q, &r);
+  if (sign < 0) q = I64_neg(q);
+  return q;
+}
+
+static int64 I64_mod(int64 x, int64 y)
+{
+  int64 q, r;
+  int32 sign;
+
+  sign = x.h;
+  if ((int32) x.h < 0) x = I64_neg(x);
+  if ((int32) y.h < 0) y = I64_neg(y);
+  I64_udivmod(x, y, &q, &r);
+  if (sign < 0) r = I64_neg(r);
+  return r;
+}
+
+/* Coercions */
+
+static int64 I64_of_int32(int32 x)
+{
+  int64 res;
+  res.l = x;
+  res.h = x >> 31;
+  return res;
+}
+
+#define I64_to_int32(x) ((int32) (x).l)
+
+/* Note: we assume sizeof(intnat) = 4 here, which is true otherwise
+   autoconfiguration would have selected native 64-bit integers */
+#define I64_of_intnat I64_of_int32
+#define I64_to_intnat I64_to_int32
+
+static double I64_to_double(int64 x)
+{
+  double res;
+  int32 sign = x.h;
+  if (sign < 0) x = I64_neg(x);
+  res = ldexp((double) x.h, 32) + x.l;
+  if (sign < 0) res = -res;
+  return res;
+}
+
+static int64 I64_of_double(double f)
+{
+  int64 res;
+  double frac, integ;
+  int neg;
+
+  neg = (f < 0);
+  f = fabs(f);
+  frac = modf(ldexp(f, -32), &integ);
+  res.h = (uint32) integ;
+  res.l = (uint32) ldexp(frac, 32);
+  if (neg) res = I64_neg(res);
+  return res;
+}
+
+#endif /* CAML_INT64_EMUL_H */
diff --git a/kernel/byterun/int64_native.h b/kernel/byterun/int64_native.h
new file mode 100644
index 000000000..2341e9989
--- /dev/null
+++ b/kernel/byterun/int64_native.h
@@ -0,0 +1,50 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Objective Caml                            */
+/*                                                                     */
+/*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         */
+/*                                                                     */
+/*  Copyright 2002 Institut National de Recherche en Informatique et   */
+/*  en Automatique.  All rights reserved.  This file is distributed    */
+/*  under the terms of the GNU Library General Public License, with    */
+/*  the special exception on linking described in file ../LICENSE.     */
+/*                                                                     */
+/***********************************************************************/
+
+/* $Id: int64_native.h,v 1.5 2005/09/22 14:21:50 xleroy Exp $ */
+
+/* Wrapper macros around native 64-bit integer arithmetic,
+   so that it has the same interface as the software emulation
+   provided in int64_emul.h */
+
+#ifndef CAML_INT64_NATIVE_H
+#define CAML_INT64_NATIVE_H
+
+#define I64_literal(hi,lo) ((int64)(hi) << 32 | (lo))
+#define I64_compare(x,y) (((x) > (y)) - ((x) < (y)))
+#define I64_ult(x,y) ((uint64)(x) < (uint64)(y))
+#define I64_neg(x) (-(x))
+#define I64_add(x,y) ((x) + (y))
+#define I64_sub(x,y) ((x) - (y))
+#define I64_mul(x,y) ((x) * (y))
+#define I64_is_zero(x) ((x) == 0)
+#define I64_is_negative(x) ((x) < 0)
+#define I64_div(x,y) ((x) / (y))
+#define I64_mod(x,y) ((x) % (y))
+#define I64_udivmod(x,y,quo,rem) \
+  (*(rem) = (uint64)(x) % (uint64)(y), \
+   *(quo) = (uint64)(x) / (uint64)(y))
+#define I64_and(x,y) ((x) & (y))
+#define I64_or(x,y) ((x) | (y))
+#define I64_xor(x,y) ((x) ^ (y))
+#define I64_lsl(x,y) ((x) << (y))
+#define I64_asr(x,y) ((x) >> (y))
+#define I64_lsr(x,y) ((uint64)(x) >> (y))
+#define I64_to_intnat(x) ((intnat) (x))
+#define I64_of_intnat(x) ((intnat) (x))
+#define I64_to_int32(x) ((int32) (x))
+#define I64_of_int32(x) ((int64) (x))
+#define I64_to_double(x) ((double)(x))
+#define I64_of_double(x) ((int64)(x))
+
+#endif /* CAML_INT64_NATIVE_H */
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index a9b16f29c..ee8cb1eea 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -17,6 +17,7 @@ type structured_constant =
   | Const_b0 of tag                
   | Const_bn of tag * structured_constant array
 
+
 type reloc_table = (tag * int) array 
 
 type annot_switch = 
@@ -63,6 +64,40 @@ type instruction =
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
+(* spiwack: instructions concerning integers *)
+  | Kbranch of Label.t                  (* jump to label *)
+  | Kaddint31                           (* adds the int31 in the accu 
+                                           and the one ontop of the stack *)
+  | Kaddcint31                          (* makes the sum and keeps the carry *)
+  | Kaddcarrycint31                     (* sum +1, keeps the carry *)
+  | Ksubint31                           (* subtraction modulo *)
+  | Ksubcint31                          (* subtraction, keeps the carry *)
+  | Ksubcarrycint31                      (* subtraction -1, keeps the carry *)
+  | Kmulint31                           (* multiplication modulo *)
+  | Kmulcint31                          (* multiplication, result in two
+					   int31, for exact computation *)
+  | Kdiv21int31                          (* divides a double size integer
+                                           (represented by an int31 in the 
+					   accumulator and one on the top of 
+					   the stack) by an int31. The result
+					   is a pair of the quotient and the 
+					   rest.
+					   If the divisor is 0, it returns
+					   0. *)
+  | Kdivint31                           (* euclidian division (returns a pair
+					   quotient,rest) *)
+  | Kaddmuldivint31                     (* generic operation for shifting and
+					   cycling. Takes 3 int31 i j and s,
+					   and returns x*2^s+y/(2^(31-s) *)
+  | Kcompareint31                        (* unsigned comparison of int31
+					   cf COMPAREINT31 in 
+					   kernel/byterun/coq_interp.c
+					   for more info *)
+  | Kisconst of Label.t                 (* conditional jump *)
+  | Kareconst of int*Label.t            (* conditional jump *)
+  | Kcompint31                          (* dynamic compilation of int31 *)
+  | Kdecompint31                        (* dynamic decompilation of int31 *)
+(* /spiwack *)
 
 and bytecodes = instruction list
 
@@ -70,6 +105,31 @@ type fv_elem = FVnamed of identifier | FVrel of int
 
 type fv = fv_elem array
 
+(* spiwack: this exception is expected to be raised by function expecting
+            closed terms. *)
+exception NotClosed
+
+
+(*spiwack: both type have been moved from Cbytegen because I needed then
+  for the retroknowledge *)
+type vm_env = {
+    size : int;              (* longueur de la liste [n] *)
+    fv_rev : fv_elem list    (* [fvn; ... ;fv1] *)
+  }    
+   
+   
+type comp_env = { 
+    nb_stack : int;              (* nbre de variables sur la pile          *)
+    in_stack : int list;         (* position dans la pile                  *)
+    nb_rec : int;                (* nbre de fonctions mutuellement         *)
+                                 (* recursives =  nbr                      *)
+    pos_rec  : instruction list; (* instruction d'acces pour les variables *)
+                                 (*  de point fix ou de cofix              *)
+    offset : int;                 
+    in_env : vm_env ref 
+  } 
+
+
 
 (* --- Pretty print *)
 open Format
@@ -123,6 +183,27 @@ let rec instruction ppf = function
   | Kstop -> fprintf ppf "\tstop"
   | Ksequence (c1,c2) ->
       fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 
+(* spiwack *)
+  | Kbranch lbl -> fprintf ppf "\tbranch %i" lbl
+  | Kaddint31 -> fprintf ppf "\taddint31"
+  | Kaddcint31 -> fprintf ppf "\taddcint31"
+  | Kaddcarrycint31 -> fprintf ppf "\taddcarrycint31"
+  | Ksubint31 -> fprintf ppf "\tsubint31"
+  | Ksubcint31 -> fprintf ppf "\tsubcint31"
+  | Ksubcarrycint31 -> fprintf ppf "\tsubcarrycint31"
+  | Kmulint31 -> fprintf ppf "\tmulint31"
+  | Kmulcint31 -> fprintf ppf "\tmulcint31"
+  | Kdiv21int31 -> fprintf ppf "\tdiv21int31"
+  | Kdivint31 -> fprintf ppf "\tdivint31"
+  | Kcompareint31 -> fprintf ppf "\tcompareint31"
+  | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31"
+  | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl
+  | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
+  | Kcompint31 -> fprintf ppf "\tcompint31"
+  | Kdecompint31 -> fprintf ppf "\tdecompint"
+
+(* /spiwack *)
+
 
 and instruction_list ppf = function
     [] -> ()
@@ -130,6 +211,26 @@ and instruction_list ppf = function
       fprintf ppf "L%i:%a" lbl instruction_list il
   | instr :: il ->
       fprintf ppf "%a@ %a" instruction instr instruction_list il
+
+
+(*spiwack: moved this type in this file  because I needed it for 
+  retroknowledge which can't depend from cbytegen *)
+type block = 
+  | Bconstr of constr
+  | Bstrconst of structured_constant
+  | Bmakeblock of int * block array
+  | Bconstruct_app of int * int * int * block array
+                  (* tag , nparams, arity *)
+  | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
+                (* spiwack: compilation given by a function *)
+                (* compilation function (see get_vm_constant_dynamic_info in 
+                   retroknowledge.mli for more info) , argument array  *)
+
+
  
 let draw_instr c =
   fprintf std_formatter "@[<v 0>%a@]" instruction_list c
+
+let string_of_instr c =
+  fprintf str_formatter "@[<v 0>%a@]" instruction_list c;
+  flush_str_formatter ()
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 215b6ad4a..a2d4f7e01 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -61,6 +61,40 @@ type instruction =
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
+(* spiwack: instructions concerning integers *)
+  | Kbranch of Label.t                  (* jump to label, is it needed ? *)
+  | Kaddint31                           (* adds the int31 in the accu 
+                                           and the one ontop of the stack *)
+  | Kaddcint31                          (* makes the sum and keeps the carry *)
+  | Kaddcarrycint31                     (* sum +1, keeps the carry *)
+  | Ksubint31                           (* subtraction modulo *)
+  | Ksubcint31                          (* subtraction, keeps the carry *)
+  | Ksubcarrycint31                     (* subtraction -1, keeps the carry *)
+  | Kmulint31                           (* multiplication modulo *)
+  | Kmulcint31                          (* multiplication, result in two
+					   int31, for exact computation *)
+  | Kdiv21int31                         (* divides a double size integer
+                                           (represented by an int31 in the 
+					   accumulator and one on the top of 
+					   the stack) by an int31. The result
+					   is a pair of the quotient and the 
+					   rest.
+					   If the divisor is 0, it returns
+					   0. *)
+  | Kdivint31                           (* euclidian division (returns a pair
+					   quotient,rest) *)
+  | Kaddmuldivint31                     (* generic operation for shifting and
+					   cycling. Takes 3 int31 i j and s,
+					   and returns x*2^s+y/(2^(31-s) *)
+  | Kcompareint31                        (* unsigned comparison of int31
+					   cf COMPAREINT31 in 
+					   kernel/byterun/coq_interp.c
+					   for more info *)
+  | Kisconst of Label.t                 (* conditional jump *)
+  | Kareconst of int*Label.t            (* conditional jump *)
+  | Kcompint31                          (* dynamic compilation of int31 *)
+  | Kdecompint31                        (* dynamix decompilation of int31 *)
+(* /spiwack *)
 
 
 and bytecodes = instruction list
@@ -69,5 +103,43 @@ type fv_elem = FVnamed of identifier | FVrel of int
 
 type fv = fv_elem array
 
+
+(* spiwack: this exception is expected to be raised by function expecting
+            closed terms. *)
+exception NotClosed
+
+(*spiwack: both type have been moved from Cbytegen because I needed then
+  for the retroknowledge *)
+type vm_env = {
+    size : int;              (* longueur de la liste [n] *)
+    fv_rev : fv_elem list    (* [fvn; ... ;fv1] *)
+  }    
+   
+   
+type comp_env = { 
+    nb_stack : int;              (* nbre de variables sur la pile          *)
+    in_stack : int list;         (* position dans la pile                  *)
+    nb_rec : int;                (* nbre de fonctions mutuellement         *)
+                                 (* recursives =  nbr                      *)
+    pos_rec  : instruction list; (* instruction d'acces pour les variables *)
+                                 (*  de point fix ou de cofix              *)
+    offset : int;                 
+    in_env : vm_env ref 
+  } 
+
 val draw_instr : bytecodes -> unit
 
+val string_of_instr : bytecodes -> string
+
+
+
+(*spiwack: moved this here because I needed it for retroknowledge *)
+type block = 
+  | Bconstr of constr
+  | Bstrconst of structured_constant
+  | Bmakeblock of int * block array
+  | Bconstruct_app of int * int * int * block array
+                  (* tag , nparams, arity *)
+  | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
+                (* compilation function (see get_vm_constant_dynamic_info in 
+                   retroknowledge.mli for more info) , argument array  *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index e1f89fadb..2664abe1f 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -83,24 +83,9 @@ open Pre_env
    
 (* On conserve la fct de cofix pour la conversion                         *)
    
-type vm_env = {
-    size : int;              (* longueur de la liste [n] *)
-    fv_rev : fv_elem list    (* [fvn; ... ;fv1] *)
-  }    
-   
+    
 let empty_fv = { size= 0;  fv_rev = [] }
-   
-type comp_env = { 
-    nb_stack : int;              (* nbre de variables sur la pile          *)
-    in_stack : int list;         (* position dans la pile                  *)
-    nb_rec : int;                (* nbre de fonctions mutuellement         *)
-                                 (* recursives =  nbr                      *)
-    pos_rec  : instruction list; (* instruction d'acces pour les variables *)
-                                 (*  de point fix ou de cofix              *)
-    offset : int;                 
-    in_env : vm_env ref 
-  } 
-
+  
 let fv r = !(r.in_env)
    
 let empty_comp_env ()= 
@@ -231,17 +216,40 @@ let rec discard_dead_code cont = cont
 
 let label_code = function
   | Klabel lbl :: _ as cont -> (lbl, cont)
+  | Kbranch lbl :: _ as cont -> (lbl, cont)
   | cont -> let lbl = Label.create() in (lbl, Klabel lbl :: cont)
 
 (* Return a branch to the continuation. That is, an instruction that,
    when executed, branches to the continuation or performs what the
    continuation performs. We avoid generating branches to returns. *)
-
+(* spiwack: make_branch was only used once. Changed it back to the ZAM
+      one to match the appropriate semantics (old one avoided the 
+      introduction of an unconditional branch operation, which seemed
+      appropriate for the 31-bit integers' code). As a memory, I leave
+      the former version in this comment.
 let make_branch cont =
   match cont with
   | (Kreturn _ as return) :: cont' -> return, cont'
   | Klabel lbl as b :: _ -> b, cont
   | _ -> let b = Klabel(Label.create()) in b,b::cont
+*)
+
+let rec make_branch_2 lbl n cont =
+  function
+    Kreturn m :: _ -> (Kreturn (n + m), cont)
+  | Klabel _ :: c  -> make_branch_2 lbl n cont c
+  | Kpop m :: c    -> make_branch_2 lbl (n + m) cont c
+  | _              ->
+      match lbl with
+        Some lbl -> (Kbranch lbl, cont)
+      | None     -> let lbl = Label.create() in (Kbranch lbl, Klabel lbl :: cont)
+
+let make_branch cont =
+  match cont with
+    (Kbranch _ as branch) :: _ -> (branch, cont)
+  | (Kreturn _ as return) :: _ -> (return, cont)
+  | Klabel lbl :: _ -> make_branch_2 (Some lbl) 0 cont cont
+  | _ ->  make_branch_2 (None) 0 cont cont
 
 (* Check if we're in tailcall position *)
 
@@ -315,52 +323,105 @@ let code_construct tag nparams arity cont =
     fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)];
     Kclosure(lbl,0) :: cont
 
-type block = 
-  | Bconstr of constr
-  | Bstrconst of structured_constant
-  | Bmakeblock of int * block array
-  | Bconstruct_app of int * int * int * block array
-                  (* tag , nparams, arity *)
-
 let get_strcst = function
   | Bstrconst sc -> sc
   | _ -> raise Not_found 
 
-let rec str_const c =
+
+let rec str_const c = 
   match kind_of_term c with
   | Sort s -> Bstrconst (Const_sorts s)
   | Cast(c,_,_) -> str_const c 
   | App(f,args) -> 
       begin
 	match kind_of_term f with
-	| Construct((kn,j),i) -> 
+	| Construct(((kn,j),i) as cstr) -> 
+            begin
 	    let oib = lookup_mind kn !global_env in
 	    let oip = oib.mind_packets.(j) in
 	    let num,arity = oip.mind_reloc_tbl.(i-1) in
 	    let nparams = oib.mind_nparams in
 	    if nparams + arity = Array.length args then
-	      if arity = 0 then Bstrconst(Const_b0 num)
-	      else
-		let rargs = Array.sub args nparams arity in
-		let b_args = Array.map str_const rargs in
-		try 
-		  let sc_args = Array.map get_strcst b_args in
-		  Bstrconst(Const_bn(num, sc_args))
-		with Not_found ->
-		  Bmakeblock(num,b_args)
+              (* spiwack: *)
+              (* 1/ tries to compile the constructor in an optimal way,
+                    it is supposed to work only if the arguments are
+                    all fully constructed, fails with Cbytecodes.NotClosed. 
+                    it can also raise Not_found when there is no special
+                    treatment for this constructor 
+                    for instance: tries to to compile an integer of the 
+                        form I31 D1 D2 ... D31 to [D1D2...D31] as 
+                        a processor number (a caml number actually) *)
+              try 
+		try
+		  Bstrconst (Retroknowledge.get_vm_constant_static_info 
+                                              (!global_env).retroknowledge
+                                              (kind_of_term f) args)
+                with NotClosed ->
+		  (* 2/ if the arguments are not all closed (this is 
+                        expectingly (and it is currently the case) the only 
+                        reason why this exception is raised) tries to 
+                        give a clever, run-time behavior to the constructor.
+                        Raises Not_found if there is no special treatment
+                        for this integer.
+                        this is done in a lazy fashion, using the constructor
+                        Bspecial because it needs to know the continuation
+                        and such, which can't be done at this time.
+                        for instance, for int31: if one of the digit is 
+                            not closed, it's not impossible that the number
+                            gets fully instanciated at run-time, thus to ensure
+                            uniqueness of the representation in the vm
+                            it is necessary to try and build a caml integer 
+                            during the execution *)
+		  let rargs = Array.sub args nparams arity in
+		  let b_args = Array.map str_const rargs in
+		  Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
+                                           (!global_env).retroknowledge
+                                           (kind_of_term f)),
+                           b_args)
+              with Not_found ->
+		(* 3/ if no special behavior is available, then the compiler
+		      falls back to the normal behavior *)
+		if arity = 0 then Bstrconst(Const_b0 num)
+		else
+		  let rargs = Array.sub args nparams arity in
+		  let b_args = Array.map str_const rargs in
+		  try 
+		    let sc_args = Array.map get_strcst b_args in
+		    Bstrconst(Const_bn(num, sc_args))
+		  with Not_found ->
+		    Bmakeblock(num,b_args)
 	    else  
-	      let b_args = Array.map str_const args in
-	      Bconstruct_app(num, nparams, arity, b_args)
+              let b_args = Array.map str_const args in
+	     (* spiwack: tries first to apply the run-time compilation
+                behavior of the constructor, as in 2/ above *)
+	      try 
+		Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
+                                           (!global_env).retroknowledge
+                                           (kind_of_term f)),
+                         b_args)
+	      with Not_found ->
+	        Bconstruct_app(num, nparams, arity, b_args)
+              end
 	| _ -> Bconstr c
       end
   | Ind ind -> Bstrconst (Const_ind ind)
-  | Construct ((kn,j),i) ->  
-      let oib = lookup_mind kn !global_env in 
-      let oip = oib.mind_packets.(j) in
-      let num,arity = oip.mind_reloc_tbl.(i-1) in
-      let nparams = oib.mind_nparams in
-      if nparams + arity = 0 then Bstrconst(Const_b0 num)
-      else Bconstruct_app(num,nparams,arity,[||])
+  | Construct ((kn,j),i as cstr) ->  
+      begin
+      (* spiwack: tries first to apply the run-time compilation 
+           behavior of the constructor, as in 2/ above *)
+      try
+	Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
+                                           (!global_env).retroknowledge
+                                           (kind_of_term c)),
+                         [| |])
+      with Not_found ->
+	let oib = lookup_mind kn !global_env in 
+	let oip = oib.mind_packets.(j) in
+	let num,arity = oip.mind_reloc_tbl.(i-1) in
+	let nparams = oib.mind_nparams in
+	if nparams + arity = 0 then Bstrconst(Const_b0 num)
+	else Bconstruct_app(num,nparams,arity,[||])
+      end
   | _ -> Bconstr c
 
 (* compilation des applications *)
@@ -413,6 +474,7 @@ let rec get_allias env kn =
   | BCallias kn' -> get_allias env kn'
   | _ -> kn
 
+  
 (* compilation des expressions *)
  
 let rec compile_constr reloc c sz cont =
@@ -424,8 +486,7 @@ let rec compile_constr reloc c sz cont =
 
   | Rel i -> pos_rel i reloc sz :: cont
   | Var id -> pos_named id reloc :: cont
-  | Const kn -> Kgetglobal (get_allias !global_env kn) :: cont
-  
+  | Const kn -> compile_const reloc kn [||] sz cont
   | Sort _  | Ind _ | Construct _ ->
       compile_str_cst reloc (str_const c) sz cont
   
@@ -452,6 +513,7 @@ let rec compile_constr reloc c sz cont =
       begin 
 	match kind_of_term f with
 	| Construct _ -> compile_str_cst reloc (str_const c) sz cont
+        | Const kn -> compile_const reloc kn args sz cont
 	| _ -> comp_app compile_constr compile_constr reloc f args sz cont 
       end
   | Fix ((rec_args,init),(_,type_bodies,rec_bodies)) ->
@@ -569,11 +631,19 @@ let rec compile_constr reloc c sz cont =
       done;
       c :=  Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
       let code_sw = 
-	match branch1 with
-	| Klabel lbl -> Kpush_retaddr lbl ::  !c
+ 	match branch1 with 
+        (* spiwack : branch1 can't be a lbl anymore it's a Branch instead 
+	| Klabel lbl -> Kpush_retaddr lbl ::  !c *)
+        | Kbranch lbl -> Kpush_retaddr lbl ::  !c
 	| _ -> !c 
       in
-      compile_constr reloc a sz code_sw
+      compile_constr reloc a sz 
+      (try 
+	let entry = Term.Ind ind in
+	Retroknowledge.get_vm_before_match_info (!global_env).retroknowledge
+	                                       entry code_sw
+      with Not_found ->
+	code_sw)
        
 and compile_str_cst reloc sc sz cont =
   match sc with
@@ -588,6 +658,40 @@ and compile_str_cst reloc sc sz cont =
 	comp_app 
 	  (fun _ _ _ cont -> code_construct tag nparams arity cont) 
 	  compile_str_cst reloc () args sz cont
+  | Bspecial (comp_fx, args) -> comp_fx reloc args sz cont
+
+
+(* spiwack : compilation of constants with their arguments. 
+   Makes a special treatment with 31-bit integer addition *)
+and compile_const =
+  let code_construct kn cont = 
+     let f_cont = 
+         let else_lbl = Label.create () in
+         Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
+          Kaddint31:: Kreturn 0:: Klabel else_lbl::
+         (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
+          Kgetglobal (get_allias !global_env kn)::
+          Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
+     in
+     let lbl = Label.create () in 
+     fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)];
+     Kclosure(lbl, 0)::cont
+  in
+  fun reloc-> fun  kn -> fun args -> fun sz -> fun cont ->
+  let nargs = Array.length args in
+  (* spiwack: checks if there is a specific way to compile the constant
+              if there is not, Not_found is raised, and the function
+              falls back on its normal behavior *)
+  try
+    Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge
+                  (kind_of_term (mkConst kn)) reloc args sz cont
+  with Not_found -> 
+    if nargs = 0 then
+      Kgetglobal (get_allias !global_env kn) :: cont
+    else
+      comp_app (fun _ _ _ cont -> 
+                   Kgetglobal (get_allias !global_env kn) :: cont)
+        compile_constr reloc () args sz cont
       
 let compile env c =
   set_global_env env;
@@ -625,3 +729,138 @@ let compile_constant_body env body opaque boxed =
 	    let to_patch = to_memory res in
 	    BCdefined (false, to_patch)
 
+
+(* spiwack: additional function which allow different part of compilation of the
+      31-bit integers *)
+
+let make_areconst n else_lbl cont =
+  if n <=0 then
+    cont
+  else
+    Kareconst (n, else_lbl)::cont
+
+
+(* try to compile int31 as a const_b0. Succeed if all the arguments are closed
+   fails otherwise by raising NotClosed*)
+let compile_structured_int31 fc args =
+  if not fc then raise Not_found else 
+  Const_b0
+    (Array.fold_left 
+       (fun temp_i -> fun t -> match kind_of_term t with
+          | Construct (_,d) -> 2*temp_i+d-1
+          | _ -> raise NotClosed)
+       0 args
+    )
+
+(* this function is used for the compilation of the constructor of
+   the int31, it is used when it appears not fully applied, or 
+   applied to at least one non-closed digit *)
+let dynamic_int31_compilation fc reloc args sz cont =
+  if not fc then raise Not_found else
+    let nargs = Array.length args in
+      if nargs = 31 then
+	let (escape,labeled_cont) = make_branch cont in
+	let else_lbl = Label.create() in
+	  comp_args compile_str_cst reloc args sz 
+            ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont)
+      else 
+	let code_construct cont = (* spiwack: variant of the global code_construct
+                                     which handles dynamic compilation of 
+                                     integers *)
+          let f_cont = 
+            let else_lbl = Label.create () in
+	      [Kacc 0; Kpop 1; Kisconst else_lbl; Kareconst(30,else_lbl);
+               Kcompint31; Kreturn 0; Klabel else_lbl; Kmakeblock(31, 1); Kreturn 0]
+	  in 
+	  let lbl = Label.create() in
+	    fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)];
+	    Kclosure(lbl,0) :: cont
+	in 
+	  if nargs = 0 then
+	    code_construct cont
+	  else
+	    comp_app (fun _ _ _ cont -> code_construct cont)
+              compile_str_cst reloc () args sz cont
+       
+(*(* template compilation for 2ary operation, it probably possible
+   to make a generic such function with arity abstracted *)
+let op2_compilation op =
+  let code_construct normal cont =  (*kn cont =*)
+     let f_cont = 
+         let else_lbl = Label.create () in
+         Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
+          op:: Kreturn 0:: Klabel else_lbl::
+         (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
+          (*Kgetglobal (get_allias !global_env kn):: *)
+          normal::
+          Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
+     in
+     let lbl = Label.create () in 
+     fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)];
+     Kclosure(lbl, 0)::cont
+  in
+  fun normal fc _ reloc args sz cont ->
+  if not fc then raise Not_found else
+  let nargs = Array.length args in
+  if nargs=2 then (*if it is a fully applied addition*)
+    let (escape, labeled_cont) = make_branch cont in
+    let else_lbl = Label.create () in
+      comp_args compile_constr reloc args sz 
+	(Kisconst else_lbl::(make_areconst 1  else_lbl 
+           (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
+           (op::escape::Klabel else_lbl::Kpush::
+           (* works as comp_app with nargs = 2 and non-tailcall cont*)
+           (*Kgetglobal (get_allias !global_env kn):: *)
+           normal::
+           Kapply 2::labeled_cont)))
+  else if nargs=0 then
+    code_construct normal cont
+  else
+    comp_app (fun _ _ _ cont -> code_construct normal cont)
+      compile_constr reloc () args sz cont *)
+
+(*template for n-ary operation, invariant: n>=1,
+  the operations does the following : 
+  1/ checks if all the arguments are constants (i.e. non-block values) 
+  2/ if they are, uses the "op" instruction to execute
+  3/ if at least one is not, branches to the normal behavior: 
+      Kgetglobal (get_allias !global_env kn) *)
+let op_compilation n op =
+  let code_construct kn cont = 
+     let f_cont = 
+         let else_lbl = Label.create () in
+         Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
+          op:: Kreturn 0:: Klabel else_lbl::
+         (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
+          Kgetglobal (get_allias !global_env kn)::
+          Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *)
+     in
+     let lbl = Label.create () in 
+     fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)];
+     Kclosure(lbl, 0)::cont
+  in
+  fun kn fc reloc args sz cont ->
+  if not fc then raise Not_found else
+  let nargs = Array.length args in
+  if nargs=n then (*if it is a fully applied addition*)
+    let (escape, labeled_cont) = make_branch cont in
+    let else_lbl = Label.create () in
+      comp_args compile_constr reloc args sz 
+	(Kisconst else_lbl::(make_areconst (n-1) else_lbl 
+           (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
+           (op::escape::Klabel else_lbl::Kpush::
+           (* works as comp_app with nargs = n and non-tailcall cont*)
+           Kgetglobal (get_allias !global_env kn)::
+           Kapply n::labeled_cont)))
+  else if nargs=0 then
+    code_construct kn cont
+  else
+    comp_app (fun _ _ _ cont -> code_construct kn cont)
+      compile_constr reloc () args sz cont
+
+let int31_escape_before_match fc cont =
+  if not fc then
+    raise Not_found
+  else
+    let escape_lbl, labeled_cont = label_code cont in
+      (Kisconst escape_lbl)::Kdecompint31::labeled_cont
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index f761e4f60..829ac46e2 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -6,7 +6,6 @@ open Declarations
 open Pre_env
 
 
-
 val compile : env -> constr -> bytecodes * bytecodes * fv
                               (* init, fun, fv *)
 
@@ -15,3 +14,28 @@ val compile_constant_body :
                                  (* opaque *) (* boxed *)
 
 
+(* arnaud : a commenter *)
+(* spiwack: this function contains the information needed to perform
+            the static compilation of int31 (trying and obtaining
+            a 31-bit integer in processor representation at compile time) *)
+val compile_structured_int31 : bool -> constr array -> 
+                               structured_constant
+
+(* this function contains the information needed to perform
+        the dynamic compilation of int31 (trying and obtaining a
+        31-bit integer in processor representation at runtime when
+        it failed at compile time *)
+val dynamic_int31_compilation : bool -> comp_env -> 
+                                block array -> 
+                                int -> bytecodes -> bytecodes
+
+(*spiwack: template for the compilation n-ary operation, invariant: n>=1.
+           works as follow: checks if all the arguments are non-pointers
+           if they are applies the operation (second argument) if not
+           all of them are, returns to a coq definition (third argument) *)
+val op_compilation : int -> instruction -> constant -> bool -> comp_env ->
+                             constr array -> int -> bytecodes-> bytecodes
+
+(*spiwack: compiling function to insert dynamic decompilation before 
+           matching integers (in case they are in processor representation) *)
+val int31_escape_before_match : bool -> bytecodes -> bytecodes
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 1b6d8923e..dffb0f2d5 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -111,7 +111,10 @@ let out_label_with_orig orig lbl =
     Label_defined def ->
       out_int((def - orig) asr 2)
   | Label_undefined patchlist ->
-      if patchlist = [] then
+      (* spiwack: patchlist is supposed to be non-empty all the time
+         thus I commented that out. If there is no problem I suggest
+         removing it for next release (cur: 8.1) *)
+      (*if patchlist = [] then *)
 	(!label_table).(lbl) <-
           Label_undefined((!out_position, orig) :: patchlist);
       out_int 0
@@ -222,9 +225,28 @@ let emit_instr = function
   | Ksetfield n ->
       if n <= 1 then out (opSETFIELD0+n) 
       else (out opSETFIELD;out_int n)
+  | Ksequence _ -> raise (Invalid_argument "Cemitcodes.emit_instr")
+  (* spiwack *)
+  | Kbranch lbl -> out opBRANCH; out_label lbl
+  | Kaddint31 -> out opADDINT31
+  | Kaddcint31 -> out opADDCINT31
+  | Kaddcarrycint31 -> out opADDCARRYCINT31
+  | Ksubint31 -> out opSUBINT31
+  | Ksubcint31 -> out opSUBCINT31
+  | Ksubcarrycint31 -> out opSUBCARRYCINT31
+  | Kmulint31 -> out opMULINT31
+  | Kmulcint31 -> out opMULCINT31
+  | Kdiv21int31 -> out opDIV21INT31
+  | Kdivint31 -> out opDIVINT31
+  | Kaddmuldivint31 -> out opADDMULDIVINT31
+  | Kcompareint31 -> out opCOMPAREINT31
+  | Kisconst lbl -> out opISCONST; out_label lbl
+  | Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl
+  | Kcompint31 -> out opCOMPINT31
+  | Kdecompint31 -> out opDECOMPINT31
+  (*/spiwack *)
   | Kstop -> 
       out opSTOP
-  | Ksequence _ -> raise (Invalid_argument "Cemitcodes.emit_instr")
 
 (* Emission of a list of instructions. Include some peephole optimization. *)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 1be251a50..eb49ba620 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -285,5 +285,6 @@ and module_body =
       mod_user_type : module_type_body option;
       mod_type : module_type_body;
       mod_equiv : module_path option;
-      mod_constraints : constraints }
+      mod_constraints : constraints;
+      mod_retroknowledge : Retroknowledge.action list}
 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 7f7f7dcc3..2f32d8639 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -218,7 +218,8 @@ and module_body =
       mod_user_type : module_type_body option;
       mod_type : module_type_body;
       mod_equiv : module_path option;
-      mod_constraints : constraints }
+      mod_constraints : constraints;
+      mod_retroknowledge : Retroknowledge.action list}
     (*    [type_of(mod_expr)]  <: [mod_user_type] (if given)  *)
     (*  if equiv given then constraints are empty *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a9ba253b0..683527045 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -358,6 +358,7 @@ let insert_after_hyp (ctxt,vals) id d check =
     | _, _ -> assert false
   in aux ctxt vals
 
+
 (* To be used in Logic.clear_hyps *)
 let remove_hyps ids check_context check_value (ctxt, vals) =
   let ctxt,vals,rmv = 
@@ -371,3 +372,222 @@ let remove_hyps ids check_context check_value (ctxt, vals) =
 		     ctxt vals ([],[],[])
   in ((ctxt,vals),rmv)
 
+
+
+
+
+
+(*spiwack: the following functions assemble the pieces of the retroknowledge
+   note that the "consistent" register function is available in the module
+   Safetyping, Environ only synchronizes the proactive and the reactive parts*)
+
+open Retroknowledge
+
+(* lifting of the "get" functions works also for "mem"*)
+let retroknowledge f env =
+  f env.retroknowledge
+
+let registered env field =
+    retroknowledge mem env field
+
+(* spiwack: this unregistration function is not in operation yet. It should
+            not be used *)
+(* this unregistration function assumes that no "constr" can hold two different
+   places in the retroknowledge. There is no reason why it shouldn't be true,
+   but in case someone needs it, remember to add special branches to the
+   unregister function *)
+let unregister env field =
+  match field with
+    | KInt31 (_,Int31Type) -> 
+	(*there is only one matching kind due to the fact that Environ.env
+          is abstract, and that the only function which add elements to the
+          retroknowledge is Environ.register which enforces this shape *)
+        let Ind i31t = retroknowledge find env field in 
+	let i31c = Construct (i31t, 1) in
+	  {env with retroknowledge = 
+	      remove (retroknowledge clear_info env i31c) field}
+    |_ -> {env with retroknowledge =
+	   try 
+	     remove (retroknowledge clear_info env 
+                                         (retroknowledge find env field)) field
+	   with Not_found ->
+	     retroknowledge remove env field}
+
+
+
+(* the Environ.register function syncrhonizes the proactive and reactive 
+   retroknowledge. *)
+let register =
+
+  (* subfunction used for static decompilation of int31 (after a vm_compute,
+     see pretyping/vnorm.ml for more information) *)
+  let constr_of_int31 =
+    let nth_digit_plus_one i n = (* calculates the nth (starting with 0)
+                                    digit of i and adds 1 to it 
+                                    (nth_digit_plus_one 1 3 = 2) *)
+      if (land) i ((lsl) 1 n) = 0 then
+        1
+      else
+        2
+    in
+      fun ind -> fun digit_ind -> fun tag ->
+	let array_of_int i =
+	  Array.init 31 (fun n -> mkConstruct
+			   (digit_ind, nth_digit_plus_one i (30-n)))
+	in
+	  mkApp(mkConstruct(ind, 1), array_of_int tag)
+  in
+
+  (* subfunction which adds the information bound to the constructor of
+     the int31 type to the reactive retroknowledge *)
+  let add_int31c retroknowledge c = 
+    let rk = add_vm_constant_static_info retroknowledge c 
+                                         Cbytegen.compile_structured_int31
+    in
+    add_vm_constant_dynamic_info rk c Cbytegen.dynamic_int31_compilation
+  in
+
+  (* subfunction which adds the compiling information of an
+     int31 operation which has a specific vm instruction (associates
+     it to the name of the coq definition in the reactive retroknowledge) *)
+  let add_int31_op retroknowledge v n op kn =
+    add_vm_compiling_info retroknowledge v (Cbytegen.op_compilation n op kn)
+  in
+
+fun env field value ->
+  (* subfunction which shortens the (very often use) registration of binary
+     operators to the reactive retroknowledge. *)
+  let add_int31_binop_from_const op =
+    match value with
+      | Const kn ->  retroknowledge add_int31_op env value 2 
+	                               op kn
+      | _ -> anomaly "Environ.register: should be a constant"
+  in
+  (* subfunction which completes the function constr_of_int31 above
+     by performing the actual retroknowledge operations *)
+  let add_int31_decompilation_from_type rk = 
+    (* invariant : the type of bits is registered, otherwise the function 
+       would raise Not_found. The invariant is enforced in safe_typing.ml *)
+    match field with
+      | KInt31 (grp, Int31Type) -> 
+	  (match Retroknowledge.find rk (KInt31 (grp,Int31Bits)) with
+	    | Ind i31bit_type ->  
+		(match value with 
+		  | Ind i31t -> 
+		      Retroknowledge.add_vm_decompile_constant_info rk
+		               value (constr_of_int31 i31t i31bit_type)
+		  | _ -> anomaly "Environ.register: should be an inductive type")
+	    | _ -> anomaly "Environ.register: Int31Bits should be an inductive type")
+      | _ -> anomaly "Environ.register: add_int31_decompilation_from_type called with an abnormal field"
+  in
+  {env with retroknowledge = 
+  let retroknowledge_with_reactive_info = 
+  match field with
+    | KInt31 (_, Int31Type) -> 
+        let i31c = match value with
+                     | Ind i31t -> (Construct (i31t, 1))
+		     | _ -> anomaly "Environ.register: should be an inductive type"
+	in
+	add_int31_decompilation_from_type 
+	  (add_vm_before_match_info 
+	     (retroknowledge add_int31c env i31c) 
+	     value Cbytegen.int31_escape_before_match)
+    | KInt31 (_, Int31Plus) -> add_int31_binop_from_const Cbytecodes.Kaddint31
+    | KInt31 (_, Int31PlusC) -> add_int31_binop_from_const Cbytecodes.Kaddcint31
+    | KInt31 (_, Int31PlusCarryC) -> add_int31_binop_from_const Cbytecodes.Kaddcarrycint31
+    | KInt31 (_, Int31Minus) -> add_int31_binop_from_const Cbytecodes.Ksubint31
+    | KInt31 (_, Int31MinusC) -> add_int31_binop_from_const Cbytecodes.Ksubcint31
+    | KInt31 (_, Int31MinusCarryC) -> add_int31_binop_from_const 
+	                                           Cbytecodes.Ksubcarrycint31
+    | KInt31 (_, Int31PlusC) -> add_int31_binop_from_const Cbytecodes.Kaddcint31
+    | KInt31 (_, Int31Times) -> add_int31_binop_from_const Cbytecodes.Kmulint31
+    | KInt31 (_, Int31TimesC) -> add_int31_binop_from_const Cbytecodes.Kmulcint31
+    | KInt31 (_, Int31Div21) -> (* this is a ternary operation *)
+                                (match value with
+				 | Const kn ->
+				     retroknowledge add_int31_op env value 3 
+	                               Cbytecodes.Kdiv21int31 kn
+				 | _ -> anomaly "Environ.register: should be a constant")
+    | KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31
+    | KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *)
+                                (match value with
+				 | Const kn ->
+				     retroknowledge add_int31_op env value 3 
+	                               Cbytecodes.Kaddmuldivint31 kn
+				 | _ -> anomaly "Environ.register: should be a constant")
+    | KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31
+    | _ -> env.retroknowledge
+  in
+  Retroknowledge.add_field retroknowledge_with_reactive_info field value
+  }
+
+
+(* spiwack: the following definitions are used by the function 
+   needed_assumption which gives as an output the set of all
+   axioms and sections variables on which a given term depends
+   in a context (expectingly the Global context) *)
+type assumption =
+  | Variable of identifier*constr
+  | Axiom of constant*constr
+
+module OrderedAssumption = 
+struct 
+  type t = assumption
+  let compare = compare
+end
+
+module AssumptionSet = Set.Make (OrderedAssumption)
+
+(* definition for redability purposes *)
+let ( ** ) s1 s2  = AssumptionSet.union s1 s2
+
+let rec needed_assumptions t env =   
+ (* goes recursively into the terms to see if it depends on assumptions
+    the 3 important cases are : Var _ which simply means that the term refers
+    to a section variable,
+                                Rel _ which means the term is a variable
+    which has been bound earlier by a Lambda or a Prod (returns [] )
+                                Const _ where we need to first unfold
+    the constant and return the needed assumptions of its body in the 
+    environnement *)
+  match kind_of_term t with
+    | Var id -> AssumptionSet.singleton (Variable (id,named_type id env))
+    | Meta _ | Evar _ -> assert false
+    | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) -> 
+                   (needed_assumptions e1 env)**(needed_assumptions e2 env)
+    | LetIn (_,e1,e2,e3) ->(needed_assumptions e1 env)**
+                           (needed_assumptions e2 env)**
+                           (needed_assumptions e3 env)
+    | App (e1, e_array) -> (needed_assumptions e1 env)**
+                   (Array.fold_right (fun e -> fun s -> 
+                                               (needed_assumptions e env)**s)
+                                      e_array AssumptionSet.empty)
+    | Case (_,e1,e2,e_array) -> (needed_assumptions e1 env)**
+                                (needed_assumptions e2 env)**
+                   (Array.fold_right (fun e -> fun s -> 
+                                               (needed_assumptions e env)**s)
+                                      e_array AssumptionSet.empty)
+    | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) ->
+                   Array.fold_right (fun e -> fun s -> 
+                                              (needed_assumptions e env)**s)
+                                      e1_array
+                   (Array.fold_right (fun e -> fun s -> 
+                                              (needed_assumptions e env)**s)
+                                      e2_array AssumptionSet.empty)
+    | Const kn -> 
+	let cb = lookup_constant kn env in
+        (match cb.Declarations.const_body with
+        | None -> 
+	    let ctype = 
+	      match cb.Declarations.const_type with
+		| PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+		| NonPolymorphicType t -> t
+	    in
+	    AssumptionSet.singleton (Axiom (kn,ctype))
+        | Some body -> needed_assumptions (Declarations.force body) env)
+    | _ -> AssumptionSet.empty (* closed atomic types + rel *)
+
+(* /spiwack *)
+
+
+
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 96c2ba276..293c55a69 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -219,3 +219,27 @@ val insert_after_hyp : named_context_val -> variable ->
 
 val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val * identifier list
 
+
+(* spiwack: functions manipulating the retroknowledge *)
+open Retroknowledge
+
+val retroknowledge : (retroknowledge->'a) -> env -> 'a
+
+val registered : env -> field -> bool
+
+val unregister : env -> field -> env
+
+val register : env -> field -> Retroknowledge.entry -> env
+
+(* spiwack: a few declarations for the "Print Assumption" command *)
+type assumption =
+  | Variable of identifier*Term.constr
+  | Axiom of constant*Term.constr
+
+module OrderedAssumption :  Set.OrderedType with type t = assumption
+
+module AssumptionSet : Set.S with type elt = assumption
+
+val needed_assumptions : constr -> env -> AssumptionSet.t
+
+
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index ad5df805b..93d01f12a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -170,7 +170,8 @@ and translate_module env  me =
 	  mod_user_type = Some mtb;
 	  mod_type = mtb;
 	  mod_equiv = None;
-	  mod_constraints = Constraint.empty }
+	  mod_constraints = Constraint.empty;
+	  mod_retroknowledge = [] } 
     | Some mexpr, _ -> 
 	let meq_o = (* do we have a transparent module ? *)
 	  try       (* TODO: transparent field in module_entry *)
@@ -193,7 +194,11 @@ and translate_module env  me =
 	    mod_user_type = mod_user_type;
 	    mod_expr = Some meb;
 	    mod_equiv = meq_o;
-	    mod_constraints = cst }
+	    mod_constraints = cst;
+	    mod_retroknowledge = []} (* spiwack: not so sure about that. It may
+					cause a bug when closing nested modules.
+					If it does, I don't really know how to
+					fix the bug.*)
 
 (* translate_mexpr : env -> module_expr -> module_expr_body * module_type_body *)
 and translate_mexpr env mexpr = match mexpr with
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 96d19552a..3e89112ae 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -95,14 +95,16 @@ let module_body_of_spec msb =
       mod_equiv = msb.msb_equiv;
       mod_expr = None;
       mod_user_type = None;
-      mod_constraints = Constraint.empty}
+      mod_constraints = Constraint.empty;
+      mod_retroknowledge = []}
 
 let module_body_of_type mtb = 
   { mod_type = mtb;
     mod_equiv = None;
     mod_expr = None;
     mod_user_type = None;
-    mod_constraints = Constraint.empty}
+    mod_constraints = Constraint.empty;
+    mod_retroknowledge = []}
 
 
 (* the constraints are not important here *)
@@ -170,6 +172,32 @@ and subst_module  sub mb =
 let subst_signature_msid msid mp = 
   subst_signature (map_msid msid mp)
 
+
+(* spiwack: here comes the function which takes care of importing 
+   the retroknowledge declared in the library *)
+(* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
+let add_retroknowledge msid mp =
+  let subst = add_msid msid mp empty_subst in
+  let subst_and_perform rkaction env =
+    match rkaction with
+      | Retroknowledge.RKRegister (f, e) ->
+	  Environ.register env f 
+	  (match e with 
+	    | Const kn -> kind_of_term (subst_mps subst (mkConst kn))
+	    | Ind ind -> kind_of_term (subst_mps subst (mkInd ind))
+	    | _ -> anomaly "Modops.add_retroknowledge: had to import an unsupported kind of term")
+  in
+  fun lclrk env ->
+  (* The order of the declaration matters, for instance (and it's at the
+     time this comment is being written, the only relevent instance) the
+     int31 type registration absolutely needs int31 bits to be registered.
+     Since the local_retroknowledge is stored in reverse order (each new
+     registration is added at the top of the list) we need a fold_right
+     for things to go right (the pun is not intented). So we lose 
+     tail recursivity, but the world will have exploded before any module
+     imports 10 000 retroknowledge registration.*)
+  List.fold_right subst_and_perform lclrk env
+
 (* we assume that the substitution of "mp" into "msid" is already done
 (or unnecessary) *)
 let rec add_signature mp sign env = 
@@ -192,7 +220,8 @@ and add_module mp mb env =
     match scrape_modtype env mb.mod_type with
       | MTBident _ -> anomaly "scrape_modtype does not work!"
       | MTBsig (msid,sign) -> 
-	  add_signature mp (subst_signature_msid msid mp sign) env
+	  add_retroknowledge msid mp (mb.mod_retroknowledge)
+	    (add_signature mp (subst_signature_msid msid mp sign) env)
       | MTBfunsig _ -> env
 
 
@@ -306,7 +335,7 @@ and strengthen_sig env msid sign mp = match sign with
       let env' = add_module 
 		   (MPdot (MPself msid,l)) 
 		   (module_body_of_spec mb) 
-		   env 
+		   env
       in
       let rest' = strengthen_sig env' msid rest mp in
 	item'::rest'
diff --git a/kernel/modops.mli b/kernel/modops.mli
index c209eac1a..d7cdb59ac 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -49,7 +49,7 @@ val add_signature :
 
 (* adds a module and its components, but not the constraints *)
 val add_module :
-  module_path -> module_body -> env -> env
+  module_path -> module_body ->  env -> env
 
 val check_modpath_equiv : env -> module_path -> module_path -> unit
 
diff --git a/kernel/names.ml b/kernel/names.ml
index 09c98eafc..c153169ab 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -332,3 +332,41 @@ type id_key = inv_rel_key tableKey
 
 
 
+(* spiwack : internal representation printing *)
+
+let string_of_identifier id = id
+let string_of_module_ident id = id
+let string_of_label lbl = lbl (* not public *)
+let string_of_dir_path path = "["^String.concat "; " (List.map string_of_module_ident path)^"]"
+let string_of_name =
+  function
+  | Name id -> "Name "^id
+  | Anonymous -> "Anonymous"
+
+let rec string_of_module_path = (* not public *)
+  function
+  | MPfile path -> "MPfile "^string_of_dir_path path
+  | MPbound _ -> "MPbound "^"?" (*of mod_bound_id*)
+  | MPself _ -> "MPself "^"?" (* of mod_self_id *)
+  | MPdot (mpath, lbl) -> 
+         "MPdot ("^string_of_module_path mpath^", "^string_of_label lbl^")"
+          (* of module_path * label *)
+
+let string_of_kernel_name = (* not public *)
+   function
+   |(mpath, path, lbl) -> 
+         "("^string_of_module_path mpath^", "^
+             string_of_dir_path path^", "^
+             string_of_label lbl ^")"
+
+let string_of_constant = string_of_kernel_name
+let string_of_mutual_inductive = string_of_kernel_name
+let string_of_inductive = 
+   function
+   | (mind, i) -> "("^string_of_mutual_inductive mind^", "^string_of_int i^")"
+let string_of_constructor =
+   function
+   | (ind, i) -> "("^string_of_inductive ind^", "^string_of_int i^")"
+
+
+(* /spiwack *)
diff --git a/kernel/names.mli b/kernel/names.mli
index 64edf1702..dee798da0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -174,3 +174,15 @@ type inv_rel_key = int (* index in the [rel_context] part of environment
 			  of de Bruijn indice *)
 
 type id_key = inv_rel_key tableKey
+
+
+
+(* spiwack : function used for printing identifiers *)
+val string_of_identifier : identifier-> string
+val string_of_module_ident : module_ident-> string
+val string_of_dir_path : dir_path -> string
+val string_of_name : name -> string
+val string_of_constant : constant -> string
+val string_of_mutual_inductive : mutual_inductive -> string
+val string_of_inductive : inductive -> string
+val string_of_constructor : constructor -> string
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 7a7e00e90..4f2498dc3 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -48,7 +48,8 @@ type env = {
   env_rel_context   : rel_context;
   env_rel_val       : lazy_val list;
   env_nb_rel        : int;
-  env_stratification : stratification }
+  env_stratification : stratification;
+  retroknowledge : Retroknowledge.retroknowledge }
 
 type named_context_val = named_context * named_vals
 
@@ -67,7 +68,8 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = initial_universes;
-    env_engagement = None } }
+    env_engagement = None };
+  retroknowledge = Retroknowledge.initial_retroknowledge }
 
 
 (* Rel context *)
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 728f28be0..511f56e65 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -48,7 +48,8 @@ type env = {
     env_rel_context   : rel_context;
     env_rel_val       : lazy_val list;
     env_nb_rel        : int;
-    env_stratification : stratification }
+    env_stratification : stratification; 
+    retroknowledge : Retroknowledge.retroknowledge }
 
 type named_context_val = named_context * named_vals
 
@@ -80,5 +81,3 @@ val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
 
 (* Find the ultimate inductive in the [mind_equiv] chain *)
 val scrape_mind : env -> mutual_inductive -> mutual_inductive
-
-
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
new file mode 100644
index 000000000..f064cd8b9
--- /dev/null
+++ b/kernel/retroknowledge.ml
@@ -0,0 +1,277 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \V/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: retroknowledge.ml ??? 2006-??-?? ??:??:??Z spiwack $ *)
+
+open Term
+open Names
+
+(* Type declarations, these types shouldn't be exported they are accessed
+   through specific functions. As being mutable and all it is wiser *)
+(* These types are put into two distinct categories: proactive and reactive.
+   Proactive information allows to find the name of a combinator, constructor
+   or inductive type handling a specific function.
+   Reactive information is, on the other hand, everything you need to know
+   about a specific name.*)
+
+(* aliased type for clarity purpose*)
+type entry =  (constr, types) kind_of_term
+
+(* the following types correspond to the different "things"
+   the kernel can learn about. These are the fields of the proactive knowledge*)
+type nat_field =
+  | NatType
+  | NatPlus
+  | NatTimes
+  
+type n_field = 
+  | NPositive
+  | NType
+  | NTwice
+  | NTwicePlusOne
+  | NPhi
+  | NPhiInv
+  | NPlus
+  | NTimes
+
+type int31_field = 
+  | Int31Bits
+  | Int31Type
+  | Int31Twice
+  | Int31TwicePlusOne
+  | Int31Phi
+  | Int31PhiInv
+  | Int31Plus
+  | Int31PlusC
+  | Int31PlusCarryC
+  | Int31Minus
+  | Int31MinusC
+  | Int31MinusCarryC
+  | Int31Times
+  | Int31TimesC
+  | Int31Div21
+  | Int31Div
+  | Int31AddMulDiv
+  | Int31Compare
+
+type field =
+  | KEq
+  | KNat of nat_field
+  | KN of n_field
+  | KInt31 of string*int31_field
+
+
+(* record representing all the flags of the internal state of the kernel *)
+type flags = {fastcomputation : bool}
+
+
+
+
+
+(*A definition of maps from strings to pro_int31, to be able
+  to have any amount of coq representation for the 31bits integers *)
+module OrderedField =
+struct
+  type t = field
+  let compare = compare
+end
+
+module Proactive = Map.Make (OrderedField)
+
+
+type proactive = entry Proactive.t
+
+(* the reactive knowledge is represented as a functionaly map 
+   from the type of terms (actually it is the terms whose outermost
+   layer is unfolded (typically by Term.kind_of_term)) to the 
+   type reactive_end which is a record containing all the kind of reactive
+   information needed *)
+(* todo: because of the bug with output state, reactive_end should eventually
+   contain no function. A forseen possibility is to make it a map from
+   a finite type describing the fields to the field of proactive retroknowledge
+   (and then to make as many functions as needed in environ.ml) *)
+
+module OrderedEntry =
+struct
+  type t = entry
+  let compare = compare
+end
+
+module Reactive = Map.Make (OrderedEntry)
+
+type reactive_end = {(*information required by the compiler of the VM *)
+  vm_compiling :
+      (*fastcomputation flag -> continuation -> result *)
+      (bool->Cbytecodes.comp_env->constr array ->
+       int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+      option;
+  vm_constant_static :
+      (*fastcomputation flag -> constructor -> args -> result*)
+      (bool->constr array->Cbytecodes.structured_constant)
+      option;
+  vm_constant_dynamic :
+      (*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *)
+      (bool->Cbytecodes.comp_env->Cbytecodes.block array->int->
+         Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+      option;
+  (* fastcomputation flag -> cont -> result *)
+  vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
+  (* tag (= compiled int for instance) -> result *)
+  vm_decompile_const : (int -> Term.constr) option}
+
+
+
+and reactive = reactive_end Reactive.t
+
+and retroknowledge = {flags : flags; proactive : proactive; reactive : reactive}
+
+(* This type represent an atomic action of the retroknowledge. It
+   is stored in the compiled libraries *)
+(* As per now, there is only the possibility of registering things
+   the possibility of unregistering or changing the flag is under study *)
+type action =
+    | RKRegister of field*entry
+
+
+(*initialisation*)
+let initial_flags = 
+      {fastcomputation = true;}
+
+let initial_proactive = 
+  (Proactive.empty:proactive)
+
+let initial_reactive = 
+  (Reactive.empty:reactive)
+
+let initial_retroknowledge =
+  {flags = initial_flags; 
+   proactive = initial_proactive; 
+   reactive = initial_reactive }
+
+let empty_reactive_end =
+  { vm_compiling = None ;
+    vm_constant_static = None;
+    vm_constant_dynamic = None;
+    vm_before_match = None;
+    vm_decompile_const = None }
+
+
+
+
+(* acces functions for proactive retroknowledge *)
+let add_field knowledge field value =
+  {knowledge with proactive = Proactive.add field value knowledge.proactive}
+
+let mem knowledge field =
+  Proactive.mem field knowledge.proactive
+
+let remove knowledge field =
+  {knowledge with proactive = Proactive.remove field knowledge.proactive}
+
+let find knowledge field =
+  Proactive.find field knowledge.proactive
+
+
+
+
+
+(*access functions for reactive retroknowledge*)
+
+(* used for compiling of functions (add, mult, etc..) *)
+let get_vm_compiling_info knowledge key = 
+  match (Reactive.find key knowledge.reactive).vm_compiling
+  with
+    | None -> raise Not_found
+    | Some f -> f knowledge.flags.fastcomputation
+
+(* used for compilation of fully applied constructors *)
+let get_vm_constant_static_info knowledge key =
+  match (Reactive.find key knowledge.reactive).vm_constant_static
+  with
+    | None -> raise Not_found
+    | Some f -> f knowledge.flags.fastcomputation
+
+(* used for compilation of partially applied constructors *)
+let get_vm_constant_dynamic_info knowledge key =
+  match (Reactive.find key knowledge.reactive).vm_constant_dynamic
+  with
+    | None -> raise Not_found
+    | Some f -> f knowledge.flags.fastcomputation
+
+let get_vm_before_match_info knowledge key = 
+  match (Reactive.find key knowledge.reactive).vm_before_match
+  with
+    | None -> raise Not_found
+    | Some f -> f knowledge.flags.fastcomputation
+
+let get_vm_decompile_constant_info knowledge key = 
+  match (Reactive.find key knowledge.reactive).vm_decompile_const
+  with
+    | None -> raise Not_found
+    | Some f -> f
+  
+
+
+(* functions manipulating reactive knowledge *)
+let add_vm_compiling_info knowledge value nfo =
+  {knowledge with reactive =
+   try
+     Reactive.add value
+       {(Reactive.find value (knowledge.reactive)) with vm_compiling = Some nfo}
+       knowledge.reactive
+   with Not_found ->
+     Reactive.add value {empty_reactive_end with vm_compiling = Some nfo}
+       knowledge.reactive
+  }
+
+let add_vm_constant_static_info knowledge value nfo =
+  {knowledge with reactive =
+   try
+     Reactive.add value
+       {(Reactive.find value (knowledge.reactive)) with vm_constant_static = Some nfo}
+       knowledge.reactive
+   with Not_found ->
+     Reactive.add value {empty_reactive_end with vm_constant_static = Some nfo}
+       knowledge.reactive
+  }
+
+let add_vm_constant_dynamic_info knowledge value nfo =
+  {knowledge with reactive =
+   try
+     Reactive.add value
+       {(Reactive.find value (knowledge.reactive)) with vm_constant_dynamic = Some nfo}
+       knowledge.reactive
+   with Not_found ->
+     Reactive.add value {empty_reactive_end with vm_constant_dynamic = Some nfo}
+       knowledge.reactive
+  }
+
+let add_vm_before_match_info knowledge value nfo =
+  {knowledge with reactive =
+   try
+     Reactive.add value
+       {(Reactive.find value (knowledge.reactive)) with vm_before_match = Some nfo}
+       knowledge.reactive
+   with Not_found ->
+     Reactive.add value {empty_reactive_end with vm_before_match = Some nfo}
+       knowledge.reactive
+  }
+
+let add_vm_decompile_constant_info knowledge value nfo =
+  {knowledge with reactive =
+   try
+     Reactive.add value
+       {(Reactive.find value (knowledge.reactive)) with vm_decompile_const = Some nfo}
+       knowledge.reactive
+   with Not_found ->
+     Reactive.add value {empty_reactive_end with vm_decompile_const = Some nfo}
+       knowledge.reactive
+  }
+
+let clear_info knowledge value =
+  {knowledge with reactive = Reactive.remove value knowledge.reactive}
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
new file mode 100644
index 000000000..cba055560
--- /dev/null
+++ b/kernel/retroknowledge.mli
@@ -0,0 +1,152 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: retroknowledge.mli ??? 2006-??-?? ??:??:??Z spiwack $ i*)
+
+(*i*)
+open Names
+open Term
+(*i*)
+
+type retroknowledge
+
+(* aliased type for clarity purpose*)
+type entry =  (constr, types) kind_of_term
+
+(* the following types correspond to the different "things"
+   the kernel can learn about.*)
+type nat_field =
+  | NatType
+  | NatPlus
+  | NatTimes
+  
+type n_field = 
+  | NPositive
+  | NType
+  | NTwice
+  | NTwicePlusOne
+  | NPhi
+  | NPhiInv
+  | NPlus
+  | NTimes
+
+type int31_field = 
+  | Int31Bits
+  | Int31Type
+  | Int31Twice
+  | Int31TwicePlusOne
+  | Int31Phi
+  | Int31PhiInv
+  | Int31Plus
+  | Int31PlusC
+  | Int31PlusCarryC
+  | Int31Minus
+  | Int31MinusC
+  | Int31MinusCarryC
+  | Int31Times
+  | Int31TimesC
+  | Int31Div21
+  | Int31Div
+  | Int31AddMulDiv
+  | Int31Compare
+
+type field =
+  | KEq
+  | KNat of nat_field
+  | KN of n_field
+  | KInt31 of string*int31_field
+
+
+(* This type represent an atomic action of the retroknowledge. It
+   is stored in the compiled libraries *)
+(* As per now, there is only the possibility of registering things
+   the possibility of unregistering or changing the flag is under study *)
+type action =
+    | RKRegister of field*entry
+
+
+(* initial value for retroknowledge *)
+val initial_retroknowledge : retroknowledge
+
+
+(* Given an identifier id (usually Const _)
+   and the continuation cont of the bytecode compilation
+   returns the compilation of id in cont if it has a specific treatment
+   or raises Not_found if id should be compiled as usual *)
+val get_vm_compiling_info  : retroknowledge -> entry -> Cbytecodes.comp_env ->
+                             constr array -> 
+                             int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes
+(*Given an identifier id (usually Construct _)
+   and its argument array, returns a function that tries an ad-hoc optimisated
+   compilation (in the case of the 31-bit integers it means compiling them
+   directly into an integer)
+   raises Not_found if id should be compiled as usual, and expectingly
+   CBytecodes.NotClosed if the term is not a closed constructor pattern 
+   (a constant for the compiler) *)
+val get_vm_constant_static_info : retroknowledge -> entry ->
+                                   constr array ->
+                                   Cbytecodes.structured_constant
+
+(*Given an identifier id (usually Construct _ )
+   its argument array and a continuation, returns the compiled version
+   of id+args+cont when id has a specific treatment (in the case of
+   31-bit integers, that would be the dynamic compilation into integers)
+   or raises Not_found if id should be compiled as usual *)
+val get_vm_constant_dynamic_info : retroknowledge -> entry -> 
+                                Cbytecodes.comp_env -> 
+                                Cbytecodes.block array -> 
+                                int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes
+(* Given a type identifier, this function is used before compiling a match 
+   over this type. In the case of 31-bit integers for instance, it is used 
+   to add the instruction sequence which would perform a dynamic decompilation
+   in case the argument of the match is not in coq representation *)
+val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
+                                                       -> Cbytecodes.bytecodes
+
+(* Given a type identifier, this function is used by pretyping/vnorm.ml to 
+   recover the elements of that type from their compiled form if it's non 
+   standard (it is used (and can be used) only when the compiled form
+   is not a block *)
+val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr
+
+
+(* the following functions are solely used in Pre_env and Environ to implement
+   the functions  register and unregister (and mem) of Environ *)
+val add_field : retroknowledge -> field -> entry -> retroknowledge
+val mem : retroknowledge -> field -> bool
+val remove : retroknowledge -> field -> retroknowledge
+val find : retroknowledge -> field -> entry
+
+(* the following function manipulate the reactive information of values
+   they are only used by the functions of Pre_env, and Environ to implement
+   the functions register and unregister of Environ *)
+val add_vm_compiling_info : retroknowledge-> entry -> 
+                            (bool -> Cbytecodes.comp_env -> constr array -> int ->
+                            Cbytecodes.bytecodes -> Cbytecodes.bytecodes) ->
+                            retroknowledge
+val add_vm_constant_static_info : retroknowledge-> entry -> 
+                                  (bool->constr array->
+                                      Cbytecodes.structured_constant) ->
+                                  retroknowledge
+val add_vm_constant_dynamic_info : retroknowledge-> entry -> 
+                                   (bool -> Cbytecodes.comp_env -> 
+                                   Cbytecodes.block array -> int -> 
+                                   Cbytecodes.bytecodes -> Cbytecodes.bytecodes) ->
+                                   retroknowledge
+val add_vm_before_match_info : retroknowledge -> entry ->
+                              (bool->Cbytecodes.bytecodes->Cbytecodes.bytecodes) ->
+                              retroknowledge
+
+val add_vm_decompile_constant_info : retroknowledge -> entry -> 
+                                    (int -> constr) -> retroknowledge
+                                      
+
+val clear_info : retroknowledge-> entry -> retroknowledge
+
+
+
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9cfce4303..efc2fa865 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -52,7 +52,8 @@ type safe_environment =
       revsign : module_signature_body;
       revstruct : module_structure_body;
       imports : library_info list;
-      loads : (module_path * module_body) list }
+      loads : (module_path * module_body) list;
+      local_retroknowledge : Retroknowledge.action list}
 
 (*
   { old = senv.old;
@@ -79,12 +80,65 @@ let rec empty_environment =
     revsign = [];
     revstruct = [];
     imports = [];
-    loads = [] }
+    loads = [];
+    local_retroknowledge = [] }
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
 
+
+
+
+
+
+
+
+
+(*spiwack: functions for safe retroknowledge *)
+
+(* terms which are closed under the environnement env, i.e
+   terms which only depends on constant who are themselves closed *)
+let closed env term = 
+  AssumptionSet.is_empty (needed_assumptions env term)
+
+(* the set of safe terms in an environement any recursive set of
+   terms who are known not to prove inconsistent statement. It should
+   include at least all the closed terms. But it could contain other ones
+   like the axiom of excluded middle for instance *)
+let safe =
+  closed
+
+
+
+(* universal lifting, used for the "get" operations mostly *)
+let retroknowledge f senv = 
+  Environ.retroknowledge f (env_of_senv senv)
+
+let register senv field value by_clause = 
+  (* todo : value closed, by_clause safe, by_clause of the proper type*)
+  (* spiwack : updates the safe_env with the information that the register
+     action has to be performed (again) when the environement is imported *)
+  {senv with env = Environ.register senv.env field value;
+             local_retroknowledge = 
+      Retroknowledge.RKRegister (field,value)::senv.local_retroknowledge
+  }
+
+(* spiwack : currently unused *)
+let unregister senv field  =
+  (*spiwack: todo: do things properly or delete *)
+  {senv with env = Environ.unregister senv.env field}
+(* /spiwack *)
+
+
+
+
+
+
+
+
+
+
 (* Insertion of section variables. They are now typed before being
    added to the environment. *)
 
@@ -154,7 +208,8 @@ let add_constant dir l decl senv =
 	  revsign = (l,SPBconst cb)::senv.revsign;
 	  revstruct = (l,SEBconst cb)::senv.revstruct;
 	  imports = senv.imports;
-	  loads = senv.loads }
+	  loads = senv.loads ;
+	  local_retroknowledge = senv.local_retroknowledge }
     
 
 (* Insertion of inductive types. *)
@@ -181,7 +236,8 @@ let add_mind dir l mie senv =
 	revsign = (l,SPBmind mib)::senv.revsign;
 	revstruct = (l,SEBmind mib)::senv.revstruct;
 	imports = senv.imports;
-	loads = senv.loads }
+	loads = senv.loads;
+        local_retroknowledge = senv.local_retroknowledge }
 
 
 (* Insertion of module types *)
@@ -199,8 +255,8 @@ let add_modtype l mte senv =
 	revsign = (l,SPBmodtype mtb)::senv.revsign;
 	revstruct = (l,SEBmodtype mtb)::senv.revstruct;
 	imports = senv.imports;
-	loads = senv.loads }
-
+	loads = senv.loads;
+        local_retroknowledge = senv.local_retroknowledge }
 
 
 (* full_add_module adds module with universes and constraints *)
@@ -224,7 +280,8 @@ let add_module l me senv =
 	revsign = (l,SPBmodule mspec)::senv.revsign;
 	revstruct = (l,SEBmodule mb)::senv.revstruct;
 	imports = senv.imports;
-	loads = senv.loads }
+	loads = senv.loads;
+        local_retroknowledge = senv.local_retroknowledge }
 
 
 (* Interactive modules *)
@@ -246,7 +303,9 @@ let start_module l senv =
 	revsign = [];
 	revstruct = [];
 	imports = senv.imports;
-	loads = [] }
+	loads = [];
+	(* spiwack : not sure, but I hope it's correct *)
+        local_retroknowledge = [] }
 
 let end_module l restype senv = 
   let oldsenv = senv.old in
@@ -285,7 +344,8 @@ let end_module l restype senv =
       mod_user_type = mod_user_type;
       mod_type = mtb;
       mod_equiv = None;
-      mod_constraints = cst }
+      mod_constraints = cst;
+      mod_retroknowledge = senv.local_retroknowledge}
   in
   let mspec = 
     { msb_modtype = mtb;
@@ -310,7 +370,8 @@ let end_module l restype senv =
 	revsign = (l,SPBmodule mspec)::oldsenv.revsign;
 	revstruct = (l,SEBmodule mb)::oldsenv.revstruct;
 	imports = senv.imports;
-	loads = senv.loads@oldsenv.loads }
+	loads = senv.loads@oldsenv.loads;
+	local_retroknowledge = senv.local_retroknowledge@oldsenv.local_retroknowledge }
 
 
 (* Adding parameters to modules or module types *)
@@ -334,7 +395,8 @@ let add_module_parameter mbid mte senv =
     revsign = [];
     revstruct = [];
     imports = senv.imports;
-    loads = [] }
+    loads = [];
+    local_retroknowledge = senv.local_retroknowledge }
 
 
 (* Interactive module types *)
@@ -356,7 +418,9 @@ let start_modtype l senv =
 	revsign = [];
 	revstruct = [];
 	imports = senv.imports;
-	loads = [] }
+	loads = [];
+	(* spiwack: not 100% sure, but I think it should be like that *)
+        local_retroknowledge = []}
 
 let end_modtype l senv = 
   let oldsenv = senv.old in
@@ -396,7 +460,11 @@ let end_modtype l senv =
 	revsign = (l,SPBmodtype mtb)::oldsenv.revsign;
 	revstruct = (l,SEBmodtype mtb)::oldsenv.revstruct;
 	imports = senv.imports;
-	loads = senv.loads@oldsenv.loads }
+	loads = senv.loads@oldsenv.loads;
+        (* spiwack : if there is a bug with retroknowledge in nested modules
+                     it's likely to come from here *)
+        local_retroknowledge = 
+                   senv.local_retroknowledge@oldsenv.local_retroknowledge}
   
 
 let current_modpath senv = senv.modinfo.modpath
@@ -422,7 +490,6 @@ let set_engagement c senv =
 type compiled_library = 
     dir_path * module_body * library_info list * engagement option
 
-
 (* We check that only initial state Require's were performed before 
    [start_library] was called *)
 
@@ -455,7 +522,10 @@ let start_library dir senv =
 	revsign = [];
 	revstruct = [];
 	imports = senv.imports;
-	loads = [] }
+	loads = [];
+        local_retroknowledge = [] }
+
+
 
 
 let export senv dir = 
@@ -475,7 +545,8 @@ let export senv dir =
       mod_type = MTBsig (modinfo.msid, List.rev senv.revsign);
       mod_user_type = None;
       mod_equiv = None;
-      mod_constraints = Constraint.empty }
+      mod_constraints = Constraint.empty;
+      mod_retroknowledge = senv.local_retroknowledge}
   in
     modinfo.msid, (dir,mb,senv.imports,engagement senv.env)
 
@@ -492,6 +563,8 @@ let check_imports senv needed =
   in
   List.iter check needed
 
+
+
 (* we have an inefficiency: Since loaded files are added to the
 environment every time a module is closed, their components are
 calculated many times. Thic could be avoided in several ways:
@@ -571,3 +644,6 @@ let j_type j = j.uj_type
 let safe_infer senv = infer (env_of_senv senv)
     
 let typing senv = Typeops.typing (env_of_senv senv)
+
+
+
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1b4d932b5..fe028c073 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -126,3 +126,12 @@ val safe_infer : safe_environment -> constr -> judgment * Univ.constraints
 val typing : safe_environment -> constr -> judgment
 
 
+
+(*spiwack: safe retroknowledge functionalities *)
+
+open Retroknowledge
+
+val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
+
+val register : safe_environment -> field -> Retroknowledge.entry -> constr
+                                         -> safe_environment
diff --git a/kernel/term.ml b/kernel/term.ml
index 6a0fe60f6..3386f45f5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1182,3 +1182,49 @@ type values
 
 
 
+(* spiwack : internal representation printing *)
+let string_of_sorts =
+  function 
+  | Prop Pos -> "Prop Pos"
+  | Prop Null -> "Prop Null"
+  | Type u -> "Type "^string_of_universe u
+
+let string_of_cast_kind = 
+  function
+  |VMcast -> "VMcast"
+  | DEFAULTcast -> "DEFAULTcast"
+
+let rec string_of_constr = 
+  let string_of_term string_of_expr string_of_type = function
+  | Rel i -> "Rel "^string_of_int i
+  | Var id -> "Var "^string_of_identifier id
+  | Meta mv -> "Meta "^"mv?" (* need a function for printing metavariables *)
+  | Evar ev -> "Evar "^"ev?" (* ??     of 'constr pexistential *)
+  | Sort s -> "Sort "^string_of_sorts s
+  | Cast (e,ck,t) -> 
+         "Cast ("^string_of_expr e^", "^string_of_cast_kind ck^", "^
+                 string_of_type t^")" 
+  | Prod (n, t1, t2) -> 
+          "Prod ("^string_of_name n^", "^string_of_type t1^", "^
+                   string_of_type t2^")"  
+  | Lambda (n,t,e) ->
+          "Lambda ("^string_of_name n^", "^string_of_type t^", "^
+                    string_of_expr e^")"
+  | LetIn (n, e1, t, e2) -> 
+           "LetIn ("^string_of_name n^", "^string_of_expr e1^", "^
+           string_of_type t^", "^string_of_expr e2^")"
+  | App   (e, args) ->  "App ("^string_of_expr e^", [|"^
+          String.concat "; " (Array.to_list (Array.map string_of_expr args)) ^
+          "|])"
+  | Const c ->  "Const "^string_of_constant c
+  | Ind   ind ->  "Ind "^string_of_inductive ind
+  | Construct ctr -> "Construct "^string_of_constructor ctr
+  | Case(_,_,_,_)  -> "Case ..."    
+             (*    of case_info * 'constr * 'constr * 'constr array   *)
+  | Fix _  -> "Fix ..."  (*    of ('constr, 'types) pfixpoint *)
+  | CoFix _ -> "CoFix ..."  (*     of ('constr, 'types) pcofixpoint *)
+in 
+fun x -> string_of_term string_of_constr string_of_constr x
+
+
+(* /spiwack *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 0d40da969..4133ca892 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -547,3 +547,9 @@ val hcons1_types : types -> types
 (**************************************)
 
 type values
+
+
+(*************************************************************)
+
+(* spiwack: printing of internal representation of constr *)
+val string_of_constr : constr -> string
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 17bd10fc9..1abc393b5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -575,3 +575,18 @@ module Huniv =
 let hcons1_univ u =
   let _,_,hdir,_,_,_ = Names.hcons_names() in
   Hashcons.simple_hcons Huniv.f hdir u
+
+
+
+(* spiwack: function for internal representation printing *)
+let string_of_universe =
+  let string_of_universe_level = function
+  | Base -> "Base"
+  | Level (path,i) -> "Level ("^Names.string_of_dir_path path^", "^string_of_int i^")"
+in
+function 
+  | Atom u -> "Atom "^string_of_universe_level u
+  | Max (l1,l2) -> "Max (["^
+               String.concat "; " (List.map string_of_universe_level l1)^"], ["^
+               String.concat "; " (List.map string_of_universe_level l2)
+               ^"])"
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 518c4a62b..39505173e 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -77,3 +77,7 @@ val pr_universes : universes -> Pp.std_ppcmds
 val dump_universes : out_channel -> universes -> unit
 
 val hcons1_univ : universe -> universe
+
+
+(* spiwack: function for internal representation printing *)
+val string_of_universe : universe -> string