Vmbytecodes
module Label : sig ... end
type instruction =
| Klabel of Label.t | |
| Kacc of int | (* accu = sp |
| Kenvacc of int | (* accu = coq_env |
| Koffsetclosure of int | (* accu = &coq_env |
| 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 |
| Ksetfield of int | (* accu |
| 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 caml_prim * Label.t |
and bytecodes = instruction list
type fv = fv_elem array
val caml_prim_to_prim : caml_prim -> CPrimitives.t