Module Vmbytecodes
module Label : sig ... endtype instruction=|Klabel of Label.t|Kacc of intaccu = sp
n|Kenvacc of intaccu = coq_env
n|Koffsetclosure of intaccu = &coq_env
n|Kpushsp = accu :: sp
|Kpop of intsp = skipn n sp
|Kpush_retaddr of Label.tsp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0
|Kshort_apply of intnumber of arguments (arguments on top of stack)
|Kapply of intnumber of arguments (arguments on top of stack)
|Kappterm of int * intnumber of arguments, slot size
|Kreturn of intslot size
|Kjump|Krestart|Kgrab of intnumber of arguments
|Kgrabrec of intrec arg
|Kclosure of Label.t * intlabel, number of free variables
|Kclosurerec of int * int * Label.t array * Label.t arraynb fv, init, lbl types, lbl bodies
|Kclosurecofix of int * int * Label.t array * Label.t arraynb fv, init, lbl types, lbl bodies
|Kgetglobal of Names.Constant.t|Kconst of Vmvalues.structured_constant|Kmakeblock of int * Vmvalues.tagallocate an ocaml block. Index 0 ** is accu, all others are popped from ** the top of the stack
|Kmakeswitchblock of Label.t * Label.t * Vmvalues.annot_switch * int|Kswitch of Label.t array * Label.t arrayconsts,blocks
|Kpushfields of int|Kfield of intaccu = accu
n|Ksetfield of intaccu
n= sp0; sp = pop sp|Kstop|Ksequence of bytecodes|Kproj of Names.Projection.Repr.t|Kensurestackcapacity of int|Kbranch of Label.tjump to label, is it needed ?
|Kprim of CPrimitives.t * Constr.pconstant|Kcamlprim of CPrimitives.t * Label.tand bytecodes= instruction list
type fv_elem=|FVnamed of Names.Id.t|FVrel of int|FVuniv_var of int|FVevar of Evar.ttype fv= fv_elem array