module 6507-Processor where open import Data.Bool using (Bool; true; false; if_then_else_) open import Data.Maybe using (Maybe; just; nothing) open import Data.Product using (_×_; proj₁) open import Word.Base using (Word; split) open import 6502-Processor using (State) -- After one cycle, return an `s`. record Cycle (s : Set) : Set where field -- In phase 1 of a cycle, the processor sets the address and read/write pin. addr : Word 13 r/w : Bool -- In phase 2 of a cycle, the data is transferred, into or out of the processor. continuation : if r/w then (Word 8 → Maybe s) else (Word 8 × s) full-state : Set full-state = 6502-Processor.full-state -- One cycle at a time. cycle : full-state -> Cycle full-state cycle s with 6502-Processor.cycle s ... | record { addr = addr ; r/w = r/w ; continuation = continuation } = record { addr = proj₁ (split addr) ; r/w = r/w ; continuation = continuation }