mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-15 01:25:05 +03:00
af72159e60
Sphinx provides a retargatable documentation system for documentation, and code. Allowing for HTML, LaTeX, and ePub documents to be generated from a single source. ReadTheDocs is a free service for Open Source Projects that provides continuous delivery of documents that use either Sphinx or MakeDoc. This commit provides Sphinx based versions of: + The Idris Tutorial + The Effects Tutorial + Select articles from the Wiki to begin a language reference + Select articles from the Wiki to begin short guides. The examples from the effect tutorial have been integrated as well. In the `docs` folder see `README.md` for dependencies, Sphinx is easily obtainable from all major Linux ditributions and through brew on Mac OS X. + Running `make html` will produce a monolithic html website for use with readthedocs. + Running `make latexpdf` will produce individual PDFs for each of the above tutorials. + Running `make epub` will produce a monolithic epub. This will need to be adapted to either produce one of the above document sets, or individual epubs. Future work will be to: + Integrate idris with readthedocs for documentation generation for tagged released.. + Add latex and html generation to the travis builds. + Add
95 lines
2.8 KiB
Idris
95 lines
2.8 KiB
Idris
module main
|
|
|
|
data Bit : Nat -> Type where
|
|
b0 : Bit 0
|
|
b1 : Bit 1
|
|
|
|
instance Show (Bit n) where
|
|
show b0 = "0"
|
|
show b1 = "1"
|
|
|
|
infixl 5 #
|
|
|
|
data Binary : (width : Nat) -> (value : Nat) -> Type where
|
|
zero : Binary Z Z
|
|
(#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
|
|
|
|
instance Show (Binary w k) where
|
|
show zero = ""
|
|
show (bin # bit) = show bin ++ show bit
|
|
|
|
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
|
|
|
|
main : IO ()
|
|
main = do let n1 = zero # b1 # b0 # b1 # b0
|
|
let n2 = zero # b1 # b1 # b1 # b0
|
|
print (adc n1 n2 b0)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
---------- Proofs ----------
|
|
|
|
-- There is almost certainly an easier proof. I don't care, for now :)
|
|
|
|
main.adc_lemma_2 = proof {
|
|
intro c,w,v,bit0,num0;
|
|
intro b0,v1,bit1,num1,b1;
|
|
intro bc,x,x1,bx,bx1,prf;
|
|
intro;
|
|
rewrite sym (plusZeroRightNeutral v);
|
|
rewrite sym (plusZeroRightNeutral v1);
|
|
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 sym (plusCommutative (plus v v) bit1);
|
|
rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));
|
|
rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));
|
|
rewrite sym prf;
|
|
rewrite sym (plusZeroRightNeutral x);
|
|
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 plusAssociative (plus x v) (plus x v) (plus v1 v1);
|
|
rewrite plusAssociative x v (plus v1 v1);
|
|
rewrite sym (plusAssociative v v1 v1);
|
|
rewrite sym (plusAssociative x (plus v v1) v1);
|
|
rewrite sym (plusAssociative x v v1);
|
|
rewrite sym (plusCommutative (plus (plus x v) v1) v1);
|
|
rewrite plusZeroRightNeutral (plus (plus x v) v1);
|
|
rewrite sym (plusAssociative (plus x v) v1 (plus (plus (plus x v) v1) Z));
|
|
trivial;
|
|
}
|
|
|
|
main.adc_lemma_1 = proof {
|
|
intros;
|
|
rewrite sym (plusZeroRightNeutral c) ;
|
|
trivial;
|
|
}
|