From f19ff322973c2dffd4f1f34386057ac1e08a227d Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@cs.harvard.edu>
Date: Wed, 22 Jul 2015 12:29:13 -0700
Subject: a small amount of documentation on the virtual machine.

---
 kernel/cbytecodes.mli | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'kernel/cbytecodes.mli')

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              *)
-- 
cgit v1.2.3