The numbers and the search intervals of ratpoints-lean

ratpoints-lean reads the numbers of its command line as main.c of ratpoints reads them: the integers of the coefficient list as scan_mpz reads them, the C longs of the height bound and of the options as scan_long reads them with strtol, the real numbers of the options as scan_double reads them with strtod, and the ends of the search intervals of -l and -u as scan_end reads them: the rational number that the word denotes, or an infinity, and the double that the library is given for it, outward of it. With these exact ends it decides, as process of main.c does, whether a point that the search finds lies in the search region of the command line (Ratpoints.Cli.inRegion); it joins intervals whose doubles meet, as join_intervals does before the library is called; and it prints the doubles of the search intervals as printf of glibc prints them under %f (Ratpoints.Cli.printF), in messages 3 and 8 of the report.

Main definitions

• Ratpoints.Cli.longOfString?: a C long, as scan_long reads it.
• Ratpoints.Cli.strtod, Ratpoints.Cli.scanDouble?: a real number, as strtod and scan_double read it.
• Ratpoints.Cli.ExactEnd, Ratpoints.Cli.scanEnd: an end of a search interval of the command line, the number it is and the double the library is given for it.
• Ratpoints.Cli.inRegion: whether x = a / b lies in the intervals of the command line.
• Ratpoints.Cli.joinIntervals: the intervals that the library is given.
• Ratpoints.Cli.printF: a double as printf prints it under %f.

Implementation notes

The numbers are read as main.c reads them, by readers of their own: core's String.toInt? takes neither a leading + nor white space around the number, and core's String.toNat? takes the digit separator _, which main.c refuses. The double that strtod reads is the double nearest to the exact value of the word (Ratpoints.Double.ofRatio, and Ratpoints.Double.ofDyadic for a hexadecimal word), which glibc computes, whose size is decided by bounds before a power of 10 or 2 is expanded, so that a word with a huge exponent costs no more than another. The components with a loop are of type Id α.

Reading numbers

def Ratpoints.Cli.isSpace (ch : Char) : Bool

Whether ch is white space for isspace in the C locale, in which main.c runs: a space, or a character from the tab \t to the carriage return \r (tab, line feed, vertical tab, form feed, carriage return). Core's Char.isWhitespace leaves out the vertical tab and the form feed.

Equations

• Ratpoints.Cli.isSpace ch = (ch == ' ' || decide ('\t' ≤ ch) && decide (ch ≤ '\x0d'))

def Ratpoints.Cli.words (s : List Char) : List (List Char)

The words of s: its maximal runs of characters that are not C white space (Ratpoints.Cli.isSpace), in order. List.splitBy cuts s into the maximal runs of white space and of other characters, and the words are the latter.

Equations

• Ratpoints.Cli.words s = List.filter (fun (w : List Char) => !w.any Ratpoints.Cli.isSpace) (List.splitBy (fun (a b : Char) => Ratpoints.Cli.isSpace a == Ratpoints.Cli.isSpace b) s)

def Ratpoints.Cli.isDigits (s : List Char) : Bool

Whether s is a nonempty list of decimal digits.

Equations

• Ratpoints.Cli.isDigits s = (!s.isEmpty && s.all Char.isDigit)

def Ratpoints.Cli.natOfDigits? (ds : List Char) : Option Nat

The natural number that ds denotes, if it is a nonempty list of decimal digits.

Equations

• Ratpoints.Cli.natOfDigits? ds = if Ratpoints.Cli.isDigits ds = true then some (List.foldl (fun (n : Nat) (ch : Char) => 10 * n + (ch.toNat - '0'.toNat)) 0 ds) else none

def Ratpoints.Cli.dropSign : List Char → List Char

The characters of s after an optional sign - or +.

Equations

• Ratpoints.Cli.dropSign ('-' :: s) = s
• Ratpoints.Cli.dropSign ('+' :: s) = s
• Ratpoints.Cli.dropSign x✝ = x✝

def Ratpoints.Cli.intOfWord? (w : List Char) : Option Int

