module Word.Base where open import Agda.Builtin.Equality using (_≡_; refl) import Data.Bool as Bool open import Data.Product using (_×_; _,_; proj₁; proj₂) open import Data.Unit using (⊤) open import Data.Maybe using (Maybe; just; nothing) open import Data.Nat using (ℕ; zero; suc; _<ᵇ_; _+_; _*_) open import Data.Integer using (ℤ; _%ℕ_; _/ℕ_) open import Relation.Nullary using (does) open import Bit using (Bit; true; false; unknown; not; _∧_; _xor_) -------------------------------------------------------------------------------- data Word : ℕ → Set where ∅ : Word 0 push-low : {n : ℕ} → Bit × Word n → Word (suc n) pattern _● w = push-low (true , w) pattern _○ w = push-low (false , w) pattern _◍ w = push-low (unknown , w) -------------------------------------------------------------------------------- pop-low : {n : ℕ} → Word (suc n) → Bit × Word n pop-low (push-low x) = x push-high : {n : ℕ} → Word n × Bit → Word (suc n) push-high (∅ , b) = push-low (b , ∅) push-high (push-low (b₁ , w) , b₂) = push-low (b₁ , push-high (w , b₂)) pop-high : {n : ℕ} → Word (suc n) → Word n × Bit pop-high {0} (push-low (b , ∅)) = (∅ , b) pop-high {suc n} (push-low (b₁ , w)) = let (w , b₂) = pop-high w in (push-low (b₁ , w) , b₂) -------------------------------------------------------------------------------- bit : {n : ℕ} → Word n → (i : ℕ) → {{Bool.T (i <ᵇ n)}} → Bit bit (push-low (b , w)) zero = b bit (push-low (b , w)) (suc i) {{pf}} = bit w i {{pf}} -------------------------------------------------------------------------------- _≡ᵇ_ : {n : ℕ} → Word n → Word n → Bit ∅ ≡ᵇ ∅ = true push-low (b₀ , w₀) ≡ᵇ push-low (b₁ , w₁) = not (b₀ xor b₁) ∧ (w₀ ≡ᵇ w₁) -------------------------------------------------------------------------------- op₀ : {n : ℕ} → Bit → Word n op₁ : {n : ℕ} → (Bit → Bit) → (Word n → Word n) op₂ : {n : ℕ} → (Bit → Bit → Bit) → (Word n → Word n → Word n) op₀ {zero} f = ∅ op₀ {suc n} f = push-low (f , op₀ f) op₁ f ∅ = ∅ op₁ f (push-low (b₀ , w₀)) = push-low (f b₀ , op₁ f w₀) op₂ f ∅ ∅ = ∅ op₂ f (push-low (b₀ , w₀)) (push-low (b₁ , w₁)) = push-low (f b₀ b₁ , op₂ f w₀ w₁) -------------------------------------------------------------------------------- concat : {m n : ℕ} → Word m × Word n → Word (m + n) concat (∅ , w₁) = w₁ concat (push-low (b , w₀) , w₁) = push-low (b , concat (w₀ , w₁)) split : {m n : ℕ} → Word (m + n) → Word m × Word n split {zero} w = (∅ , w) split {suc m} (push-low (b , w)) = let (w₀ , w₁) = split w in (push-low (b , w₀) , w₁) -------------------------------------------------------------------------------- word-from-int : {n : ℕ} → ℤ → Word n word-from-int {zero} _ = ∅ word-from-int {suc n} x = push-low (Bit.bit-from-bool (x %ℕ 2 Data.Nat.≡ᵇ 0) , word-from-int (x /ℕ 2)) nat-from-word : {n : ℕ} → Word n → Maybe ℕ nat-from-word ∅ = Maybe.just 0 nat-from-word (push-low (b , w)) with Bit.bool-from-bit b | nat-from-word w ... | just b | just w = just ((Bool.if b then 1 else 0) + 2 * w) ... | _ | _ = nothing -------------------------------------------------------------------------------- add-with-carry : {n : ℕ} → Bit → Word n → Word n → Word n × Bit add-with-carry carry ∅ ∅ = (∅ , carry) add-with-carry carry-in (push-low (b₀ , w₀)) (push-low (b₁ , w₁)) = let b₂ = carry-in xor b₀ xor b₁ carry = Bit.majority carry-in b₀ b₁ (w₂ , carry-out) = add-with-carry carry w₀ w₁ in (push-low (b₂ , w₂) , carry-out) sub-with-inverted-borrow : {n : ℕ} → Bit → Word n → Word n → Word n × Bit sub-with-inverted-borrow inverted-borrow w₀ w₁ = add-with-carry inverted-borrow w₀ (op₁ not w₁) -------------------------------------------------------------------------------- add : {n : ℕ} → Word n → Word n → Word n add w₀ w₁ = proj₁ (add-with-carry false w₀ w₁) increment : {n : ℕ} → ℤ → Word n → Word n increment n w = add (word-from-int n) w --------------------------------------------------------------------------------