@@ -0,0 +1,141 @@
1+module main
2+
3+import parity
4+import system
5+
6+data Bit : Nat -> Set where
7+ b0 : Bit 0
8+ b1 : Bit 1
9+
10+instance Show (Bit n) where
11+ show b0 = "0"
12+ show b1 = "1"
13+
14+infixl 5 #
15+
16+data Binary : (width : Nat) -> (value : Nat) -> Set where
17+ zero : Binary O O
18+ (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
19+
20+instance Show (Binary w k) where
21+ show zero = ""
22+ show (bin # bit) = show bin ++ show bit
23+
24+pad : Binary w n -> Binary (S w) n
25+pad zero = zero # b0
26+pad (num # x) = pad num # x
27+
28+natToBin : (width : Nat) -> (n : Nat) ->
29+ Maybe (Binary width n)
30+natToBin O (S k) = Nothing
31+natToBin O O = Just zero
32+natToBin (S k) O = do x <- natToBin k O
33+ Just (pad x)
34+natToBin (S w) (S k) with (parity k)
35+ natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j
36+ let value = jbin # b1
37+ ?ntbEven
38+ natToBin (S w) (S (S (plus j j))) | odd = do jbin <- natToBin w (S j)
39+ let value = jbin # b0
40+ ?ntbOdd
41+
42+testBin : Maybe (Binary 8 42)
43+testBin = natToBin _ _
44+
45+pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
46+term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))
47+
48+addBit : Bit x -> Bit y -> Bit c ->
49+ (bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))
50+addBit b0 b0 b0 = bitpair b0 b0
51+addBit b0 b0 b1 = bitpair b0 b1
52+addBit b0 b1 b0 = bitpair b0 b1
53+addBit b0 b1 b1 = bitpair b1 b0
54+addBit b1 b0 b0 = bitpair b0 b1
55+addBit b1 b0 b1 = bitpair b1 b0
56+addBit b1 b1 b0 = bitpair b1 b0
57+addBit b1 b1 b1 = bitpair b1 b1
58+
59+adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)
60+adc zero zero carry ?= zero # carry
61+adc (numx # bx) (numy # by) carry
62+ ?= let (bitpair carry0 lsb) = addBit bx by carry in
63+ adc numx numy carry0 # lsb
64+
65+readNum : IO Nat
66+readNum = do putStr "Enter a number:"
67+ i <- getLine
68+ let n : Int = cast i
69+ return (fromInteger n)
70+
71+main : IO ()
72+main = do let Just bin1 = natToBin 8 42
73+ print bin1
74+ let Just bin2 = natToBin 8 89
75+ print bin2
76+ print (adc bin1 bin2 b0)
77+
78+
79+
80+
81+
82+
83+
84+---------- Proofs ----------
85+
86+main.ntbOdd = proof {
87+ intro w,j;
88+ rewrite sym (plusZeroRightNeutral j);
89+ rewrite plusSuccRightSucc j j;
90+ intros;
91+ refine Just;
92+ trivial;
93+}
94+
95+main.ntbEven = proof {
96+ compute;
97+ intro w,j;
98+ rewrite sym (plusZeroRightNeutral j);
99+ intros;
100+ refine Just;
101+ trivial;
102+}
103+
104+-- There is almost certainly an easier proof. I don't care, for now :)
105+
106+main.adc_lemma_2 = proof {
107+ intro c,w,v,bit0,num0;
108+ intro b0,v1,bit1,num1,b1;
109+ intro bc,x,x1,bx,bx1;
110+ rewrite sym (plusZeroRightNeutral x);
111+ rewrite sym (plusZeroRightNeutral v1);
112+ rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));
113+ rewrite sym (plusZeroRightNeutral v);
114+ intros;
115+ rewrite sym (plusAssociative (plus c (plus bit0 (plus v v))) bit1 (plus v1 v1));
116+ rewrite (plusAssociative c (plus bit0 (plus v v)) bit1);
117+ rewrite (plusAssociative bit0 (plus v v) bit1);
118+ rewrite plusCommutative bit1 (plus v v);
119+ rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));
120+ rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));
121+ rewrite sym b;
122+ rewrite plusAssociative x1 (plus x x) (plus v v);
123+ rewrite plusAssociative x x (plus v v);
124+ rewrite sym (plusAssociative x v v);
125+ rewrite plusCommutative v (plus x v);
126+ rewrite sym (plusAssociative x v (plus x v));
127+ rewrite (plusAssociative x1 (plus (plus x v) (plus x v)) (plus v1 v1));
128+ rewrite sym (plusAssociative (plus (plus x v) (plus x v)) v1 v1);
129+ rewrite (plusAssociative (plus x v) (plus x v) v1);
130+ rewrite (plusCommutative v1 (plus x v));
131+ rewrite sym (plusAssociative (plus x v) v1 (plus x v));
132+ rewrite (plusAssociative (plus (plus x v) v1) (plus x v) v1);
133+ trivial;
134+}
135+
136+main.adc_lemma_1 = proof {
137+ intros;
138+ rewrite sym (plusZeroRightNeutral c) ;
139+ trivial;
140+}
141+