Int31 literals in native compiler.

6 files changed, 87 insertions, 34 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 5fa0d41e0..511bb5f77 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -257,6 +257,7 @@ type primitive =
   | Cast_accu
   | Upd_cofix
   | Force_cofix
+  | Mk_uint
   | Mk_meta
   | Mk_evar
 
@@ -298,8 +299,9 @@ let primitive_hash = function
 | Cast_accu -> 11
 | Upd_cofix -> 12
 | Force_cofix -> 13
-| Mk_meta -> 14
-| Mk_evar -> 15
+| Mk_uint -> 14
+| Mk_meta -> 15
+| Mk_evar -> 16
 
 type mllambda =
   | MLlocal        of lname 
@@ -314,7 +316,8 @@ type mllambda =
                               (* argument, prefix, accu branch, branches *)
   | MLconstruct    of string * constructor * mllambda array
                    (* prefix, constructor name, arguments *)
-  | MLint          of bool * int   (* true if the type sould be int *)
+  | MLint          of int
+  | MLuint         of Uint31.t
   | MLsetref       of string * mllambda
   | MLsequence     of mllambda * mllambda
 
@@ -371,8 +374,10 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
       String.equal pf1 pf2 &&
       eq_constructor cs1 cs2 &&
       Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2
-  | MLint (ty1,v1), MLint (ty2,v2) ->
-      ty1 == ty2 && Int.equal v1 v2
+  | MLint i1, MLint i2 ->
+      Int.equal i1 i2
+  | MLuint i1, MLuint i2 ->
+      Uint31.equal i1 i2
   | MLsetref (id1, ml1), MLsetref (id2, ml2) ->
       String.equal id1 id2 &&
       eq_mllambda gn1 gn2 n env1 env2 ml1 ml2
@@ -440,16 +445,18 @@ let rec hash_mllambda gn n env t =
       let hpf = String.hash pf in
       let hcs = constructor_hash cs in
       combinesmall 10 (hash_mllambda_array gn n env (combine hpf hcs) args)
-  | MLint (ty,v) ->
-      combinesmall 11 (combine (if ty then 0 else 1) v)
+  | MLint i ->
+      combinesmall 11 i
+  | MLuint i ->
+      combinesmall 12 (Uint31.to_int i)
   | MLsetref (id, ml) ->
       let hid = String.hash id in
       let hml = hash_mllambda gn n env ml in
