Created
June 17, 2015 17:15
-
-
Save Taneb/f2021eab65ba59aa3693 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Nat where | |
newtype Nat = Nat [Nat] deriving (Show, Eq) | |
double :: Nat -> Nat | |
double (Nat []) = Nat [] | |
double (Nat (a : as)) = Nat (succ a : as) | |
half :: Nat -> Nat | |
half (Nat []) = Nat [] | |
half (Nat (Nat [] : as)) = Nat as | |
half (Nat (a : as)) = Nat (pred a : as) | |
instance Enum Nat where | |
succ (Nat []) = Nat [Nat []] | |
succ (Nat xs) = go (Nat []) xs | |
where | |
go n (Nat [] : as) = go (succ n) as | |
go n (a : as) = Nat (n : pred a : as) | |
go n [] = Nat [n] | |
pred (Nat []) = error "Nat: pred 0" | |
pred (Nat (Nat [] : b : bs)) = Nat (succ b : bs) | |
pred (Nat (n : ns)) = Nat . go n $ case ns of | |
[] -> [] | |
(b : bs) -> succ b : bs | |
where | |
go (Nat []) = id | |
go x = (:) (Nat []) . go (pred x) | |
fromEnum (Nat []) = 0 | |
fromEnum (Nat (a : as)) = 2^fromEnum a * (1 + 2 * fromEnum (Nat as)) | |
toEnum 0 = Nat [] | |
toEnum n = | |
let (a, Nat b) = go (Nat []) n | |
in Nat (a : b) | |
where | |
go i x | even x = go (succ i) (x `div` 2) | |
| otherwise = (i, toEnum $ x `div` 2) | |
instance Num Nat where | |
Nat [] + y = y | |
x + Nat [] = x | |
Nat (Nat [] : xs) + Nat (Nat [] : ys) = double . succ $ Nat xs + Nat ys | |
Nat (Nat [] : xs) + y = succ . double $ Nat xs + half y | |
x + Nat (Nat [] : ys) = succ . double $ half x + Nat ys | |
x + y = double $ half x + half y | |
Nat [] * _ = 0 -- 0 * y = 0 | |
_ * Nat [] = 0 -- x * 0 = 0 | |
Nat (Nat [] : x) * Nat (Nat [] : y) = succ (double (Nat x + Nat y + double (Nat x * Nat y))) -- (1 + 2x) * (1 + 2y) = 1 + 2(x + y + 2xy) | |
x@(Nat (Nat [] : _)) * y = double (x * half y) | |
x * y = double (half x * y) | |
x - Nat [] = x | |
Nat [] - _ = error "Negative Nat" | |
Nat (Nat [] : x) - Nat (Nat [] : y) = double (Nat x - Nat y) | |
Nat (Nat [] : x) - y = succ . double $ Nat x - half y | |
x - Nat (Nat [] : y) = pred . double $ half x - Nat y | |
x - y = double (half x - half y) | |
negate (Nat []) = Nat [] | |
negate _ = error "Negative Nat" | |
abs = id | |
signum (Nat []) = 0 | |
signum _ = 1 | |
fromInteger 0 = Nat [] | |
fromInteger n = | |
let (a, Nat b) = go (Nat []) n | |
in Nat (a : b) | |
where | |
go i x | even x = go (succ i) (x `div` 2) | |
| otherwise = (i, fromInteger $ x `div` 2) | |
instance Ord Nat where | |
Nat [] <= _ = True | |
_ <= Nat [] = False | |
Nat (Nat [] : x) <= Nat (Nat [] : y) = Nat x <= Nat y | |
Nat (Nat [] : x) <= y = Nat x < half y | |
x <= Nat (Nat [] : y) = half x < succ (Nat y) | |
x <= y = half x <= half y | |
instance Real Nat where | |
toRational = toRational . toInteger | |
normalize :: Nat -> (Nat, Nat) -> (Nat, Nat) | |
normalize d (q, r) | r >= d = (q + 1, r - d) | |
| otherwise = (q, r) | |
instance Integral Nat where | |
-- I HAVE NOT TESTED THIS!!! | |
_ `quotRem` Nat [] = error "Divide by zero" | |
Nat [] `quotRem` _ = (0, 0) | |
a `quotRem` Nat [Nat []] = (a, 0) | |
Nat [Nat []] `quotRem` _ = (0, 1) | |
a@(Nat (Nat [] : _)) `quotRem` b = let (q, r) = half a `quotRem` b | |
in normalize b (double q, succ $ double r) | |
a `quotRem` b@(Nat (Nat [] : _)) = let (q, r) = half a `quotRem` b | |
in normalize b (double q, double r) | |
x `quotRem` y = | |
let (q, r) = half x `quotRem` half y | |
in (q, double r) | |
divMod = quotRem | |
toInteger (Nat []) = 0 | |
toInteger (Nat (a : as)) = 2 ^ toInteger a * (1 + 2 * toInteger (Nat as)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment