blob: 3d409ca4835e0fb27c461f139a2da5ae79f50cb7 (
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
{-# OPTIONS --safe --without-K #-}
module Helium.Data.BitVec where
open import Algebra.Core
open import Data.Bool as B using () renaming (Bool to Bit; false to 0#; true to 1#)
open import Data.Fin hiding (_+_; _-_)
open import Data.Fin.Properties using (toℕ-fromℕ)
open import Data.Nat as N hiding (_+_)
open import Data.Product
open import Data.Vec hiding (map; replicate)
open import Relation.Binary.PropositionalEquality using (cong)
private
variable
l m n : ℕ
infixr 6 _∧_ _+_ _-_
infixr 5 _∨_ _xor_
-- Type
BitVec : ℕ → Set
BitVec = Vec Bit
-- Constants
replicate : Bit → BitVec n
replicate {zero} b = []
replicate {suc n} b = b ∷ replicate b
zeroes : BitVec n
zeroes = replicate 0#
ones : BitVec n
ones = replicate 1#
one : BitVec (suc n)
one {zero} = 1# ∷ []
one {suc n} = 0# ∷ one
-- Bitwise operations
bitwise : Op₁ Bit → Op₁ (BitVec n)
bitwise f [] = []
bitwise f (x ∷ xs) = f x ∷ bitwise f xs
bitwise₂ : Op₂ Bit → Op₂ (BitVec n)
bitwise₂ _∙_ [] [] = []
bitwise₂ _∙_ (x ∷ xs) (y ∷ ys) = x ∙ y ∷ bitwise₂ _∙_ xs ys
not : BitVec n → BitVec n
not = bitwise B.not
_∧_ : BitVec n → BitVec n → BitVec n
_∧_ = bitwise₂ B._∧_
_∨_ : BitVec n → BitVec n → BitVec n
_∨_ = bitwise₂ B._∨_
_xor_ : BitVec n → BitVec n → BitVec n
_xor_ = bitwise₂ B._xor_
-- Arithmetic operations
add-carry : Bit → BitVec n → BitVec n → Bit
add-carry c [] [] = c
add-carry c (x ∷ xs) (y ∷ ys) = add-carry c xs ys B.∧ (x B.xor y) B.xor (x B.∧ y)
add-rem : Bit → BitVec n → BitVec n → BitVec n
add-rem c [] [] = []
add-rem c (x ∷ xs) (y ∷ ys) = (add-carry c xs ys B.xor x B.xor y) ∷ add-rem c xs ys
add : Bit → BitVec n → BitVec n → BitVec (suc n)
add c xs ys = add-carry c xs ys ∷ add-rem c xs ys
_+_ : BitVec n → BitVec n → BitVec n
xs + ys = add-rem 0# xs ys
_-_ : BitVec n → BitVec n → BitVec n
xs - ys = add-rem 1# xs (not ys)
-- Conversions
bitToFin : Bit → Fin 2
bitToFin 0# = zero
bitToFin 1# = suc zero
finToBit : Fin 2 → Bit
finToBit zero = 0#
finToBit (suc zero) = 1#
toFin : BitVec n → Fin (2 ^ n)
toFin [] = zero
toFin (b ∷ bs) = combine (bitToFin b) (toFin bs)
fromFin : Fin (2 ^ n) → BitVec n
fromFin {zero} x = []
fromFin {suc n} x = uncurry (_∷_) (map finToBit fromFin (remQuot (2 ^ n) x))
|
