← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/arith/DivMod.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/arith/DivMod.agda
1
 
 
2
 
module DivMod where
3
 
 
4
 
open import Lib.Vec
5
 
open import Lib.Nat
6
 
open import Lib.Id
7
 
open import Lib.Logic
8
 
open import Lib.Fin
9
 
 
10
 
module Direct where
11
 
 
12
 
  data DivMod : Nat -> Nat -> Set where
13
 
    dm : forall {b} q (r : Fin b) -> DivMod (toNat r + q * b) b
14
 
 
15
 
  getQ : forall {a b} -> DivMod a b -> Nat
16
 
  getQ (dm q _) = q
17
 
 
18
 
  getR : forall {a b} -> DivMod a b -> Nat
19
 
  getR (dm _ r) = toNat r
20
 
 
21
 
  divModˢ : (a b : Nat) -> DivMod a (suc b)
22
 
  divModˢ zero    b = dm 0 zero
23
 
  divModˢ (suc a) b with divModˢ a b
24
 
  divModˢ (suc ._) b | dm q r with maxView r 
25
 
  divModˢ (suc ._) b | dm q .(fromNat b) | theMax
26
 
    with toNat (fromNat b) | lem-toNat-fromNat b
27
 
  ...  | .b | refl = dm {suc b} (suc q) zero
28
 
  divModˢ (suc ._) b | dm q .(weaken i)  | notMax i
29
 
    with toNat (weaken i) | lem-toNat-weaken i
30
 
  ...  | .(toNat i) | refl = dm q (suc i) 
31
 
 
32
 
  divMod : (a b : Nat){nz : NonZero b} -> DivMod a b
33
 
  divMod a zero {}
34
 
  divMod a (suc b) = divModˢ a b
35
 
 
36
 
module Inductive where
37
 
 
38
 
  data DivMod : Nat -> Nat -> Set where
39
 
    dmZ : forall {b} (i : Fin b) -> DivMod (toNat i) b
40
 
    dmS : forall {a b} -> DivMod a b -> DivMod (b + a) b
41
 
 
42
 
  getQ : forall {a b} -> DivMod a b -> Nat
43
 
  getQ (dmZ _) = 0
44
 
  getQ (dmS d) = suc (getQ d)
45
 
 
46
 
  getR : forall {a b} -> DivMod a b -> Nat
47
 
  getR (dmZ r) = toNat r
48
 
  getR (dmS d) = getR d
49
 
 
50
 
  data BoundView (n : Nat) : Nat -> Set where
51
 
    below : (i : Fin n) -> BoundView n (toNat i)
52
 
    above : forall a    -> BoundView n (n + a)
53
 
 
54
 
  boundView : (a b : Nat) -> BoundView a b
55
 
  boundView zero b = above b
56
 
  boundView (suc a) zero    = below zero
57
 
  boundView (suc a) (suc b) with boundView a b
58
 
  boundView (suc a) (suc .(toNat i)) | below i = below (suc i)
59
 
  boundView (suc a) (suc .(a + k))   | above k = above k
60
 
 
61
 
  data _≤_ : Nat -> Nat -> Set where
62
 
    leqZ : forall {n}            -> zero  ≤ n
63
 
    leqS : forall {n m} -> n ≤ m -> suc n ≤ suc m
64
 
 
65
 
  ≤-suc : forall {a b} -> a ≤ b -> a ≤ suc b
66
 
  ≤-suc leqZ     = leqZ
67
 
  ≤-suc (leqS p) = leqS (≤-suc p)
68
 
 
69
 
  plus-≤ : forall a {b c} -> a + b ≤ c -> b ≤ c
70
 
  plus-≤ zero    p        = p
71
 
  plus-≤ (suc a) (leqS p) = ≤-suc (plus-≤ a p)
72
 
 
73
 
  ≤-refl : forall {a} -> a ≤ a
74
 
  ≤-refl {zero} = leqZ
75
 
  ≤-refl {suc n} = leqS ≤-refl
76
 
 
77
 
  -- Recursion over a bound on a (needed for termination).
78
 
  divModˢ : forall {size} a b -> a ≤ size -> DivMod a (suc b)
79
 
  divModˢ a b prf with boundView (suc b) a
80
 
  divModˢ .(toNat r)   b _          | below r = dmZ r
81
 
  divModˢ .(suc b + k) b (leqS prf) | above k = dmS (divModˢ k b (plus-≤ b prf))
82
 
 
83
 
  divMod : forall a b {nz : NonZero b} -> DivMod a b
84
 
  divMod a zero {}
85
 
  divMod a (suc b) = divModˢ a b ≤-refl
86
 
 
87
 
  -- We ought to prove that the inductive version behaves the same as the
88
 
  -- direct version... but that's more work than we're willing to spend.
89
 
 
90
 
open Inductive
91
 
 
92
 
_div_ : (a b : Nat){nz : NonZero b} -> Nat
93
 
_div_ a b {nz} = getQ (divMod a b {nz})
94
 
 
95
 
_mod_ : (a b : Nat){nz : NonZero b} -> Nat
96
 
_mod_ a b {nz} = getR (divMod a b {nz})
97
 
 
98