COMMITED BYTECODE COMPILER

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

11 files changed, 32 insertions, 12 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index ceb23cc782..33a9272d04 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -15,6 +15,7 @@ open Names
 open Environ
 open Univ
 open Evd
+open Conv_oracle
 open Closure
 open Esubst
 
@@ -91,7 +92,7 @@ let contract_cofixp env (i,(_,_,bds as bodies)) =
   subst_bodies_from_i 0 env, bds.(i)
 
 let make_constr_ref n = function
-  | FarRelKey p -> mkRel (n+p)
+  | RelKey p -> mkRel (n+p)
   | VarKey id -> mkVar id
   | ConstKey cst -> mkConst cst
 
@@ -127,7 +128,7 @@ let stack_app appl stack =
 open RedFlags
 
 let red_set_ref flags = function
-  | FarRelKey _ -> red_set flags fDELTA
+  | RelKey _ -> red_set flags fDELTA
   | VarKey id -> red_set flags (fVAR id)
   | ConstKey sp -> red_set flags (fCONST sp)
 
@@ -195,7 +196,7 @@ let rec norm_head info env t stack =
         | Inl (0,v)      -> strip_appl v stack
         | Inl (n,v)      -> strip_appl (shift_value n v) stack
         | Inr (n,None)   -> (VAL(0, mkRel n), stack)
-        | Inr (n,Some p) -> norm_head_ref (n-p) info env stack (FarRelKey p))
+        | Inr (n,Some p) -> norm_head_ref (n-p) info env stack (RelKey p))
 
   | Var id -> norm_head_ref 0 info env stack (VarKey id)
 
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 1214663346..981692ebdb 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -17,6 +17,7 @@ open Termops
 open Sign
 open Environ
 open Evd
+open Reduction
 open Reductionops
 open Rawterm
 open Pattern
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2ed26c92c5..93d9ba9064 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -11,6 +11,7 @@
 open Util
 open Names
 open Term
+open Reduction
 open Reductionops
 open Closure
 open Environ
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 52a8997144..c199eb0083 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -458,7 +458,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
   let (isevars',_,rsign) = 
     array_fold_left2
       (fun (isevars,sgn,rsgn) a1 a2 ->
-        let (isevars',b) = conv_algo env isevars CONV a1 a2 in
+        let (isevars',b) = conv_algo env isevars Reduction.CONV a1 a2 in
 	 if b then 
 	   (isevars',List.tl sgn, add_named_decl (List.hd sgn) rsgn)
 	 else 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index e9c60e18ec..5c0f42852d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -198,10 +198,7 @@ type hole_kind =
   | InternalHole
   | TomatchTypeParameter of inductive * int
 
-type conv_pb = 
-  | CONV 
-  | CUMUL
-
+type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * constr * constr
 type evar_defs =
     { evars : evar_map;
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 4487c92209..9f10d2dfe8 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -129,9 +129,7 @@ val evar_define : evar -> constr -> evar_defs -> evar_defs
 val evar_source : existential_key -> evar_defs -> loc * hole_kind
 
 (* Unification constraints *)
-type conv_pb = 
-  | CONV 
-  | CUMUL
+type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * constr * constr
 val add_conv_pb :  evar_constraint -> evar_defs -> evar_defs
 val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 0a9722b878..d93a583c40 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -350,6 +350,7 @@ type ('a,'b) red_expr_gen =
   | Fold of 'a list
   | Pattern of 'a occurrences list
   | ExtraRedExpr of string * 'a
+  | CbvVm
 
 type ('a,'b) may_eval =
   | ConstrTerm of 'a
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index ff1f86c58a..7e8b8b8949 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -123,6 +123,7 @@ type ('a,'b) red_expr_gen =
   | Fold of 'a list
   | Pattern of 'a occurrences list
   | ExtraRedExpr of string * 'a
+  | CbvVm
 
 type ('a,'b) may_eval =
   | ConstrTerm of 'a
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a48881bd74..9ec71866b9 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -285,6 +285,17 @@ let reference_eval sigma env = function
        end)
   | ref -> compute_consteval sigma env ref
 
+let rev_firstn_liftn fn ln = 
+  let rec rfprec p res l = 
+    if p = 0 then 
+      res 
+    else
+      match l with
+        | [] -> invalid_arg "Reduction.rev_firstn_liftn"
+        | a::rest -> rfprec (p-1) ((lift ln a)::res) rest
+  in 
+  rfprec fn []
+
 (* If f is bound to EliminationFix (n',infos), then n' is the minimal
    number of args for starting the reduction and infos is
    (nbfix,[(yi1,Ti1);...;(yip,Tip)],n) indicating that f converts
@@ -292,7 +303,6 @@ let reference_eval sigma env = function
    yij = Rel(n+1-j)
 
    f is applied to largs and we need for recursive calls to build the function
-
       g := [xp:Tip',...,x1:Ti1'](f a1 ... an)
 
    s.t. (g u1 ... up) reduces to (Fix(..) u1 ... up)
@@ -790,6 +800,11 @@ let cbv_betadeltaiota env sigma =  cbv_norm_flags betadeltaiota env sigma
 
 let compute = cbv_betadeltaiota
 
+(* call by value reduction functions using virtual machine *)
+let cbv_vm env _ c =
+  let ctyp = (fst (Typeops.infer env c)).uj_type in
+  Vconv.cbv_vm env c ctyp
+
 (* Pattern *)
 
 (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only
@@ -860,6 +875,7 @@ let reduction_of_redexp = function
   | ExtraRedExpr (s,c) ->
       (try Stringmap.find s !red_expr_tab
       with Not_found -> error("unknown user-defined reduction \""^s^"\""))
+  | CbvVm -> cbv_vm 
 (* Used in several tactics. *)
 
 exception NotStepReducible
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 2ac908ad47..0c093694c1 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -51,6 +51,9 @@ val cbv_norm_flags : Closure.RedFlags.reds ->  reduction_function
   val cbv_betadeltaiota :  reduction_function
   val compute :  reduction_function  (* = [cbv_betadeltaiota] *)
 
+(* Call by value strategy (uses virtual machine) *)
+val cbv_vm : reduction_function
+
 (* [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
    with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 314e361c3a..b5e175dd82 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -17,6 +17,7 @@ open Termops
 open Sign
 open Environ
 open Evd
+open Reduction
 open Reductionops
 open Rawterm
 open Pattern