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