The command-line program ratpoints-lean

ratpoints-lean has the command line of ratpoints: the coefficient list 'a_0 a_1 ... a_n' of y ^ 2 = a_n x ^ n + ⋯ + a_0 as one argument (constant term first), the height bound and the options. It reads them as main.c of ratpoints does, with its checks, messages and exit statuses, in its order, and prints what ratpoints prints: unless -q is given, the report, with the banner of ratpoints-lean, the curve, the height bound and the search region of the command line before the points, and after them the numbers of the moduli used, what the search did, the search intervals that it searched and the count of the points found, and, under -v, in place of the height bound and the messages after the points but the count, the report of the library (Ratpoints.Report), between the points as ratpoints prints it; under -x, the pairs that pass the sieve of the model, with the moduli that the search chooses from the curve as ratpoints chooses them (Ratpoints.sievingInfo) and corrects between the blocks of the run (Ratpoints.Sieve.adaptPrimes), and over the numerators of the search intervals that the Sturm step leaves, which are those that ratpoints prints; and the points, through the callback process of main.c (Ratpoints.Cli.process), which the search calls for each point it finds (Ratpoints.findPointsVerbose), in the format of -f with the strings of -fs, -fm and -fe, the points at infinity passed over under -i (neither printed nor counted), none printed under -z, and the search stopped under -1 at the first point that process does not pass over (the first point counted, printed or not). It reads -p -n -N -r -R -U -C -A -P -Q -W -F -j -J into the options of the sieve (Ratpoints.SieveOptions) and ignores -t, the number of threads; it reads -k -K -s -S, -x -X -y -Y and -dl -du into the options of the search (Ratpoints.Options): whether the polynomial may be reversed, the depth of the Sturm step, whether the points are checked exactly, whether both points of a pair are delivered, and the range of the denominators; and it reads the search intervals of -l and -u as main.c does, the ends as the numbers they are (Ratpoints.Cli.ExactEnd) and the doubles outward of them, which it gives the search, joined where they meet (Ratpoints.Cli.joinIntervals), and against whose exact ends process checks each point. It runs the search with these options of the sieve, its array size set to Ratpoints.defaultArraySize, and these options of the search, so that it refuses a binary form that is not squarefree with error 8 and, after a reversal, prints the points of the reversed polynomial mapped back to the caller's curve, as ratpoints does with the same options.

Main definitions

• Ratpoints.Cli.input: the coefficients, the height bound and the options of a command line.
• Ratpoints.Cli.Intervals: the reading of the search intervals of -l and -u.
• Ratpoints.Cli.process: the callback of the search, which prints the points.
• Ratpoints.Cli.run: what the program prints and its exit status, on a command line.
• Ratpoints.Cli.main: the program.

Implementation notes

The numbers and the ends of the search intervals are read in Ratpoints.Model.CliNumbers. The text that main.c prints as it goes is collected and written once at the end. The callback Ratpoints.Cli.process, a function, and Ratpoints.Cli.run, the pure core of the program, run the loops of Ratpoints.Cli.inRegion and Ratpoints.Cli.joinIntervals with Id.run.

Messages

def Ratpoints.Cli.version : String

The version of ratpoints-lean, which its banner names: that of the release of ratpoints that it models.

Equations

• Ratpoints.Cli.version = "3.1.1"

def Ratpoints.Cli.banner : String

The banner of ratpoints-lean, which it prints with the usage. Its first line names the program and its version, as that of ratpoints does, so that the test scripts of ratpoints, which leave out the line beginning This is ratpoints-, leave it out too; the rest says what the program is, under which licence it is released and where it lives.

C: main.c:43-48

Deviation: the text is that of ratpoints-lean.

Equations

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

def Ratpoints.Cli.usage : String

The usage of ratpoints-lean: that of ratpoints, all options included.

C: main.c:77-88

Deviation: the program is called ratpoints-lean, and the lines below the first are indented to match.

Equations

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

inductive Ratpoints.Cli.Failure : Type

The ways in which ratpoints-lean refuses its command line: the errors of main.c that a command line can cause, those of the reading of the command line and error 8, which main.c gives for a binary form that the library refuses as not squarefree; and error 9, which main.c gives for the codes of the library other than RATPOINTS_NON_SQUAREFREE and RATPOINTS_NO_MEMORY (error 10, which the model cannot return), among them the refusal of search intervals that the command line never passes.

• tooFewArguments : Failure

  Error 2 of main.c: fewer than two arguments.

• tooManyCoefficients : Failure

  Error 3 of main.c: more than Ratpoints.maxDegree + 1 coefficients.

• incorrectHeight : Failure

  Error 4 of main.c: a height bound that is not a C long of at least 1.

• tooFewCoefficients : Failure

  Error 5 of main.c: fewer than two coefficients.

• optionSyntax : Failure

  Error 6 of main.c: an option that ratpoints does not have, a word without a leading - among the options, or an option whose argument is missing or malformed, but for -l and -u.

