← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda-stdlib/wily

« back to all changes in this revision

Viewing changes to src/Data/Nat/DivMod.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-05-27 19:29:25 UTC
  • mfrom: (8.1.1 experimental)
  • Revision ID: package-import@ubuntu.com-20130527192925-q2tadfousmn0xeav
Tags: 0.7-2
Upload to unstable 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Nat/DivMod.agda
56
56
 
57
57
-- A specification of integer division.
58
58
 
59
 
data DivMod : ℕ → ℕ → Set where
60
 
  result : {divisor : ℕ} (q : ℕ) (r : Fin divisor) →
61
 
           DivMod (toℕ r + q * divisor) divisor
62
 
 
63
 
 
64
 
data DivMod' (dividend divisor : ℕ) : Set where
65
 
  result : (q : ℕ) (r : Fin divisor)
66
 
           (eq : dividend ≡ toℕ r + q * divisor) →
67
 
           DivMod' dividend divisor
 
59
record DivMod (dividend divisor : ℕ) : Set where
 
60
  constructor result
 
61
  field
 
62
    quotient  : ℕ
 
63
    remainder : Fin divisor
 
64
    property  : dividend ≡ toℕ remainder + quotient * divisor
68
65
 
69
66
-- Integer division with remainder.
70
67
 
77
72
-- properly (see "Inductive Families Need Not Store Their Indices"
78
73
-- (Brady, McBride, McKinna, TYPES 2003)).
79
74
 
80
 
_divMod'_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
81
 
            DivMod' dividend divisor
82
 
_divMod'_ m n {≢0} = <-rec Pred dm m n {≢0}
 
75
_divMod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
 
76
           DivMod dividend divisor
 
77
_divMod_ m n {≢0} = <-rec Pred dm m n {≢0}
83
78
  where
84
79
  Pred : ℕ → Set
85
80
  Pred dividend = (divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
86
 
                  DivMod' dividend divisor
 
81
                  DivMod dividend divisor
87
82
 
88
 
  1+_ : ∀ {k n} → DivMod' (suc k) n → DivMod' (suc n + k) n
 
83
  1+_ : ∀ {k n} → DivMod (suc k) n → DivMod (suc n + k) n
89
84
  1+_ {k} {n} (result q r eq) = result (1 + q) r (lem₃ n k q r eq)
90
85
 
91
86
  dm : (dividend : ℕ) → <-Rec Pred dividend → Pred dividend
99
94
    1+ rec (suc k) le (suc n)
100
95
    where le = s≤′s (s≤′s (n≤′m+n n k))
101
96
 
102
 
 
103
 
_divMod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
104
 
           DivMod dividend divisor
105
 
_divMod_ m n {≢0} with _divMod'_ m n {≢0}
106
 
.(toℕ r + q * n) divMod n | result q r refl = result q r
107
 
 
108
97
-- Integer division.
109
98
 
110
99
_div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ
111
 
_div_ m n {≢0} with _divMod_ m n {≢0}
112
 
.(toℕ r + q * n) div n | result q r = q
 
100
_div_ m n {≢0} = DivMod.quotient $ _divMod_ m n {≢0}
113
101
 
114
102
-- The remainder after integer division.
115
103
 
116
104
_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor
117
 
_mod_ m n {≢0} with _divMod_ m n {≢0}
118
 
.(toℕ r + q * n) mod n | result q r = r
 
105
_mod_ m n {≢0} = DivMod.remainder $ _divMod_ m n {≢0}