New implementation of the conversion test, using normalization by evaluation to

native OCaml code.

Warning: the "retroknowledge" mechanism has not been ported to the native
compiler, because integers and persistent arrays will ultimately be defined as
primitive constructions. Until then, computation on numbers may be faster using
the VM, since it takes advantage of machine integers.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 1 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index c4c821a9e5..91ef038ee5 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -28,6 +28,9 @@ let cbv_vm env _ c =
   let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
   Vnorm.cbv_vm env c ctyp
 
+let cbv_native env _ c =
+  let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
+  Nativenorm.native_norm env c ctyp
 
 let set_strategy_one ref l  =
   let k =
@@ -206,7 +209,16 @@ let rec reduction_of_red_expr = function
     let redfun = contextually b lp vmfun in
     (redfun, VMcast)
   | CbvVm None -> (cbv_vm, VMcast)
-
+  | CbvNative (Some lp) ->
+    let b = is_reference (snd lp) in
+    let lp = out_with_occurrences lp in
+    let nativefun _ env map c =
+      let tpe = Retyping.get_type_of env map c in
+      Nativenorm.native_norm env c tpe
+    in
+    let redfun = contextually b lp nativefun in
+    (redfun, NATIVEcast)
+  | CbvNative None -> (cbv_native, NATIVEcast)
 
 let subst_flags subs flags =
   { flags with rConst = List.map subs flags.rConst }