diff options
| author |  bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-08 09:16:42 +0000 |
|---|---|---|
| committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-08 09:16:42 +0000 |
| commit | a26efb5269114b8c23f823b9eabcccbdc71a6e92 (patch) | |
| tree | fc83958cf7c76678e18b80f9a6a47ba0d2c172f2 /kernel | |
| parent | 8e4b7319caa0754401c8b868e9ce9490a867d7f1 (diff) | |
adding eta in the vm
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13896 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/vconv.ml | 2 | ||||
| -rw-r--r-- | kernel/vm.ml | 52 | ||||
| -rw-r--r-- | kernel/vm.mli | 1 |
3 files changed, 54 insertions, 1 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 96445f696..bf3640e35 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -74,6 +74,8 @@ and conv_whd pb k whd1 whd2 cu = else raise NotConvertible | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom pb k a1 stk1 a2 stk2 cu + | Vfun _, _ | _, Vfun _ -> + conv_val CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu | _, Vatom_stk(Aiddef(_,v),stk) -> conv_whd pb k whd1 (force_whd v stk) cu | Vatom_stk(Aiddef(_,v),stk), _ -> diff --git a/kernel/vm.ml b/kernel/vm.ml index 51528dbf2..86aed5d93 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -536,6 +536,7 @@ let branch_of_switch k sw = Array.map eval_branch sw.sw_annot.rtbl + (* Evaluation *) let rec whd_stack v stk = @@ -586,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 - + + diff --git a/kernel/vm.mli b/kernel/vm.mli index cd5999f04..58228eb85 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -117,4 +117,5 @@ val branch_of_switch : int -> vswitch -> (int * values) array val whd_stack : values -> stack -> whd val force_whd : values -> stack -> whd +val eta_whd : int -> whd -> values |