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

1 files changed, 17 insertions, 3 deletions

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 631349c074..c9733c5fd8 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 =