• intervals : Failure

  Error 7 of main.c: an end of a search interval (-l, -u) that is missing or no number, two lower or two upper ends in a row, more than Ratpoints.maxDegree intervals, or ends that are not ordered.

• notSquarefree : Failure

  Error 8 of main.c: a binary form that is not squarefree (Ratpoints.Refusal.notSquarefree).

• badArgs : Failure

  Error 9 of main.c: a code of the library other than RATPOINTS_NON_SQUAREFREE and RATPOINTS_NO_MEMORY, for the model the refusal of search intervals (Ratpoints.Refusal.badArgs), which no command line causes.

• incorrectCoefficients : Failure

  Error 11 of main.c: a coefficient that is not an integer.

def Ratpoints.Cli.Failure.message : Failure → String

What ratpoints-lean prints on a failure: what the function error of main.c prints for the same error, a blank line, the message and a blank line; for error 2 the banner and the usage instead, which error 6 prints after its message, as its case falls through to that of error 2.

C: main.c:1036-1048, main.c:1050-1053

Deviation: the banner and the usage are those of ratpoints-lean.

Equations

• Ratpoints.Cli.Failure.tooFewArguments.message = toString "\n" ++ toString Ratpoints.Cli.banner ++ toString "\n" ++ toString Ratpoints.Cli.usage
• Ratpoints.Cli.Failure.tooManyCoefficients.message = "\nToo many coefficients.\n\n"
• Ratpoints.Cli.Failure.incorrectHeight.message = "\nIncorrect height argument.\n\n"
• Ratpoints.Cli.Failure.tooFewCoefficients.message = "\nThe polynomial must have degree at least 1.\n\n"
• Ratpoints.Cli.Failure.optionSyntax.message = toString "\nWrong syntax for optional arguments:\n\n\n" ++ toString Ratpoints.Cli.banner ++ toString "\n" ++ toString Ratpoints.Cli.usage
• Ratpoints.Cli.Failure.intervals.message = "\nIncorrect interval arguments (not numbers, not alternating, too many, or not ordered).\n\n"
• Ratpoints.Cli.Failure.notSquarefree.message = "\nPolynomial is not square-free.\n\n"
• Ratpoints.Cli.Failure.badArgs.message = "\nBug no. 1 - please report!\n\n"
• Ratpoints.Cli.Failure.incorrectCoefficients.message = "\nIncorrect coefficients (not integers separated by blanks).\n\n"

def Ratpoints.Cli.Failure.status : Failure → UInt32

The exit status of ratpoints-lean on a failure: the number of the error of main.c, with which its function error exits.

C: main.c:1054-1056

Equations

• Ratpoints.Cli.Failure.tooFewArguments.status = 2
• Ratpoints.Cli.Failure.tooManyCoefficients.status = 3
• Ratpoints.Cli.Failure.incorrectHeight.status = 4
• Ratpoints.Cli.Failure.tooFewCoefficients.status = 5
• Ratpoints.Cli.Failure.optionSyntax.status = 6
• Ratpoints.Cli.Failure.intervals.status = 7
• Ratpoints.Cli.Failure.notSquarefree.status = 8
• Ratpoints.Cli.Failure.badArgs.status = 9
• Ratpoints.Cli.Failure.incorrectCoefficients.status = 11

def Ratpoints.Cli.Failure.ofRefusal : Refusal → Failure

The failure of ratpoints-lean for a refusal of the search (Ratpoints.findPointsWith, whose refusals are those of Ratpoints.findPoints): the error of main.c with the number that Ratpoints.Refusal names, as main.c turns the code RATPOINTS_NON_SQUAREFREE that the library returns into error 8 and its codes other than RATPOINTS_NO_MEMORY (error 10) into error 9, among them RATPOINTS_BAD_ARGS (Ratpoints.Refusal.badArgs). The reading of the command line (Ratpoints.Cli.input) refuses the inputs of the other refusals first, and the command line gives no search intervals that the library refuses, so that of the refusals of Ratpoints.findPointsWith, which Ratpoints.Cli.run maps by it, only Ratpoints.Refusal.notSquarefree can reach it.

C: main.c:256-261

Deviation: no error 10, since the model has no failure for lack of memory; the refusals of the coefficients and of the height (Ratpoints.Refusal.tooManyCoefficients, Ratpoints.Refusal.tooFewCoefficients, Ratpoints.Refusal.incorrectHeight) mapped to the errors 3, 5 and 4 with which read_input refuses those inputs before the library is called, where line 260 gives error 9 for the code RATPOINTS_BAD_ARGS with which the library refuses those it can be given (lines 4557-4558, 4633 and 4658 of find_points.c); no command line reaches them; no mpz_clear.

Equations

