pub(super) const HELPERS: [(&str, &str); 7] = [
(
"jsNumber",
r#"/-- ECMAScript Number::toString: the shortest decimal that reads back as the
value, the nearer one and then the even one on a tie, laid out as JavaScript
prints it; exact Nat arithmetic on the bits. -/
def ml_js_layout (digits : List Char) (n : Int) : String :=
let k : Int := digits.length
let text := String.ofList
let zeros (count : Int) := List.replicate count.toNat '0'
if k ≤ n ∧ n ≤ 21 then text (digits ++ zeros (n - k))
else if 0 < n ∧ n ≤ 21 then text (digits.take n.toNat ++ '.' :: digits.drop n.toNat)
else if -6 < n ∧ n ≤ 0 then text ('0' :: '.' :: zeros (-n) ++ digits)
else
let e := n - 1
let exp := (if e < 0 then "e-" else "e+") ++ toString e.natAbs
if k == 1 then text digits ++ exp
else text (digits.take 1 ++ '.' :: digits.drop 1) ++ exp
/-- `c · 10^q` compared with `x · s / d`. -/
def ml_js_cmp (c : Nat) (q : Int) (x s d : Nat) : Ordering :=
if 0 ≤ q then compare (c * 10 ^ q.toNat * d) (x * s)
else compare (c * d) (x * s * 10 ^ (-q).toNat)
def ml_js_shortest (m : Nat) (e : Int) (lowerCloser : Bool) : String :=
-- The value is 4m and the rounding interval [lo, hi], in units of 2^(e-2) = s / d.
let s := 2 ^ (e - 2).toNat
let d := 2 ^ (2 - e).toNat
let v := 4 * m
let lo := if lowerCloser then v - 1 else v - 2
let hi := v + 2
let inclusive := m % 2 == 0
let above (c : Nat) (q : Int) : Bool :=
match ml_js_cmp c q lo s d with
| .gt => true | .eq => inclusive | .lt => false
let below (c : Nat) (q : Int) : Bool :=
match ml_js_cmp c q hi s d with
| .lt => true | .eq => inclusive | .gt => false
-- floor (log10 value) from the bit length, then corrected exactly
let bits : Int := (Nat.log2 m : Int) + 1 + e
let guess : Int := Int.fdiv ((bits - 1) * 78913) 262144
let e10 :=
if ml_js_cmp 1 (guess + 1) v s d != .gt then guess + 1
else if ml_js_cmp 1 guess v s d == .gt then guess - 1
else guess
let rec search (fuel : Nat) (p : Nat) : String :=
match fuel with
| 0 => ""
| fuel + 1 =>
let q : Int := e10 - p + 1
let c :=
if 0 ≤ q then v * s / (d * 10 ^ q.toNat)
else v * s * 10 ^ (-q).toNat / d
let lowOk := above c q ∧ below c q
let highOk := above (c + 1) q ∧ below (c + 1) q
if lowOk ∨ highOk then
let pick :=
if lowOk ∧ highOk then
match ml_js_cmp (2 * c + 1) q (2 * v) s d with
| .gt => c | .lt => c + 1 | .eq => if c % 2 == 0 then c else c + 1
else if lowOk then c else c + 1
let text := (toString pick).toList
let n : Int := q + text.length
ml_js_layout (text.reverse.dropWhile (· == '0')).reverse n
else search fuel (p + 1)
search 17 1
def ml_js_number (x : Float) : String :=
let bits : Nat := x.toBits.toNat
let negative := bits ≥ 2 ^ 63
let exponent : Nat := (bits / 2 ^ 52) % 2048
let fraction : Nat := bits % 2 ^ 52
if exponent == 2047 then
if fraction != 0 then "NaN" else if negative then "-Infinity" else "Infinity"
else if exponent == 0 ∧ fraction == 0 then "0"
else
let body :=
if exponent == 0 then ml_js_shortest fraction (-1074) false
else ml_js_shortest (fraction + 2 ^ 52) ((exponent : Int) - 1075) (fraction == 0 ∧ exponent > 1)
if negative then "-" ++ body else body"#,
),
(
"jsConsole",
r#"/-- What console.log prints: -0 as "-0", where String(-0) is "0". -/
def ml_js_console (x : Float) : String :=
if x.toBits == 0x8000000000000000 then "-0" else ml_js_number x"#,
),
(
"floatRem",
r"/-- ECMAScript `%` on binary64 (C fmod): the exact remainder, truncated, with
the sign of the dividend; computed on the bits, so it is exact. -/
def ml_float_rem (x y : Float) : Float :=
let decompose (f : Float) : Nat × Int :=
let b : Nat := f.toBits.toNat
let exponent : Nat := (b / 2 ^ 52) % 2048
let fraction : Nat := b % 2 ^ 52
if exponent == 0 then (fraction, -1074) else (fraction + 2 ^ 52, (exponent : Int) - 1075)
if x.isNaN || y.isNaN || x.isInf || y == 0 then 0 / 0
else if y.isInf || x == 0 then x
else
let (mx, ex) := decompose x
let (my, ey) := decompose y
let e := min ex ey
let r := (mx * 2 ^ (ex - e).toNat) % (my * 2 ^ (ey - e).toNat)
let magnitude := Float.scaleB (Float.ofNat r) e
if x.toBits.toNat ≥ 2 ^ 63 then -magnitude else magnitude",
),
(
"floatSame",
r"/-- SameValue, as Object.is and assert.strictEqual compare: NaN equals NaN,
and 0 differs from -0. -/
def ml_float_same (a b : Float) : Bool :=
if a.isNaN then b.isNaN else a.toBits == b.toBits",
),
(
"math",
r"/-- Math.trunc: towards zero, a zero result keeping the sign of the argument. -/
def ml_trunc (x : Float) : Float := if x < 0 then x.ceil else x.floor
/-- Math.round: the nearest integer, the one towards +Infinity on a tie, and -0 from -0.5 up to 0. -/
def ml_round (x : Float) : Float :=
if x.isNaN || x.isInf || x == 0 then x
else if x > 0 ∧ x < 0.5 then 0
else if x < 0 ∧ x ≥ -0.5 then -0.0
else if x - x.floor ≥ 0.5 then x.floor + 1 else x.floor
/-- Math.sign: 1 or -1, and -0, 0 and NaN as they are. -/
def ml_sign (x : Float) : Float := if x > 0 then 1 else if x < 0 then -1 else x
/-- Math.max of two Numbers: NaN when either is, and 0 above -0. -/
def ml_max (a b : Float) : Float :=
if a > b then a else if b > a then b else if a == b then (if 1 / a < 0 then b else a) else 0.0 / 0.0
/-- Math.min of two Numbers: NaN when either is, and -0 below 0. -/
def ml_min (a b : Float) : Float :=
if a < b then a else if b < a then b else if a == b then (if 1 / a < 0 then a else b) else 0.0 / 0.0
def ml_is_integer (x : Float) : Bool := x.isFinite && ml_trunc x == x
def ml_is_safe_integer (x : Float) : Bool := ml_is_integer x && decide (x.abs ≤ 9007199254740991)",
),
(
"arrayAt",
r#"/-- The element at an index; a read outside the array, undefined in JavaScript, panics. -/
def ml_array_at {α : Type} [Inhabited α] (values : Array α) (index : Int) : α :=
if h : 0 ≤ index ∧ index.toNat < values.size then values[index.toNat]'h.2
else panic! "array index out of range""#,
),
(
"arrayAtFloat",
r#"/-- The index a Number names: a non-negative integer, -0 included. -/
def ml_array_at_float {α : Type} [Inhabited α] (values : Array α) (index : Float) : α :=
if index ≥ 0 && index.floor == index && index < 9007199254740992 then ml_array_at values (Int.ofNat index.toUInt64.toNat)
else panic! "array index out of range""#,
),
];