2012-10-22 23:37:35 +04:00
|
|
|
module Main
|
2012-10-08 00:36:09 +04:00
|
|
|
|
2012-10-22 23:37:35 +04:00
|
|
|
import Parity
|
|
|
|
import System
|
2012-10-08 00:36:09 +04:00
|
|
|
|
2012-12-12 03:02:17 +04:00
|
|
|
data Bit : Nat -> Type where
|
2012-10-21 18:48:53 +04:00
|
|
|
b0 : Bit O
|
|
|
|
b1 : Bit (S O)
|
2012-10-08 00:36:09 +04:00
|
|
|
|
|
|
|
instance Show (Bit n) where
|
2012-10-16 21:44:22 +04:00
|
|
|
show = show' where
|
|
|
|
show' : Bit x -> String
|
|
|
|
show' b0 = "0"
|
|
|
|
show' b1 = "1"
|
2012-10-08 00:36:09 +04:00
|
|
|
|
|
|
|
infixl 5 #
|
|
|
|
|
2012-12-12 03:02:17 +04:00
|
|
|
data Binary : (width : Nat) -> (value : Nat) -> Type where
|
2012-10-08 00:36:09 +04:00
|
|
|
zero : Binary O O
|
|
|
|
(#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
|
|
|
|
|
|
|
|
instance Show (Binary w k) where
|
2013-02-07 21:37:03 +04:00
|
|
|
show zero = ""
|
|
|
|
show (bin # bit) = show bin ++ show bit
|
2012-10-08 00:36:09 +04:00
|
|
|
|
|
|
|
pad : Binary w n -> Binary (S w) n
|
|
|
|
pad zero = zero # b0
|
2012-11-27 16:47:40 +04:00
|
|
|
pad (num # x) = pad num # x
|
2012-10-08 00:36:09 +04:00
|
|
|
|
|
|
|
natToBin : (width : Nat) -> (n : Nat) ->
|
|
|
|
Maybe (Binary width n)
|
|
|
|
natToBin O (S k) = Nothing
|
|
|
|
natToBin O O = Just zero
|
|
|
|
natToBin (S k) O = do x <- natToBin k O
|
|
|
|
Just (pad x)
|
|
|
|
natToBin (S w) (S k) with (parity k)
|
|
|
|
natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j
|
2012-11-28 08:29:47 +04:00
|
|
|
let value = jbin # b1
|
2012-10-08 00:36:09 +04:00
|
|
|
?ntbEven
|
|
|
|
natToBin (S w) (S (S (plus j j))) | odd = do jbin <- natToBin w (S j)
|
|
|
|
let value = jbin # b0
|
|
|
|
?ntbOdd
|
|
|
|
|
|
|
|
testBin : Maybe (Binary 8 42)
|
|
|
|
testBin = natToBin _ _
|
|
|
|
|
|
|
|
pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
|
|
|
|
term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))
|
|
|
|
|
|
|
|
addBit : Bit x -> Bit y -> Bit c ->
|
|
|
|
(bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))
|
|
|
|
addBit b0 b0 b0 = bitpair b0 b0
|
|
|
|
addBit b0 b0 b1 = bitpair b0 b1
|
|
|
|
addBit b0 b1 b0 = bitpair b0 b1
|
|
|
|
addBit b0 b1 b1 = bitpair b1 b0
|
|
|
|
addBit b1 b0 b0 = bitpair b0 b1
|
|
|
|
addBit b1 b0 b1 = bitpair b1 b0
|
|
|
|
addBit b1 b1 b0 = bitpair b1 b0
|
|
|
|
addBit b1 b1 b1 = bitpair b1 b1
|
|
|
|
|
|
|
|
adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)
|
|
|
|
adc zero zero carry ?= zero # carry
|
|
|
|
adc (numx # bx) (numy # by) carry
|
|
|
|
?= let (bitpair carry0 lsb) = addBit bx by carry in
|
|
|
|
adc numx numy carry0 # lsb
|
|
|
|
|
|
|
|
readNum : IO Nat
|
|
|
|
readNum = do putStr "Enter a number:"
|
|
|
|
i <- getLine
|
2013-05-18 00:06:23 +04:00
|
|
|
let n : Integer = cast i
|
2012-10-08 00:36:09 +04:00
|
|
|
return (fromInteger n)
|
|
|
|
|
|
|
|
main : IO ()
|
|
|
|
main = do let Just bin1 = natToBin 8 42
|
|
|
|
print bin1
|
|
|
|
let Just bin2 = natToBin 8 89
|
|
|
|
print bin2
|
|
|
|
print (adc bin1 bin2 b0)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
---------- Proofs ----------
|
|
|
|
|
2012-10-22 23:37:35 +04:00
|
|
|
Main.ntbOdd = proof {
|
2012-10-08 00:36:09 +04:00
|
|
|
intro w,j;
|
|
|
|
rewrite sym (plusZeroRightNeutral j);
|
|
|
|
rewrite plusSuccRightSucc j j;
|
|
|
|
intros;
|
|
|
|
refine Just;
|
|
|
|
trivial;
|
|
|
|
}
|
|
|
|
|
2012-10-22 23:37:35 +04:00
|
|
|
Main.ntbEven = proof {
|
2012-10-08 00:36:09 +04:00
|
|
|
compute;
|
|
|
|
intro w,j;
|
|
|
|
rewrite sym (plusZeroRightNeutral j);
|
|
|
|
intros;
|
|
|
|
refine Just;
|
|
|
|
trivial;
|
|
|
|
}
|
|
|
|
|
|
|
|
-- There is almost certainly an easier proof. I don't care, for now :)
|
|
|
|
|
2012-10-22 23:37:35 +04:00
|
|
|
Main.adc_lemma_2 = proof {
|
2012-10-08 00:36:09 +04:00
|
|
|
intro c,w,v,bit0,num0;
|
|
|
|
intro b0,v1,bit1,num1,b1;
|
|
|
|
intro bc,x,x1,bx,bx1;
|
|
|
|
rewrite sym (plusZeroRightNeutral x);
|
|
|
|
rewrite sym (plusZeroRightNeutral v1);
|
|
|
|
rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));
|
|
|
|
rewrite sym (plusZeroRightNeutral v);
|
|
|
|
intros;
|
|
|
|
rewrite sym (plusAssociative (plus c (plus bit0 (plus v v))) bit1 (plus v1 v1));
|
|
|
|
rewrite (plusAssociative c (plus bit0 (plus v v)) bit1);
|
|
|
|
rewrite (plusAssociative bit0 (plus v v) bit1);
|
|
|
|
rewrite plusCommutative bit1 (plus v v);
|
|
|
|
rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));
|
|
|
|
rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));
|
|
|
|
rewrite sym b;
|
|
|
|
rewrite plusAssociative x1 (plus x x) (plus v v);
|
|
|
|
rewrite plusAssociative x x (plus v v);
|
|
|
|
rewrite sym (plusAssociative x v v);
|
|
|
|
rewrite plusCommutative v (plus x v);
|
|
|
|
rewrite sym (plusAssociative x v (plus x v));
|
|
|
|
rewrite (plusAssociative x1 (plus (plus x v) (plus x v)) (plus v1 v1));
|
|
|
|
rewrite sym (plusAssociative (plus (plus x v) (plus x v)) v1 v1);
|
|
|
|
rewrite (plusAssociative (plus x v) (plus x v) v1);
|
|
|
|
rewrite (plusCommutative v1 (plus x v));
|
|
|
|
rewrite sym (plusAssociative (plus x v) v1 (plus x v));
|
|
|
|
rewrite (plusAssociative (plus (plus x v) v1) (plus x v) v1);
|
|
|
|
trivial;
|
|
|
|
}
|
|
|
|
|
2012-10-22 23:37:35 +04:00
|
|
|
Main.adc_lemma_1 = proof {
|
2012-10-08 00:36:09 +04:00
|
|
|
intros;
|
|
|
|
rewrite sym (plusZeroRightNeutral c) ;
|
|
|
|
trivial;
|
|
|
|
}
|
|
|
|
|