meta_language/translation/emit_rocq/
floats.rs1pub const FLOAT_PRELUDE: &[&str] = &[
7 "From Stdlib Require Import NArith ZArith Lia Recdef String List Ascii Floats.",
8 r#"Set Warnings "-inexact-float"."#,
9];
10
11pub(super) const JS_NUMBER: &str = r#"(* ECMAScript Number::toString for binary64: the shortest decimal that rounds
12 back to the value (the nearest one, the even one on a tie), laid out as
13 JavaScript prints it. Exact Z arithmetic on the decomposed float. *)
14Fixpoint ml_js_zeros (n : nat) : string :=
15 match n with O => EmptyString | S k => String "0"%char (ml_js_zeros k) end.
16Fixpoint ml_js_trim (s : string) : string :=
17 match s with
18 | EmptyString => EmptyString
19 | String c rest =>
20 let r := ml_js_trim rest in
21 if andb (Ascii.eqb c "0"%char) (String.eqb r EmptyString) then EmptyString else String c r
22 end.
23Definition ml_js_layout (digits : string) (n : Z) : string :=
24 let len := String.length digits in
25 let k := Z.of_nat len in
26 if andb (Z.leb k n) (Z.leb n 21) then (digits ++ ml_js_zeros (Z.to_nat (n - k)))%string
27 else if andb (Z.ltb 0 n) (Z.leb n 21) then
28 (substring 0 (Z.to_nat n) digits ++ "." ++ substring (Z.to_nat n) len digits)%string
29 else if andb (Z.ltb (-6) n) (Z.leb n 0) then ("0." ++ ml_js_zeros (Z.to_nat (- n)) ++ digits)%string
30 else
31 let e := (n - 1)%Z in
32 let exp := ((if Z.ltb e 0 then "e-" else "e+") ++ ml_N_to_string (Z.abs_N e))%string in
33 if Z.eqb k 1 then (digits ++ exp)%string
34 else (substring 0 1 digits ++ "." ++ substring 1 len digits ++ exp)%string.
35(* The value is v * 2^sh for a scaled mantissa v. c * 10^q compared with
36 x * 2^sh, and floor (v * 2^sh / 10^q), with shifts for the powers of 2. *)
37Definition ml_js_cmp (c q x sh : Z) : comparison :=
38 Z.compare (Z.shiftl (c * 10 ^ Z.max q 0) (Z.max (- sh) 0))
39 (Z.shiftl (x * 10 ^ Z.max (- q) 0) (Z.max sh 0)).
40Definition ml_js_floor (v q sh : Z) : Z :=
41 Z.div (Z.shiftl (v * 10 ^ Z.max (- q) 0) (Z.max sh 0))
42 (Z.shiftl (10 ^ Z.max q 0) (Z.max (- sh) 0)).
43(* With p significant digits: the candidate in the rounding interval nearest
44 to the value (the even one on a tie), as (digits, exponent). *)
45Definition ml_js_candidate (p e10 v lo hi sh : Z) (inclusive : bool) : option (Z * Z) :=
46 let q := (e10 - p + 1)%Z in
47 let c := ml_js_floor v q sh in
48 let inside (c : Z) :=
49 andb (match ml_js_cmp c q lo sh with Gt => true | Eq => inclusive | Lt => false end)
50 (match ml_js_cmp c q hi sh with Lt => true | Eq => inclusive | Gt => false end) in
51 let low := inside c in
52 let high := inside (c + 1)%Z in
53 if andb low high then
54 match ml_js_cmp (2 * c + 1) q (2 * v) sh with
55 | Gt => Some (c, q) | Lt => Some ((c + 1)%Z, q) | Eq => Some (if Z.even c then c else (c + 1)%Z, q)
56 end
57 else if low then Some (c, q) else if high then Some ((c + 1)%Z, q) else None.
58(* A candidate with p digits is one with p + 1 digits too, so the fewest
59 digits are found by bisection over [first, last]; 17 always suffice. *)
60Fixpoint ml_js_fewest (fuel : nat) (first last e10 v lo hi sh : Z) (inclusive : bool) : Z * Z :=
61 match fuel with
62 | S fuel =>
63 if Z.ltb first last then
64 let middle := Z.div (first + last) 2 in
65 match ml_js_candidate middle e10 v lo hi sh inclusive with
66 | Some _ => ml_js_fewest fuel first middle e10 v lo hi sh inclusive
67 | None => ml_js_fewest fuel (middle + 1) last e10 v lo hi sh inclusive
68 end
69 else match ml_js_candidate last e10 v lo hi sh inclusive with Some r => r | None => (0, 0)%Z end
70 | O => match ml_js_candidate last e10 v lo hi sh inclusive with Some r => r | None => (0, 0)%Z end
71 end.
72Definition ml_js_shortest (m e : Z) (lowerCloser : bool) : string :=
73 let sh := (e - 2)%Z in
74 let v := (4 * m)%Z in
75 let lo := if lowerCloser then (v - 1)%Z else (v - 2)%Z in
76 let guess := Z.div ((Z.log2 m + e) * 78913) 262144 in
77 let e10 :=
78 match ml_js_cmp 1 (guess + 1) v sh with
79 | Gt => match ml_js_cmp 1 guess v sh with Gt => (guess - 1)%Z | _ => guess end
80 | _ => (guess + 1)%Z
81 end in
82 let (pick, q) := ml_js_fewest 5 1 17 e10 v lo (v + 2) sh (Z.even m) in
83 let text := ml_N_to_string (Z.to_N pick) in
84 ml_js_layout (ml_js_trim text) (q + Z.of_nat (String.length text)).
85Definition ml_js_number (x : float) : string :=
86 match Prim2SF x with
87 | S754_zero _ => "0"
88 | S754_infinity negative => if negative then "-Infinity" else "Infinity"
89 | S754_nan => "NaN"
90 | S754_finite negative m e =>
91 let body := ml_js_shortest (Zpos m) e (andb (Pos.eqb m (2 ^ 52)) (Z.ltb (-1074) e)) in
92 if negative then ("-" ++ body)%string else body
93 end."#;
94
95pub(super) const JS_CONSOLE: &str = r#"(* What console.log prints: -0 as "-0", where String(-0) is "0". *)
96Definition ml_js_console (x : float) : string :=
97 if andb (PrimFloat.is_zero x) (PrimFloat.get_sign x) then "-0" else ml_js_number x."#;
98
99pub(super) const FLOAT_SAME: &str = r"(* SameValue: NaN equals NaN, and 0 and -0 differ. *)
100Definition ml_float_same (a b : float) : bool :=
101 if PrimFloat.is_nan a then PrimFloat.is_nan b
102 else andb (PrimFloat.eqb a b) (Bool.eqb (PrimFloat.get_sign a) (PrimFloat.get_sign b)).";
103
104pub(super) const FLOAT_REM: &str = r"(* ECMAScript % on binary64 (C fmod): the exact truncated remainder with the
105 sign of the dividend, computed on the mantissas, so it is exact. *)
106Definition ml_float_rem (x y : float) : float :=
107 if orb (orb (PrimFloat.is_nan x) (PrimFloat.is_nan y)) (orb (PrimFloat.is_infinity x) (PrimFloat.is_zero y))
108 then PrimFloat.div 0 0
109 else if orb (PrimFloat.is_infinity y) (PrimFloat.is_zero x) then x
110 else match Prim2SF x, Prim2SF y with
111 | S754_finite sx mx ex, S754_finite _ my ey =>
112 let e := Z.min ex ey in
113 let r := Z.modulo (Z.pos mx * 2 ^ (ex - e)) (Z.pos my * 2 ^ (ey - e)) in
114 let magnitude := Z.ldexp (PrimFloat.of_uint63 (Uint63.of_Z r)) e in
115 if sx then PrimFloat.opp magnitude else magnitude
116 | _, _ => x
117 end.";