The command-line program on the fast search

ratpoints-lean 'a₀ a₁ … aₙ' H [-dl b] [-du b] [-q] prints the points of height at most H on y ^ 2 = a₀ zᴰ + a₁ x zᴰ⁻¹ + ⋯ + aₙ xⁿ zᴰ⁻ⁿ that Ratpoints.FastMask.fastPoints lists, one per line as (x : y : z), the points at infinity included; -dl and -du bound the denominators from below and above, and -q is accepted and ignored. On an argument that it cannot read it prints a message on the standard error and exits with status 1.

Main definitions

• Ratpoints.FastCli.main: the program.

structure Ratpoints.FastCli.Args : Type

The arguments of a run: the coefficients, the height bound and the bounds of the denominators.

• coeffs : List Int

  The coefficients a₀, …, aₙ.

• H : Nat

  The height bound.

• bLow : Int

  The lower bound of the denominators.

• bHigh : Int

  The upper bound of the denominators; below 1 for none.

def Ratpoints.FastCli.readOptions (a : Args) : List String → Except String Args

The options after the height bound, read into a.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.FastCli.readOptions a [] = Except.ok a
• Ratpoints.FastCli.readOptions a ("-q" :: rest) = Ratpoints.FastCli.readOptions a rest
• Ratpoints.FastCli.readOptions a (o :: tail) = Except.error (toString "unknown or incomplete option '" ++ toString o ++ toString "'")

def Ratpoints.FastCli.readArgs : List String → Except String Args

The arguments of the command line.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.FastCli.readArgs x✝ = Except.error "usage: ratpoints-lean 'a_0 a_1 ... a_n' H [-dl b] [-du b] [-q]"

def Ratpoints.FastCli.pointLine (p : Int × Int × Int) : String

The line of a point.

Equations

• Ratpoints.FastCli.pointLine p = toString "(" ++ toString p.fst ++ toString " : " ++ toString p.snd.fst ++ toString " : " ++ toString p.snd.snd ++ toString ")"

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

The program: the points of Ratpoints.FastMask.fastPoints, one per line.

Equations

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