From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- kernel/cbytecodes.ml | 60 ++++++++++++++++++++++++++-------------------------- 1 file changed, 30 insertions(+), 30 deletions(-) (limited to 'kernel/cbytecodes.ml') diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index ceba6e82..f4d0bb2b 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -1,7 +1,7 @@ open Names open Term -type tag = int +type tag = int let id_tag = 0 let iddef_tag = 1 @@ -14,22 +14,22 @@ let cofix_evaluated_tag = 6 type structured_constant = | Const_sorts of sorts | Const_ind of inductive - | Const_b0 of tag + | Const_b0 of tag | Const_bn of tag * structured_constant array -type reloc_table = (tag * int) array +type reloc_table = (tag * int) array -type annot_switch = +type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool} - -module Label = + +module Label = struct type t = int let no = -1 let counter = ref no let create () = incr counter; !counter - let reset_label_counter () = counter := no + let reset_label_counter () = counter := no end @@ -49,24 +49,24 @@ type instruction = | 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 + | 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 + | Kclosurecofix of int * int * Label.t array * Label.t array (* nb fv, init, lbl types, lbl bodies *) | Kgetglobal of constant | Kconst of structured_constant | Kmakeblock of int * tag (* size, tag *) - | Kmakeprod + | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int | Kswitch of Label.t array * Label.t array (* consts,blocks *) - | Kpushfields of int + | 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 *) - | Kaddint31 (* adds the int31 in the accu + | 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 *) @@ -77,10 +77,10 @@ type instruction = | Kmulcint31 (* multiplication, result in two int31, for exact computation *) | Kdiv21int31 (* divides a double size integer - (represented by an int31 in the - accumulator and one on the top of + (represented by an int31 in the + accumulator and one on the top of the stack) by an int31. The result - is a pair of the quotient and the + is a pair of the quotient and the rest. If the divisor is 0, it returns 0. *) @@ -90,11 +90,11 @@ type instruction = cycling. Takes 3 int31 i j and s, and returns x*2^s+y/(2^(31-s) *) | Kcompareint31 (* unsigned comparison of int31 - cf COMPAREINT31 in + 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 + | 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 *) @@ -118,19 +118,19 @@ exception NotClosed type vm_env = { size : int; (* longueur de la liste [n] *) fv_rev : fv_elem list (* [fvn; ... ;fv1] *) - } - - -type comp_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 *) (* 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 - } + offset : int; + in_env : vm_env ref + } @@ -176,7 +176,7 @@ let rec instruction ppf = function | Kmakeprod -> fprintf ppf "\tmakeprod" | Kmakeswitchblock(lblt,lbls,_,sz) -> fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz - | Kswitch(lblc,lblb) -> + | Kswitch(lblc,lblb) -> fprintf ppf "\tswitch"; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; @@ -185,7 +185,7 @@ let rec instruction ppf = function | Kfield n -> fprintf ppf "\tgetfield %i" n | Kstop -> fprintf ppf "\tstop" | Ksequence (c1,c2) -> - fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 + fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 (* spiwack *) | Kbranch lbl -> fprintf ppf "\tbranch %i" lbl | Kaddint31 -> fprintf ppf "\taddint31" @@ -218,9 +218,9 @@ and instruction_list ppf = function fprintf ppf "%a@ %a" instruction instr instruction_list il -(*spiwack: moved this type in this file because I needed it for +(*spiwack: moved this type in this file because I needed it for retroknowledge which can't depend from cbytegen *) -type block = +type block = | Bconstr of constr | Bstrconst of structured_constant | Bmakeblock of int * block array @@ -228,10 +228,10 @@ type block = (* tag , nparams, arity *) | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array (* spiwack: compilation given by a function *) - (* 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 *) - + let draw_instr c = fprintf std_formatter "@[%a@]" instruction_list c -- cgit v1.2.3