shttpd/doc/parsers/numeric-bases.rst

.. SPDX-License-Identifier: GPL-2.0 or GPL-3.0
.. Copyright © 2019 Ariadne Devos

Parsing base-N numbers
======================

For now, only ASCII decimal is supported,
Some logical constructs are defined here,
see <sHT/lex/nat.h> for the C API.

decimal := [0-9]

The set of ASCII decimal digits

decimal->nat (c : decimal) : { k : nat | 0 ≤ k < 10 } := c - ascii->nat '0'

Convert an ASCII decimal digit into its numeric value.
(In ASCII, '0', '1' .. '9' are contiguous, mapping to 0 .. 9)

string->nat (length : nat) (d : { k : nat | 0 ≤ k < length } → { k : nat | 0 ≤ k < 10 }) → nat := sum (k <- 0 \to length) (d(k) * exp(10, length - k - 1))

Convert a decimal ASCII string `d` into its numeric value,
leading zeroes are allowed

Theorem digit_minus_zero_k (k : { k : ℕ | 0 ⩽ k ⩽ 9 }) (a : uint8_t) : a - '0' ⩽ k ↔ '0' ⩽ a ⩽ '0' + k
Proof.
⇔ 0 ⩽ a - '0' ⩽ k ↔ '0' ⩽ a ⩽ '0' + k
⇔ (retype a : ℕ) 0 ⩽ wrap(uint8_t, a - '0') ⩽ k ↔ '0' ⩽ a ⩽ '0' + k
⇔ 0 + '0' ⩽ wrap(uint8_t, a - '0') + '0' ⩽ k + '0' ↔ '0' ⩽ a ⩽ '0' + k
⇔ 0 + '0' ⩽ wrap(uint8_t, a - '0' + '0') + '0' ⩽ k + '0' ↔ '0' ⩽ a ⩽ '0' + k
⇔ '0' ⩽ wrap(uint8_t, a) ⩽ '0' + k ↔ '0' ⩽ a ⩽ '0' + k (eval, reorder)
⇔ '0' ⩽ a ⩽ '0' + k ↔ '0' ⩽ a ⩽ '0' + k
⇔ ⊤
Qed.

Theorem digit_minus_zero (a : uint8_t) := digit_minus_zero_k 9.