• Ratpoints.Cli.Failure.ofRefusal Ratpoints.Refusal.tooManyCoefficients = Ratpoints.Cli.Failure.tooManyCoefficients
• Ratpoints.Cli.Failure.ofRefusal Ratpoints.Refusal.tooFewCoefficients = Ratpoints.Cli.Failure.tooFewCoefficients
• Ratpoints.Cli.Failure.ofRefusal Ratpoints.Refusal.incorrectHeight = Ratpoints.Cli.Failure.incorrectHeight
• Ratpoints.Cli.Failure.ofRefusal Ratpoints.Refusal.notSquarefree = Ratpoints.Cli.Failure.notSquarefree
• Ratpoints.Cli.Failure.ofRefusal Ratpoints.Refusal.badArgs = Ratpoints.Cli.Failure.badArgs

The command line

def Ratpoints.Cli.coefficients (s : String) : Except Failure (List Int)

The coefficient list that the first argument s of the command line gives, constant term first, as main.c reads it: integers as Ratpoints.Cli.intOfWord? reads them, separated by C white space, which may also stand before the first and after the last. A word that is not an integer fails with error 11, wherever it stands; then more than Ratpoints.maxDegree + 1 integers fail with error 3, and fewer than two with error 5.

C: main.c:54, main.c:318, main.c:362-375

Deviation: a list of Ints for the global array c of RATPOINTS_MAX_DEGREE + 1 GMP integers; the integers beyond these, which main.c reads into the variable fff only to check them, are read like the others.

Equations

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

def Ratpoints.Cli.heightBound (s : String) : Except Failure Nat

The height bound that the second argument s of the command line gives, as main.c reads it: a C long as Ratpoints.Cli.longOfString? reads it, at least 1, so from 1 to 2⁶³ - 1; anything else fails with error 4.

C: main.c:378-379

Equations

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

inductive Ratpoints.Cli.OptionArg : Type

The kinds of argument that the options of ratpoints-lean take.

• long : OptionArg

  A C long, as Ratpoints.Cli.longOfString? reads it.

• double : OptionArg

  A C double, as Ratpoints.Cli.scanDouble? reads it.

• optionalLong : OptionArg

  An optional C long: the next word, if there is one and it does not start with -, which is then a C long as Ratpoints.Cli.longOfString? reads it.

• word : OptionArg

  A string: the next word, whatever it is, also one that starts with -.

• bound : OptionArg

  An end of a search interval, as Ratpoints.Cli.scanEnd reads it, with the checks of Ratpoints.Cli.Intervals.lower and Ratpoints.Cli.Intervals.upper; a missing or malformed one fails with error 7.

def Ratpoints.Cli.OptionArg.accepts (arg : OptionArg) (a : String) : Bool

Whether a is an argument of the kind arg.

Equations

• Ratpoints.Cli.OptionArg.long.accepts a = (Ratpoints.Cli.longOfString? a).isSome
• Ratpoints.Cli.OptionArg.optionalLong.accepts a = (Ratpoints.Cli.longOfString? a).isSome
• Ratpoints.Cli.OptionArg.double.accepts a = (Ratpoints.Cli.scanDouble? a).isSome
• Ratpoints.Cli.OptionArg.word.accepts a = true
• Ratpoints.Cli.OptionArg.bound.accepts a = true

def Ratpoints.Cli.optionArg (o : String) : Except Failure (Option OptionArg)

The kind of argument that the option o takes, or none if it takes none, for an option that ratpoints-lean reads. main.c tells an option by the character after its -, and for -f and -d by the one after that, ignoring the rest of the word, so that -quiet is -q and -fsx is -fs. The tuning options -p -F -t -n -N -R -A -P take a C long, -r -U -C -Q -W a C double, -S an optional C long, the options of the output -f -fs -fm -fe a string, the bounds of the denominators -dl -du a C long, the ends of the search intervals -l -u an end, and -q -v -j -J -k -K -s, the switches of the check and of the pairs -x -X -y -Y, and those of the output -z -Z -1 -i -I, nothing. Every other word, among them a word without a leading -, a word -f… with a third character other than s, m and e and a word -d… with one other than l and u, fails with error 6.

Equations

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

structure Ratpoints.Cli.Output : Type

The settings of the output of ratpoints-lean, the global variables of main.c, with their defaults, those of a command line without options: whether the report is left out (-q), whether it is the report of -v (the bit RATPOINTS_VERBOSE of the flags), whether the search stops at the first point counted (-1), whether the points at infinity are kept (-I, and not -i), whether no point is printed (-z, and not -Z), the format of a point (-f), none for the default (Ratpoints.Cli.defaultFormat), the strings before, between and after the points (-fs, -fm, -fe), none for none, and the exact ends of the search intervals of the command line, which process reads (ends, as the options -l and -u fill it: Ratpoints.Cli.Intervals).

C: main.c:57-64, main.c:383-390, ratpoints.h:407

Deviation: a structure for the global variables; Option String for the strings and the format, none for the null pointer, and Lean strings for the C strings of the command line, which the Lean runtime decodes as UTF-8 (bytes that do not form UTF-8 are read as U+FFFD, one for each malformed sequence as the Lean runtime cuts them, where main.c copies the bytes); the bit RATPOINTS_VERBOSE of args->flags a field here, from which the program makes the print channel of the library (Ratpoints.Cli.run).

