From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- kernel/cbytecodes.mli | 73 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) (limited to 'kernel/cbytecodes.mli') diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 215b6ad4..c24b5a53 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -61,6 +61,43 @@ type instruction = | 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 + 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 + int31, for exact computation *) + | 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 + is a pair of the quotient and the + rest. + If the divisor is 0, it returns + 0. *) + | Kdivint31 (* euclidian division (returns a pair + quotient,rest) *) + | 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 + 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 + 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 *) and bytecodes = instruction list @@ -69,5 +106,41 @@ 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 + 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] *) + } + + +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 + } + val draw_instr : bytecodes -> unit + + +(*spiwack: moved this here because I needed it for retroknowledge *) +type block = + | Bconstr of constr + | Bstrconst of structured_constant + | Bmakeblock of int * block array + | Bconstruct_app of int * int * int * block array + (* tag , nparams, arity *) + | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array + (* compilation function (see get_vm_constant_dynamic_info in + retroknowledge.mli for more info) , argument array *) -- cgit v1.2.3