The integer that the word w is, as scan_mpz of main.c reads it: an optional sign - or +, then at least one decimal digit and nothing else. There is no bound on its size. scan_mpz also checks that white space or the end of the argument follows the digits, which a word of Ratpoints.Cli.words satisfies.

C: main.c:700-717

Equations

• Ratpoints.Cli.intOfWord? w = Option.map (fun (n : Int) => if w.head? = some '-' then -n else n) do let a ← Ratpoints.Cli.natOfDigits? (Ratpoints.Cli.dropSign w) pure ↑a

def Ratpoints.Cli.onlyWord? (s : String) : Option (List Char)

The one word of s, if s has exactly one word (Ratpoints.Cli.words): strtol and strtod skip the white space before a number, and only_space_after of main.c checks that nothing but white space follows it.

C: main.c:724-728

Equations

• Ratpoints.Cli.onlyWord? s = match Ratpoints.Cli.words s.toList with | [w] => some w | x => none

def Ratpoints.Cli.longOfString? (s : String) : Option Int

The C long that s is, as scan_long of main.c reads it with strtol in base 10: an integer as Ratpoints.Cli.intOfWord? reads it, with nothing but C white space before and after it (Ratpoints.Cli.onlyWord?), from -2⁶³ to 2⁶³ - 1; for a value beyond these bounds strtol reports the error ERANGE.

C: main.c:733-740

Deviation: an Int for a long.

Equations

• Ratpoints.Cli.longOfString? s = Option.filter (fun (n : Int) => decide (-2 ^ 63 ≤ n) && decide (n < 2 ^ 63)) ((Ratpoints.Cli.onlyWord? s).bind Ratpoints.Cli.intOfWord?)

Real numbers

def Ratpoints.Cli.isFloatBody (isDigit : Char → Bool) (exp s : List Char) : Bool

Whether s is a floating constant as strtod reads it, without its sign and, for a hexadecimal one, without its prefix 0x, and nothing else: the mantissa, a maximal run of digits (those that satisfy isDigit) and points with at most one point and at least one digit, and then optionally the exponent, a character of exp, an optional sign and at least one decimal digit.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.isInfWord (v : List Char) : Bool

Whether the characters v, a word without its sign, are an infinity for strtod: inf or infinity in any case.

Equations

• Ratpoints.Cli.isInfWord v = ["inf".toList, "infinity".toList].contains (List.map Char.toLower v)

def Ratpoints.Cli.isDoubleWord (w : List Char) : Bool

Whether the word w is a number for strtod in the C locale, other than a NaN: an optional sign, then inf or infinity in any case (Ratpoints.Cli.isInfWord), or a decimal floating constant with the exponent e or E (Ratpoints.Cli.isFloatBody), or 0x or 0X and a hexadecimal one with the exponent p or P.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.digitValue (ch : Char) : Nat

The value of the hexadecimal digit ch: 0 to 9 for the decimal digits, and 10 to 15 for a to f and for A to F, as mpz_set_str of GMP reads the digits of base 16 (and of base 10, which are among them).

Equations

• Ratpoints.Cli.digitValue ch = if ch.isDigit = true then ch.toNat - '0'.toNat else if (decide ('a' ≤ ch) && decide (ch ≤ 'f')) = true then ch.toNat - 'a'.toNat + 10 else ch.toNat - 'A'.toNat + 10

def Ratpoints.Cli.natOfDigitsIn (b : Nat) (ds : List Char) : Nat

The natural number that the digits ds give in the base b, as mpz_set_str of GMP reads them.

Equations

• Ratpoints.Cli.natOfDigitsIn b ds = List.foldl (fun (n : Nat) (ch : Char) => b * n + Ratpoints.Cli.digitValue ch) 0 ds

def Ratpoints.Cli.mantissaDigits (isDigit : Char → Bool) (point : Bool) : List Char → List Char × Nat × List Char

The digits of the mantissa at the start of s, the characters that satisfy isDigit with points among them, as the loop of scan_end of main.c reads them, point saying whether a point has been passed: the digits in their order, without the points, the number of those after a point, and the rest of s from the first character that is neither a digit nor a point.

C: main.c:822-834

Deviation: a recursion over the characters, for the loop over the C string and the array digits, whose length is the number n of the digits.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Cli.mantissaDigits isDigit point ('.' :: s) = Ratpoints.Cli.mantissaDigits isDigit true s
• Ratpoints.Cli.mantissaDigits isDigit point [] = ([], 0, [])

def Ratpoints.Cli.floatParts (w : List Char) : Bool × Bool × List Char × Nat × List Char

The parts of the floating constant w of Ratpoints.Cli.isDoubleWord that is not an infinity, as scan_end of main.c reads them: whether it is negative (its sign -), whether it is hexadecimal (0x or 0X after the sign), the digits of the mantissa without the point, the number of them after the point (Ratpoints.Cli.mantissaDigits), and what follows them, the exponent: e, E, p or P, an optional sign and decimal digits, or nothing. strtod reads the same parts (Ratpoints.Cli.strtod).

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.exponentDigits (rest : List Char) : Bool × List Char

Whether the exponent rest of a floating constant (Ratpoints.Cli.floatParts) is negative, and its decimal digits: after e, E, p or P, a sign - or + and then the digits; for no exponent, not negative and no digits.

Equations

• Ratpoints.Cli.exponentDigits (x :: '-' :: s) = if "eEpP".contains x = true then (true, s) else (false, [])
• Ratpoints.Cli.exponentDigits (x :: '+' :: s) = if "eEpP".contains x = true then (false, s) else (false, [])
• Ratpoints.Cli.exponentDigits (x :: t) = if "eEpP".contains x = true then (false, t) else (false, [])
• Ratpoints.Cli.exponentDigits [] = (false, [])

def Ratpoints.Cli.nearestBinary (neg : Bool) (m : Nat) (t : Int) : Double

The double nearest to ±m 2 ^ t, the sign - for neg, its size decided first by the length of m in bits: an infinity when m 2 ^ t ≥ 2 ^ 1024, a zero when m 2 ^ t < 2 ^ (-1075), and otherwise the rounding of Ratpoints.Double.ofDyadic, whose shift is then bounded by the length of m and the range of the doubles.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.nearestDecimal (neg : Bool) (m : Nat) (t : Int) : Double

The double nearest to ±m 10 ^ t, the sign - for neg (Ratpoints.Double.ofRatio), with two shortcuts by the bounds 2 ^ (log₂ m) ≤ m and 2 ^ (3 u) ≤ 10 ^ u: for t ≥ 0 an infinity when they put m 10 ^ t at or above 2 ^ 1024, for t < 0 a zero when they put it below 2 ^ (-1075). Otherwise the power of 10 is expanded and the quotient rounded by Ratpoints.Double.ofRatio, which also gives the infinities and the zeros that the shortcuts miss; the exponent is then bounded by the length of m in bits and the range of the doubles.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.strtod (w : List Char) : Double

The double that strtod of glibc reads from the word w of Ratpoints.Cli.isDoubleWord, a floating constant or an infinity, in the C locale: ±∞ for an infinity, and otherwise the double nearest to the exact value ±m 10 ^ (ex - k), or ±m 2 ^ (ex - 4 k) for a hexadecimal constant, of the digits m of its mantissa, the number k of them after the point and its exponent ex, with ties to even (Ratpoints.Cli.nearestDecimal, Ratpoints.Cli.nearestBinary): a zero of the sign of w for a value of size at most 2 ^ (-1075), and an infinity of its sign for one of size at least 2 ^ 1024 - 2 ^ 970, as glibc rounds it, correctly. This is what glibc computes, not how: the size of the value is decided by bounds before a power is expanded, so that a word with a huge exponent costs no more than another. The proofs show only half of a faithful rounding: for a word that is not an infinity and a finite nonzero result, the exact value of the word lies below the successor of the result (Ratpoints.Cli.lt_nextUp_strtod).

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.scanDouble? (s : String) : Option Double

