aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/byterun/coq_fix_code.c1
-rw-r--r--kernel/byterun/coq_instruct.h1
-rw-r--r--kernel/byterun/coq_interp.c30
-rw-r--r--kernel/cbytecodes.ml7
-rw-r--r--kernel/cbytecodes.mli3
-rw-r--r--kernel/cemitcodes.ml2
-rw-r--r--kernel/environ.ml11
-rw-r--r--kernel/retroknowledge.ml6
-rw-r--r--kernel/retroknowledge.mli6
-rw-r--r--tactics/extraargs.ml413
-rw-r--r--theories/Ints/Int31.v5
11 files changed, 72 insertions, 13 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
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 327bd24f7..c3377bca1 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -282,9 +282,9 @@ let pr_r_int31_field _ _ _ i31f =
let pr_retroknowledge_field _ _ _ f =
match f with
- | Retroknowledge.KEq -> str "equality"
+ (* | Retroknowledge.KEq -> str "equality"
| Retroknowledge.KNat natf -> pr_r_nat_field () () () natf
- | Retroknowledge.KN nf -> pr_r_n_field () () () nf
+ | Retroknowledge.KN nf -> pr_r_n_field () () () nf *)
| Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field () () () i31f) ++
str "in " ++ str group
@@ -331,13 +331,16 @@ PRINTED BY pr_r_int31_field
| [ "int31" "div" ] -> [ Retroknowledge.Int31Div ]
| [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ]
| [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ]
+| [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ]
+| [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ]
+
END
ARGUMENT EXTEND retroknowledge_field
TYPED AS r_field
PRINTED BY pr_retroknowledge_field
-| [ "equality" ] -> [ Retroknowledge.KEq ]
+(*| [ "equality" ] -> [ Retroknowledge.KEq ]
| [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ]
-| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]
+| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]*)
| [ retroknowledge_int31 (i) "in" string(g)] -> [ Retroknowledge.KInt31(g,i) ]
-END \ No newline at end of file
+END
diff --git a/theories/Ints/Int31.v b/theories/Ints/Int31.v
index 59e45c320..918c54232 100644
--- a/theories/Ints/Int31.v
+++ b/theories/Ints/Int31.v
@@ -402,4 +402,7 @@ Definition tail031 (i:int31) :=
| D1 => n
end)
i On
-. \ No newline at end of file
+.
+
+Register head031 as int31 head0 in "coq_int31" by True.
+Register tail031 as int31 tail0 in "coq_int31" by True.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 21:05:35 +0000