diff options
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index 70298764..53483a22 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -170,7 +170,7 @@ type whd = external push_ra : tcode -> unit = "coq_push_ra" external push_val : values -> unit = "coq_push_val" external push_arguments : arguments -> unit = "coq_push_arguments" -external push_vstack : vstack -> unit = "coq_push_vstack" +external push_vstack : vstack -> int -> unit = "coq_push_vstack" (* interpreteur *) @@ -206,7 +206,9 @@ let apply_varray vf varray = else begin push_ra stop; - push_vstack varray; + (* The fun code of [vf] will make sure we have enough stack, so we put 0 + here. *) + push_vstack varray 0; interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end @@ -232,7 +234,7 @@ let uni_lvl_val (v : values) : Univ.universe_level = | Vatom_stk (a,stk) -> str "Vatom_stk" | _ -> assert false in - Errors.anomaly + CErrors.anomaly Pp.( strbrk "Parsing virtual machine value expected universe level, got " ++ pr) @@ -282,7 +284,7 @@ let rec whd_accu a stk = | _ -> assert false end | tg -> - Errors.anomaly + CErrors.anomaly Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg) external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" @@ -306,7 +308,7 @@ let whd_val : values -> whd = | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) + | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) else Vconstr_block(Obj.obj o) @@ -560,7 +562,9 @@ let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl let case_info sw = sw.sw_annot.ci let type_of_switch sw = - push_vstack sw.sw_stk; + (* The fun code of types will make sure we have enough stack, so we put 0 + here. *) + push_vstack sw.sw_stk 0; interprete sw.sw_type_code crazy_val sw.sw_env 0 let branch_arg k (tag,arity) = @@ -580,9 +584,10 @@ let branch_arg k (tag,arity) = let apply_switch sw arg = let tc = sw.sw_annot.tailcall in if tc then - (push_ra stop;push_vstack sw.sw_stk) + (push_ra stop;push_vstack sw.sw_stk sw.sw_annot.max_stack_size) else - (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); + (push_vstack sw.sw_stk sw.sw_annot.max_stack_size; + push_ra (popstop_code (Array.length sw.sw_stk))); interprete sw.sw_code arg sw.sw_env 0 let branch_of_switch k sw = |