The double that s is, as scan_double of main.c reads it with strtod: a word of Ratpoints.Cli.isDoubleWord, with nothing but C white space before and after it (Ratpoints.Cli.onlyWord?), read by Ratpoints.Cli.strtod, so that a number beyond the range of the doubles is read as an infinity or as a zero; none for anything else, among them a NaN.

C: main.c:746-752

Deviation: the NaN refused by its syntax, which Ratpoints.Cli.isDoubleWord does not accept, for the test isnan of the double that strtod reads.

Equations

• Ratpoints.Cli.scanDouble? s = (Ratpoints.Cli.onlyWord? s).bind fun (w : List Char) => if Ratpoints.Cli.isDoubleWord w = true then some (Ratpoints.Cli.strtod w) else none

The ends of the search intervals

structure Ratpoints.Cli.ExactEnd : Type

exact_end of main.c: an end of a search interval of the command line as the number it denotes, inf being -1 for -∞, 1 for +∞ and 0 for the rational number q.

C: main.c:71

Deviation: an Int for the int inf, and a rational number of core for the mpq_t q, 0 by default as mpq_init sets it.

• inf : Int

  inf: -1 for -∞, 1 for +∞, 0 for the rational number q.

• q : Rat

  q: the end, when it is a rational number.

@[instance_reducible]

instance Ratpoints.Cli.instInhabitedExactEnd : Inhabited ExactEnd

Equations

• Ratpoints.Cli.instInhabitedExactEnd = { default := Ratpoints.Cli.instInhabitedExactEnd.default }

@[instance_reducible]

instance Ratpoints.Cli.instDecidableEqExactEnd : DecidableEq ExactEnd

Equations

• Ratpoints.Cli.instDecidableEqExactEnd = Ratpoints.Cli.instDecidableEqExactEnd.decEq

def Ratpoints.Cli.instDecidableEqExactEnd.decEq (x✝ x✝¹ : ExactEnd) : Decidable (x✝ = x✝¹)

Equations

