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/cbytecodes.ml | 28 +++++++++++++++++++++++-----
 1 file changed, 23 insertions(+), 5 deletions(-)

(limited to 'kernel/cbytecodes.ml')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index f9cf2691..810c3469 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -43,7 +43,7 @@ type structured_constant =
 type reloc_table = (tag * int) array
 
 type annot_switch =
-   {ci : case_info; rtbl : reloc_table; tailcall : bool}
+   {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
 
 module Label =
   struct
@@ -87,6 +87,7 @@ type instruction =
   | Ksequence of bytecodes * bytecodes
   | Kproj of int * Constant.t  (* index of the projected argument,
                                            name of projection *)
+  | Kensurestackcapacity of int
 (* spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (* jump to label *)
   | Kaddint31                           (* adds the int31 in the accu
@@ -142,11 +143,29 @@ type fv = fv_elem array
 exception NotClosed
 
 
+module Fv_elem =
+struct
+type t = fv_elem
+
+let compare e1 e2 = match e1, e2 with
+| FVnamed id1, FVnamed id2 -> Id.compare id1 id2
+| FVnamed _, _ -> -1
+| FVrel _, FVnamed _ -> 1
+| FVrel r1, FVrel r2 -> Int.compare r1 r2
+| FVrel _, FVuniv_var _ -> -1
+| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2
+| FVuniv_var i1, _ -> 1
+
+end
+
+module FvMap = Map.Make(Fv_elem)
+
 (*spiwack: both type have been moved from Cbytegen because I needed then
   for the retroknowledge *)
 type vm_env = {
     size : int;              (* longueur de la liste [n] *)
-    fv_rev : fv_elem list    (* [fvn; ... ;fv1] *)
+    fv_rev : fv_elem list;   (* [fvn; ... ;fv1] *)
+    fv_fwd : int FvMap.t;    (* reverse mapping *)
   }
 
 
@@ -184,9 +203,6 @@ let rec pp_struct_const = function
 
 let pp_lbl lbl = str "L" ++ int lbl
 
-let pp_pcon (id,u) =
-  pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}"
-
 let pp_fv_elem = function
   | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
   | FVrel i -> str "Rel(" ++ int i ++ str ")"
@@ -249,6 +265,8 @@ let rec pp_instr i =
 
   | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p
 
+  | Kensurestackcapacity size -> str "growstack " ++ int size
+
   | Kaddint31 -> str "addint31"
   | Kaddcint31 -> str "addcint31"
   | Kaddcarrycint31 -> str "addcarrycint31"
-- 
cgit v1.2.3