Finish initial definition of bitvectors.

1 files changed, 109 insertions, 0 deletions

diff --git a/src/Helium/Data/Bits.agda b/src/Helium/Data/Bits.agda
new file mode 100644
index 0000000..255bd9d
--- /dev/null
+++ b/src/Helium/Data/Bits.agda
@@ -0,0 +1,109 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Data.Bits where
+
+open import Algebra
+open import Algebra.Morphism.Definitions
+open import Data.Fin as Fin hiding (_+_; _≟_)
+import Data.Fin.Properties as Finₚ
+open import Data.Nat as ℕ using (ℕ; suc; _+_)
+import Data.Nat.Properties as ℕₚ
+open import Function
+open import Level using (_⊔_) renaming (suc to ℓsuc)
+open import Relation.Binary
+import Relation.Binary.PropositionalEquality as P
+
+private
+  variable
+    k l m n : ℕ
+
+
+module _
+  {a ℓ} {A : ℕ → Set a}
+  (_≈_ : ∀ {m n} → REL (A m) (A n) ℓ)
+  where
+
+  private
+    variable
+      u v x y z : A n
+
+    infix 4 _≗_
+
+    _≗_ : ∀ {b} {B : Set b} → REL (B → A m) (B → A n) (b ⊔ ℓ)
+    f ≗ g = ∀ {x} → f x ≈ g x
+
+  record IsBits (_∨_ _∧_ : ∀ {n} → Op₂ (A n))
+                (¬_ : ∀ {n} → Op₁ (A n))
+                (0# 1# : ∀ {n} → A n)
+                (_∶_ : ∀ {m n} → A m → A n → A (m + n))
+                (slice : ∀ {n} (i : Fin (suc n)) j → A n → A (toℕ (i - j)))
+                (update : ∀ {n} (i : Fin (suc n)) j → Op₁ (A (toℕ (i - j))) → Op₁ (A n))
+                : Set (a ⊔ ℓ) where
+    infix 4 _≟_
+    field
+      -- boolean algebraic properties
+      isBooleanAlgebra : IsBooleanAlgebra (_≈_ {n}) _∨_ _∧_ ¬_ 0# 1#
+      _≟_ : Decidable (_≈_ {m} {n})
+
+      -- _∶_ properties
+      ∶-cong      : x ≈ y → u ≈ v → (x ∶ u) ≈ (y ∶ v)
+      ∶-assoc     : ((x ∶ y) ∶ z) ≈ (x ∶ (y ∶ z))
+      ∶-identityˡ : ∀ {ε : A 0} → (ε ∶ x) ≈ x
+      ∶-identityʳ : ∀ {ε : A 0} → (x ∶ ε) ≈ x
+      ∶-swap-∨ : ((x ∨ y) ∶ (u ∨ v)) ≈ ((x ∶ u) ∨ (y ∶ v))
+      ∶-swap-∧ : ((x ∧ y) ∶ (u ∧ v)) ≈ ((x ∶ u) ∧ (y ∶ v))
+      ∶-homo-¬ : ((¬ x) ∶ (¬ y)) ≈ (¬ (x ∶ y))
+      1#∶1# : (1# {m} ∶ 1# {n}) ≈ 1# {m + n}
+      0#∶0# : (0# {m} ∶ 0# {n}) ≈ 0# {m + n}
+
+      -- slice properties
+      slice-cong : ∀ {i j} → x ≈ y → slice i j x ≈ slice i j y
+      slice-fromℕ-zero : ∀ {x : A n} → slice (fromℕ n) zero x ≈ x
+      slice-inject : ∀ {x : A m} {y : A n} {i i′ j j′} →
+        .(i≡i′ : toℕ i P.≡ toℕ i′) .(j≡j′ : toℕ j P.≡ toℕ j′) →
+        slice i′ j′ (x ∶ y) ≈ slice i j y
+      slice-raise : ∀ {x : A m} {y : A n} {i i′ j j′} →
+        .(n+i≡i′ : n + toℕ i P.≡ toℕ i′) .(n+j≡j′ : n + toℕ j P.≡ toℕ j′) →
+        slice i′ j′ (x ∶ y) ≈ slice i j x
+
+      -- update properties
+      update-cong : ∀ {i j f} → (∀ {x y} → x ≈ y → f x ≈ f y) → x ≈ y → update i j f x ≈ update i j f y
+      update² : ∀ {i j f g} → update i j f ∘ update {n} i j g ≗ update {n} i j (f ∘ g)
+      slice-update : ∀ {i j f} → slice {n} i j ∘ update {n} i j f ≗ f ∘ slice i j
+
+record RawBits a ℓ : Set (ℓsuc a ⊔ ℓsuc ℓ) where
+  infix 8 ¬_
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infixr 5 _∶_
+  infix 4 _≈_
+  field
+    BitVec : ℕ → Set a
+    _≈_    : REL (BitVec m) (BitVec n) ℓ
+    _∨_    : Op₂ (BitVec n)
+    _∧_    : Op₂ (BitVec n)
+    ¬_     : Op₁ (BitVec n)
+    0#     : BitVec n
+    1#     : BitVec n
+    _∶_    : BitVec m → BitVec n → BitVec (m + n)
+    slice  : ∀ (i : Fin (suc n)) j → BitVec n → BitVec (toℕ (i - j))
+    update : ∀ (i : Fin (suc n)) j → Op₁ (BitVec (toℕ (i - j))) → Op₁ (BitVec n)
+
+record Bits a ℓ : Set (ℓsuc a ⊔ ℓsuc ℓ) where
+  infix 8 ¬_
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infixr 5 _∶_
+  infix 4 _≈_
+  field
+    BitVec : ℕ → Set a
+    _≈_    : REL (BitVec m) (BitVec n) ℓ
+    _∨_    : Op₂ (BitVec n)
+    _∧_    : Op₂ (BitVec n)
+    ¬_     : Op₁ (BitVec n)
+    0#     : BitVec n
+    1#     : BitVec n
+    _∶_    : BitVec m → BitVec n → BitVec (m + n)
+    slice  : ∀ (i : Fin (suc n)) j → BitVec n → BitVec (toℕ (i - j))
+    update : ∀ (i : Fin (suc n)) j → Op₁ (BitVec (toℕ (i - j))) → Op₁ (BitVec n)
+    isBits : IsBits _≈_ _∨_ _∧_ ¬_ 0# 1# _∶_ slice update