13
13
open import Relation.Nullary.Decidable
14
14
open import Data.Char using (Char)
15
15
open import Data.List
16
open import Data.Product
16
17
open import Data.Vec as Vec using (Vec; _∷_; [])
17
18
open import Induction.Nat
18
19
open import Data.Nat.DivMod
20
open import Relation.Binary.PropositionalEquality
21
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
21
22
open import Function
23
24
------------------------------------------------------------------------
94
95
-- This function should be linear in n, if optimised properly (see
95
96
-- Data.Nat.DivMod).
97
data Digits (base : ℕ) : ℕ → Set where
98
digits : (ds : List (Fin base)) → Digits base (fromDigits ds)
100
98
toDigits : (base : ℕ) {base≥2 : True (2 ≤? base)} (n : ℕ) →
99
∃ λ (ds : List (Fin base)) → fromDigits ds ≡ n
102
100
toDigits zero {base≥2 = ()} _
103
101
toDigits (suc zero) {base≥2 = ()} _
104
102
toDigits (suc (suc k)) n = <-rec Pred helper n
106
104
base = suc (suc k)
105
Pred = λ n → ∃ λ ds → fromDigits ds ≡ n
109
cons : ∀ {n} (r : Fin base) → Pred n → Pred (toℕ r + n * base)
110
cons r (digits ds) = digits (r ∷ ds)
107
cons : ∀ {m} (r : Fin base) → Pred m → Pred (toℕ r + m * base)
108
cons r (ds , eq) = (r ∷ ds , P.cong (λ i → toℕ r + i * base) eq)
112
110
helper : ∀ n → <-Rec Pred n → Pred n
113
helper n rec with n divMod base
114
helper .(toℕ r + 0 * base) rec | result zero r = digits (r ∷ [])
115
helper .(toℕ r + suc x * base) rec | result (suc x) r =
111
helper n rec with n divMod base
112
helper .(toℕ r + 0 * base) rec | result zero r refl = ([ r ] , refl)
113
helper .(toℕ r + suc x * base) rec | result (suc x) r refl =
116
114
cons r (rec (suc x) (lem (pred (suc x)) k (toℕ r)))
118
theDigits : (base : ℕ) {base≥2 : True (2 ≤? base)} (n : ℕ) →
120
theDigits base {base≥2} n with toDigits base {base≥2} n
121
theDigits base .(fromDigits ds) | digits ds = ds
added
removed
src/Data/Digit.agda
