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

--------------------------------------------------------------------------------