From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 kernel/vm.ml | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

(limited to 'kernel/vm.ml')

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 =
-- 
cgit v1.2.3