diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2014-04-06 14:59:59 -0400 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 01:05:48 -0400 |
commit | b0f3857eca168ee5d843e86b7678ac3d5375b07c (patch) | |
tree | 9e4f0916dbbe6e4826fb6dc4376d1e5d449e7183 /kernel | |
parent | aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 (diff) |
Full support for int31 values in native compiler.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/environ.ml | 11 | ||||
-rw-r--r-- | kernel/nativecode.ml | 13 | ||||
-rw-r--r-- | kernel/nativeinstr.mli | 1 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 24 | ||||
-rw-r--r-- | kernel/nativelambda.mli | 7 | ||||
-rw-r--r-- | kernel/nativevalues.ml | 12 | ||||
-rw-r--r-- | kernel/nativevalues.mli | 1 | ||||
-rw-r--r-- | kernel/retroknowledge.ml | 3 | ||||
-rw-r--r-- | kernel/retroknowledge.mli | 10 |
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 |