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 }

{-
mapCycle : {a b : Set} → (a → b) → Cycle a → Cycle b
Cycle.addr (mapCycle f c) = Cycle.addr c
Cycle.r/w (mapCycle f c) = Cycle.r/w c
Cycle.continuation (mapCycle f c) with Cycle.r/w c | Cycle.continuation c
... | true | continuation = λ w → Data.Maybe.map f (continuation w)
... | false | (w , a) = (w , f a)
-}

{-
_>>=_ : {a b : Set} → Cycles a → (a → Cycles b) → Cycles b
zero x >>= f = f x
suc c >>= f =
  suc (record {
    addr = Cycle.addr c;
    r/w = Cycle.r/w c;
    continuation = (λ {
      true continuation → λ w → Data.Maybe.map (λ a → a >>= f) (continuation w);
      false (w , a) → (w , a >>= f)
    }) (Cycle.r/w c) (Cycle.continuation c)
  })
-}

{-
_>>=_ : {a b : Set} → Cycles a → (a → Cycles b) → Cycles b
zero x >>= f = f x
suc x >>= f = suc (mapCycle (λ a → a >>= f) x)
-}

full-state : Set
full-state = Cycles State

cycle : Cycles State -> Cycle (Cycles State)

cycle : full-state -> Cycle full-state