-      combinesmall 12 (combine hid hml)
+      combinesmall 13 (combine hid hml)
   | MLsequence (ml, ml') ->
       let hml = hash_mllambda gn n env ml in
       let hml' = hash_mllambda gn n env ml' in
-      combinesmall 13 (combine hml hml')
+      combinesmall 14 (combine hml hml')
 
 and hash_mllambda_letrec gn n env init defs =
   let hash_def (_,args,ml) =
@@ -480,7 +487,7 @@ let fv_lam l =
     match l with
     | MLlocal l ->
 	if LNset.mem l bind then fv else LNset.add l fv
-    | MLglobal _ | MLprimitive _  | MLint _ -> fv
+    | MLglobal _ | MLprimitive _  | MLint _ | MLuint _ -> fv
     | MLlam (ln,body) ->
 	let bind = Array.fold_right LNset.add ln bind in
 	aux body bind fv
@@ -731,7 +738,7 @@ let fv_args env fvn fvr =
   if Int.equal size 0 then empty_args 
   else 
     begin
-      let args = Array.make size (MLint (false,0)) in
+      let args = Array.make size (MLint 0) in
       let fvn = ref fvn in
       let i = ref 0 in
       while not (List.is_empty !fvn) do
@@ -751,28 +758,36 @@ let fv_args env fvn fvr =
     end
 
 let get_value_code i =
-  MLapp (MLglobal (Ginternal "get_value"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+  MLapp (MLglobal (Ginternal "get_value"),
+    [|MLglobal symbols_tbl_name; MLint i|])
 
 let get_sort_code i =
-  MLapp (MLglobal (Ginternal "get_sort"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+  MLapp (MLglobal (Ginternal "get_sort"),
+    [|MLglobal symbols_tbl_name; MLint i|])
 
 let get_name_code i =
-  MLapp (MLglobal (Ginternal "get_name"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+  MLapp (MLglobal (Ginternal "get_name"),
+    [|MLglobal symbols_tbl_name; MLint i|])
 
 let get_const_code i =
-  MLapp (MLglobal (Ginternal "get_const"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+  MLapp (MLglobal (Ginternal "get_const"),
+    [|MLglobal symbols_tbl_name; MLint i|])
 
 let get_match_code i =
-  MLapp (MLglobal (Ginternal "get_match"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+  MLapp (MLglobal (Ginternal "get_match"),
+    [|MLglobal symbols_tbl_name; MLint i|])
 
 let get_ind_code i =
-  MLapp (MLglobal (Ginternal "get_ind"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+  MLapp (MLglobal (Ginternal "get_ind"),
+    [|MLglobal symbols_tbl_name; MLint i|])
 
 let get_meta_code i =
-  MLapp (MLglobal (Ginternal "get_meta"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+  MLapp (MLglobal (Ginternal "get_meta"),
+    [|MLglobal symbols_tbl_name; MLint i|])
 
 let get_evar_code i =
-  MLapp (MLglobal (Ginternal "get_evar"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+  MLapp (MLglobal (Ginternal "get_evar"),
+    [|MLglobal symbols_tbl_name; MLint i|])
 
 type rlist =
   | Rnil 
@@ -1042,6 +1057,7 @@ let merge_branches t =
       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|])
   | Lval v ->
       let i = push_symbol (SymbValue v) in get_value_code i
   | Lsort s ->
@@ -1077,7 +1093,7 @@ let mllambda_of_lambda auxdefs l t =
 
 let can_subst l = 
   match l with
-  | MLlocal _ | MLint _ | MLglobal _ -> true
+  | MLlocal _ | MLint _ | MLuint _ | MLglobal _ -> true
   | _ -> false
 
 let subst s l =
@@ -1086,7 +1102,7 @@ let subst s l =
     let rec aux l =
       match l with
       | MLlocal id -> (try LNmap.find id s with Not_found -> l)
-      | MLglobal _ | MLprimitive _ | MLint _ -> l
+      | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> l
       | MLlam(params,body) -> MLlam(params, aux body)
       | MLletrec(defs,body) ->
 	let arec (f,params,body) = (f,params,aux body) in
@@ -1154,7 +1170,7 @@ let optimize gdef l =
   let rec optimize s l =
     match l with
     | MLlocal id -> (try LNmap.find id s with Not_found -> l)
-    | MLglobal _ | MLprimitive _ | MLint _ -> l
+    | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> l
     | MLlam(params,body) -> 
 	MLlam(params, optimize s body)
     | MLletrec(decls,body) ->
@@ -1352,9 +1368,8 @@ let pp_mllam fmt l =
     | MLconstruct(prefix,c,args) ->
         Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]" 
           (string_of_construct prefix c) pp_cargs args
-    | MLint(int, i) ->
-	if int then pp_int fmt i
-	else Format.fprintf fmt "(val_of_int %a)" pp_int i
+    | MLint i -> pp_int fmt i
+    | MLuint i -> Format.fprintf fmt "(Uint31.of_int %a)" pp_int (Uint31.to_int i)
     | MLsetref (s, body) ->
 	Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body
     | MLsequence(l1,l2) ->
@@ -1454,6 +1469,7 @@ let pp_mllam fmt l =
     | Cast_accu -> Format.fprintf fmt "cast_accu"
     | Upd_cofix -> Format.fprintf fmt "upd_cofix"
     | Force_cofix -> Format.fprintf fmt "force_cofix"
+    | Mk_uint -> Format.fprintf fmt "mk_uint"
     | Mk_meta -> Format.fprintf fmt "mk_meta_accu"
     | Mk_evar -> Format.fprintf fmt "mk_evar_accu"
   in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index a757f013a..376de3980 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -34,6 +34,7 @@ type lambda =
 	(* A fully applied constructor *)
   | Lconstruct    of string * constructor (* prefix, constructor name *)
 	(* A partially applied constructor *)
+  | Luint          of Uint31.t
   | Lval          of Nativevalues.t
   | Lsort         of sorts
   | Lind          of string * inductive (* prefix, inductive name *)
@@ -110,8 +111,8 @@ let get_const_prefix env c =
 
 let map_lam_with_binders g f n lam =
   match lam with
-  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lconstruct _
-  | Llazy | Lforce | Lmeta _ | Levar _ -> lam
+  | Lrel _ | Lvar _  | Lconst _ | Luint _ | Lval _ | Lsort _ | Lind _
+  | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> lam
   | Lprod(dom,codom) -> 
       let dom' = f n dom in
       let codom' = f n codom in
@@ -313,7 +314,7 @@ let rec occurence k kind lam =
       if Int.equal n k then 
 	if kind then false else raise Not_found
       else kind
-  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _
+  | Lvar _  | Lconst _  | Luint _ | Lval _ | Lsort _ | Lind _
   | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind
   | Lprod(dom, codom) ->
       occurence k (occurence k kind dom) codom
@@ -666,8 +667,23 @@ and lambda_of_app env sigma f args =
       let expected = nparams + arity in
       let nargs = Array.length args in
       if Int.equal nargs expected then 
-	let args = lambda_of_args env sigma nparams args in
-	makeblock !global_env c tag args
+(*        try
+	  try
+	    Bstrconst (Retroknowledge.get_vm_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 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)
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 98314348a..751f11978 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -32,6 +32,7 @@ type lambda =
 	(* A fully applied constructor *)
   | Lconstruct    of string * constructor (* prefix, constructor name *)
 	(* A partially applied constructor *)
+  | Luint          of Uint31.t
   | Lval          of Nativevalues.t
   | Lsort         of sorts
   | Lind          of string * inductive (* prefix, inductive name *)
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 632889080..b7fb6956f 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -126,7 +126,21 @@ type reactive_end = {(*information required by the compiler of the VM *)
   (* 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}
+  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->Cbytecodes.structured_constant)
+      option;
+  native_constant_dynamic :
+      (bool->Cbytecodes.comp_env->Cbytecodes.block array->int->
+         Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+      option;
+  native_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
+  native_decompile_const : (int -> Term.constr) option
+}
 
 
 
@@ -162,7 +176,13 @@ let empty_reactive_end =
     vm_constant_static = None;
     vm_constant_dynamic = None;
     vm_before_match = None;
-    vm_decompile_const = None }
+    vm_decompile_const = None;
+    native_compiling = None;
+    native_constant_static = None;
+    native_constant_dynamic = None;
+    native_before_match = None;
+    native_decompile_const = None
+  }
 
 
 
diff --git a/kernel/uint31.ml b/kernel/uint31.ml
index 8c6e2c14c..0f1c1444b 100644
--- a/kernel/uint31.ml
+++ b/kernel/uint31.ml
@@ -117,7 +117,7 @@ let le_32 x y =
 let le_64 (x:int) (y:int) = x <= y
 let le = select le_32 le_64
 
-let eq x y = x == y
+let equal (x:int) (y:int) = x == y
     
 let cmp_32 x y = Int32.compare (uint_32 x) (uint_32 y)
 (* Do not remove the type information it is really important for 
diff --git a/kernel/uint31.mli b/kernel/uint31.mli
index 2094df6fa..fdfb2d95a 100644
--- a/kernel/uint31.mli
+++ b/kernel/uint31.mli
@@ -29,7 +29,7 @@ val div21   : t -> t -> t -> t * t
       
       (* comparison *)
 val lt      : t -> t -> bool
-val eq      : t -> t -> bool
+val equal   : t -> t -> bool
 val le      : t -> t -> bool
 val compare : t -> t -> int