------------------------------------------------------------------------ -- The Agda standard library -- -- Digits and digit expansions ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.Digit where open import Data.Nat.Base open import Data.Nat.Properties open import Data.Nat.Solver open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ) open import Data.Bool.Base using (Bool; true; false) open import Data.Char using (Char) open import Data.List.Base open import Data.Product open import Data.Vec.Base as Vec using (Vec; _∷_; []) open import Data.Nat.DivMod open import Data.Nat.Induction open import Relation.Nullary using (does) open import Relation.Nullary.Decidable open import Relation.Binary using (Decidable) open import Relation.Binary.PropositionalEquality as P using (_≡_; refl) open import Function ------------------------------------------------------------------------ -- Digits -- Digit b is the type of digits in base b. Digit : ℕ → Set Digit b = Fin b -- Some specific digit kinds. Decimal = Digit 10 Bit = Digit 2 -- Some named digits. 0b : Bit 0b = zero 1b : Bit 1b = suc zero ------------------------------------------------------------------------ -- Converting between `ℕ` and `expansions of ℕ` toNatDigits : (base : ℕ) {base≤16 : True (1 ≤? base)} → ℕ → List ℕ toNatDigits base@(suc zero) n = replicate n 1 toNatDigits base@(suc (suc b)) n = aux (<-wellFounded-fast n) [] where aux : {n : ℕ} → Acc _<_ n → List ℕ → List ℕ aux {zero} _ xs = (0 ∷ xs) aux {n@(suc _)} (acc wf) xs with does (0 <? n / base) ... | false = (n % base) ∷ xs ... | true = aux (wf (n / base) q<n) ((n % base) ∷ xs) where q<n : n / base < n q<n = m/n<m n base (s≤s (s≤s z≤n)) ------------------------------------------------------------------------ -- Converting between `ℕ` and expansions of `Digit base` Expansion : ℕ → Set Expansion base = List (Digit base) -- fromDigits takes a digit expansion of a natural number, starting -- with the _least_ significant digit, and returns the corresponding -- natural number. fromDigits : ∀ {base} → Expansion base → ℕ fromDigits [] = 0 fromDigits {base} (d ∷ ds) = toℕ d + fromDigits ds * base -- toDigits b n yields the digits of n, in base b, starting with the -- _least_ significant digit. -- -- Note that the list of digits is always non-empty. toDigits : (base : ℕ) {base≥2 : True (2 ≤? base)} (n : ℕ) → ∃ λ (ds : Expansion base) → fromDigits ds ≡ n toDigits (suc (suc k)) n = <′-rec Pred helper n where base = suc (suc k) Pred = λ n → ∃ λ ds → fromDigits ds ≡ n cons : ∀ {m} (r : Digit base) → Pred m → Pred (toℕ r + m * base) cons r (ds , eq) = (r ∷ ds , P.cong (λ i → toℕ r + i * base) eq) open ≤-Reasoning open +-*-Solver lem : ∀ x k r → 2 + x ≤′ r + (1 + x) * (2 + k) lem x k r = ≤⇒≤′ $ begin 2 + x ≤⟨ m≤m+n _ _ ⟩ 2 + x + (x + (1 + x) * k + r) ≡⟨ solve 3 (λ x r k → con 2 :+ x :+ (x :+ (con 1 :+ x) :* k :+ r) := r :+ (con 1 :+ x) :* (con 2 :+ k)) refl x r k ⟩ r + (1 + x) * (2 + k) ∎ helper : ∀ n → <′-Rec Pred n → Pred n helper n rec with n divMod base helper .(toℕ r + 0 * base) rec | result zero r refl = ([ r ] , refl) helper .(toℕ r + suc x * base) rec | result (suc x) r refl = cons r (rec (suc x) (lem (pred (suc x)) k (toℕ r))) ------------------------------------------------------------------------ -- Showing digits -- The characters used to show the first 16 digits. digitChars : Vec Char 16 digitChars = '0' ∷ '1' ∷ '2' ∷ '3' ∷ '4' ∷ '5' ∷ '6' ∷ '7' ∷ '8' ∷ '9' ∷ 'a' ∷ 'b' ∷ 'c' ∷ 'd' ∷ 'e' ∷ 'f' ∷ [] -- showDigit shows digits in base ≤ 16. showDigit : ∀ {base} {base≤16 : True (base ≤? 16)} → Digit base → Char showDigit {base≤16 = base≤16} d = Vec.lookup digitChars (Fin.inject≤ d (toWitness base≤16))