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/nativelambda.ml | |
| parent | aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 (diff) | |
Full support for int31 values in native compiler.
Diffstat (limited to 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 24 |
1 files changed, 23 insertions, 1 deletions
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)) |