diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /kernel/cbytecodes.mli | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'kernel/cbytecodes.mli')
-rw-r--r-- | kernel/cbytecodes.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 6fa0841a..b8de7619 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -39,7 +39,7 @@ val pp_struct_const : structured_constant -> Pp.std_ppcmds 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 : sig @@ -84,6 +84,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, is it needed ? *) @@ -139,11 +140,14 @@ type fv = fv_elem array closed terms. *) exception NotClosed +module FvMap : Map.S with type key = fv_elem + (*spiwack: both type have been moved from Cbytegen because I needed them for the retroknowledge *) type vm_env = { size : int; (** length of the list [n] *) - fv_rev : fv_elem list (** [fvn; ... ;fv1] *) + fv_rev : fv_elem list; (** [fvn; ... ;fv1] *) + fv_fwd : int FvMap.t; (** reverse mapping *) } |