• quiet : Bool

  quiet: whether the report is left out.

• verbose : Bool

  The bit RATPOINTS_VERBOSE of the flags: whether the report is that of -v.

• onePoint : Bool

  one_point: whether the search stops at the first point that process does not pass over (the first point counted, printed or not).

• pointsAtInfty : Bool

  points_at_infty: whether the points at infinity are kept (counted, able to stop the search under -1, and printed unless -z), not passed over as under -i.

• noOutput : Bool

  no_output: whether no point is printed (they are counted).

• printFormat : Option String

  print_format: the format of a point, none for the default.

• stringBefore : Option String

  string_before: the string before the points.

• stringBetween : Option String

  string_between: the string between two points.

• stringAfter : Option String

  string_after: the string after the points.

• ends : Array ExactEnd

  ends: the exact ends of the search intervals of the command line, ends[2 i] ≤ x ≤ ends[2 i + 1] for the i-th, as Ratpoints.Cli.input takes them from the reading of the options (Ratpoints.Cli.Intervals.ends).

structure Ratpoints.Cli.Intervals : Type

The state of the reading of the search intervals by read_input of main.c: whether the last end read is a lower one (l_seen), the number of the intervals read (num_inter), and the arrays domain and ends of main.c as the options -l and -u fill them, of 2 maxDegree entries, the doubles of the ends that the library is given and the exact ends, ends[2 i] ≤ x ≤ ends[2 i + 1] for the i-th interval.

C: main.c:66, main.c:73, main.c:317, main.c:319

Deviation: a structure for the two locals of read_input and the two global arrays, whose entries are zero (the doubles) and 0 (the exact ends, as mpq_init sets them, main.c:205) at the start; pairs of doubles for the entries of the type ratpoints_interval; a natural number for the long num_inter.

• lSeen : Bool

  l_seen: whether the last end read is a lower one, whose interval is not complete.

• numInter : Nat

  num_inter: the number of the complete intervals read.

• domain : Array (Double × Double)

  domain: the doubles of the ends of the intervals, the lower and the upper one, that the library is given.

• ends : Array ExactEnd

  ends: the exact ends of the intervals, ends[2 i] the lower and ends[2 i + 1] the upper end of the i-th.

def Ratpoints.Cli.Intervals.lower (iv : Intervals) (a : String) : Except Failure Intervals

The reading iv of the search intervals after a lower end a (-l a), as read_input of main.c reads it: error 7 after another lower end (-l -l), when Ratpoints.maxDegree intervals have been read, when a is not a number (Ratpoints.Cli.scanEnd with the direction -1), and when it is not above the upper end of the interval before, compared as the numbers they are (Ratpoints.Cli.cmpEnd); otherwise the exact end and its double as the lower end of the next interval, which is not complete.

C: main.c:401-413

Equations

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

def Ratpoints.Cli.Intervals.upper (iv : Intervals) (H : Nat) (a : String) : Except Failure Intervals

The reading iv of the search intervals after an upper end a (-u a), for the height bound H, as read_input of main.c reads it: without a lower end before it, the lower end of the first interval is -∞, with the double of -Ratpoints.Cli.heightEnd H, and the upper end of another one fails with error 7 (-u -u); error 7 when a is not a number (Ratpoints.Cli.scanEnd with the direction 1); its double is the upper one of the interval, whose lower double is -∞ when the interval has no lower end and its upper double lies below -Ratpoints.Cli.heightEnd H (an interval that holds no x of the search, made [-∞, u] rather than turned around); error 7 when the lower end is above the upper one, compared as the numbers they are (Ratpoints.Cli.cmpEnd); otherwise the interval is complete.

C: main.c:417-436

Equations

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

def Ratpoints.Cli.Intervals.complete (iv : Intervals) (H : Nat) : Intervals

The reading iv of the search intervals completed after the options, for the height bound H, as read_input of main.c completes it: an interval with a lower end and no upper one ends at +∞, with the double Ratpoints.Cli.heightEnd H, or +∞ when that lies below its lower double (an interval that holds no x of the search, made [l, +∞] rather than turned around).

C: main.c:669, main.c:673-678

Equations

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

def Ratpoints.Cli.Output.store (u : Output) (o : String) (a : Option String) : Output

The settings of the output u with the field that the option o sets, with its argument a if it takes one: the report left out for -q and that of -v for -v, the format for -f, the strings for -fs, -fm and -fe, no point printed for -z and the points printed for -Z, one point for -1, the points at infinity passed over for -i and kept for -I; u itself for every other option.

Equations

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

def Ratpoints.Options.store (t : Options) (o : String) (a : Option String) : Options

The options t of the search with the field that the option o sets, with its argument a if it takes one: the reversal forbidden for -k and allowed for -K; the depth -1 of the Sturm step for -s, and for -S the C long of a, or Ratpoints.defaultSturm if there is none; the C long of a as the least denominator for -dl and as the largest for -du; the exact check off for -x and on for -X; one point of each pair for -y and both for -Y; t itself for every other option.

