Module Vmbytecodes
module Label : sig ... end
type instruction
=
|
Klabel of Label.t
|
Kacc of int
accu = sp
n
|
Kenvacc of int
accu = coq_env
n
|
Koffsetclosure of int
accu = &coq_env
n
|
Kpush
sp = accu :: sp
|
Kpop of int
sp = skipn n sp
|
Kpush_retaddr of Label.t
sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0
|
Kshort_apply of int
number of arguments (arguments on top of stack)
|
Kapply of int
number of arguments (arguments on top of stack)
|
Kappterm of int * int
number of arguments, slot size
|
Kreturn of int
slot size
|
Kjump
|
Krestart
|
Kgrab of int
number of arguments
|
Kgrabrec of int
rec arg
|
Kclosure of Label.t * int
label, number of free variables
|
Kclosurerec of int * int * Label.t array * Label.t array
nb fv, init, lbl types, lbl bodies
|
Kclosurecofix of int * int * Label.t array * Label.t array
nb fv, init, lbl types, lbl bodies
|
Kgetglobal of Names.Constant.t
|
Kconst of Vmvalues.structured_constant
|
Kmakeblock of int * Vmvalues.tag
allocate 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 array
consts,blocks
|
Kpushfields of int
|
Kfield of int
accu = accu
n
|
Ksetfield of int
accu
n
= sp0
; sp = pop sp|
Kstop
|
Ksequence of bytecodes
|
Kproj of Names.Projection.Repr.t
|
Kensurestackcapacity of int
|
Kbranch of Label.t
jump to label, is it needed ?
|
Kprim of CPrimitives.t * Constr.pconstant
|
Kcamlprim of CPrimitives.t * Label.t
and bytecodes
= instruction list
type fv_elem
=
|
FVnamed of Names.Id.t
|
FVrel of int
|
FVuniv_var of int
|
FVevar of Evar.t
type fv
= fv_elem array