aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-08 09:16:42 +0000
committerGravatar bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-08 09:16:42 +0000
commita26efb5269114b8c23f823b9eabcccbdc71a6e92 (patch)
treefc83958cf7c76678e18b80f9a6a47ba0d2c172f2 /kernel
parent8e4b7319caa0754401c8b868e9ce9490a867d7f1 (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.ml2
-rw-r--r--kernel/vm.ml52
-rw-r--r--kernel/vm.mli1
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