diff options
author | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-20 09:43:36 +0000 |
---|---|---|
committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-20 09:43:36 +0000 |
commit | f4586d1e8b1116340574d9660117f93e7a1e4e3b (patch) | |
tree | 15b7dff4ed22b762446e4ae1f426e8f8aa2de52c /kernel | |
parent | 4708506ca1b34e93835b163db102f6860c89190c (diff) |
ajout de head0 et tail0 en natif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/byterun/coq_fix_code.c | 1 | ||||
-rw-r--r-- | kernel/byterun/coq_instruct.h | 1 | ||||
-rw-r--r-- | kernel/byterun/coq_interp.c | 30 | ||||
-rw-r--r-- | kernel/cbytecodes.ml | 7 | ||||
-rw-r--r-- | kernel/cbytecodes.mli | 3 | ||||
-rw-r--r-- | kernel/cemitcodes.ml | 2 | ||||
-rw-r--r-- | kernel/environ.ml | 11 | ||||
-rw-r--r-- | kernel/retroknowledge.ml | 6 | ||||
-rw-r--r-- | kernel/retroknowledge.mli | 6 |
9 files changed, 60 insertions, 7 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 961c49785..55b907adf 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -45,6 +45,7 @@ void init_arity () { arity[SUBINT31]=arity[SUBCINT31]=arity[SUBCARRYCINT31]= arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]= arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]= + arity[HEAD0INT31]=arity[TAIL0INT31]= arity[COMPINT31]=arity[DECOMPINT31]=0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 00156ebe8..8a45e9739 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -42,6 +42,7 @@ enum instructions { SUBINT31, SUBCINT31, SUBCARRYCINT31, MULCINT31, MULINT31, DIV21INT31, DIVINT31, ADDMULDIVINT31, COMPAREINT31, + HEAD0INT31, TAIL0INT31, ISCONST, ARECONST, COMPINT31, DECOMPINT31, /* /spiwack */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e7eb1bc8d..ccfb2515a 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1255,6 +1255,36 @@ value coq_interprete Next; } + Instruct (HEAD0INT31) { + int r = 0; + uint32 x; + print_instr("HEAD0INT31"); + x = (uint32) accu; + if (!(x & 0xFFFF0000)) { x <<= 16; r += 16; } + if (!(x & 0xFF000000)) { x <<= 8; r += 8; } + if (!(x & 0xF0000000)) { x <<= 4; r += 4; } + if (!(x & 0xC0000000)) { x <<= 2; r += 2; } + if (!(x & 0x80000000)) { x <<=1; r += 1; } + if (!(x & 0x80000000)) { r += 1; } + accu = value_of_uint32(r); + Next; + } + + Instruct (TAIL0INT31) { + int r = 0; + uint32 x; + print_instr("TAIL0INT31"); + x = (((uint32) accu >> 1) | 0x80000000); + if (!(x & 0xFFFF)) { x >>= 16; r += 16; } + if (!(x & 0x00FF)) { x >>= 8; r += 8; } + if (!(x & 0x000F)) { x >>= 4; r += 4; } + if (!(x & 0x0003)) { x >>= 2; r += 2; } + if (!(x & 0x0001)) { x >>=1; r += 1; } + if (!(x & 0x0001)) { r += 1; } + accu = value_of_uint32(r); + Next; + } + Instruct (ISCONST) { /* Branches if the accu does not contain a constant (i.e., a non-block value) */ diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index ee8cb1eea..84d04d67e 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -89,10 +89,13 @@ type instruction = | 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 + ie low bits *) | Kisconst of Label.t (* conditional jump *) | Kareconst of int*Label.t (* conditional jump *) | Kcompint31 (* dynamic compilation of int31 *) @@ -196,6 +199,8 @@ let rec instruction ppf = function | Kdiv21int31 -> fprintf ppf "\tdiv21int31" | Kdivint31 -> fprintf ppf "\tdivint31" | Kcompareint31 -> fprintf ppf "\tcompareint31" + | Khead0int31 -> fprintf ppf "\thead0int31" + | Ktail0int31 -> fprintf ppf "\ttail0int31" | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31" | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index a2d4f7e01..86b465543 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -90,6 +90,9 @@ type instruction = 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 *) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index dffb0f2d5..7617c454d 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -240,6 +240,8 @@ let emit_instr = function | Kdivint31 -> out opDIVINT31 | Kaddmuldivint31 -> out opADDMULDIVINT31 | Kcompareint31 -> out opCOMPAREINT31 + | Khead0int31 -> out opHEAD0INT31 + | Ktail0int31 -> out opTAIL0INT31 | Kisconst lbl -> out opISCONST; out_label lbl | Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl | Kcompint31 -> out opCOMPINT31 diff --git a/kernel/environ.ml b/kernel/environ.ml index 082458fab..9143db37d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -463,6 +463,12 @@ fun env field value -> op kn | _ -> anomaly "Environ.register: should be a constant" in + let add_int31_unop_from_const op = + match value with + | Const kn -> retroknowledge add_int31_op env value 1 + op kn + | _ -> anomaly "Environ.register: should be a constant" + in (* subfunction which completes the function constr_of_int31 above by performing the actual retroknowledge operations *) let add_int31_decompilation_from_type rk = @@ -499,7 +505,6 @@ fun env field value -> | KInt31 (_, Int31MinusC) -> add_int31_binop_from_const Cbytecodes.Ksubcint31 | KInt31 (_, Int31MinusCarryC) -> add_int31_binop_from_const Cbytecodes.Ksubcarrycint31 - | KInt31 (_, Int31PlusC) -> add_int31_binop_from_const Cbytecodes.Kaddcint31 | KInt31 (_, Int31Times) -> add_int31_binop_from_const Cbytecodes.Kmulint31 | KInt31 (_, Int31TimesC) -> add_int31_binop_from_const Cbytecodes.Kmulcint31 | KInt31 (_, Int31Div21) -> (* this is a ternary operation *) @@ -516,7 +521,9 @@ fun env field value -> Cbytecodes.Kaddmuldivint31 kn | _ -> anomaly "Environ.register: should be a constant") | KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31 - | _ -> env.retroknowledge + | KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31 + | KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31 + | _ -> env.retroknowledge in Retroknowledge.add_field retroknowledge_with_reactive_info field value } diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index f064cd8b9..b82556c78 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -58,11 +58,13 @@ type int31_field = | Int31Div | Int31AddMulDiv | Int31Compare + | Int31Head0 + | Int31Tail0 type field = - | KEq + (* | KEq | KNat of nat_field - | KN of n_field + | KN of n_field *) | KInt31 of string*int31_field diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index cba055560..999bf0ede 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -54,11 +54,13 @@ type int31_field = | Int31Div | Int31AddMulDiv | Int31Compare + | Int31Head0 + | Int31Tail0 type field = - | KEq +(* | KEq | KNat of nat_field - | KN of n_field + | KN of n_field *) | KInt31 of string*int31_field |