Partial support for open terms in int31.

11 files changed, 142 insertions, 37 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4c1d9bddc..4ce42c919 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -465,7 +465,13 @@ let register =
     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
+    let rk =
+      add_vm_constant_dynamic_info rk c Cbytegen.dynamic_int31_compilation
+    in
+    let rk =
+      add_native_constant_static_info rk c Nativelambda.compile_static_int31
+    in
+    add_native_constant_dynamic_info rk c Nativelambda.compile_dynamic_int31
   in
 
   (* subfunction which adds the compiling information of an
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c294345e8..1ddad2149 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -259,6 +259,7 @@ type primitive =
   | Upd_cofix
   | Force_cofix
   | Mk_uint
+  | Mk_I31_accu
   | Mk_meta
   | Mk_evar
 
@@ -301,8 +302,9 @@ let primitive_hash = function
 | Upd_cofix -> 12
 | Force_cofix -> 13
 | Mk_uint -> 14
-| Mk_meta -> 15
-| Mk_evar -> 16
+| Mk_I31_accu -> 15
+| Mk_meta -> 16
+| Mk_evar -> 17
 
 type mllambda =
   | MLlocal        of lname 
@@ -1053,12 +1055,19 @@ let merge_branches t =
 			       Array.concat [fv_args;lf_args;pargsi]))|]) in
 	(lname, paramsi, body) in
       MLletrec(Array.mapi mkrec lf, lf_args.(start)) *)
-   
+
   | Lmakeblock (prefix,cn,_,args) ->
       MLconstruct(prefix,cn,Array.map (ml_of_lam env l) args)
   | Lconstruct (prefix, cn) ->
       MLglobal (Gconstruct (prefix, cn))
-  | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
+  | Luint v ->
+     (match v with
+     | UintVal i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
+     | UintDigits (prefix,cn,ds) ->
+	let c = MLglobal (Gconstruct (prefix, cn)) in
+	let ds = Array.map (ml_of_lam env l) ds in
+	let i31 = MLapp (MLprimitive Mk_I31_accu, [|c|]) in
+	MLapp(i31, ds))
   | Lval v ->
       let i = push_symbol (SymbValue v) in get_value_code i
   | Lsort s ->
@@ -1471,6 +1480,7 @@ let pp_mllam fmt l =
     | Upd_cofix -> Format.fprintf fmt "upd_cofix"
     | Force_cofix -> Format.fprintf fmt "force_cofix"
     | Mk_uint -> Format.fprintf fmt "mk_uint"
+    | Mk_I31_accu -> Format.fprintf fmt "mk_I31_accu"
     | Mk_meta -> Format.fprintf fmt "mk_meta_accu"
     | Mk_evar -> Format.fprintf fmt "mk_evar_accu"
   in
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index 4e0291ed9..9c5add4df 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -12,7 +12,13 @@ open Nativevalues
 (** This file defines the lambda code for the native compiler. It has been
 extracted from Nativelambda.ml because of the retroknowledge architecture. *)
 
-type lambda =
+type prefix = string
+
+type uint =
+  | UintVal of Uint31.t
+  | UintDigits of prefix * constructor * lambda array
+
+and lambda =
   | Lrel          of name * int 
   | Lvar          of identifier
   | Lmeta         of metavariable * lambda (* type *)
@@ -21,21 +27,21 @@ type lambda =
   | Llam          of name array * lambda  
   | Llet          of name * lambda * lambda
   | Lapp          of lambda * lambda array
-  | Lconst        of string * constant (* prefix, constant name *)
+  | Lconst        of prefix * constant
   | Lcase         of annot_sw * lambda * lambda * lam_branches 
                   (* annotations, term being matched, accu, branches *)
   | Lif           of lambda * lambda * lambda
   | Lfix          of (int array * int) * fix_decl 
   | Lcofix        of int * fix_decl 
-  | Lmakeblock    of string * constructor * int * lambda array
+  | Lmakeblock    of prefix * constructor * int * lambda array
                   (* prefix, constructor name, constructor tag, arguments *)
 	(* A fully applied constructor *)
-  | Lconstruct    of string * constructor (* prefix, constructor name *)
+  | Lconstruct    of prefix * constructor
 	(* A partially applied constructor *)
-  | Luint          of Uint31.t
+  | Luint         of uint
   | Lval          of Nativevalues.t
   | Lsort         of sorts
-  | Lind          of string * inductive (* prefix, inductive name *)
+  | Lind          of prefix * inductive
   | Llazy
   | Lforce
 
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 297ac6b99..179d8d58b 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -639,26 +639,21 @@ and lambda_of_app env sigma f args =
       let tag, nparams, arity = Renv.get_construct_info env c in
       let expected = nparams + arity in
       let nargs = Array.length args in
+      let prefix = get_mind_prefix !global_env (fst (fst c)) in
       if Int.equal nargs expected then 
       try
 	try
 	  Retroknowledge.get_native_constant_static_info
                          (!global_env).retroknowledge
                          f args
