module TIA where

open import Data.Bool as Bool using (Bool)
open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; ⌊_/2⌋; _<_; _<ᵇ_; _<?_; _>?_)
open import Data.Product using (_×_; _,_; proj₂)
open import Data.Unit using (⊤)
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Relation.Nullary using (yes; no; does)

open import Bit
open import Word.Base as Word using (Word; _○; _●; ∅; op₀)
open import memory using (memory)

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

hblank : ℕ
hblank = 68

picture-width : ℕ
picture-width = 160

width : ℕ
width = hblank + picture-width

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

record collision-latches : Set where
  field
    M₀-P₀ : Bit
    M₀-P₁ : Bit
    M₁-P₁ : Bit
    M₁-P₀ : Bit
    P₀-BL : Bit
    P₀-PF : Bit
    P₁-BL : Bit
    P₁-PF : Bit
    M₀-BL : Bit
    M₀-PF : Bit
    M₁-BL : Bit
    M₁-PF : Bit
    --
    BL-PF : Bit
    M₀-M₁ : Bit
    P₀-P₁ : Bit

read-collisions : Word 3 → collision-latches → Bit × Bit
read-collisions (∅ ○ ○ ○) record { M₀-P₀ = D6 ; M₀-P₁ = D7 } = D6 , D7
read-collisions (∅ ○ ○ ●) record { M₁-P₁ = D6 ; M₁-P₀ = D7 } = D6 , D7
read-collisions (∅ ○ ● ○) record { P₀-BL = D6 ; P₀-PF = D7 } = D6 , D7
read-collisions (∅ ○ ● ●) record { P₁-BL = D6 ; P₁-PF = D7 } = D6 , D7
read-collisions (∅ ● ○ ○) record { M₀-BL = D6 ; M₀-PF = D7 } = D6 , D7
read-collisions (∅ ● ○ ●) record { M₁-BL = D6 ; M₁-PF = D7 } = D6 , D7
read-collisions (∅ ● ● ○) record { BL-PF = D7 } = unknown , D7
read-collisions (∅ ● ● ●) record { M₀-M₁ = D6 ; P₀-P₁ = D7 } = D6 , D7
read-collisions _ _ = unknown , unknown

write-collisions : Bit → Bit → Bit → Bit → Bit → Bit → collision-latches → collision-latches 
write-collisions M₀ M₁ P₀ P₁ BL PF collisions =
  record {
    M₀-P₀ = collision-latches.M₀-P₀ collisions ∨ (M₀ ∧ P₀);
    M₀-P₁ = collision-latches.M₀-P₁ collisions ∨ (M₀ ∧ P₁);
    M₁-P₁ = collision-latches.M₁-P₁ collisions ∨ (M₁ ∧ P₁);
    M₁-P₀ = collision-latches.M₁-P₀ collisions ∨ (M₁ ∧ P₀);
    P₀-BL = collision-latches.P₀-BL collisions ∨ (P₀ ∧ BL);
    P₀-PF = collision-latches.P₀-PF collisions ∨ (P₀ ∧ PF);
    P₁-BL = collision-latches.P₁-BL collisions ∨ (P₁ ∧ BL);
    P₁-PF = collision-latches.P₁-PF collisions ∨ (P₁ ∧ PF);
    M₀-BL = collision-latches.M₀-BL collisions ∨ (M₀ ∧ BL);
    M₀-PF = collision-latches.M₀-PF collisions ∨ (M₀ ∧ PF);
    M₁-BL = collision-latches.M₁-BL collisions ∨ (M₁ ∧ BL);
    M₁-PF = collision-latches.M₁-PF collisions ∨ (M₁ ∧ PF);
    BL-PF = collision-latches.BL-PF collisions ∨ (BL ∧ PF);
    M₀-M₁ = collision-latches.M₀-M₁ collisions ∨ (M₀ ∧ M₁);
    P₀-P₁ = collision-latches.P₀-P₁ collisions ∨ (P₀ ∧ P₁)
  }

clear-collisions : collision-latches
clear-collisions =
  record {
    M₀-P₀ = false;
    M₀-P₁ = false;
    M₁-P₁ = false;
    M₁-P₀ = false;
    P₀-BL = false;
    P₀-PF = false;
    P₁-BL = false;
    P₁-PF = false;
    M₀-BL = false;
    M₀-PF = false;
    M₁-BL = false;
    M₁-PF = false;
    BL-PF = false;
    M₀-M₁ = false;
    P₀-P₁ = false
  }

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

