From f73d7c4614d000f068550b5144d80b7eceed58e9 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 29 Apr 2010 09:56:37 +0000 Subject: Move from ocamlweb to ocamdoc to generate mli documentation dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/cbytecodes.mli | 85 ++++++++++++++++++++++++++------------------------- 1 file changed, 43 insertions(+), 42 deletions(-) (limited to 'kernel/cbytecodes.mli') diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index f4dc0b14d..a8860d6d8 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -38,42 +38,43 @@ type instruction = | Kpush | Kpop of int | Kpush_retaddr of Label.t - | Kapply of int (* number of arguments *) - | Kappterm of int * int (* number of arguments, slot size *) - | Kreturn of int (* slot size *) + | Kapply of int (** number of arguments *) + | 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 *) + | 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 *) + (** nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array - (* nb fv, init, lbl types, lbl bodies *) + (** nb fv, init, lbl types, lbl bodies *) | Kgetglobal of constant | Kconst of structured_constant - | Kmakeblock of int * tag (* size, tag *) + | Kmakeblock of int * tag (** size, tag *) | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int - | Kswitch of Label.t array * Label.t array (* consts,blocks *) + | Kswitch of Label.t array * Label.t array (** consts,blocks *) | Kpushfields of int | Kfield of int | Ksetfield of int | Kstop | Ksequence of bytecodes * bytecodes -(* spiwack: instructions concerning integers *) - | Kbranch of Label.t (* jump to label, is it needed ? *) - | Kaddint31 (* adds the int31 in the accu + +(** spiwack: instructions concerning integers *) + | Kbranch of Label.t (** jump to label, is it needed ? *) + | Kaddint31 (** adds the int31 in the accu and the one ontop of the stack *) - | Kaddcint31 (* makes the sum and keeps the carry *) - | Kaddcarrycint31 (* sum +1, keeps the carry *) - | Ksubint31 (* subtraction modulo *) - | Ksubcint31 (* subtraction, keeps the carry *) - | Ksubcarrycint31 (* subtraction -1, keeps the carry *) - | Kmulint31 (* multiplication modulo *) - | Kmulcint31 (* multiplication, result in two + | Kaddcint31 (** makes the sum and keeps the carry *) + | Kaddcarrycint31 (** sum +1, keeps the carry *) + | Ksubint31 (** subtraction modulo *) + | Ksubcint31 (** subtraction, keeps the carry *) + | Ksubcarrycint31 (** subtraction -1, keeps the carry *) + | Kmulint31 (** multiplication modulo *) + | Kmulcint31 (** multiplication, result in two int31, for exact computation *) - | Kdiv21int31 (* divides a double size integer + | Kdiv21int31 (** divides a double size integer (represented by an int31 in the accumulator and one on the top of the stack) by an int31. The result @@ -81,23 +82,23 @@ type instruction = rest. If the divisor is 0, it returns 0. *) - | Kdivint31 (* euclidian division (returns a pair + | Kdivint31 (** euclidian division (returns a pair quotient,rest) *) - | Kaddmuldivint31 (* generic operation for shifting and + | Kaddmuldivint31 (** generic operation for shifting and cycling. Takes 3 int31 i j and s, and returns x*2^s+y/(2^(31-s) *) - | Kcompareint31 (* unsigned comparison of int31 + | Kcompareint31 (** unsigned comparison of int31 cf COMPAREINT31 in kernel/byterun/coq_interp.c for more info *) - | Khead0int31 (* Give the numbers of 0 in head of a in31*) - | Ktail0int31 (* Give the numbers of 0 in tail of a in31 + | Khead0int31 (** Give the numbers of 0 in head of a in31*) + | Ktail0int31 (** Give the numbers of 0 in tail of a in31 ie low bits *) - | Kisconst of Label.t (* conditional jump *) - | Kareconst of int*Label.t (* conditional jump *) - | Kcompint31 (* dynamic compilation of int31 *) - | Kdecompint31 (* dynamix decompilation of int31 *) -(* /spiwack *) + | Kisconst of Label.t (** conditional jump *) + | Kareconst of int*Label.t (** conditional jump *) + | Kcompint31 (** dynamic compilation of int31 *) + | Kdecompint31 (** dynamix decompilation of int31 + /spiwack *) and bytecodes = instruction list @@ -107,25 +108,25 @@ type fv_elem = FVnamed of identifier | FVrel of int type fv = fv_elem array -(* spiwack: this exception is expected to be raised by function expecting +(** spiwack: this exception is expected to be raised by function expecting closed terms. *) exception NotClosed (*spiwack: both type have been moved from Cbytegen because I needed then for the retroknowledge *) type vm_env = { - size : int; (* longueur de la liste [n] *) - fv_rev : fv_elem list (* [fvn; ... ;fv1] *) + size : int; (** longueur de la liste [n] *) + fv_rev : fv_elem list (** [fvn; ... ;fv1] *) } 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 *) - (* recursives = nbr *) - pos_rec : instruction list; (* instruction d'acces pour les variables *) - (* de point fix ou de cofix *) + nb_stack : int; (** nbre de variables sur la pile *) + in_stack : int list; (** position dans la pile *) + nb_rec : int; (** nbre de fonctions mutuellement *) + (** recursives = nbr *) + pos_rec : instruction list; (** instruction d'acces pour les variables *) + (** de point fix ou de cofix *) offset : int; in_env : vm_env ref } @@ -140,7 +141,7 @@ type block = | Bstrconst of structured_constant | Bmakeblock of int * block array | Bconstruct_app of int * int * int * block array - (* tag , nparams, arity *) + (** tag , nparams, arity *) | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array - (* compilation function (see get_vm_constant_dynamic_info in + (** compilation function (see get_vm_constant_dynamic_info in retroknowledge.mli for more info) , argument array *) -- cgit v1.2.3