-          with NotClosed -> assert false
-(*
-    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
-                                           f),
-                           b_args)
- *)
+          with NotClosed ->
+	    let args = lambda_of_args env sigma nparams args in
+	    Retroknowledge.get_native_constant_dynamic_info
+                           (!global_env).retroknowledge f prefix c args
         with Not_found ->
 	  let args = lambda_of_args env sigma nparams args in
 	  makeblock !global_env c tag args
       else
-        let prefix = get_mind_prefix !global_env (fst (fst c)) in
         mkLapp (Lconstruct (prefix, c)) (lambda_of_args env sigma 0 args)
   | _ -> 
       let f = lambda_of_constr env sigma f in
@@ -695,3 +690,17 @@ let lambda_of_constr env sigma c =
 
 let mk_lazy c =
   mkLapp Llazy [|c|]
+
+(** Retroknowledge, to be removed once we move to primitive machine integers *)
+let compile_static_int31 fc args =
+  if not fc then raise Not_found else
+    Luint (UintVal
+    (Uint31.of_int (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)))
+
+let compile_dynamic_int31 fc prefix c args =
+  if not fc then raise Not_found else
+  Luint (UintDigits (prefix,c,args))
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index d4be2279d..b97e01006 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -29,3 +29,8 @@ val mk_lazy : lambda -> lambda
 val get_allias : env -> constant -> constant
 
 val lambda_of_constr : env -> evars -> Constr.constr -> lambda
+
+val compile_static_int31 : bool -> Constr.constr array -> lambda
+
+val compile_dynamic_int31 : bool -> Nativeinstr.prefix -> Names.constructor ->
+			    Nativeinstr.lambda array -> Nativeinstr.lambda
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 98094f795..2a0052a60 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -221,7 +221,8 @@ let dummy_value : unit -> t =
 
 let cast_accu v = (Obj.magic v:accumulator)
 
-let mk_int x = Obj.magic x
+let mk_int (x : int) = (Obj.magic x : t)
+let mk_uint (x : Uint31.t) = (Obj.magic x : t)
 
 type block
 
@@ -253,6 +254,12 @@ let kind_of_value (v:t) =
            or ??? what is 1002*)
         Vfun v
 
