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 }