blob: 742bba27ccec86129e62dd1d905b282fd991cf66 (
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
47
48
49
50
51
52
53
54
55
|
-- Unary and binary natural numbers, and conversions between them. AR 8/10/2003
-- To be used as an example of transfer.
abstract Nat = Numerals ** {
cat Nat ;
fun
One : Nat ; -- 1
Succ : Nat -> Nat ; -- n'
data Nat = One | Succ ;
cat Bin ;
fun
BOne : Bin ; -- 1
BX : Bin -> Bin ; -- b 0
BXPlus : Bin -> Bin ; -- b 1
data Bin = BOne | BX | BXPlus ;
fun succ : Bin -> Bin ;
def
succ BOne = BX BOne ;
succ (BX b) = BXPlus b ;
succ (BXPlus BOne) = BX (BX BOne) ;
succ b = succAux b (lastZero b) ;
fun lastZero : Bin -> Nat ;
def
lastZero (BX _) = One ;
lastZero (BXPlus b) = Succ (lastZero b) ;
fun succAux : Bin -> Nat -> Bin ;
def
succAux (BXPlus b) One = BX (succ b) ;
succAux (BXPlus b) (Succ n) = BX (succAux b n) ;
succAux b _ = succ b ;
-- this is the transfer function
fun nat2bin : Nat -> Bin ;
def
nat2bin One = BOne ;
nat2bin (Succ n) = succ (nat2bin n) ;
-- and the other way round
fun bin2nat : Bin -> Nat ;
def
bin2nat BOne = One ;
bin2nat (BX b) = double (bin2nat b) ;
bin2nat (BXPlus b) = Succ (double (bin2nat b)) ;
fun double : Nat -> Nat ;
def
double One = Succ One ;
double (Succ n) = Succ (Succ (double n)) ;
}
|
