mathlib3 documentation

data.buffer.parser.numeral

Numeral parsers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file expands on the existing nat : parser ℕ to provide parsers into any type α that can be represented by a numeral, which relies on α having a 0, 1, and addition operation. There are also convenience parsers that ensure that the numeral parsed in is not larger than the cardinality of the type α , if it is known that fintype α. Additionally, there are convenience parsers that parse in starting from "1", which can be useful for positive ordinals; or parser from a given character or character range.

Main definitions #

parser.numeral : The parser which uses nat.cast to map the result of parser.nat to the desired α
parser.numeral.of_fintype : The parser which guards to make sure the parsed numeral is within the cardinality of the target fintype type α.

Implementation details #

When the parser.numeral or related parsers are invoked, the desired type is provided explicitly. In many cases, it can be inferred, so one can write, for example

def get_fin : string → fin 5 :=
sum.elim (λ _, 0) id ∘ parser.run_string (parser.numeral.of_fintype _)

In the definitions of the parsers (except for parser.numeral), there is an explicit nat.bin_cast instead an explicit or implicit nat.cast.

@[protected, instance]

def parser.numeral.mono (α : Type) [has_zero α] [has_one α] [has_add α] :

(parser.numeral α).mono

@[protected, instance]

def parser.numeral.prog (α : Type) [has_zero α] [has_one α] [has_add α] :

(parser.numeral α).prog

@[protected, instance]

def parser.numeral.bounded (α : Type) [has_zero α] [has_one α] [has_add α] :

(parser.numeral α).bounded

def parser.numeral (α : Type) [has_zero α] [has_one α] [has_add α] :

Parse a string of digits as a numeral while casting it to target type α.

Equations

parser.numeral α = nat.bin_cast <$> parser.nat

Instances for parser.numeral

def parser.numeral.of_fintype (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] :

Parse a string of digits as a numeral while casting it to target type α, which has a [fintype α] constraint. The parser ensures that the numeral parsed in is within the cardinality of the type α.

Equations

