From 229bd0de77ab5bba7eb2ad5362c526c098d62ac7 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Fri, 10 Dec 2021 17:41:42 +0000
Subject: Define BitVec as a bit-vector.

---
 src/Helium/Data/BitVec.agda | 104 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 104 insertions(+)
 create mode 100644 src/Helium/Data/BitVec.agda

diff --git a/src/Helium/Data/BitVec.agda b/src/Helium/Data/BitVec.agda
new file mode 100644
index 0000000..3d409ca
--- /dev/null
+++ b/src/Helium/Data/BitVec.agda
@@ -0,0 +1,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))
-- 
cgit v1.2.3