{-# OPTIONS --safe #-}

module Data.Binary.Skew where

open import Prelude
open import Data.Nat
open import Data.List

𝔹 : Type
𝔹 = List β„•

inc : 𝔹 β†’ 𝔹
inc [] = zero ∷ []
inc (x ∷ []) = zero ∷ x ∷ []
inc (x₁ ∷ zero   ∷ xs) = suc x₁ ∷ xs
inc (x₁ ∷ suc xβ‚‚ ∷ xs) = zero ∷ x₁ ∷ xβ‚‚ ∷ xs

⟦_β‡‘βŸ§ : β„• β†’ 𝔹
⟦ zero β‡‘βŸ§ = []
⟦ suc n β‡‘βŸ§ = inc ⟦ n β‡‘βŸ§

2Γ—_ : β„• β†’ β„•
2Γ— n = n + n

infixr 5 1π•“βˆ·_ 1𝕓⋯_∷_
1π•“βˆ·_ : β„• β†’ β„•
1π•“βˆ· n = 1 + 2Γ— n

1𝕓⋯_∷_ : β„• β†’ β„• β†’ β„•
1𝕓⋯ zero  ∷ a = a
1𝕓⋯ suc n ∷ a = 1π•“βˆ· 1𝕓⋯ n ∷ a

⟦∷_β‡“βŸ§^ : (β„• β†’ β„•) β†’ β„• β†’ β„•
⟦∷ xs β‡“βŸ§^ aβ€² = aβ€² + xs (1π•“βˆ· aβ€²)

⟦_∷_β‡“βŸ§^ : β„• β†’ (β„• β†’ β„•) β†’ β„• β†’ β„•
⟦ x ∷ xs β‡“βŸ§^ a = ⟦∷ xs β‡“βŸ§^  (1𝕓⋯ x ∷ a)

⟦_β‡“βŸ§β€² : 𝔹 β†’ β„• β†’ β„•
-- ⟦_β‡“βŸ§β€² = foldr ⟦_∷_β‡“βŸ§^ (const 0)
⟦ [] β‡“βŸ§β€² = const 0
⟦ x ∷ xs β‡“βŸ§β€² = ⟦ x ∷ ⟦ xs β‡“βŸ§β€² β‡“βŸ§^

⟦_β‡“βŸ§ : 𝔹 β†’ β„•
⟦ [] β‡“βŸ§     = zero
⟦ x ∷ xs β‡“βŸ§ = let a = 1𝕓⋯ x ∷ 1 in a + ⟦ xs β‡“βŸ§β€² a

-- open import Testers

-- _ : testIsoβ„• (⟦_β‡‘βŸ§β€² iff (flip ⟦_β‡“βŸ§β€² 1)) 10
-- _ = refl

open import Path.Reasoning
import Data.Nat.Properties as β„•

1𝕓-distrib : βˆ€ n x β†’ 1𝕓⋯ n ∷ 1π•“βˆ· x ≑ 1𝕓⋯ suc n ∷ x
1𝕓-distrib zero x = refl
1𝕓-distrib (suc n) x = cong 1π•“βˆ·_ (1𝕓-distrib n x)

inc-suc : βˆ€ x β†’ ⟦ inc x β‡“βŸ§ ≑ suc ⟦ x β‡“βŸ§
inc-suc []                 = refl
inc-suc (x  ∷ [])          = refl
inc-suc (x  ∷ zero   ∷ xs) = cong suc (β„•.+-assoc (1𝕓⋯ x ∷ 1) (1𝕓⋯ x ∷ 1) _)
inc-suc (x₁ ∷ suc xβ‚‚ ∷ xs) = cong (suc ∘ ((1𝕓⋯ x₁ ∷ 1) +_) ∘ ⟦∷ ⟦ xs β‡“βŸ§β€² β‡“βŸ§^) (1𝕓-distrib xβ‚‚ (1𝕓⋯ x₁ ∷ 1))

𝔹-rightInv : βˆ€ x β†’ ⟦ ⟦ x β‡‘βŸ§ β‡“βŸ§ ≑ x
𝔹-rightInv zero = refl
𝔹-rightInv (suc x) = inc-suc ⟦ x β‡‘βŸ§ ΝΎ cong suc (𝔹-rightInv x)

-- 𝔹-leftInv : βˆ€ x β†’ ⟦ ⟦ x β‡“βŸ§ β‡‘βŸ§ ≑ x
-- 𝔹-leftInv []       = refl
-- 𝔹-leftInv (x ∷ xs) = {!!}

-- -- inc-2*-1ᡇ : βˆ€ n β†’ inc ⟦ n β„•.* 2 β‡‘βŸ§ ≑ 1ᡇ ⟦ n β‡‘βŸ§
-- -- inc-2*-1ᡇ zero    i = 1ᡇ 0ᡇ
-- -- inc-2*-1ᡇ (suc n) i = inc (inc (inc-2*-1ᡇ n i))

-- -- 𝔹⇔ℕ : 𝔹 ⇔ β„•
-- -- 𝔹⇔ℕ .fun = ⟦_β‡“βŸ§
-- -- 𝔹⇔ℕ .inv = ⟦_β‡‘βŸ§
-- -- 𝔹⇔ℕ .rightInv x = {!!}
-- -- 𝔹⇔ℕ .leftInv = {!!}