parser.numeral.of_fintype α = parser.nat >>= λ (c : ℕ), parser.decorate_error (λ («_» : unit), " ++ to_string (to_string (fintype.card α)) ++ ">") (guard (c < fintype.card α)) >>= λ (_x : unit), has_pure.pure c.bin_cast

Instances for parser.numeral.of_fintype

@[protected, instance]

def parser.numeral.of_fintype.prog (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] :

(parser.numeral.of_fintype α).prog

@[protected, instance]

def parser.numeral.of_fintype.mono (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] :

(parser.numeral.of_fintype α).mono

@[protected, instance]

def parser.numeral.of_fintype.bounded (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] :

(parser.numeral.of_fintype α).bounded

@[protected, instance]

def parser.numeral.from_one.bounded (α : Type) [has_zero α] [has_one α] [has_add α] :

(parser.numeral.from_one α).bounded

@[protected, instance]

def parser.numeral.from_one.mono (α : Type) [has_zero α] [has_one α] [has_add α] :

(parser.numeral.from_one α).mono

@[protected, instance]

def parser.numeral.from_one.prog (α : Type) [has_zero α] [has_one α] [has_add α] :

(parser.numeral.from_one α).prog

def parser.numeral.from_one (α : Type) [has_zero α] [has_one α] [has_add α] :

Parse a string of digits as a numeral while casting it to target type α. The parsing starts at "1", so "1" is parsed in as nat.cast 0. Providing "0" to the parser causes a failure.

Equations

parser.numeral.from_one α = parser.nat >>= λ (c : ℕ), parser.decorate_error (λ («_» : unit), "") (guard (0 < c)) >>= λ (_x : unit), has_pure.pure (c - 1).bin_cast

Instances for parser.numeral.from_one

def parser.numeral.from_one.of_fintype (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] :

Parse a string of digits as a numeral while casting it to target type α, which has a [fintype α] constraint. The parser ensures that the numeral parsed in is within the cardinality of the type α. The parsing starts at "1", so "1" is parsed in as nat.cast 0. Providing "0" to the parser causes a failure.

Equations

parser.numeral.from_one.of_fintype α = parser.nat >>= λ (c : ℕ), parser.decorate_error (λ («_» : unit), " ++ to_string (to_string (fintype.card α)) ++ ">") (guard (0 < c ∧ c ≤ fintype.card α)) >>= λ (_x : unit), has_pure.pure (c - 1).bin_cast

Instances for parser.numeral.from_one.of_fintype

@[protected, instance]

def parser.numeral.from_one.of_fintype.prog (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] :

(parser.numeral.from_one.of_fintype α).prog

@[protected, instance]

def parser.numeral.from_one.of_fintype.bounded (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] :

(parser.numeral.from_one.of_fintype α).bounded

@[protected, instance]

def parser.numeral.from_one.of_fintype.mono (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] :

(parser.numeral.from_one.of_fintype α).mono

@[protected, instance]

def parser.numeral.char.step (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :

(parser.numeral.char α fromc toc).step

@[protected, instance]

def parser.numeral.char.err_static (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :

(parser.numeral.char α fromc toc).err_static

def parser.numeral.char (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :

Parse a character as a numeral while casting it to target type α, The parser ensures that the character parsed in is within the bounds set by fromc and toc, and subtracts the value of fromc from the parsed in character.

Equations

parser.numeral.char α fromc toc = parser.decorate_error (λ («_» : unit), " ++ to_string fromc.to_string ++ ("' to '" ++ to_string toc.to_string ++ "' inclusively>")) (parser.sat (λ (c : char), fromc ≤ c ∧ c ≤ toc)) >>= λ (c : char), has_pure.pure (c.to_nat - fromc.to_nat).bin_cast

Instances for parser.numeral.char

@[protected, instance]

def parser.numeral.char.mono (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :

(parser.numeral.char α fromc toc).mono

@[protected, instance]

def parser.numeral.char.bounded (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :

(parser.numeral.char α fromc toc).bounded

@[protected, instance]

def parser.numeral.char.of_fintype.step (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] (fromc : char) :

(parser.numeral.char.of_fintype α fromc).step

@[protected, instance]

def parser.numeral.char.of_fintype.mono (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] (fromc : char) :

(parser.numeral.char.of_fintype α fromc).mono

def parser.numeral.char.of_fintype (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] (fromc : char) :

Parse a character as a numeral while casting it to target type α, which has a [fintype α] constraint. The parser ensures that the character parsed in is greater or equal to fromc and and subtracts the value of fromc from the parsed in character. There is also a check that the resulting value is within the cardinality of the type α.

Equations

parser.numeral.char.of_fintype α fromc = parser.decorate_error (λ («_» : unit), " ++ to_string fromc.to_string ++ ("' to '\n " ++ to_string (char.of_nat (fromc.to_nat + fintype.card α - 1)).to_string ++ "' inclusively>")) (parser.sat (λ (c : char), fromc ≤ c ∧ c.to_nat - fintype.card α < fromc.to_nat)) >>= λ (c : char), has_pure.pure (c.to_nat - fromc.to_nat).bin_cast

Instances for parser.numeral.char.of_fintype

@[protected, instance]

def parser.numeral.char.of_fintype.err_static (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] (fromc : char) :

(parser.numeral.char.of_fintype α fromc).err_static

@[protected, instance]

def parser.numeral.char.of_fintype.bounded (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] (fromc : char) :

(parser.numeral.char.of_fintype α fromc).bounded

Specific numeral types #

def parser.int :

Matches an integer, like 43 or -2. Large numbers may cause performance issues, so don't run this parser on untrusted input.

Equations

parser.int = (coe <$> parser.nat <|> parser.ch '-' >> has_neg.neg <$> coe <$> parser.nat)

def parser.rat :

Matches an rational number, like 43/1 or -2/3. Requires that the negation is in the numerator, and that both a numerator and denominator are provided (e.g. will not match 43). Large numbers may cause performance issues, so don't run this parser on untrusted input.

Equations

parser.rat = (λ (x : ℤ) (y : ℕ), ↑x / ↑y) <$> parser.int <*> (parser.ch '/' >> parser.nat)