Equations

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

def Ratpoints.SieveOptions.store (s : SieveOptions) (o : String) (a : Option String) : SieveOptions

The options of the sieve s with the field that the option o sets, with its argument a: the C long of a for -p -n -N -R -A -P -F and its double for -r -U -C -Q -W, as main.c reads them (Ratpoints.Cli.longOfString?, Ratpoints.Cli.scanDouble?); the Jacobi test off for -j and on for -J. It models no C code of its own: it is the part of Ratpoints.Cli.checkOptions that sets the fields of Ratpoints.SieveOptions.

Equations

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

def Ratpoints.Cli.checkOptions (H : Nat) (s : SieveOptions × Options × Output × Intervals) : List String → Except Failure (SieveOptions × Options × Output × Intervals)

The values of the options of the command line for the height bound H, the options of the sieve (Ratpoints.SieveOptions), the options of the search (Ratpoints.Options), the settings of the output (Ratpoints.Cli.Output) and the reading of the search intervals (Ratpoints.Cli.Intervals), starting from s, or the first failure among the options, the words that follow the coefficients and the height bound on the command line, read from left to right as main.c reads them: an option that fails by Ratpoints.Cli.optionArg, or one whose argument is missing or malformed (error 6, and error 7 for -l and -u), fails; -p, -n, -N, -R, -A, -P and -F set the fields of Ratpoints.SieveOptions to the C long that follows them and -r, -U, -C, -Q and -W to the double, the last one winning, and -j switches the Jacobi test off and -J on again, as main.c sets the fields and the flags of its ratpoints_args (Ratpoints.SieveOptions.store); -k forbids the reversal of the polynomial and -K allows it again, -s sets the depth of the Sturm step to -1, which switches the step off, and -S to the C long that the next word gives if there is one and it does not start with -, and else to Ratpoints.defaultSturm, so that the step is on unless that depth is negative; -dl and -du set the least and the largest denominator to the C long that follows them; -l and -u read a lower and an upper end of a search interval (Ratpoints.Cli.Intervals.lower, Ratpoints.Cli.Intervals.upper); -x switches the exact check off and -X on again, -y makes the search deliver one point of each pair and -Y both; -f, -fs, -fm and -fe take the next word, whatever it is, as the format or the string, and -q -v -z -Z -1 -i -I set the settings of the output (Ratpoints.Cli.Output.store); of each setting the last one wins. It ignores -t, the number of threads of the C program.

C: main.c:393-400, main.c:414-416, main.c:437-532, main.c:533-577, main.c:578-593, main.c:594-601, main.c:602-637, main.c:638-649, main.c:650-668

Deviation: the argument of -t, the number of threads, checked and then ignored, since the model sieves the blocks of the run in turn on one thread, which gives the output of every number of threads; the strings of -f, -fs, -fm and -fe kept as values, for the copies that main.c allocates, with error 10 when the allocation fails, which the model cannot meet.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Cli.checkOptions H s [] = pure s

def Ratpoints.Cli.checkOptions.store (s : SieveOptions × Options × Output × Intervals) (o : String) (a : Option String) : SieveOptions × Options × Output × Intervals

s with the field that the option o sets, with its argument a if it takes one: the options of the sieve by Ratpoints.SieveOptions.store, the options of the search by Ratpoints.Options.store and the settings of the output by Ratpoints.Cli.Output.store.

Equations

• Ratpoints.Cli.checkOptions.store (s_2, t, u, iv) o a = (s_2.store o a, t.store o a, u.store o a, iv)

def Ratpoints.Cli.defaultFormat (o : Options) : String

The format of a point that main.c takes when the command line gives none: (%x : %z) and a line feed when the points are not checked exactly or only one point of each pair is delivered (Ratpoints.Options.noCheck, Ratpoints.Options.noY), else (%x : %y : %z) and a line feed.

C: main.c:681-685

Equations

• Ratpoints.Cli.defaultFormat o = if (o.noCheck || o.noY) = true then "(%x : %z)\n" else "(%x : %y : %z)\n"

def Ratpoints.Cli.input : List String → Except Failure (List Int × Nat × SieveOptions × Options × Output)

What a command line (the words after the name of the program) gives: the coefficient list, the height bound, the options of the sieve (Ratpoints.SieveOptions), the options of the search and the settings of the output, or the first failure, in the order of main.c: fewer than two words fail with error 2; then come the coefficients (Ratpoints.Cli.coefficients), the height bound (Ratpoints.Cli.heightBound) and the options (Ratpoints.Cli.checkOptions), read from the defaults of Ratpoints.SieveOptions, Ratpoints.Options with the height bound as the largest denominator, Ratpoints.Cli.Output and Ratpoints.Cli.Intervals, the values of a command line without options; then an interval with a lower end and no upper one is completed (Ratpoints.Cli.Intervals.complete), the search intervals of the options are those read, their doubles, and the exact ends those of the settings of the output, the format is the default (Ratpoints.Cli.defaultFormat) unless an option -f gave one, and -q cancels -v.

