Full support for int31 values in native compiler.

9 files changed, 68 insertions, 14 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4ce42c919..5a40b1c2a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -481,6 +481,12 @@ let register =
     add_vm_compiling_info retroknowledge v (Cbytegen.op_compilation n op kn)
   in
 
+  let add_int31_before_match rk v =
+    let rk = add_vm_before_match_info rk v Cbytegen.int31_escape_before_match in
+    let rk = add_native_before_match_info rk v Nativelambda.before_match_int31 in
+    rk
+  in
+
 fun env field value ->
   (* subfunction which shortens the (very often use) registration of binary
      operators to the reactive retroknowledge. *)
@@ -522,9 +528,8 @@ fun env field value ->
 		     | _ -> anomaly ~label:"Environ.register" (Pp.str "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)
+	  (add_int31_before_match
+	     (retroknowledge add_int31c env i31c) value)
     | 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
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1ddad2149..c4ede775e 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -260,6 +260,7 @@ type primitive =
   | Force_cofix
   | Mk_uint
   | Mk_I31_accu
+  | Decomp_uint
   | Mk_meta
   | Mk_evar
 
@@ -303,8 +304,9 @@ let primitive_hash = function
 | Force_cofix -> 13
 | Mk_uint -> 14
 | Mk_I31_accu -> 15
-| Mk_meta -> 16
-| Mk_evar -> 17
+| Decomp_uint -> 16
+| Mk_meta -> 17
+| Mk_evar -> 18
 
 type mllambda =
   | MLlocal        of lname 
@@ -1067,7 +1069,11 @@ let merge_branches t =
 	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))
+	MLapp(i31, ds)
+     | UintDecomp (prefix,cn,t) ->
+	let c = MLglobal (Gconstruct (prefix, cn)) in
+	let t = ml_of_lam env l t in
+	MLapp (MLprimitive Decomp_uint, [|c;t|]))
   | Lval v ->
       let i = push_symbol (SymbValue v) in get_value_code i
   | Lsort s ->
@@ -1481,6 +1487,7 @@ let pp_mllam fmt l =
     | Force_cofix -> Format.fprintf fmt "force_cofix"
     | Mk_uint -> Format.fprintf fmt "mk_uint"
     | Mk_I31_accu -> Format.fprintf fmt "mk_I31_accu"
+    | Decomp_uint -> Format.fprintf fmt "decomp_uint"
     | 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 9c5add4df..bba011475 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -17,6 +17,7 @@ type prefix = string
 type uint =
   | UintVal of Uint31.t
   | UintDigits of prefix * constructor * lambda array
+  | UintDecomp of prefix * constructor * lambda
 
 and lambda =
   | Lrel          of name * int 
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 179d8d58b..f6fb25ab0 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -581,6 +581,13 @@ let rec lambda_of_constr env sigma c =
       in
       (* translation of the argument *)
       let la = lambda_of_constr env sigma a in
+      let entry = mkInd ind in
+      let la =
+	try
+	  Retroknowledge.get_native_before_match_info (!global_env).retroknowledge
+						      entry prefix (ind,1) la
+	with Not_found -> la
+      in
       (* translation of the type *)
       let lt = lambda_of_constr env sigma t in
       (* translation of branches *)
@@ -647,6 +654,7 @@ and lambda_of_app env sigma f args =
                          (!global_env).retroknowledge
                          f args
           with NotClosed ->
+	    assert (Int.equal nparams 0); (* should be fine for int31 *)
 	    let args = lambda_of_args env sigma nparams args in
 	    Retroknowledge.get_native_constant_dynamic_info
                            (!global_env).retroknowledge f prefix c args
@@ -654,7 +662,12 @@ and lambda_of_app env sigma f args =
 	  let args = lambda_of_args env sigma nparams args in
 	  makeblock !global_env c tag args
       else
-        mkLapp (Lconstruct (prefix, c)) (lambda_of_args env sigma 0 args)
+	let args = lambda_of_args env sigma 0 args in
+	(try
+	    Retroknowledge.get_native_constant_dynamic_info
+              (!global_env).retroknowledge f prefix c args
+	  with Not_found ->
+            mkLapp (Lconstruct (prefix, c)) args)
   | _ -> 
       let f = lambda_of_constr env sigma f in
       let args = lambda_of_args env sigma 0 args in
@@ -704,3 +717,12 @@ let compile_static_int31 fc args =
 let compile_dynamic_int31 fc prefix c args =
   if not fc then raise Not_found else
   Luint (UintDigits (prefix,c,args))
+
+let before_match_int31 fc prefix c t =
+  if not fc then
+    raise Not_found
+  else
+  match t with
+  | Luint (UintVal i) -> assert false
+  | Luint (UintDigits (prefix,c,args)) -> assert false
+  | _ -> Luint (UintDecomp (prefix,c,t))
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index b97e01006..8ff0d727c 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -32,5 +32,8 @@ 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
+val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array ->
+			    lambda
+
+val before_match_int31 : bool -> prefix -> constructor -> lambda -> lambda
+
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 2a0052a60..7f2785cf9 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -260,6 +260,8 @@ let is_int (x:t) =
   let o = Obj.repr x in
   Obj.is_int o
 
+let to_int (x:t) = (Obj.magic x : int)
+
 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) -
@@ -334,3 +336,13 @@ let mk_I31_accu c x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17
   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
+
+let decomp_uint c v =
+  if is_int v then
+    let r = ref c in
+    let v = to_int v in
+    for i = 30 downto 0 do
+      r := (!r) (mk_int ((v lsr i) land 1));
+    done;
+    !r
+  else v
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 4c918e116..821b23168 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -113,3 +113,4 @@ val str_encode : 'a -> string
 val str_decode : string -> 'a
 
 val mk_I31_accu : t
+val decomp_uint : t -> t -> t
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index b39ae94a5..f4b57d085 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -141,7 +141,8 @@ type reactive_end = {(*information required by the compiler of the VM *)
       (bool -> Nativeinstr.prefix -> constructor ->
        Nativeinstr.lambda array -> Nativeinstr.lambda) option;
 
-  native_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
+  native_before_match : (bool -> Nativeinstr.prefix -> constructor ->
+			 Nativeinstr.lambda -> Nativeinstr.lambda) option;
 
   native_decompile_const : (int -> Term.constr) option
 }
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index ff084f71b..644fb7074 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -130,8 +130,9 @@ val get_native_constant_dynamic_info : retroknowledge -> entry ->
 				       Nativeinstr.lambda array ->
 				       Nativeinstr.lambda
 
-val get_native_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
-                                                       -> Cbytecodes.bytecodes
+val get_native_before_match_info : retroknowledge -> entry ->
+				   Nativeinstr.prefix -> constructor ->
+				   Nativeinstr.lambda -> Nativeinstr.lambda
 
 val get_native_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr
 
@@ -182,8 +183,9 @@ val add_native_constant_dynamic_info : retroknowledge -> entry ->
                                    retroknowledge
 
 val add_native_before_match_info : retroknowledge -> entry ->
-                              (bool->Cbytecodes.bytecodes->Cbytecodes.bytecodes) ->
-                              retroknowledge
+				   (bool -> Nativeinstr.prefix -> constructor ->
+				      Nativeinstr.lambda -> Nativeinstr.lambda) ->
+				   retroknowledge
 
 val add_native_decompile_constant_info : retroknowledge -> entry ->
                                     (int -> constr) -> retroknowledge