diff options
| author |  Gregory Malecha <gmalecha@cs.harvard.edu> | 2015-07-22 12:29:13 -0700 |
|---|---|---|
| committer |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-07-23 07:10:33 +0200 |
| commit | f19ff322973c2dffd4f1f34386057ac1e08a227d (patch) | |
| tree | 93f2733d2f2e6639e53f72e12184ac63e593ecb3 /kernel/cbytecodes.mli | |
| parent | d95d2f57c795195eb8fff75a01fc50b1016ce1ca (diff) | |
a small amount of documentation on the virtual machine.
Diffstat (limited to 'kernel/cbytecodes.mli')
| -rw-r--r-- | kernel/cbytecodes.mli | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 745ef311b..8f594a45b 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -44,13 +44,13 @@ module Label : type instruction = | Klabel of Label.t - | Kacc of int - | Kenvacc of int - | Koffsetclosure of int - | Kpush - | Kpop of int - | Kpush_retaddr of Label.t - | Kapply of int (** number of arguments *) + | 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 *) + | 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 @@ -62,15 +62,15 @@ type instruction = (** 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 pconstant + | Kgetglobal of pconstant (** accu = coq_global_data[c] *) | Kconst of structured_constant - | Kmakeblock of int * tag (** size, tag *) + | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block *) | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int | Kswitch of Label.t array * Label.t array (** consts,blocks *) | Kpushfields of int - | Kfield of int - | Ksetfield of int + | Kfield of int (** accu = accu[n] *) + | Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *) | Kstop | Ksequence of bytecodes * bytecodes | Kproj of int * Constant.t (** index of the projected argument, @@ -136,9 +136,9 @@ type vm_env = { type comp_env = { - nb_stack : int; (** nbre de variables sur la pile *) - in_stack : int list; (** position dans la pile *) - nb_rec : int; (** nbre de fonctions mutuellement *) + nb_stack : int; (** number of variables on the stack *) + in_stack : int list; (** position in the stack *) + nb_rec : int; (** number of mutually recursive functions *) (** recursives = nbr *) pos_rec : instruction list; (** instruction d'acces pour les variables *) (** de point fix ou de cofix *) |