diff options
Diffstat (limited to 'kernel/vm.ml')
-rw-r--r-- | kernel/vm.ml | 64 |
1 files changed, 53 insertions, 11 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index c24de162..ebf1e8fd 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-2012 *) (* \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 - + + |