Int31 decompilation in native compiler was still partial. Now fixed.

3 files changed, 27 insertions, 9 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index be0b65d91..d306599ad 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -484,10 +484,13 @@ let register =
     add_native_compiling_info rk v (Nativelambda.compile_prim prim kn)
   in
 
-  let add_int31_before_match rk v =
+  let add_int31_before_match rk grp 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
+    match kind_of_term (Retroknowledge.find rk (KInt31 (grp,Int31Bits))) with
+    | Ind i31bit_type ->
+    add_native_before_match_info rk v (Nativelambda.before_match_int31 i31bit_type)
+    | _ ->
+       anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type")
   in
 
 fun env field value ->
@@ -525,14 +528,14 @@ fun env field value ->
   {env with retroknowledge =
   let retroknowledge_with_reactive_info =
   match field with
-    | KInt31 (_, Int31Type) ->
+    | KInt31 (grp, Int31Type) ->
         let i31c = match kind_of_term value with
                      | Ind i31t -> mkConstruct (i31t, 1)
 		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type")
 	in
 	add_int31_decompilation_from_type
 	  (add_int31_before_match
-	     (retroknowledge add_int31c env i31c) value)
+	     (retroknowledge add_int31c env i31c) grp value)
     | KInt31 (_, Int31Plus) -> add_int31_binop_from_const Cbytecodes.Kaddint31
 							  Primitives.Int31add
     | KInt31 (_, Int31PlusC) -> add_int31_binop_from_const Cbytecodes.Kaddcint31
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 631349c07..c9733c5fd 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -727,13 +727,27 @@ 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 =
+(* We are relying here on the order of digits constructors *)
+let digits_from_uint digits_ind prefix i =
+  let d0 = Lconstruct (prefix, (digits_ind, 1)) in
+  let d1 = Lconstruct (prefix, (digits_ind, 2)) in
+  let digits = Array.make 31 d0 in
+  for k = 0 to 30 do
+    if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then
+      digits.(30-k) <- d1
+  done;
+  digits
+
+let before_match_int31 digits_ind 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 (UintVal i) ->
+     let digits = digits_from_uint digits_ind prefix i in
+     mkLapp (Lconstruct (prefix,c)) digits
+  | Luint (UintDigits (prefix,c,args)) ->
+     mkLapp (Lconstruct (prefix,c)) args
   | _ -> Luint (UintDecomp (prefix,c,t))
 
 let compile_prim prim kn fc prefix args =
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index afebf8087..da1a07d5d 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -35,7 +35,8 @@ val compile_static_int31 : bool -> Constr.constr array -> lambda
 val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array ->
 			    lambda
 
-val before_match_int31 : bool -> prefix -> constructor -> lambda -> lambda
+val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda ->
+			 lambda
 
 val compile_prim : Primitives.t -> constant -> bool -> prefix -> lambda array ->
 		   lambda