• Ratpoints.Cli.instDecidableEqExactEnd.decEq { inf := a, q := a_1 } { inf := b, q := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Ratpoints.Cli.instReprExactEnd : Repr ExactEnd

Equations

• Ratpoints.Cli.instReprExactEnd = { reprPrec := Ratpoints.Cli.instReprExactEnd.repr }

def Ratpoints.Cli.instReprExactEnd.repr : ExactEnd → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.outward (x : Double) (v : Rat) (dir : Int) : Id Double

The double that outward of main.c gives for an end v of an interval of the command line, starting from the double x nearest to it, the direction dir < 0 for a lower end and dir > 0 for an upper one: while x is finite and lies above v (for a lower end) or below it (for an upper one), the double next to it outward (Ratpoints.Double.nextDown, Ratpoints.Double.nextUp), so that the result is the largest double ≤ v, or the smallest double ≥ v, when x is a double nearest to v, or an infinity on the safe side of v.

C: main.c:761-763, main.c:766-773, main.c:775-776

Deviation: the exact value of x (Ratpoints.Double.toRat) compared with v as rational numbers of core, for the GMP rational t, mpq_set_d and mpq_cmp; no mpq_init and mpq_clear.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.scanEnd (s : String) (dir : Int) : Id (Option (ExactEnd × Double))

The end of a search interval that s is, as scan_end of main.c reads it, and the double that the library is given for it, dir < 0 for a lower end and dir > 0 for an upper one; none when s is not a number for Ratpoints.Cli.scanDouble?. For an infinite double x read by strtod, also for a number beyond the range of the doubles, the infinite end of its sign and x itself. Otherwise the number that s denotes, from the parts of its word (Ratpoints.Cli.floatParts): 0 when its digits m are 0; when strtod reads 0 for it although m ≠ 0, 2 ^ (-1075), half the least positive double, which lies between 0 and every other x of the search as the number itself does; and otherwise m 2 ^ (ex - 4 k) for a hexadecimal number and m 10 ^ (ex - k) for a decimal one, for the k digits after the point and the exponent ex that scan_end accumulates, which stops taking digits once it reaches LONG_MAX / 20 (it is then that of a number beyond the range of the doubles or of 0); negated for the sign -. The double is that of Ratpoints.Cli.outward from x towards that number.

C: main.c:798-806, main.c:808-819, main.c:835-847, main.c:849, main.c:851-865, main.c:868-873, main.c:875-876, main.c:878-880

Deviation: the end and the double returned, or none, for the exact_end and the double that scan_end writes through pointers with its return value, the end of an infinity with q = 0, which scan_end leaves as it is (it is not read); the parts of the word read by Ratpoints.Cli.floatParts from the word of Ratpoints.Cli.onlyWord?, which is s without its white space; rational numbers of core for the GMP integers and rationals m, p and e->q, without mpz_init, mpz_clear, malloc and free (and the error 10 when malloc fails, which the model cannot meet).

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.heightEnd (H : Nat) : Double

The end that height_end of main.c gives for a missing first -l (negated) and a missing last -u: the double of the height bound H (Ratpoints.Double.ofInt64), moved up to the next double when it is below 2 ^ 63 and its value below H, so that the interval holds every x = a / b with |a| ≤ H, as the default interval of the library does.

C: main.c:299-305

Deviation: a natural number for the long height, at most 2 ^ 63 - 1.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.cmpEnd (e f : ExactEnd) : Int

The sign of the end e minus the end f, as cmp_end of main.c computes it: e.inf - f.inf when one of them is infinite, so that two infinities of one sign are equal, and else the sign of e.q - f.q.

C: main.c:309-313

Deviation: the sign as -1, 0 or 1, for the value of mpq_cmp, of which main.c reads only the sign.

Equations

• Ratpoints.Cli.cmpEnd e f = if (e.inf != 0 || f.inf != 0) = true then e.inf - f.inf else if e.q < f.q then -1 else if f.q < e.q then 1 else 0

def Ratpoints.Cli.cmpEndX (e : ExactEnd) (a b : Int) : Int

The sign of the end e minus x = a / b, for b > 0, as cmp_end_x of main.c computes it: e.inf when e is infinite, and else the sign of e.q - a / b.

C: main.c:116-120

Deviation: the sign as -1, 0 or 1, for the value of mpq_cmp_si, of which main.c reads only the sign; integers for the longs.

Equations

• Ratpoints.Cli.cmpEndX e a b = if (e.inf != 0) = true then e.inf else if e.q < Rat.divInt a b then -1 else if Rat.divInt a b < e.q then 1 else 0

def Ratpoints.Cli.inRegion (a b : Int) (e : Array ExactEnd) (n : Nat) : Id Bool

Whether x = a / b, b > 0, lies in one of the n intervals of the command line whose ends are e[2 i] ≤ x ≤ e[2 i + 1], which are increasing and disjoint, as in_region of main.c decides it: the binary search finds the first interval that does not end below x, which must hold it.

C: main.c:126-137

Deviation: natural numbers for the long indices, an array for the pointer e.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Cli.joinIntervals (dom : List (Double × Double)) : Id (List (Double × Double))

The search intervals that main.c gives the library for the intervals dom of the command line, as join_intervals makes them: in turn from the second, an interval whose lower end is at most the upper end of the interval it may be joined to is joined to it, the least of the lower ends and the greatest of the upper ends, and every other interval is the next one, to which the following may be joined, so that intervals whose doubles meet or overlap become one.

C: main.c:891-905

Deviation: a list for the array args->domain and the number args->num_inter of its intervals, written back in place by join_intervals, and natural numbers for the long indices.

Equations

• One or more equations did not get rendered due to their size.

Printing doubles

def Ratpoints.Cli.printF (x : Double) : String

What printf of glibc prints for the double x under the conversion %f, which %lf is too: the exact value of x rounded to six places after the point, ties to even, in full however large it is, after a - whenever the sign bit is set, also for -0.0 and for a negative value that rounds to 0; inf for an infinity and nan for a NaN, after a - when the sign bit is set (Ratpoints.Double.printFixed with p = 6).

Equations

• Ratpoints.Cli.printF x = Ratpoints.Double.printFixed 6 x

Examples