Finish initial definition of bitvectors.

1 files changed, 0 insertions, 104 deletions

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