search

sbp / idris-bi

Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq
https://github.com/idris-lang/Idris-dev/issues/3976
36 stars 5 forks source link

Direct compilation for BIP / view for Data.Bits? #13

Open clayrat opened 7 years ago

clayrat commented 7 years ago

Might be quite useful to link Bip/Bin/Biz to un/signed machine words, perhaps by making a covering function for Data.Bits.

sbp commented 7 years ago

Agreed, and this is something that I can work on.

clayrat commented 7 years ago

One thing that we definitely need for this to happen are the bounded versions (the analogue of Prelude's Fin), so that we could fix the byte length. This however will definitely mess up the arithmetics, wonder if Coq has some solution here? One way out would be to define it as modular arithmetics, just have to figure out if real-world bytes behave like that :)

clayrat commented 7 years ago

This looks relevant: https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v

clayrat commented 6 years ago

https://github.com/maximedenes/native-coq/tree/master/theories/Numbers also looks fitting

clayrat commented 6 years ago

As well as https://github.com/artart78/coq-bits It even has an accompanying paper https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/coq-bitset/flops/paper.pdf