C: main.c:210-214, main.c:315-316, main.c:333-336, main.c:380, main.c:679, main.c:688, main.c:691-692

Deviation: read_input never returns a value other than 0, so the usage that main.c prints then (lines 212 and 213) has no counterpart; the largest denominator -1 of line 336, which line 380 replaces by the height bound, not set; the search intervals a list of the intervals read, for the pointer args->domain to the array domain and the number args->num_inter.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Cli.input x✝ = throw Ratpoints.Cli.Failure.tooFewArguments

The points

def Ratpoints.Cli.escape (ch : Char) : String

What main.c prints for a backslash followed by the character ch in a format or in a string: a tab for t, a line feed for n, a backslash for a backslash, a percent sign for %, and the backslash and ch as they are for every other character.

C: main.c:178-182, main.c:961-965

Deviation: one function for the two switches of process and print_string, which agree.

Equations

• Ratpoints.Cli.escape 't' = "\t"
• Ratpoints.Cli.escape 'n' = "\n"
• Ratpoints.Cli.escape '\\' = "\\"
• Ratpoints.Cli.escape '%' = "%"
• Ratpoints.Cli.escape ch = "\\".push ch

def Ratpoints.Cli.printString (s : Option String) : String

What print_string of main.c prints for the string s: nothing for none; otherwise its characters as they are, but a backslash, which Ratpoints.Cli.escape prints with the character after it, and a backslash at the end, which prints itself and ends the string.

C: main.c:952-960, main.c:966-968

Deviation: a recursion over the characters, for the loop over the C string.

Equations

• Ratpoints.Cli.printString s = Ratpoints.Cli.printString.go (s.getD "").toList

def Ratpoints.Cli.printString.go : List Char → String

What print_string prints for the characters s.

Equations

• Ratpoints.Cli.printString.go [] = ""
• Ratpoints.Cli.printString.go ['\\'] = "\\"
• Ratpoints.Cli.printString.go ('\\' :: ch :: s) = Ratpoints.Cli.escape ch ++ Ratpoints.Cli.printString.go s
• Ratpoints.Cli.printString.go (ch :: s) = ch.toString ++ Ratpoints.Cli.printString.go s

def Ratpoints.Cli.formatPoint (noY : Bool) (x z y : Int) : List Char → String

What process of main.c prints for the point (x : y : z) in the format fmt, character by character: %x, %y and %z print x, y and z in decimal, but %y prints itself when noY is set (the points were not checked exactly or only one point of each pair is delivered), a percent sign before another character prints both, and one at the end prints itself and ends the format; a backslash and the character after it print as Ratpoints.Cli.escape prints them, and one at the end prints itself and ends the format; every other character prints itself.

C: main.c:157-177, main.c:183-186

Deviation: a recursion over the characters, for the loop over the C string; an Int for the GMP integer y and for the longs x and z, which print alike.

Equations

• Ratpoints.Cli.formatPoint noY x z y [] = ""
• Ratpoints.Cli.formatPoint noY x z y ['%'] = "%"
• Ratpoints.Cli.formatPoint noY x z y ('%' :: 'x' :: fmt) = toString x ++ Ratpoints.Cli.formatPoint noY x z y fmt
• Ratpoints.Cli.formatPoint noY x z y ('%' :: 'y' :: fmt) = (if noY = true then "%y" else toString y) ++ Ratpoints.Cli.formatPoint noY x z y fmt
• Ratpoints.Cli.formatPoint noY x z y ('%' :: 'z' :: fmt) = toString z ++ Ratpoints.Cli.formatPoint noY x z y fmt
• Ratpoints.Cli.formatPoint noY x z y ('%' :: ch :: fmt) = "%".push ch ++ Ratpoints.Cli.formatPoint noY x z y fmt
• Ratpoints.Cli.formatPoint noY x z y ['\\'] = "\\"
• Ratpoints.Cli.formatPoint noY x z y ('\\' :: ch :: fmt) = Ratpoints.Cli.escape ch ++ Ratpoints.Cli.formatPoint noY x z y fmt
• Ratpoints.Cli.formatPoint noY x z y (ch :: fmt) = ch.toString ++ Ratpoints.Cli.formatPoint noY x z y fmt

structure Ratpoints.Cli.Data : Type

The data that main.c passes to its callback process through info: whether it has printed a point (print_between), the settings of the output that it reads, whether %y prints itself (no_y), the number of the search intervals of the command line and their exact ends, against which process checks the points, and the text printed so far.

C: main.c:110-113

Deviation: the text printed so far, for the standard output, to which process prints; an array for the pointer ends and a natural number for the long num_inter.

• printBetween : Bool

  print_between: whether a point was printed, so that the next one comes after -fm.

• noOutput : Bool

  no_output: whether no point is printed.

• onePoint : Bool

  one_point: whether the search stops at the first point that process does not pass over (the first point counted, printed or not).