+(** Support for machine integers *)
+
+let is_int (x:t) =
+  let o = Obj.repr x in
+  Obj.is_int o
+
 let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i)
 let bohcnv = Array.init 256 (fun i -> i -
                                       (if 0x30 <= i then 0x30 else 0) -
@@ -278,4 +285,52 @@ let str_decode s =
   done;
   Marshal.from_string (Buffer.contents mshl_expr) 0
 
-
+(** Retroknowledge, to be removed when we switch to primitive integers *)
+
+(* This will be unsafe with 63-bits integers *)
+let digit_to_uint d = (Obj.magic d : Uint31.t)
+
+let mk_I31_accu c x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17
+		  x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 =
+  if is_int x0 && is_int x1 && is_int x2 && is_int x3 && is_int x4 && is_int x5
+     && is_int x6 && is_int x7 && is_int x8 && is_int x9 && is_int x10
+     && is_int x11 && is_int x12 && is_int x13 && is_int x14 && is_int x15
+     && is_int x16 && is_int x17 && is_int x18 && is_int x19 && is_int x20
+     && is_int x21 && is_int x22 && is_int x23 && is_int x24 && is_int x25
+     && is_int x26 && is_int x27 && is_int x28 && is_int x29 && is_int x30
+  then
+    let r = digit_to_uint x0 in
+    let r = Uint31.add_digit r (digit_to_uint x1) in
+    let r = Uint31.add_digit r (digit_to_uint x2) in
+    let r = Uint31.add_digit r (digit_to_uint x3) in
+    let r = Uint31.add_digit r (digit_to_uint x4) in
+    let r = Uint31.add_digit r (digit_to_uint x5) in
+    let r = Uint31.add_digit r (digit_to_uint x6) in
+    let r = Uint31.add_digit r (digit_to_uint x7) in
+    let r = Uint31.add_digit r (digit_to_uint x8) in
+    let r = Uint31.add_digit r (digit_to_uint x9) in
+    let r = Uint31.add_digit r (digit_to_uint x10) in
+    let r = Uint31.add_digit r (digit_to_uint x11) in
+    let r = Uint31.add_digit r (digit_to_uint x12) in
+    let r = Uint31.add_digit r (digit_to_uint x13) in
+    let r = Uint31.add_digit r (digit_to_uint x14) in
+    let r = Uint31.add_digit r (digit_to_uint x15) in
+    let r = Uint31.add_digit r (digit_to_uint x16) in
+    let r = Uint31.add_digit r (digit_to_uint x17) in
+    let r = Uint31.add_digit r (digit_to_uint x18) in
+    let r = Uint31.add_digit r (digit_to_uint x19) in
+    let r = Uint31.add_digit r (digit_to_uint x20) in
+    let r = Uint31.add_digit r (digit_to_uint x21) in
+    let r = Uint31.add_digit r (digit_to_uint x22) in
+    let r = Uint31.add_digit r (digit_to_uint x23) in
+    let r = Uint31.add_digit r (digit_to_uint x24) in
+    let r = Uint31.add_digit r (digit_to_uint x25) in
+    let r = Uint31.add_digit r (digit_to_uint x26) in
+    let r = Uint31.add_digit r (digit_to_uint x27) in
+    let r = Uint31.add_digit r (digit_to_uint x28) in
+    let r = Uint31.add_digit r (digit_to_uint x29) in
+    let r = Uint31.add_digit r (digit_to_uint x30) in
+    mk_uint r
+  else
+    c x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20
+      x21 x22 x23 x24 x25 x26 x27 x28 x29 x30
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 150811b72..4c918e116 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -75,6 +75,7 @@ val mk_block : tag -> t array -> t
 
 
 val mk_int : int -> t
+val mk_uint : Uint31.t -> t
 
 val napply : t -> t array -> t
 (* Functions over accumulators *)
@@ -110,3 +111,5 @@ val is_accu : t -> bool
 
 val str_encode : 'a -> string
 val str_decode : string -> 'a
+
+val mk_I31_accu : t
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 1049ab94d..b39ae94a5 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -13,6 +13,7 @@
 (* This file defines the knowledge that the kernel is able to optimize
    for evaluation in the bytecode virtual machine *)
 
+open Names
 open Term
 
 (* Type declarations, these types shouldn't be exported they are accessed
@@ -127,17 +128,21 @@ type reactive_end = {(*information required by the compiler of the VM *)
   vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
   (* tag (= compiled int for instance) -> result *)
   vm_decompile_const : (int -> Term.constr) option;
+
   native_compiling :
       (bool->Cbytecodes.comp_env->constr array ->
        int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
       option;
+
   native_constant_static :
       (bool -> constr array -> Nativeinstr.lambda) option;
+
   native_constant_dynamic :
-      (bool->Cbytecodes.comp_env->Cbytecodes.block array->int->
-         Cbytecodes.bytecodes->Cbytecodes.bytecodes)
-      option;
+      (bool -> Nativeinstr.prefix -> constructor ->
+       Nativeinstr.lambda array -> Nativeinstr.lambda) option;
+
   native_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
+
   native_decompile_const : (int -> Term.constr) option
 }
 
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 097d207e4..ff084f71b 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
 open Term
 
 type retroknowledge
@@ -122,12 +123,12 @@ val get_native_compiling_info  : retroknowledge -> entry -> Cbytecodes.comp_env
                              int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes
 
 val get_native_constant_static_info : retroknowledge -> entry ->
-                                   constr array -> Nativeinstr.lambda
+                                      constr array -> Nativeinstr.lambda
 
 val get_native_constant_dynamic_info : retroknowledge -> entry ->
-                                Cbytecodes.comp_env ->
-                                Cbytecodes.block array ->
-                                int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes
+                                       Nativeinstr.prefix -> constructor ->
+				       Nativeinstr.lambda array ->
+				       Nativeinstr.lambda
 
 val get_native_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
                                                        -> Cbytecodes.bytecodes
@@ -168,15 +169,18 @@ val add_native_compiling_info : retroknowledge-> entry ->
                             (bool -> Cbytecodes.comp_env -> constr array -> int ->
                             Cbytecodes.bytecodes -> Cbytecodes.bytecodes) ->
                             retroknowledge
+
 val add_native_constant_static_info : retroknowledge -> entry ->
                                   (bool -> constr array ->
                                       Nativeinstr.lambda) ->
                                   retroknowledge
-val add_native_constant_dynamic_info : retroknowledge-> entry ->
-                                   (bool -> Cbytecodes.comp_env ->
-                                   Cbytecodes.block array -> int ->
-                                   Cbytecodes.bytecodes -> Cbytecodes.bytecodes) ->
+
+val add_native_constant_dynamic_info : retroknowledge -> entry ->
+                                   (bool -> Nativeinstr.prefix -> constructor ->
+				      Nativeinstr.lambda array ->
+				      Nativeinstr.lambda) ->
                                    retroknowledge
+
 val add_native_before_match_info : retroknowledge -> entry ->
                               (bool->Cbytecodes.bytecodes->Cbytecodes.bytecodes) ->
                               retroknowledge
diff --git a/kernel/uint31.ml b/kernel/uint31.ml
index 0f1c1444b..fea12332c 100644
--- a/kernel/uint31.ml
+++ b/kernel/uint31.ml
@@ -149,5 +149,5 @@ let tail0 x =
   if !x land 0x1 = 0    then (                r := !r + 1);
   !r
 
-
- 
+let add_digit x d =
+  (x lsl 1) lor d
diff --git a/kernel/uint31.mli b/kernel/uint31.mli
index fdfb2d95a..e8b980809 100644
--- a/kernel/uint31.mli
+++ b/kernel/uint31.mli
@@ -36,4 +36,6 @@ val compare : t -> t -> int
       (* head and tail *)
 val head0   : t -> t
 val tail0   : t -> t
-  
+
+(** Used by retroknowledge *)
+val add_digit : t -> t -> t