module Data.Bin where
import Data.Nat as Nat
open Nat using (ℕ; zero; z≤n; s≤s) renaming (suc to 1+_)
open Nat.≤-Reasoning
import Data.Nat.Properties as NP
open import Data.Digit
import Data.Fin as Fin
open Fin using (Fin; zero) renaming (suc to 1+_)
import Data.Fin.Props as FP
open FP using (_+′_)
import Data.List as List; open List hiding (downFrom)
open import Data.Function
open import Data.Product
open import Algebra
open import Relation.Binary
open import Relation.Binary.Consequences
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; _≢_; refl; sym)
open import Relation.Nullary
private
module BitOrd = StrictTotalOrder (FP.strictTotalOrder 2)
infix 8 _1#
Bin⁺ : Set
Bin⁺ = List Bit
data Bin : Set where
0# : Bin
_1# : (bs : Bin⁺) → Bin
toBits : Bin → List Bit
toBits 0# = [ 0b ]
toBits (bs 1#) = bs ++ [ 1b ]
toℕ : Bin → ℕ
toℕ = fromDigits ∘ toBits
fromBits : List Bit → Bin
fromBits [] = 0#
fromBits (b ∷ bs) with fromBits bs
fromBits (b ∷ bs) | bs′ 1# = (b ∷ bs′) 1#
fromBits (zero ∷ bs) | 0# = 0#
fromBits (1+ zero ∷ bs) | 0# = [] 1#
fromBits (1+ 1+ () ∷ bs) | _
fromℕ : ℕ → Bin
fromℕ n with toDigits 2 n
fromℕ .(fromDigits bs) | digits bs = fromBits bs
infix 4 _<_
data _<_ (b₁ b₂ : Bin) : Set where
less : (lt : (Nat._<_ on₁ toℕ) b₁ b₂) → b₁ < b₂
private
<-trans : Transitive _<_
<-trans (less lt₁) (less lt₂) = less (NP.<-trans lt₁ lt₂)
asym : ∀ {b₁ b₂} → b₁ < b₂ → ¬ b₂ < b₁
asym {b₁} {b₂} (less lt) (less gt) = tri⟶asym cmp lt gt
where cmp = StrictTotalOrder.compare NP.strictTotalOrder
irr : ∀ {b₁ b₂} → b₁ < b₂ → b₁ ≢ b₂
irr lt eq = asym⟶irr (PropEq.resp _<_) sym asym eq lt
irr′ : ∀ {b} → ¬ b < b
irr′ lt = irr lt refl
∷∙ : ∀ {b₁ b₂ bs₁ bs₂} →
bs₁ 1# < bs₂ 1# → (b₁ ∷ bs₁) 1# < (b₂ ∷ bs₂) 1#
∷∙ {b₁} {b₂} {bs₁} {bs₂} (less lt) = less (begin
1 + (m₁ + n₁ * 2) ≤⟨ ≤-refl {x = 1} +-mono
(≤-pred (FP.bounded b₁) +-mono ≤-refl) ⟩
1 + (1 + n₁ * 2) ≡⟨ refl ⟩
suc n₁ * 2 ≤⟨ lt *-mono ≤-refl ⟩
n₂ * 2 ≤⟨ n≤m+n m₂ (n₂ * 2) ⟩
m₂ + n₂ * 2 ∎
)
where
open Nat; open NP; open Poset poset renaming (refl to ≤-refl)
m₁ = Fin.toℕ b₁; m₂ = Fin.toℕ b₂
n₁ = toℕ (bs₁ 1#); n₂ = toℕ (bs₂ 1#)
∙∷ : ∀ {b₁ b₂ bs} →
Fin._<_ b₁ b₂ → (b₁ ∷ bs) 1# < (b₂ ∷ bs) 1#
∙∷ {b₁} {b₂} {bs} lt = less (begin
1 + (m₁ + n * 2) ≡⟨ sym (+-assoc 1 m₁ (n * 2)) ⟩
(1 + m₁) + n * 2 ≤⟨ lt +-mono ≤-refl ⟩
m₂ + n * 2 ∎)
where
open Nat; open NP
open Poset poset renaming (refl to ≤-refl)
open CommutativeSemiring commutativeSemiring using (+-assoc)
m₁ = Fin.toℕ b₁; m₂ = Fin.toℕ b₂; n = toℕ (bs 1#)
1<[23] : ∀ {b} → [] 1# < (b ∷ []) 1#
1<[23] {b} = less (NP.n≤m+n (Fin.toℕ b) 2)
1<2+ : ∀ {bs b} → [] 1# < (b ∷ bs) 1#
1<2+ {[]} = 1<[23]
1<2+ {b ∷ bs} = <-trans 1<[23] (∷∙ {b₁ = b} (1<2+ {bs}))
0<1 : 0# < [] 1#
0<1 = less (s≤s z≤n)
0<+ : ∀ {bs} → 0# < bs 1#
0<+ {[]} = 0<1
0<+ {b ∷ bs} = <-trans 0<1 1<2+
compare⁺ : Trichotomous (_≡_ on₁ _1#) (_<_ on₁ _1#)
compare⁺ [] [] = tri≈ irr′ refl irr′
compare⁺ [] (b ∷ bs) = tri< 1<2+ (irr 1<2+) (asym 1<2+)
compare⁺ (b ∷ bs) [] = tri> (asym 1<2+) (irr 1<2+ ∘ sym) 1<2+
compare⁺ (b₁ ∷ bs₁) (b₂ ∷ bs₂) with compare⁺ bs₁ bs₂
... | tri< lt ¬eq ¬gt = tri< (∷∙ lt) (irr (∷∙ lt)) (asym (∷∙ lt))
... | tri> ¬lt ¬eq gt = tri> (asym (∷∙ gt)) (irr (∷∙ gt) ∘ sym) (∷∙ gt)
compare⁺ (b₁ ∷ bs) (b₂ ∷ .bs) | tri≈ ¬lt refl ¬gt with BitOrd.compare b₁ b₂
compare⁺ (b ∷ bs) (.b ∷ .bs) | tri≈ ¬lt refl ¬gt | tri≈ ¬lt′ refl ¬gt′ =
tri≈ irr′ refl irr′
... | tri< lt′ ¬eq ¬gt′ = tri< (∙∷ lt′) (irr (∙∷ lt′)) (asym (∙∷ lt′))
... | tri> ¬lt′ ¬eq gt′ = tri> (asym (∙∷ gt′)) (irr (∙∷ gt′) ∘ sym) (∙∷ gt′)
compare : Trichotomous _≡_ _<_
compare 0# 0# = tri≈ irr′ refl irr′
compare 0# (bs₂ 1#) = tri< 0<+ (irr 0<+) (asym 0<+)
compare (bs₁ 1#) 0# = tri> (asym 0<+) (irr 0<+ ∘ sym) 0<+
compare (bs₁ 1#) (bs₂ 1#) = compare⁺ bs₁ bs₂
strictTotalOrder : StrictTotalOrder
strictTotalOrder = record
{ carrier = Bin
; _≈_ = _≡_
; _<_ = _<_
; isStrictTotalOrder = record
{ isEquivalence = PropEq.isEquivalence
; trans = <-trans
; compare = compare
; ≈-resp-< = PropEq.resp _<_
}
}
decSetoid : DecSetoid
decSetoid = StrictTotalOrder.decSetoid strictTotalOrder
infix 4 _≟_
_≟_ : Decidable {Bin} _≡_
_≟_ = DecSetoid._≟_ decSetoid
infix 7 _*2 _*2+1
_*2 : Bin → Bin
0# *2 = 0#
(bs 1#) *2 = (0b ∷ bs) 1#
_*2+1 : Bin → Bin
0# *2+1 = [] 1#
(bs 1#) *2+1 = (1b ∷ bs) 1#
⌊_/2⌋ : Bin → Bin
⌊ 0# /2⌋ = 0#
⌊ [] 1# /2⌋ = 0#
⌊ (b ∷ bs) 1# /2⌋ = bs 1#
Carry : Set
Carry = Bit
addBits : Carry → Bit → Bit → Carry × Bit
addBits c b₁ b₂ with c +′ (b₁ +′ b₂)
... | zero = (0b , 0b)
... | 1+ zero = (0b , 1b)
... | 1+ 1+ zero = (1b , 0b)
... | 1+ 1+ 1+ zero = (1b , 1b)
... | 1+ 1+ 1+ 1+ ()
addCarryToBitList : Carry → List Bit → List Bit
addCarryToBitList zero bs = bs
addCarryToBitList (1+ zero) [] = 1b ∷ []
addCarryToBitList (1+ zero) (zero ∷ bs) = 1b ∷ bs
addCarryToBitList (1+ zero) (1+ zero ∷ bs) = 0b ∷ addCarryToBitList 1b bs
addCarryToBitList (1+ 1+ ()) _
addCarryToBitList _ ((1+ 1+ ()) ∷ _)
addBitLists : Carry → List Bit → List Bit → List Bit
addBitLists c [] bs₂ = addCarryToBitList c bs₂
addBitLists c bs₁ [] = addCarryToBitList c bs₁
addBitLists c (b₁ ∷ bs₁) (b₂ ∷ bs₂) with addBits c b₁ b₂
... | (c' , b') = b' ∷ addBitLists c' bs₁ bs₂
infixl 6 _+_
_+_ : Bin → Bin → Bin
m + n = fromBits (addBitLists 0b (toBits m) (toBits n))
infixl 7 _*_
_*_ : Bin → Bin → Bin
0# * n = 0#
[] 1# * n = n
(b ∷ bs) 1# * n with bs 1# * n
(b ∷ bs) 1# * n | 0# = 0#
(zero ∷ bs) 1# * n | bs' 1# = (0b ∷ bs') 1#
(1+ zero ∷ bs) 1# * n | bs' 1# = n + (0b ∷ bs') 1#
((1+ 1+ ()) ∷ _) 1# * _ | _
suc : Bin → Bin
suc n = [] 1# + n
⌈_/2⌉ : Bin → Bin
⌈ n /2⌉ = ⌊ suc n /2⌋
pred : Bin⁺ → Bin
pred [] = 0#
pred (zero ∷ bs) = pred bs *2+1
pred (1+ zero ∷ bs) = (zero ∷ bs) 1#
pred (1+ 1+ () ∷ bs)
downFrom : ℕ → List Bin
downFrom n = helper n (fromℕ n)
where
helper : ℕ → Bin → List Bin
helper zero 0# = []
helper (1+ n) (bs 1#) = n′ ∷ helper n n′
where n′ = pred bs
helper zero (_ 1#) = []
helper (1+ _) 0# = []