Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 53 insertions, 11 deletions

diff --git a/kernel/vm.ml b/kernel/vm.ml
index c24de162..86aed5d9 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vm.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Names
 open Term
 open Conv_oracle
@@ -462,7 +460,7 @@ let current_cofix vcf =
       else find_cofix (pos+1)
     else raise Not_found in
   try find_cofix 0
-  with _ -> assert false
+  with Not_found -> assert false
 
 let check_cofix vcf1 vcf2 =
   (current_cofix vcf1 = current_cofix vcf2) &&
@@ -538,13 +536,8 @@ let branch_of_switch k sw =
   Array.map eval_branch sw.sw_annot.rtbl
 
 
-(* Evaluation *)
-
 
-let is_accu v =
-  let o = Obj.repr v in
-  Obj.is_block o && Obj.tag o = accu_tag &&
-  fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag
+(* Evaluation *)
 
 let rec whd_stack v stk =
   match stk with
@@ -594,6 +587,55 @@ let rec force_whd v stk =
   | res -> res
 
 
+let rec eta_stack a stk v =
+  match stk with
+  | [] -> apply_vstack a [|v|]
+  | Zapp args :: stk -> eta_stack (apply_arguments a args) stk v
+  | Zfix(f,args) :: stk ->
+      let a,stk = 
+	match stk with
+	| Zapp args' :: stk ->
+	    push_ra stop;
+	    push_arguments args';
+	    push_val a;
+	    push_arguments args;
+	    let a =
+	      interprete (fun_code f) (Obj.magic f) (Obj.magic f)
+		(nargs args+ nargs args') in
+	    a, stk
+	| _ -> 
+	    push_ra stop;
+	    push_val a;
+	    push_arguments args;
+	    let a =
+	      interprete (fun_code f) (Obj.magic f) (Obj.magic f)
+		(nargs args) in
+	    a, stk in
+      eta_stack a stk v
+  | Zswitch sw :: stk ->
+      eta_stack (apply_switch sw a) stk v
+
+let eta_whd k whd =
+  let v = val_of_rel k in
+  match whd with
+  | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false
+  | Vfun f -> body_of_vfun k f
+  | Vfix(f, None) -> 
+      push_ra stop;
+      push_val v;
+      interprete (fun_code f) (Obj.magic f) (Obj.magic f) 0
+  | Vfix(f, Some args) ->
+      push_ra stop;
+      push_val v;
+      push_arguments args;
+      interprete (fun_code f) (Obj.magic f) (Obj.magic f) (nargs args) 
+  | Vcofix(_,to_up,_) ->
+      push_ra stop;
+      push_val v;
+      interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0
+  | Vatom_stk(a,stk) ->
+      eta_stack (val_of_atom a) stk v 
 
 
-
+      
+