blob: 73bc406bacb1770798a31d770bc6ce280f2f3a3a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
module Nat where
-- testing transfer from unary to binary, for Nat.gf. AR 8/10/2003
data Nat = One | Succ Nat deriving Show
data Bin = BOne | BX Bin | BXPlus Bin deriving Show
succBin:: Bin -> Bin
succBin BOne = BX BOne
succBin (BX b) = BXPlus b
succBin (BXPlus BOne) = BX (BX BOne)
succBin b = succAux b (lastZero b)
lastZero :: Bin -> Nat
lastZero (BX _) = One
lastZero (BXPlus b) = Succ (lastZero b)
succAux :: Bin -> Nat -> Bin
succAux (BXPlus b) One = BX (succBin b)
succAux (BXPlus b) (Succ n) = BX (succAux b n)
succAux b _ = succBin b
int2bin :: Int -> Bin
int2bin 1 = BOne
int2bin n = succBin (int2bin (n-1))
bin2nat :: Bin -> Nat
bin2nat BOne = One
bin2nat (BX b) = double (bin2nat b)
bin2nat (BXPlus b) = Succ (double (bin2nat b))
double :: Nat -> Nat
double One = Succ One
double (Succ n) = Succ (Succ (double n))
-- to test
prBin :: Bin -> String
prBin BOne = "1"
prBin (BX b) = prBin b ++ "0"
prBin (BXPlus b) = prBin b ++ "1"
test = map (prBin . int2bin) [1..16]
test2 = map (bin2nat . int2bin) [1..16]
|