• pointsAtInfty : Bool

  points_at_infty: whether the points at infinity are kept (counted, able to stop the search under -1, and printed unless -z), not passed over as under -i.

• noY : Bool

  no_y: whether %y prints itself.

• pf : String

  pf: the format of a point.

• stringBefore : Option String

  string_before: the string before the points.

• stringBetween : Option String

  string_between: the string between two points.

• numInter : Nat

  num_inter: the number of the search intervals of the command line, 0 for none.

• ends : Array ExactEnd

  ends: the exact ends of the search intervals of the command line.

• out : String

  The text printed so far.

def Ratpoints.Cli.Data.ofOutput (u : Output) (o : Options) : Data

The data that main.c passes to process for the settings of the output u and the options o of the search: no point printed yet, the settings of u, %y printing itself when the points are not checked exactly or only one point of each pair is delivered, and the number of the search intervals of the command line, as read before Ratpoints.Cli.joinIntervals joins them, with their exact ends.

C: main.c:235-242, main.c:246-247

Deviation: the format the one that Ratpoints.Cli.input settled, "" if none.

Equations

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

def Ratpoints.Cli.process (x z y : Int) (info : Data) : Answer Data

The callback process of main.c on the point (x : y : z) with the data info: a point at infinity (z = 0) is passed over when the points at infinity are not kept (-i), and an affine point when the command line gives search intervals and x / z lies in none of them (Ratpoints.Cli.inRegion), which the library may find just beyond an end, since it searches intervals whose ends are the doubles outward of those of the command line: such a point has the weight 0 and leaves the flag clear, so that it is neither counted nor stops the search under -1; every other point stops the search when one point is enough, and has the weight 1; it is printed unless no point is printed: after the string before the points if it is the first point printed, and else after the string between them, in the format (Ratpoints.Cli.formatPoint).

C: main.c:139-142, main.c:150-156, main.c:187-189

Deviation: the data a value, for the pointer info, and returned with the weight and the flag, for the int *quit that the library passes, which is clear at every call; the text appended to that of the data, for the standard output, and no fflush.

Equations

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

def Ratpoints.Cli.Data.print (t : String) (info : Data) : Data

The text t printed on the standard output, as the library prints its report under RATPOINTS_VERBOSE: appended to the text printed so far in the data info of process. It models no C code of its own: the print channel that Ratpoints.Cli.run passes the search under -v (Ratpoints.findPointsVerbose), for the calls of printf in the library.

Equations

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

The report

def Ratpoints.Cli.printPoly (c : List Int) : String

The polynomial with the coefficient list c, constant term first, as print_poly of main.c prints it: its terms from the highest degree c.length - 1 down, the zero ones left out, the first after - if it is negative and the others after + or -, each the absolute value of its coefficient, then x for the degree 1 and x^i for a degree i ≥ 2, the coefficient left out when it is 1 there; and a line feed.

C: main.c:913-949

Deviation: a fold over the coefficients, for the loop; no fflush.

Equations

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

inductive Ratpoints.Cli.Message : Type

The messages of the report of main.c that ratpoints-lean prints, with the data they read: message 0, the banner; message 2, the count of the points found, of the pairs when the points are not checked exactly or only one point of each pair is delivered; message 3, the search region of the command line; message 4, the numbers of the moduli used in the first stage, in the first two and in all three stages; message 5, the curve; message 6, the height bound; message 7, what the search did: whether the polynomial was reversed, whether the denominators could be restricted to squares (RATPOINTS_USE_SQUARES) or essentially to squares (RATPOINTS_USE_SQUARES1), whether the Jacobi test was off, and whether the points were not checked exactly; and message 8, the search intervals as the search leaves them.

• banner : Message

  Message 0: the banner.

• count (total : Int) (pairs : Bool) : Message

  Message 2: the count total, of the pairs when pairs is set.

• region (dom : List (Double × Double)) : Message

  Message 3: the search region of the command line, the doubles dom of its intervals before they are joined.

• moduli (sp1 sp2 sp3 : Nat) : Message

  Message 4: the numbers sp1, sp2 and sp3 of the moduli used in the first stage, in the first two and in all three stages.

• curve (c : List Int) : Message

  Message 5: the curve of the coefficient list c.

• height (H : Nat) : Message

  Message 6: the height bound H.

• flags (reversed useSquares useSquares1 noJacobi noCheck : Bool) : Message

  Message 7: the flags of the search.

• intervals (dom : List (Double × Double)) : Message

  Message 8: the search intervals dom as the search leaves them.

def Ratpoints.Cli.showIntervals (dom : List (Double × Double)) : String

The intervals dom as messages 3 and 8 of main.c print them: each as [l, u] with its ends printed under %f (Ratpoints.Cli.printF), the intervals separated by U.

Equations

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

def Ratpoints.Cli.Message.text : Message → String

The text of a message of the report, as message of main.c prints it.

C: main.c:972-976, main.c:979-1033

Deviation: the banner of ratpoints-lean (Ratpoints.Cli.banner); a constructor for each message that ratpoints-lean prints, with its data, for the number n and the arguments of the library: message 1, which the program prints when read_input fails, which it never does, is left out; the loops over the intervals of messages 3 and 8 as Ratpoints.Cli.showIntervals, the conversion %lf of message 8 being %f; the difference sp3_used - sp2_used of message 4 an integer, for the long; no fflush.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Cli.Message.banner.text = toString "\n" ++ toString Ratpoints.Cli.banner ++ toString "\n"
• (Ratpoints.Cli.Message.count total pairs).text = toString "\n" ++ toString total ++ toString " rational point" ++ toString (if pairs = true then " pair" else "") ++ toString "s found.\n\n"
• (Ratpoints.Cli.Message.region dom).text = toString "Search region:\n " ++ toString (Ratpoints.Cli.showIntervals dom) ++ toString "\n"
• (Ratpoints.Cli.Message.curve c).text = toString "\nCurve equation is y^2 = " ++ toString (Ratpoints.Cli.printPoly c) ++ toString "\n"
• (Ratpoints.Cli.Message.height H).text = toString "max. Height = " ++ toString H ++ toString "\n"
• (Ratpoints.Cli.Message.intervals dom).text = toString "Search intervals:\n" ++ toString (Ratpoints.Cli.showIntervals dom) ++ toString "\n"

def Ratpoints.Cli.preamble (c : List Int) (H : Nat) (u : Output) (dom : List (Double × Double)) : String

What main.c prints before the search for the settings of the output u: nothing when the report is left out (-q); otherwise the banner, the curve of the coefficient list c, unless the report is that of -v the height bound H and a blank line, and the search region (message 3) when the command line gives search intervals, their doubles dom before they are joined, also under -v.

C: main.c:215-220, main.c:224

Equations

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

def Ratpoints.Cli.report {σ : Type} (s : SieveOptions) (o : Options) (u : Output) (r : Outcome σ) : String

What main.c prints after the points for the settings of the output u: nothing when the report is left out (-q); otherwise, unless the report is that of -v, two line feeds, the numbers of the moduli used that the search r writes back (message 4), what the search did (message 7), from the flags that the search r writes back, the Jacobi switch of the options s and the switch of the exact check of the options o, and the search intervals as the search leaves them (message 8, from r.domain); then the count of the points found, the count total of the search, of the pairs under -x or -y (message 2).

C: main.c:268-276

Equations

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

The program

def Ratpoints.Cli.run (args : List String) : String × UInt32

What ratpoints-lean does on the command line args (the words after the name of the program): the text it prints on the standard output and its exit status. On the coefficient list c, the height bound H, the options s of the sieve, the options o of the search and the settings u of the output, as Ratpoints.Cli.input reads them, it prints the head of the report (Ratpoints.Cli.preamble, nothing under -q), and then runs the search Ratpoints.findPointsVerbose with the options s of the sieve, with the array size that the program sets, Ratpoints.defaultArraySize, the options o with the search intervals joined (Ratpoints.Cli.joinIntervals), the callback Ratpoints.Cli.process on its data (Ratpoints.Cli.Data.ofOutput, with the intervals of the command line before they are joined), and, under -v, the print channel Ratpoints.Cli.Data.print, through which the library prints its report between the points, and otherwise the print channel that prints nothing: on a refusal it prints what the library printed and the message of the failure (Ratpoints.Cli.Failure.ofRefusal) and exits with its status; otherwise it prints what the callback and the library printed, the string before the points if the callback printed no point, the string after the points and the end of the report (Ratpoints.Cli.report, nothing under -q), and exits with status 0; on a failure f of the command line it prints f.message and exits with f.status (Ratpoints.Cli.Failure.message, Ratpoints.Cli.Failure.status).

C: main.c:195-198, main.c:221-222, main.c:248, main.c:251-252, main.c:265, main.c:267, main.c:284-285

Deviation: the text written once at the end (Ratpoints.Cli.main), where main.c prints as it goes; the bit RATPOINTS_VERBOSE of the flags, which the program sets under -v and leaves clear under -q (Ratpoints.Cli.input), as the print channel that it passes the library, and one that prints nothing otherwise.

Equations

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

def Ratpoints.Cli.main (args : List String) : IO UInt32

The program ratpoints-lean: it prints the text of Ratpoints.Cli.run on the standard output, in one write once it is computed, and exits with its status. Like ratpoints, it ignores a failed write, but for one case: when the reader of the output is gone, the write fails with IO.Error.resourceVanished, since the Lean runtime ignores the signal SIGPIPE that ends ratpoints then, and the program exits quietly with the status 141 that the shell reports for ratpoints (where SIGPIPE has its default action). It flushes the standard output itself, since a short output waits in the buffer of the C library until the exit, where a failed write goes unnoticed.

Equations

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

Examples

Each of them is what ratpoints 3.1.1 does, but for the banner, also under -v, with the report of the library.