module TIA where
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 Word.Base using (Word; _○; _●; ∅)
--------------------------------------------------------------------------------
{-
vsync : ℕ
vsync = 3
vblank : ℕ
vblank = 37
picture-height : ℕ
picture-height = 192
overscan : ℕ
overscan = 30
height : ℕ
height = vsync + vblank + picture-height + overscan
-}
hblank : ℕ
hblank = 68
picture-width : ℕ
picture-width = 160
width : ℕ
width = hblank + picture-width
--------------------------------------------------------------------------------
record TIA : Set where
  field
    x : ℕ
    x-pf : x < width
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 → 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
write : Word 6 → Word 8 → TIA → Maybe TIA
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 = 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
--------------------------------------------------------------------------------
record color-lum : Set where
pixel : TIA → Maybe color-lum
pixel = {!!}
-- TODO: How do I update collision registers?
--------------------------------------------------------------------------------
-- 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.