From 9c6487ba87f448daa28158c6e916e3d932c50645 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 20 Oct 2004 13:50:08 +0000
Subject: COMMITED BYTECODE COMPILER

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.ml | 39 ++++++++++++++++++++++++++++++++-------
 1 file changed, 32 insertions(+), 7 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 28628cbda7..85d668f7a4 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -317,16 +317,15 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
     fold 0 cuniv
   else raise NotConvertible
 
-
+let clos_fconv cv_pb env t1 t2 =
+  let infos = create_clos_infos betaiotazeta env in
+  ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
 
 let fconv cv_pb env t1 t2 =
-  if eq_constr t1 t2 then 
-    Constraint.empty
-  else
-    let infos = create_clos_infos betaiotazeta env in
-    ccnv cv_pb infos ELID ELID (inject t1) (inject t2)
-      Constraint.empty
+  if eq_constr t1 t2 then Constraint.empty
+  else clos_fconv cv_pb env t1 t2
 
+let conv_cmp = fconv
 let conv = fconv CONV
 let conv_leq = fconv CUMUL
 
@@ -341,6 +340,32 @@ let conv_leq_vecti env v1 v2 =
     v1
     v2
 
+(* option for conversion *)
+let use_vm = ref true
+let vm_fconv = ref (fun _ _ _ _ -> error "VM not installed")
+let set_vm_conv_cmp f = vm_fconv := f
+
+let vm_conv cv_pb env t1 t2 =
+  if eq_constr t1 t2 then 
+    Constraint.empty
+  else if !use_vm then
+    try !vm_fconv cv_pb env t1 t2
+    with Not_found | Invalid_argument _ ->
+      (* If compilation fails, fall-back to closure conversion *)
+      clos_fconv cv_pb env t1 t2
+  else clos_fconv cv_pb env t1 t2
+
+let vm_conv_leq_vecti env v1 v2 =
+  array_fold_left2_i 
+    (fun i c t1 t2 ->
+      let c' =
+        try vm_conv CUMUL env t1 t2 
+        with NotConvertible -> raise (NotConvertibleVect i) in
+      Constraint.union c c')
+    Constraint.empty
+    v1
+    v2
+
 (*
 let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";;
 let conv_leq env t1 t2 =
-- 
cgit v1.2.3