← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/AIM6/Cat/lib/Data/Integer.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/outdated-and-incorrect/AIM6/Cat/lib/Data/Integer.agda
1
 
 
2
 
module Data.Integer where
3
 
 
4
 
import Prelude
5
 
import Data.Nat as Nat
6
 
import Data.Bool
7
 
 
8
 
open Nat using (Nat; suc; zero)
9
 
         renaming ( _+_  to _+'_
10
 
                  ; _*_  to _*'_
11
 
                  ; _<_  to _<'_
12
 
                  ; _-_  to _-'_
13
 
                  ; _==_ to _=='_
14
 
                  ; div  to div'
15
 
                  ; mod  to mod'
16
 
                  ; gcd  to gcd'
17
 
                  ; lcm  to lcm'
18
 
                  )
19
 
open Data.Bool
20
 
open Prelude
21
 
 
22
 
data Int : Set where
23
 
  pos : Nat -> Int
24
 
  neg : Nat -> Int  -- neg n = -(n + 1)
25
 
 
26
 
infix 40 _==_ _<_ _>_ _≤_ _≥_
27
 
infixl 60 _+_ _-_
28
 
infixl 70 _*_
29
 
infix  90 -_
30
 
 
31
 
-_ : Int -> Int
32
 
- pos zero    = pos zero
33
 
- pos (suc n) = neg n
34
 
- neg n       = pos (suc n)
35
 
 
36
 
_+_ : Int -> Int -> Int
37
 
pos n + pos m = pos (n +' m)
38
 
neg n + neg m = neg (n +' m +' 1)
39
 
pos n + neg m =
40
 
  ! m <' n => pos (n -' m -' 1)
41
 
  ! otherwise neg (m -' n)
42
 
neg n + pos m = pos m + neg n
43
 
 
44
 
_-_ : Int -> Int -> Int
45
 
x - y = x + - y
46
 
 
47
 
!_! : Int -> Nat
48
 
! pos n ! = n
49
 
! neg n ! = suc n
50
 
 
51
 
_*_ : Int -> Int -> Int
52
 
pos 0 * _     = pos 0
53
 
_     * pos 0 = pos 0
54
 
pos n * pos m = pos (n *' m)
55
 
neg n * neg m = pos (suc n *' suc m)
56
 
pos n * neg m = neg (n *' suc m -' 1)
57
 
neg n * pos m = neg (suc n *' m -' 1)
58
 
 
59
 
div : Int -> Int -> Int
60
 
div _             (pos 0)       = pos 0
61
 
div (pos n)       (pos m)       = pos (div' n m)
62
 
div (neg n)       (neg m)       = pos (div' (suc n) (suc m))
63
 
div (pos 0)       (neg _)       = pos 0
64
 
div (pos (suc n)) (neg m)       = neg (div' n (suc m))
65
 
div (neg n)       (pos (suc m)) = div (pos (suc n)) (neg m)
66
 
 
67
 
mod : Int -> Int -> Int
68
 
mod _ (pos 0)       = pos 0
69
 
mod (pos n) (pos m) = pos (mod' n m)
70
 
mod (neg n) (pos m) = adjust (mod' (suc n) m)
71
 
  where
72
 
    adjust : Nat -> Int
73
 
    adjust 0 = pos 0
74
 
    adjust n = pos (m -' n)
75
 
mod n (neg m)       = adjust (mod n (pos (suc m)))
76
 
  where
77
 
    adjust : Int -> Int
78
 
    adjust (pos 0) = pos 0
79
 
    adjust (neg n) = neg n  -- impossible
80
 
    adjust x       = x + neg m
81
 
 
82
 
gcd : Int -> Int -> Int
83
 
gcd a b = pos (gcd' ! a ! ! b !)
84
 
 
85
 
lcm : Int -> Int -> Int
86
 
lcm a b = pos (lcm' ! a ! ! b !)
87
 
 
88
 
_==_ : Int -> Int -> Bool
89
 
pos n == pos m = n ==' m
90
 
neg n == neg m = n ==' m
91
 
pos _ == neg _ = false
92
 
neg _ == pos _ = false
93
 
 
94
 
_<_ : Int -> Int -> Bool
95
 
pos _ < neg _ = false
96
 
neg _ < pos _ = true
97
 
pos n < pos m = n <' m
98
 
neg n < neg m = m <' n
99
 
 
100
 
_≤_ : Int -> Int -> Bool
101
 
x ≤ y = x == y || x < y
102
 
 
103
 
_≥_ = flip _≤_
104
 
_>_ = flip _<_
105