Parsers #
parser α
is the type that describes a computation that can ingest a char_buffer
and output, if successful, a term of type α
.
This file expands on the definitions in the core library, proving that all the core library
parsers are mono
. There are also lemmas on the composability of parsers.
Main definitions #
parse_result.pos
: The position of achar_buffer
at which aparser α
has finished.parser.mono
: The property that a parser only moves forward within a buffer, in both cases of success or failure.
Implementation details #
Lemmas about how parsers are mono are in the mono
namespace. That allows using projection
notation for shorter term proofs that are parallel to the definitions of the parsers in structure.
For some parse_result α
, give the position at which the result was provided, in either the
done
or the fail
case.
Equations
- (parse_result.fail n _x).pos = n
- (parse_result.done n _x).pos = n
- le' : ∀ (cb : char_buffer) (n : ℕ), n ≤ (p cb n).pos
A p : parser α
is defined to be mono
if the result p cb n
it gives,
for some cb : char_buffer
and n : ℕ
, (whether done
or fail
),
is always at a parse_result.pos
that is at least n
.
The mono
property is used mainly for proper orelse
behavior.
Instances of this typeclass
- parser.mono.pure
- parser.mono.bind
- parser.mono.and_then
- parser.mono.map
- parser.mono.seq
- parser.mono.mmap
- parser.mono.mmap'
- parser.mono.failure
- parser.mono.guard
- parser.mono.orelse
- parser.mono.decorate_errors
- parser.mono.decorate_error
- parser.mono.any_char
- parser.mono.sat
- parser.mono.eps
- parser.mono.ch
- parser.mono.char_buf
- parser.mono.one_of
- parser.mono.one_of'
- parser.mono.str
- parser.mono.remaining
- parser.mono.eof
- parser.mono.foldr_core
- parser.mono.foldr
- parser.mono.foldl_core
- parser.mono.foldl
- parser.mono.many
- parser.mono.many_char
- parser.mono.many'
- parser.mono.many1
- parser.mono.many_char1
- parser.mono.sep_by1
- parser.mono.sep_by
- parser.mono.digit
- parser.mono.nat
- parser.numeral.mono
- parser.numeral.of_fintype.mono
- parser.numeral.from_one.mono
- parser.numeral.from_one.of_fintype.mono
- parser.numeral.char.mono
- parser.numeral.char.of_fintype.mono
- of_done : ∀ {cb : char_buffer} {n n' : ℕ} {a : α}, p cb n = parse_result.done n' a → n = n'
A parser α
is defined to be static
if it does not move on success.
Instances of this typeclass
- parser.static.pure
- parser.static.bind
- parser.static.and_then
- parser.static.map
- parser.static.seq
- parser.static.mmap
- parser.static.mmap'
- parser.static.failure
- parser.static.guard
- parser.static.orelse
- parser.static.decorate_errors
- parser.static.decorate_error
- parser.static.sat
- parser.static.eps
- parser.static.one_of
- parser.static.one_of'
- parser.static.remaining
- parser.static.eof
- parser.static.foldr_core
- parser.static.foldr
- parser.static.foldl_core
- parser.static.foldl
- parser.static.many
- parser.static.many_char
- parser.static.many'
- parser.static.many1
- parser.static.many_char1
- parser.static.sep_by1
- parser.static.sep_by
- of_fail : ∀ {cb : char_buffer} {n n' : ℕ} {err : dlist string}, p cb n = parse_result.fail n' err → n = n'
A parser α
is defined to be err_static
if it does not move on error.
Instances of this typeclass
- parser.err_static.pure
- parser.err_static.bind
- parser.err_static.bind_of_unfailing
- parser.err_static.and_then
- parser.err_static.and_then_of_unfailing
- parser.err_static.map
- parser.err_static.seq
- parser.err_static.seq_of_unfailing
- parser.err_static.mmap
- parser.err_static.mmap_of_unfailing
- parser.err_static.mmap'
- parser.err_static.mmap'_of_unfailing
- parser.err_static.failure
- parser.err_static.guard
- parser.err_static.orelse
- parser.err_static.decorate_errors
- parser.err_static.decorate_error
- parser.err_static.any_char
- parser.err_static.sat_iff
- parser.err_static.eps
- parser.err_static.ch
- parser.err_static.char_buf
- parser.err_static.one_of
- parser.err_static.one_of'
- parser.err_static.str
- parser.err_static.remaining
- parser.err_static.eof
- parser.err_static.digit
- parser.err_static.nat
- parser.numeral.char.err_static
- parser.numeral.char.of_fintype.err_static
- of_done : ∀ {cb : char_buffer} {n n' : ℕ} {a : α}, p cb n = parse_result.done n' a → n' = n + 1
A parser α
is defined to be step
if it always moves exactly one char forward on success.
Instances of this typeclass
- parser.step.bind
- parser.step.bind'
- parser.step.and_then
- parser.step.and_then'
- parser.step.map
- parser.step.seq
- parser.step.seq'
- parser.step.mmap
- parser.step.mmap'
- parser.step.failure
- parser.step.guard
- parser.step.orelse
- parser.step.decorate_errors
- parser.step.decorate_error
- parser.step.any_char
- parser.step.sat
- parser.step.ch
- parser.step.one_of
- parser.step.one_of'
- parser.step.digit
- parser.numeral.char.step
- parser.numeral.char.of_fintype.step
- of_done : ∀ {cb : char_buffer} {n n' : ℕ} {a : α}, p cb n = parse_result.done n' a → n < n'
A parser α
is defined to be prog
if it always moves forward on success.
Instances of this typeclass
- parser.prog.of_step
- parser.prog.bind
- parser.prog.and_then
- parser.prog.map
- parser.prog.seq
- parser.prog.mmap
- parser.prog.mmap'
- parser.prog.failure
- parser.prog.guard
- parser.prog.orelse
- parser.prog.decorate_errors
- parser.prog.decorate_error
- parser.prog.any_char
- parser.prog.sat
- parser.prog.ch
- parser.prog.one_of
- parser.prog.one_of'
- parser.prog.many1
- parser.prog.digit
- parser.prog.nat
- parser.numeral.prog
- parser.numeral.of_fintype.prog
- parser.numeral.from_one.prog
- parser.numeral.from_one.of_fintype.prog
- ex' : ∀ {cb : char_buffer} {n : ℕ}, buffer.size cb ≤ n → (∃ (n' : ℕ) (err : dlist string), p cb n = parse_result.fail n' err)
A parser a
is defined to be bounded
if it produces a
fail
parse_result
when it is parsing outside the provided char_buffer
.
Instances of this typeclass
- parser.bounded.bind
- parser.bounded.and_then
- parser.bounded.map
- parser.bounded.seq
- parser.bounded.mmap
- parser.bounded.mmap'
- parser.bounded.failure
- parser.bounded.orelse
- parser.bounded.decorate_errors
- parser.bounded.decorate_error
- parser.bounded.any_char
- parser.bounded.sat
- parser.bounded.ch
- parser.bounded.one_of
- parser.bounded.one_of'
- parser.bounded.foldr_core_zero
- parser.bounded.foldl_core_zero
- parser.bounded.many1
- parser.bounded.many_char1
- parser.bounded.sep_by1
- parser.bounded.digit
- parser.bounded.nat
- parser.numeral.bounded
- parser.numeral.of_fintype.bounded
- parser.numeral.from_one.bounded
- parser.numeral.from_one.of_fintype.bounded
- parser.numeral.char.bounded
- parser.numeral.char.of_fintype.bounded
- ex' : ∀ (cb : char_buffer) (n : ℕ), ∃ (n' : ℕ) (a : α), p cb n = parse_result.done n' a
A parser a
is defined to be unfailing
if it always produces a done
parse_result
.
Instances of this typeclass
- parser.unfailing.pure
- parser.unfailing.bind
- parser.unfailing.and_then
- parser.unfailing.map
- parser.unfailing.seq
- parser.unfailing.mmap
- parser.unfailing.mmap'
- parser.unfailing.guard_true
- parser.unfailing.orelse
- parser.unfailing.decorate_errors
- parser.unfailing.decorate_error
- parser.unfailing.eps
- parser.unfailing.remaining
- parser.unfailing.foldr_core_of_static
- parser.unfailing.foldr_core_one_of_err_static
- ex' : ∀ {cb : char_buffer} {n : ℕ}, n < buffer.size cb → (∃ (n' : ℕ) (a : α), p cb n = parse_result.done n' a)
A parser a
is defined to be conditionally_unfailing
if it produces a
done
parse_result
as long as it is parsing within the provided char_buffer
.
Instances of this typeclass
The val : ℕ
produced by a successful parse of a cb : char_buffer
is the numerical value
represented by the string of decimal digits (possibly padded with 0s on the left)
starting from the parsing position n
and ending at position n'
. The number
of characters parsed in is necessarily n' - n
.
This is one of the directions of nat_eq_done
.
If we know that parser.nat
was successful, starting at position n
and ending at position n'
,
then it must be the case that for all k : ℕ
, n ≤ k
, k < n'
, the character at the k
th
position in cb : char_buffer
is "numeric", that is, is between '0'
and '9'
inclusive.
This is a necessary part of proving one of the directions of nat_eq_done
.
If we know that parser.nat
was successful, starting at position n
and ending at position n'
,
then it must be the case that for the ending position n'
, either it is beyond the end of the
cb : char_buffer
, or the character at that position is not "numeric", that is, between '0'
and
'9'
inclusive.
This is a necessary part of proving one of the directions of nat_eq_done
.
The val : ℕ
produced by a successful parse of a cb : char_buffer
is the numerical value
represented by the string of decimal digits (possibly padded with 0s on the left)
starting from the parsing position n
and ending at position n'
, where n < n'
. The number
of characters parsed in is necessarily n' - n
. Additionally, all of the characters in the cb
starting at position n
(inclusive) up to position n'
(exclusive) are "numeric", in that they
are between '0'
and '9'
inclusive. Such a char_buffer
would produce the ℕ
value encoded
by its decimal characters.