record TIA : Set where
  field
    x : ℕ
    x-pf : x < width

    registers : memory 6 (Word 8)
    collisions : collision-latches

advance-beam : TIA → TIA
advance-beam tia with suc (TIA.x tia) <? width
... | yes pf = record tia {x = suc (TIA.x tia); x-pf = pf}
... | no _ = record tia {x = zero; x-pf = Data.Nat.z<s}

read : Word 4 → TIA → Word 8
read w with Word.pop-high w
... | (w , unknown) = λ tia → op₀ unknown
... | (w , false) = λ (record {collisions = collisions}) →
  let (D6 , D7) = read-collisions w collisions
  in Word.concat (op₀ {6} unknown , Word.push-low (D6 , Word.push-low (D7 , ∅)))
... | (w , true) = λ tia → op₀ unknown -- TIA inputs not implemented.

write : Word 6 → Word 8 → TIA → Maybe TIA
-- Strobe writes
write (∅ ○ ○ ○ ○ ● ○) w tia = just {!!}
write (∅ ○ ○ ○ ○ ● ●) w tia = just {!!}
write (∅ ○ ● ○ ○ ○ ○) w tia = just {!!}
write (∅ ○ ● ○ ○ ○ ●) w tia = just {!!}
write (∅ ○ ● ○ ○ ● ○) w tia = just {!!}
write (∅ ○ ● ○ ○ ● ●) w tia = just {!!}
write (∅ ○ ● ○ ● ○ ○) w tia = just {!!}
write (∅ ● ○ ● ○ ● ○) w tia = just {!!}
write (∅ ● ○ ● ○ ● ●) w tia = just {!!}
write (∅ ● ○ ● ● ○ ○) w tia = just (record tia {collisions = clear-collisions})
-- Register writes
write addr w tia =
  Word.nat-from-word addr Maybe.>>= λ x →
  Bool.if (x >? 0x2C).does then nothing else
  (memory.write addr w (TIA.registers tia) Maybe.>>= λ registers →
  just (record tia {registers = registers}))

processor-paused : TIA → Bool
processor-paused TIA = {!!}

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

record color-lum : Set where
  field
    color : ℕ
    lum : ℕ

color-clock : TIA → TIA × Maybe color-lum
color-clock tia =
  let
    x = TIA.x tia ∸ hblank
    ( ( ( ( _
          , (_ , (COLUP0 , COLUP1))) ,
          (((COLUPF , COLUBK) , (CTRLPF , _)) , _)) ,
        (_ , (_ , ((_ , ENAM0) , (ENAM1 , ENABL))))) ,
      _) = TIA.registers tia
    pfp-mode = Word.bit CTRLPF 2
    score-mode = Word.bit CTRLPF 1
    left-half = bit-from-bool (x <ᵇ ⌊ picture-width /2⌋)

    M₀ = Word.bit ENAM0 1 ∧ {!!}
    M₁ = Word.bit ENAM1 1 ∧ {!!}
    P₀ = {!!}
    P₁ = {!!}
    BL = Word.bit ENABL 1 ∧ {!!}
    PF = {!!}

    draw-col₀ = M₀ ∨ P₀ ∨ (PF ∧ score-mode ∧ left-half)
    draw-col₁ = M₁ ∨ P₁ ∨ (PF ∧ score-mode ∧ not left-half)
    draw-PF-BL = PF ∨ BL

    pixel-color : Maybe (Word 8)
    pixel-color =
      -- If the pfp bit is set, the score bit doesn't matter.
      bool-from-bit (draw-PF-BL ∧ pfp-mode) Maybe.>>= λ x → Bool.if x then just COLUPF else (
      bool-from-bit draw-col₀ Maybe.>>= λ x → Bool.if x then just COLUP0 else (
      bool-from-bit draw-col₁ Maybe.>>= λ x → Bool.if x then just COLUP1 else (
      bool-from-bit draw-PF-BL Maybe.>>= λ x → Bool.if x then just COLUPF else just COLUBK)))
  in record tia {
    collisions = write-collisions M₀ M₁ P₀ P₁ BL PF (TIA.collisions tia)
  } , (
    pixel-color Maybe.>>= λ col →
    let (lum , col) = Word.split {3} {4} (proj₂ (Word.pop-low col)) in
    Word.nat-from-word lum Maybe.>>= λ lum →
    Word.nat-from-word col Maybe.>>= λ col →
    just (record {color = col; lum = lum})
  )

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

-- Is it possible that my literal overloading was sabotaged by not importing ⊤?