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 ⊤?