aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml3
-rw-r--r--Makefile.ci1
-rwxr-xr-xdev/ci/ci-basic-overlay.sh7
-rwxr-xr-xdev/ci/ci-bbv.sh8
-rw-r--r--doc/changelog/03-notations/11848-nicer-decimal-printing.rst5
-rwxr-xr-xdoc/stdlib/make-library-index3
-rw-r--r--kernel/byterun/coq_gc.h59
-rw-r--r--kernel/byterun/coq_interp.c24
-rw-r--r--kernel/byterun/coq_memory.c5
-rw-r--r--plugins/syntax/r_syntax.ml35
-rw-r--r--test-suite/output/QArithSyntax.out16
-rw-r--r--test-suite/output/RealSyntax.out18
-rw-r--r--theories/Init/Decimal.v31
-rw-r--r--theories/QArith/QArith_base.v32
14 files changed, 162 insertions, 85 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ebeee0d4e4..39c801197b 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -592,6 +592,9 @@ validate:quick:
library:ci-argosy:
extends: .ci-template
+library:ci-bbv:
+ extends: .ci-template
+
library:ci-bedrock2:
extends: .ci-template-flambda
artifacts:
diff --git a/Makefile.ci b/Makefile.ci
index f58dd9f37a..d4383fd409 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -11,6 +11,7 @@
CI_TARGETS= \
ci-aac_tactics \
ci-argosy \
+ ci-bbv \
ci-bedrock2 \
ci-bignums \
ci-color \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 70e3fe5c69..c18e556da8 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -200,6 +200,13 @@
: "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}"
########################################################################
+# bbv
+########################################################################
+: "${bbv_CI_REF:=master}"
+: "${bbv_CI_GITURL:=https://github.com/mit-plv/bbv}"
+: "${bbv_CI_ARCHIVEURL:=${bbv_CI_GITURL}/archive}"
+
+########################################################################
# bedrock2
########################################################################
: "${bedrock2_CI_REF:=tested}"
diff --git a/dev/ci/ci-bbv.sh b/dev/ci/ci-bbv.sh
new file mode 100755
index 0000000000..6892cea3e4
--- /dev/null
+++ b/dev/ci/ci-bbv.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download bbv
+
+( cd "${CI_BUILD_DIR}/bbv" && make && make install )
diff --git a/doc/changelog/03-notations/11848-nicer-decimal-printing.rst b/doc/changelog/03-notations/11848-nicer-decimal-printing.rst
new file mode 100644
index 0000000000..1d3a390f36
--- /dev/null
+++ b/doc/changelog/03-notations/11848-nicer-decimal-printing.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+ Nicer printing for decimal constants in R and Q.
+ 1.5 is now printed 1.5 rather than 15e-1.
+ (`#11848 <https://github.com/coq/coq/pull/11848>`_,
+ by Pierre Roux).
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index a51308f153..cb93a4c8cc 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -36,7 +36,8 @@ for k in $LIBDIRS; do
fi
else
if [ $h = 0 ]; then
- echo Warning: $k/$b.v will be hidden from the index
+ # Skipping file from the index
+ :
else
echo Error: none of $FILE and $HIDDEN mention $k/$b.v
exit 1
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
deleted file mode 100644
index 38eda4d11f..0000000000
--- a/kernel/byterun/coq_gc.h
+++ /dev/null
@@ -1,59 +0,0 @@
-/***********************************************************************/
-/* */
-/* Coq Compiler */
-/* */
-/* Benjamin Gregoire, projets Logical and Cristal */
-/* INRIA Rocquencourt */
-/* */
-/* */
-/***********************************************************************/
-
-#ifndef _COQ_CAML_GC_
-#define _COQ_CAML_GC_
-#include <caml/mlvalues.h>
-#include <caml/alloc.h>
-#include <caml/memory.h>
-
-typedef void (*scanning_action) (value, value *);
-
-
-CAMLextern char *young_ptr;
-CAMLextern char *young_limit;
-CAMLextern void (*scan_roots_hook) (scanning_action);
-CAMLextern void minor_collection (void);
-
-#define Caml_white (0 << 8)
-#define Caml_black (3 << 8)
-
-#ifdef HAS_OCP_MEMPROF
-
-/* This code is necessary to make the OCamlPro memory profiling branch of
- OCaml compile. */
-
-#define Make_header(wosize, tag, color) \
- caml_make_header(wosize, tag, color)
-
-#else
-
-#define Make_header(wosize, tag, color) \
- (((header_t) (((header_t) (wosize) << 10) \
- + (color) \
- + (tag_t) (tag))) \
- )
-#endif
-
-#define Alloc_small(result, wosize, tag) do{ \
- young_ptr -= Bhsize_wosize (wosize); \
- if (young_ptr < young_limit){ \
- young_ptr += Bhsize_wosize (wosize); \
- Setup_for_gc; \
- minor_collection (); \
- Restore_after_gc; \
- young_ptr -= Bhsize_wosize (wosize); \
- } \
- Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \
- (result) = Val_hp (young_ptr); \
- }while(0)
-
-
-#endif /*_COQ_CAML_GC_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 606cce0127..7588c1ce07 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -16,17 +16,37 @@
#include <stdio.h>
#include <signal.h>
#include <stdint.h>
+#include <math.h>
+
+#define CAML_INTERNALS
#include <caml/memory.h>
#include <caml/signals.h>
#include <caml/version.h>
-#include <math.h>
-#include "coq_gc.h"
+
#include "coq_instruct.h"
#include "coq_fix_code.h"
#include "coq_memory.h"
#include "coq_values.h"
#include "coq_float64.h"
+#if OCAML_VERSION < 41000
+extern void caml_minor_collection(void);
+
+#undef Alloc_small
+#define Alloc_small(result, wosize, tag) do{ \
+ caml_young_ptr -= Bhsize_wosize(wosize); \
+ if (caml_young_ptr < caml_young_limit) { \
+ caml_young_ptr += Bhsize_wosize(wosize); \
+ Setup_for_gc; \
+ caml_minor_collection(); \
+ Restore_after_gc; \
+ caml_young_ptr -= Bhsize_wosize(wosize); \
+ } \
+ Hd_hp(caml_young_ptr) = Make_header((wosize), (tag), Caml_black); \
+ (result) = Val_hp(caml_young_ptr); \
+ }while(0)
+#endif
+
#ifdef ARCH_SIXTYFOUR
#include "coq_uint63_native.h"
#else
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 91d6773b1f..6233675c66 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -10,9 +10,12 @@
#include <stdio.h>
#include <string.h>
+
+#define CAML_INTERNALS
#include <caml/alloc.h>
#include <caml/address_class.h>
-#include "coq_gc.h"
+#include <caml/roots.h>
+
#include "coq_instruct.h"
#include "coq_fix_code.h"
#include "coq_memory.h"
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index e0dc3d8989..c4e9c8b73d 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -134,7 +134,38 @@ let r_of_rawnum ?loc n =
(* Printing R via scopes *)
(**********************************************************************)
-let rawnum_of_r c = match DAst.get c with
+let rawnum_of_r c =
+ (* print i * 10^e, precondition: e <> 0 *)
+ let numTok_of_int_exp i e =
+ (* choose between 123e-2 and 1.23, this is purely heuristic
+ and doesn't play any soundness role *)
+ let choose_exponent =
+ if Bigint.is_strictly_pos e then
+ true (* don't print 12 * 10^2 as 1200 to distinguish them *)
+ else
+ let i = Bigint.to_string i in
+ let li = if i.[0] = '-' then String.length i - 1 else String.length i in
+ let e = Bigint.neg e in
+ let le = String.length (Bigint.to_string e) in
+ Bigint.(less_than (add (of_int li) (of_int le)) e) in
+ (* print 123 * 10^-2 as 123e-2 *)
+ let numTok_exponent () = NumTok.Signed.of_bigint_and_exponent i e in
+ (* print 123 * 10^-2 as 1.23, precondition e < 0 *)
+ let numTok_dot () =
+ let s, i =
+ if Bigint.is_pos_or_zero i then NumTok.SPlus, Bigint.to_string i
+ else NumTok.SMinus, Bigint.(to_string (neg i)) in
+ let ni = String.length i in
+ let e = - (Bigint.to_int e) in
+ assert (e > 0);
+ let i, f =
+ if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e
+ else "0", String.make (e - ni) '0' ^ i in
+ let i = s, NumTok.UnsignedNat.of_string i in
+ let f = NumTok.UnsignedNat.of_string f in
+ NumTok.Signed.of_decimal_and_exponent i (Some f) None in
+ if choose_exponent then numTok_exponent () else numTok_dot () in
+ match DAst.get c with
| GApp (r, [a]) when is_gr r glob_IZR ->
let n = bigint_of_z a in
NumTok.Signed.of_bigint n
@@ -151,7 +182,7 @@ let rawnum_of_r c = match DAst.get c with
let i = bigint_of_z l in
let e = bignat_of_pos e in
let e = if is_gr md glob_Rdiv then neg e else e in
- NumTok.Signed.of_bigint_and_exponent i e
+ numTok_of_int_exp i e
| _ -> raise Non_closed_number
end
| _ -> raise Non_closed_number
diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out
index 6bc04f1cef..fe6a1d25c6 100644
--- a/test-suite/output/QArithSyntax.out
+++ b/test-suite/output/QArithSyntax.out
@@ -1,14 +1,14 @@
-eq_refl : 102e-2 = 102e-2
- : 102e-2 = 102e-2
-eq_refl : 102e-1 = 102e-1
- : 102e-1 = 102e-1
+eq_refl : 1.02 = 1.02
+ : 1.02 = 1.02
+eq_refl : 10.2 = 10.2
+ : 10.2 = 10.2
eq_refl : 1020 = 1020
: 1020 = 1020
eq_refl : 102 = 102
: 102 = 102
-eq_refl : 102e-2 = 102e-2
- : 102e-2 = 102e-2
+eq_refl : 1.02 = 1.02
+ : 1.02 = 1.02
eq_refl : -1e-4 = -1e-4
: -1e-4 = -1e-4
-eq_refl : -50e-2 = -50e-2
- : -50e-2 = -50e-2
+eq_refl : -0.50 = -0.50
+ : -0.50 = -0.50
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index ebc272d9af..1685964b0f 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -2,21 +2,21 @@
: R
(-31)%R
: R
-15e-1%R
+1.5%R
: R
15%R
: R
-eq_refl : 102e-2 = 102e-2
- : 102e-2 = 102e-2
-eq_refl : 102e-1 = 102e-1
- : 102e-1 = 102e-1
+eq_refl : 1.02 = 1.02
+ : 1.02 = 1.02
+eq_refl : 10.2 = 10.2
+ : 10.2 = 10.2
eq_refl : 102e1 = 102e1
: 102e1 = 102e1
eq_refl : 102 = 102
: 102 = 102
-eq_refl : 102e-2 = 102e-2
- : 102e-2 = 102e-2
+eq_refl : 1.02 = 1.02
+ : 1.02 = 1.02
eq_refl : -1e-4 = -1e-4
: -1e-4 = -1e-4
-eq_refl : -50e-2 = -50e-2
- : -50e-2 = -50e-2
+eq_refl : -0.50 = -0.50
+ : -0.50 = -0.50
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 10c3baa2cd..855db8bc3f 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -156,6 +156,37 @@ Definition nztail_int d :=
| Neg d => let (r, n) := nztail d in pair (Neg r) n
end.
+(** [del_head n d] removes [n] digits at beginning of [d]
+ or returns [zero] if [d] has less than [n] digits. *)
+
+Fixpoint del_head n d :=
+ match n with
+ | O => d
+ | S n =>
+ match d with
+ | Nil => zero
+ | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d =>
+ del_head n d
+ end
+ end.
+
+Definition del_head_int n d :=
+ match d with
+ | Pos d => Pos (del_head n d)
+ | Neg d => Neg (del_head n d)
+ end.
+
+(** [del_tail n d] removes [n] digits at end of [d]
+ or returns [zero] if [d] has less than [n] digits. *)
+
+Fixpoint del_tail n d := rev (del_head n (rev d)).
+
+Definition del_tail_int n d :=
+ match d with
+ | Pos d => Pos (del_tail n d)
+ | Neg d => Neg (del_tail n d)
+ end.
+
Module Little.
(** Successor of little-endian numbers *)
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index a7f338aec3..bd5225d9ef 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -44,13 +44,39 @@ Definition of_decimal (d:Decimal.decimal) : Q :=
end.
Definition to_decimal (q:Q) : option Decimal.decimal :=
+ (* choose between 123e-2 and 1.23, this is purely heuristic
+ and doesn't play any soundness role *)
+ let choose_exponent i ne :=
+ let i := match i with Decimal.Pos i | Decimal.Neg i => i end in
+ let li := Decimal.nb_digits i in
+ let le := Decimal.nb_digits (Nat.to_uint ne) in
+ Nat.ltb (Nat.add li le) ne in
+ (* print 123 / 100 as 123e-2 *)
+ let decimal_exponent i ne :=
+ let e := Z.to_int (Z.opp (Z.of_nat ne)) in
+ Decimal.DecimalExp i Decimal.Nil e in
+ (* print 123 / 100 as 1.23 *)
+ let decimal_dot i ne :=
+ let ai := match i with Decimal.Pos i | Decimal.Neg i => i end in
+ let ni := Decimal.nb_digits ai in
+ if Nat.ltb ne ni then
+ let i := Decimal.del_tail_int ne i in
+ let f := Decimal.del_head (Nat.sub ni ne) ai in
+ Decimal.Decimal i f
+ else
+ let z := match i with
+ | Decimal.Pos _ => Decimal.Pos (Decimal.zero)
+ | Decimal.Neg _ => Decimal.Neg (Decimal.zero) end in
+ Decimal.Decimal z (Nat.iter (Nat.sub ne ni) Decimal.D0 ai) in
let num := Z.to_int (Qnum q) in
let (den, e_den) := Decimal.nztail (Pos.to_uint (Qden q)) in
match den with
| Decimal.D1 Decimal.Nil =>
- match Z.of_nat e_den with
- | Z0 => Some (Decimal.Decimal num Decimal.Nil)
- | e => Some (Decimal.DecimalExp num Decimal.Nil (Z.to_int (Z.opp e)))
+ match e_den with
+ | O => Some (Decimal.Decimal num Decimal.Nil)
+ | ne =>
+ if choose_exponent num ne then Some (decimal_exponent num ne)
+ else Some (decimal_dot num ne)
end
| _ => None
end.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 18:45:54 +0000