← Back to branch summary

~ubuntu-branches/ubuntu/lucid/agda-stdlib/lucid

« back to all changes in this revision

Viewing changes to src/Data/Digit.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Digit.agda
 
1
------------------------------------------------------------------------
 
2
-- Digits and digit expansions
 
3
------------------------------------------------------------------------
 
4
 
 
5
module Data.Digit where
 
6
 
 
7
open import Data.Nat
 
8
open import Data.Nat.Properties
 
9
open SemiringSolver
 
10
open import Data.Fin as Fin using (Fin; zero; suc; toℕ)
 
11
open import Relation.Nullary.Decidable
 
12
open import Data.Char using (Char)
 
13
open import Data.List
 
14
open import Data.Vec as Vec using (Vec; _∷_; [])
 
15
open import Induction.Nat
 
16
open import Data.Nat.DivMod
 
17
open ≤-Reasoning
 
18
open import Relation.Binary.PropositionalEquality
 
19
open import Data.Function
 
20
 
 
21
------------------------------------------------------------------------
 
22
-- A boring lemma
 
23
 
 
24
private
 
25
 
 
26
  lem : ∀ x k r → 2 + x ≤′ r + (1 + x) * (2 + k)
 
27
  lem x k r = ≤⇒≤′ $ begin
 
28
    2 + x
 
29
      ≤⟨ m≤m+n _ _ ⟩
 
30
    2 + x + (x + (1 + x) * k + r)
 
31
      ≡⟨ solve 3 (λ x r k → con 2 :+ x :+ (x :+ (con 1 :+ x) :* k :+ r)
 
32
                              :=
 
33
                            r :+ (con 1 :+ x) :* (con 2 :+ k))
 
34
                 refl x r k ⟩
 
35
    r + (1 + x) * (2 + k)
 
36
      ∎
 
37
 
 
38
------------------------------------------------------------------------
 
39
-- Digits
 
40
 
 
41
-- Digit b is the type of digits in base b.
 
42
 
 
43
Digit : ℕ → Set
 
44
Digit b = Fin b
 
45
 
 
46
-- Some specific digit kinds.
 
47
 
 
48
Decimal = Digit 10
 
49
Bit     = Digit 2
 
50
 
 
51
-- Some named digits.
 
52
 
 
53
0b : Bit
 
54
0b = zero
 
55
 
 
56
1b : Bit
 
57
1b = suc zero
 
58
 
 
59
------------------------------------------------------------------------
 
60
-- Showing digits
 
61
 
 
62
-- The characters used to show the first 16 digits.
 
63
 
 
64
digitChars : Vec Char 16
 
65
digitChars =
 
66
  '0' ∷ '1' ∷ '2' ∷ '3' ∷ '4' ∷ '5' ∷ '6' ∷ '7' ∷ '8' ∷ '9' ∷
 
67
  'a' ∷ 'b' ∷ 'c' ∷ 'd' ∷ 'e' ∷ 'f' ∷ []
 
68
 
 
69
-- showDigit shows digits in base ≤ 16.
 
70
 
 
71
showDigit : ∀ {base} {base≤16 : True (base ≤? 16)} →
 
72
            Digit base → Char
 
73
showDigit {base≤16 = base≤16} d =
 
74
  Vec.lookup (Fin.inject≤ d (toWitness base≤16)) digitChars
 
75
 
 
76
------------------------------------------------------------------------
 
77
-- Digit expansions
 
78
 
 
79
-- fromDigits takes a digit expansion of a natural number, starting
 
80
-- with the _least_ significant digit, and returns the corresponding
 
81
-- natural number.
 
82
 
 
83
fromDigits : ∀ {base} → List (Fin base) → ℕ
 
84
fromDigits        []       = 0
 
85
fromDigits {base} (d ∷ ds) = toℕ d + fromDigits ds * base
 
86
 
 
87
-- toDigits b n yields the digits of n, in base b, starting with the
 
88
-- _least_ significant digit.
 
89
--
 
90
-- Note that the list of digits is always non-empty.
 
91
--
 
92
-- This function should be linear in n, if optimised properly (see
 
93
-- Data.Nat.DivMod).
 
94
 
 
95
data Digits (base : ℕ) : ℕ → Set where
 
96
  digits : (ds : List (Fin base)) → Digits base (fromDigits ds)
 
97
 
 
98
toDigits : (base : ℕ) {base≥2 : True (2 ≤? base)} (n : ℕ) →
 
99
           Digits base n
 
100
toDigits zero       {base≥2 = ()} _
 
101
toDigits (suc zero) {base≥2 = ()} _
 
102
toDigits (suc (suc k)) n = <-rec Pred helper n
 
103
  where
 
104
  base = suc (suc k)
 
105
  Pred = Digits base
 
106
 
 
107
  cons : ∀ {n} (r : Fin base) → Pred n → Pred (toℕ r + n * base)
 
108
  cons r (digits ds) = digits (r ∷ ds)
 
109
 
 
110
  helper : ∀ n → <-Rec Pred n → Pred n
 
111
  helper n rec with n divMod base
 
112
  helper .(toℕ r + 0     * base) rec | result zero    r = digits (r ∷ [])
 
113
  helper .(toℕ r + suc x * base) rec | result (suc x) r =
 
114
    cons r (rec (suc x) (lem (pred (suc x)) k (toℕ r)))
 
115
 
 
116
theDigits : (base : ℕ) {base≥2 : True (2 ≤? base)} (n : ℕ) →
 
117
            List (Fin base)
 
118
theDigits base {base≥2} n       with toDigits base {base≥2} n
 
119
theDigits base .(fromDigits ds) | digits ds = ds