open import Data.Nat using (ℕ; zero; suc; _+_; _<_; _<?_)
open import Data.Product using (_×_; _,_)
open import Data.Maybe using (Maybe; just; nothing)
open import Relation.Nullary using (yes; no)

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 Word.Base using (Word; _○; _●; ∅)

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

{-
vsync : ℕ
vsync = 3
vblank : ℕ
vblank = 37
picture-height : ℕ
picture-height = 192
overscan : ℕ
overscan = 30
height : ℕ
height = vsync + vblank + picture-height + overscan
-}

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
  }
--------------------------------------------------------------------------------

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

read : Word 4 → TIA → Maybe (Word 8)
read (∅ ○ ○ ○ ○) tia = just {!!}
read (∅ ○ ○ ○ ●) tia = just {!!}
read (∅ ○ ○ ● ○) tia = just {!!}
read (∅ ○ ○ ● ●) tia = just {!!}
read (∅ ○ ● ○ ○) tia = just {!!}
read (∅ ○ ● ○ ●) tia = just {!!}
read (∅ ○ ● ● ○) tia = just {!!}
read (∅ ○ ● ● ●) tia = just {!!}
read (∅ ● ○ ○ ○) tia = just {!!}
read (∅ ● ○ ○ ●) tia = just {!!}
read (∅ ● ○ ● ○) tia = just {!!}
read (∅ ● ○ ● ●) tia = just {!!}
read (∅ ● ● ○ ○) tia = just {!!}
read (∅ ● ● ○ ●) tia = just {!!}
read (∅ ● ● ● ○) tia = nothing
read (∅ ● ● ● ●) tia = nothing

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 (∅ ○ ○ ○ ○ ○ ○) w tia = just {!!}
write (∅ ○ ○ ○ ○ ○ ●) w tia = just {!!}

-- 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 {!!}
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 {!!}
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 {!!}
write (∅ ● ○ ○ ● ● ●) w tia = just {!!}
write (∅ ● ○ ● ○ ○ ○) w tia = just {!!}
write (∅ ● ○ ● ○ ○ ●) w tia = just {!!}

write (∅ ● ○ ● ● ○ ○) w tia = just {!!}
write (∅ ● ○ ● ● ○ ●) w tia = nothing
write (∅ ● ○ ● ● ● ○) w tia = nothing
write (∅ ● ○ ● ● ● ●) w tia = nothing
write (∅ ● ● ○ ○ ○ ○) w tia = nothing
write (∅ ● ● ○ ○ ○ ●) w tia = nothing
write (∅ ● ● ○ ○ ● ○) w tia = nothing
write (∅ ● ● ○ ○ ● ●) w tia = nothing
write (∅ ● ● ○ ● ○ ○) w tia = nothing
write (∅ ● ● ○ ● ○ ●) w tia = nothing
write (∅ ● ● ○ ● ● ○) w tia = nothing
write (∅ ● ● ○ ● ● ●) w tia = nothing
write (∅ ● ● ● ○ ○ ○) w tia = nothing
write (∅ ● ● ● ○ ○ ●) w tia = nothing
write (∅ ● ● ● ○ ● ○) w tia = nothing
write (∅ ● ● ● ○ ● ●) w tia = nothing
write (∅ ● ● ● ● ○ ○) w tia = nothing
write (∅ ● ● ● ● ○ ●) w tia = nothing
write (∅ ● ● ● ● ● ○) w tia = nothing
write (∅ ● ● ● ● ● ●) w tia = nothing

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 = {!!}

  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 = {!!}

pixel : TIA → Maybe color-lum
pixel = {!!}

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

-- TODO: How do I update collision registers?

    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})
  )

-- I've run into a problem. Suppose you read from address 0.
-- The top two bits of the result are useful collision-detection information.
-- But the other six bits are unconstrained.
-- As far as I can tell, in the actual Atari 2600,
-- the wires are connected to neither power nor ground!
--
-- So how should I emulate this?
-- It doesn't make sense to crash the emulator; a reasonable program might make this read.
-- But if I hardcode a reasonable behavior, like pulling those lines high or low,
-- I limit the applicability of any proofs I may write.

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