From 2dbe106c09b60690b87e31e58d505b1f4e05b57f Mon Sep 17 00:00:00 2001 From: aspiwack Date: Fri, 11 May 2007 17:00:58 +0000 Subject: Processor integers + Print assumption (see coqdev mailing list for the details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/cbytecodes.mli | 72 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 72 insertions(+) (limited to 'kernel/cbytecodes.mli') diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 215b6ad4a..a2d4f7e01 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -61,6 +61,40 @@ 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 *) + | 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 +103,43 @@ 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 +val string_of_instr : bytecodes -> string + + + +(*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