module 6502-Processor where

open import Data.Bool as Bool using (Bool)
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Data.Product using (_×_; _,_)
import Data.Unit
open import Data.Nat using (ℕ)
import Data.Nat.Properties
open import Data.Integer using (+_; -_)
open import Function using (_∘′_; _$_; flip)
open import Relation.Nullary using (does)

open import Bit
open import Word.Base

--------------------------------------------------------------------------------

-- 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 16
    r/w : Bool

    -- In phase 2 of a cycle, the data is transferred, into or out of the processor.
    continuation : Bool.if r/w then (Word 8 → Maybe s) else (Word 8 × s)

read : {s : Set} → Word 16 → (Word 8 → Maybe s) → Cycle s
read addr continuation =
  record {
    addr = addr;
    r/w = Bool.true;
    continuation = continuation
  }

write : {s : Set} → Word 16 → Word 8 → s → Cycle s
write addr w continuation =
  record {
    addr = addr;
    r/w = Bool.false;
    continuation = (w , continuation)
  }

data Cycles : Set → Set where
  zero : {s : Set} → s → Cycles s
  suc : {s : Set} → Cycle (Cycles s) → Cycles s

CyclesBuilder : Set → Set₁
CyclesBuilder a = {b : Set} → (a → Cycles b) → Cycles b

--------------------------------------------------------------------------------

record Flags : Set where
  field
    N : Bit
    V : Bit
    D : Bit
    I : Bit
    Z : Bit
    C : Bit

byte-from-flags : Flags → Word 8
byte-from-flags flags =
  push-low (Flags.C flags ,
  push-low (Flags.Z flags ,
  push-low (Flags.I flags ,
  push-low (Flags.D flags ,
  push-low (true ,
  push-low (true ,
  push-low (Flags.V flags ,
  push-low (Flags.N flags , ∅))))))))

flags-from-byte : Word 8 → Flags 
flags-from-byte
  (push-low (c , push-low (z , push-low (i , push-low (d ,
  push-low (_ , push-low (_ , push-low (v , push-low (n , ∅)))))))))
  = record {C = c; Z = z; I = i; D = d; V = v; N = n}

record State : Set where
  field
    program-counter : Word 16
    register-A : Word 8
    register-X : Word 8
    register-Y : Word 8
    stack-pointer : Word 8
    flags : Flags

--------------------------------------------------------------------------------

data instruction : Set where
  ADC : instruction 
  AND : instruction 
  ASL : instruction 
  BCC : instruction 
  BCS : instruction 
  BEQ : instruction 
  BIT : instruction 
  BMI : instruction 
  BNE : instruction 
  BPL : instruction 
  BRK : instruction 
  BVC : instruction 
  BVS : instruction 
  CLC : instruction
  CLD : instruction 
  CLI : instruction 
  CLV : instruction 
  CMP : instruction 
  CPX : instruction 
  CPY : instruction 
  DEC : instruction 
  DEX : instruction 
  DEY : instruction 
  EOR : instruction 
  INC : instruction 
  INX : instruction 
  INY : instruction 
  JMP : instruction
  JSR : instruction 
  LDA : instruction 
  LDX : instruction 
  LDY : instruction 
  LSR : instruction 
  NOP : instruction 
  ORA : instruction 
  PHA : instruction 
  PHP : instruction 
  PLA : instruction 
  PLP : instruction 
  ROL : instruction 
  ROR : instruction 
  RTI : instruction
  RTS : instruction 
  SBC : instruction 
  SEC : instruction 
  SED : instruction 
  SEI : instruction 
  STA : instruction 
  STX : instruction 
  STY : instruction 
  TAX : instruction 
  TAY : instruction 
  TSX : instruction 
  TXA : instruction 
  TXS : instruction 
  TYA : instruction

data addressing-mode : Set where
  accumulator      : addressing-mode
  immediate        : addressing-mode
  implied          : addressing-mode
  relative         : addressing-mode
  absolute         : addressing-mode
  zero-page         : addressing-mode
  indirect         : addressing-mode
  absolute-X       : addressing-mode
  absolute-Y       : addressing-mode
  zero-page-X      : addressing-mode
  zero-page-Y      : addressing-mode
  indexed-indirect : addressing-mode
  indirect-indexed : addressing-mode

parse-opcode : (w : Word 8) → Maybe (instruction × addressing-mode)
parse-opcode (∅ ○ ○ ○ ○ ○ ○ ○ ○) = just (BRK , implied)
parse-opcode (∅ ○ ○ ○ ○ ○ ○ ○ ●) = just (ORA , indexed-indirect)
parse-opcode (∅ ○ ○ ○ ○ ○ ● ○ ●) = just (ORA , zero-page)
parse-opcode (∅ ○ ○ ○ ○ ○ ● ● ○) = just (ASL , zero-page)
parse-opcode (∅ ○ ○ ○ ○ ● ○ ○ ○) = just (PHP , implied)
parse-opcode (∅ ○ ○ ○ ○ ● ○ ○ ●) = just (ORA , immediate)
parse-opcode (∅ ○ ○ ○ ○ ● ○ ● ○) = just (ASL , accumulator)
parse-opcode (∅ ○ ○ ○ ○ ● ● ○ ●) = just (ORA , absolute)
parse-opcode (∅ ○ ○ ○ ○ ● ● ● ○) = just (ASL , absolute)
parse-opcode (∅ ○ ○ ○ ● ○ ○ ○ ○) = just (BPL , relative)
parse-opcode (∅ ○ ○ ○ ● ○ ○ ○ ●) = just (ORA , indirect-indexed)
parse-opcode (∅ ○ ○ ○ ● ○ ● ○ ●) = just (ORA , zero-page-X)
parse-opcode (∅ ○ ○ ○ ● ○ ● ● ○) = just (ASL , zero-page-X)
parse-opcode (∅ ○ ○ ○ ● ● ○ ○ ○) = just (CLC , implied)
parse-opcode (∅ ○ ○ ○ ● ● ○ ○ ●) = just (ORA , absolute-Y)
parse-opcode (∅ ○ ○ ○ ● ● ● ○ ●) = just (ORA , absolute-X)
parse-opcode (∅ ○ ○ ○ ● ● ● ● ○) = just (ASL , absolute-X)
parse-opcode (∅ ○ ○ ● ○ ○ ○ ○ ○) = just (JSR , absolute)
parse-opcode (∅ ○ ○ ● ○ ○ ○ ○ ●) = just (AND , indexed-indirect)
parse-opcode (∅ ○ ○ ● ○ ○ ● ○ ○) = just (BIT , zero-page)
parse-opcode (∅ ○ ○ ● ○ ○ ● ○ ●) = just (AND , zero-page)
parse-opcode (∅ ○ ○ ● ○ ○ ● ● ○) = just (ROL , zero-page)
parse-opcode (∅ ○ ○ ● ○ ● ○ ○ ○) = just (PLP , implied)
parse-opcode (∅ ○ ○ ● ○ ● ○ ○ ●) = just (AND , immediate)
parse-opcode (∅ ○ ○ ● ○ ● ○ ● ○) = just (ROL , accumulator)
parse-opcode (∅ ○ ○ ● ○ ● ● ○ ○) = just (BIT , absolute)
parse-opcode (∅ ○ ○ ● ○ ● ● ○ ●) = just (AND , absolute)
parse-opcode (∅ ○ ○ ● ○ ● ● ● ○) = just (ROL , absolute)
parse-opcode (∅ ○ ○ ● ● ○ ○ ○ ○) = just (BMI , relative)
parse-opcode (∅ ○ ○ ● ● ○ ○ ○ ●) = just (AND , indirect-indexed)
parse-opcode (∅ ○ ○ ● ● ○ ● ○ ●) = just (AND , zero-page-X)
parse-opcode (∅ ○ ○ ● ● ○ ● ● ○) = just (ROL , zero-page-X)
parse-opcode (∅ ○ ○ ● ● ● ○ ○ ○) = just (SEC , implied)
parse-opcode (∅ ○ ○ ● ● ● ○ ○ ●) = just (AND , absolute-Y)
parse-opcode (∅ ○ ○ ● ● ● ● ○ ●) = just (AND , absolute-X)
parse-opcode (∅ ○ ○ ● ● ● ● ● ○) = just (ROL , absolute-X)
parse-opcode (∅ ○ ● ○ ○ ○ ○ ○ ○) = just (RTI , implied)
parse-opcode (∅ ○ ● ○ ○ ○ ○ ○ ●) = just (EOR , indexed-indirect)
parse-opcode (∅ ○ ● ○ ○ ○ ● ○ ●) = just (EOR , zero-page)
parse-opcode (∅ ○ ● ○ ○ ○ ● ● ○) = just (LSR , zero-page)
parse-opcode (∅ ○ ● ○ ○ ● ○ ○ ○) = just (PHA , implied)
parse-opcode (∅ ○ ● ○ ○ ● ○ ○ ●) = just (EOR , immediate)
parse-opcode (∅ ○ ● ○ ○ ● ○ ● ○) = just (LSR , accumulator)
parse-opcode (∅ ○ ● ○ ○ ● ● ○ ○) = just (JMP , absolute)
parse-opcode (∅ ○ ● ○ ○ ● ● ○ ●) = just (EOR , absolute)
parse-opcode (∅ ○ ● ○ ○ ● ● ● ○) = just (LSR , absolute)
parse-opcode (∅ ○ ● ○ ● ○ ○ ○ ○) = just (BVC , relative)
parse-opcode (∅ ○ ● ○ ● ○ ○ ○ ●) = just (EOR , indirect-indexed)
parse-opcode (∅ ○ ● ○ ● ○ ● ○ ●) = just (EOR , zero-page-X)
parse-opcode (∅ ○ ● ○ ● ○ ● ● ○) = just (LSR , zero-page-X)
parse-opcode (∅ ○ ● ○ ● ● ○ ○ ○) = just (CLI , implied)
parse-opcode (∅ ○ ● ○ ● ● ○ ○ ●) = just (EOR , absolute-Y)
parse-opcode (∅ ○ ● ○ ● ● ● ○ ●) = just (EOR , absolute-X)
parse-opcode (∅ ○ ● ○ ● ● ● ● ○) = just (LSR , absolute-X)
parse-opcode (∅ ○ ● ● ○ ○ ○ ○ ○) = just (RTS , implied)
parse-opcode (∅ ○ ● ● ○ ○ ○ ○ ●) = just (ADC , indexed-indirect)
parse-opcode (∅ ○ ● ● ○ ○ ● ○ ●) = just (ADC , zero-page)
parse-opcode (∅ ○ ● ● ○ ○ ● ● ○) = just (ROR , zero-page)
parse-opcode (∅ ○ ● ● ○ ● ○ ○ ○) = just (PLA , implied)
parse-opcode (∅ ○ ● ● ○ ● ○ ○ ●) = just (ADC , immediate)
parse-opcode (∅ ○ ● ● ○ ● ○ ● ○) = just (ROR , accumulator)
parse-opcode (∅ ○ ● ● ○ ● ● ○ ○) = just (JMP , indirect)
parse-opcode (∅ ○ ● ● ○ ● ● ○ ●) = just (ADC , absolute)
parse-opcode (∅ ○ ● ● ○ ● ● ● ○) = just (ROR , absolute-X)
parse-opcode (∅ ○ ● ● ● ○ ○ ○ ○) = just (BVS , relative)
parse-opcode (∅ ○ ● ● ● ○ ○ ○ ●) = just (ADC , indirect-indexed)
parse-opcode (∅ ○ ● ● ● ○ ● ○ ●) = just (ADC , zero-page-X)
parse-opcode (∅ ○ ● ● ● ○ ● ● ○) = just (ROR , zero-page-X)
parse-opcode (∅ ○ ● ● ● ● ○ ○ ○) = just (SEI , implied)
parse-opcode (∅ ○ ● ● ● ● ○ ○ ●) = just (ADC , absolute-Y)
parse-opcode (∅ ○ ● ● ● ● ● ○ ●) = just (ADC , absolute-X)
parse-opcode (∅ ○ ● ● ● ● ● ● ○) = just (ROR , absolute)
parse-opcode (∅ ● ○ ○ ○ ○ ○ ○ ●) = just (STA , indexed-indirect)
parse-opcode (∅ ● ○ ○ ○ ○ ● ○ ○) = just (STY , zero-page)
parse-opcode (∅ ● ○ ○ ○ ○ ● ○ ●) = just (STA , zero-page)
parse-opcode (∅ ● ○ ○ ○ ○ ● ● ○) = just (STX , zero-page)
parse-opcode (∅ ● ○ ○ ○ ● ○ ○ ○) = just (DEY , implied)
parse-opcode (∅ ● ○ ○ ○ ● ○ ● ○) = just (TXA , implied)
parse-opcode (∅ ● ○ ○ ○ ● ● ○ ○) = just (STY , absolute)
parse-opcode (∅ ● ○ ○ ○ ● ● ○ ●) = just (STA , absolute)
parse-opcode (∅ ● ○ ○ ○ ● ● ● ○) = just (STX , absolute)
parse-opcode (∅ ● ○ ○ ● ○ ○ ○ ○) = just (BCC , relative)
parse-opcode (∅ ● ○ ○ ● ○ ○ ○ ●) = just (STA , indirect-indexed)
parse-opcode (∅ ● ○ ○ ● ○ ● ○ ○) = just (STY , zero-page-X)
parse-opcode (∅ ● ○ ○ ● ○ ● ○ ●) = just (STA , zero-page-X)
parse-opcode (∅ ● ○ ○ ● ○ ● ● ○) = just (STX , zero-page-Y)
parse-opcode (∅ ● ○ ○ ● ● ○ ○ ○) = just (TYA , implied)
parse-opcode (∅ ● ○ ○ ● ● ○ ○ ●) = just (STA , absolute-Y)
parse-opcode (∅ ● ○ ○ ● ● ○ ● ○) = just (TXS , implied)
parse-opcode (∅ ● ○ ○ ● ● ● ○ ●) = just (STA , absolute-X)
parse-opcode (∅ ● ○ ● ○ ○ ○ ○ ○) = just (LDY , immediate)
parse-opcode (∅ ● ○ ● ○ ○ ○ ○ ●) = just (LDA , indexed-indirect)
parse-opcode (∅ ● ○ ● ○ ○ ○ ● ○) = just (LDX , immediate)
parse-opcode (∅ ● ○ ● ○ ○ ● ○ ○) = just (LDY , zero-page)
parse-opcode (∅ ● ○ ● ○ ○ ● ○ ●) = just (LDA , zero-page)
parse-opcode (∅ ● ○ ● ○ ○ ● ● ○) = just (LDX , zero-page)
parse-opcode (∅ ● ○ ● ○ ● ○ ○ ○) = just (TAY , implied)
parse-opcode (∅ ● ○ ● ○ ● ○ ○ ●) = just (LDA , immediate)
parse-opcode (∅ ● ○ ● ○ ● ○ ● ○) = just (TAX , implied)
parse-opcode (∅ ● ○ ● ○ ● ● ○ ○) = just (LDY , absolute)
parse-opcode (∅ ● ○ ● ○ ● ● ○ ●) = just (LDA , absolute)
parse-opcode (∅ ● ○ ● ○ ● ● ● ○) = just (LDX , absolute)
parse-opcode (∅ ● ○ ● ● ○ ○ ○ ○) = just (BCS , relative)
parse-opcode (∅ ● ○ ● ● ○ ○ ○ ●) = just (LDA , indirect-indexed)
parse-opcode (∅ ● ○ ● ● ○ ● ○ ○) = just (LDY , zero-page-X)
parse-opcode (∅ ● ○ ● ● ○ ● ○ ●) = just (LDA , zero-page-X)
parse-opcode (∅ ● ○ ● ● ○ ● ● ○) = just (LDX , zero-page-Y)
parse-opcode (∅ ● ○ ● ● ● ○ ○ ○) = just (CLV , implied)
parse-opcode (∅ ● ○ ● ● ● ○ ○ ●) = just (LDA , absolute-Y)
parse-opcode (∅ ● ○ ● ● ● ○ ● ○) = just (TSX , implied)
parse-opcode (∅ ● ○ ● ● ● ● ○ ○) = just (LDY , absolute-X)
parse-opcode (∅ ● ○ ● ● ● ● ○ ●) = just (LDA , absolute-X)
parse-opcode (∅ ● ○ ● ● ● ● ● ○) = just (LDX , absolute-Y)
parse-opcode (∅ ● ● ○ ○ ○ ○ ○ ○) = just (CPY , immediate)
parse-opcode (∅ ● ● ○ ○ ○ ○ ○ ●) = just (CMP , indexed-indirect)
parse-opcode (∅ ● ● ○ ○ ○ ● ○ ○) = just (CPY , zero-page)
parse-opcode (∅ ● ● ○ ○ ○ ● ○ ●) = just (CMP , zero-page)
parse-opcode (∅ ● ● ○ ○ ○ ● ● ○) = just (DEC , zero-page)
parse-opcode (∅ ● ● ○ ○ ● ○ ○ ○) = just (INY , implied)
parse-opcode (∅ ● ● ○ ○ ● ○ ○ ●) = just (CMP , immediate)
parse-opcode (∅ ● ● ○ ○ ● ○ ● ○) = just (DEX , implied)
parse-opcode (∅ ● ● ○ ○ ● ● ○ ○) = just (CPY , absolute)
parse-opcode (∅ ● ● ○ ○ ● ● ○ ●) = just (CMP , absolute)
parse-opcode (∅ ● ● ○ ○ ● ● ● ○) = just (DEC , absolute)
parse-opcode (∅ ● ● ○ ● ○ ○ ○ ○) = just (BNE , relative)
parse-opcode (∅ ● ● ○ ● ○ ○ ○ ●) = just (CMP , indirect-indexed)
parse-opcode (∅ ● ● ○ ● ○ ● ○ ●) = just (CMP , zero-page-X)
parse-opcode (∅ ● ● ○ ● ○ ● ● ○) = just (DEC , zero-page-X)
parse-opcode (∅ ● ● ○ ● ● ○ ○ ○) = just (CLD , implied)
parse-opcode (∅ ● ● ○ ● ● ○ ○ ●) = just (CMP , absolute-Y)
parse-opcode (∅ ● ● ○ ● ● ● ○ ●) = just (CMP , absolute-X)
parse-opcode (∅ ● ● ○ ● ● ● ● ○) = just (DEC , absolute-X)
parse-opcode (∅ ● ● ● ○ ○ ○ ○ ○) = just (CPX , immediate)
parse-opcode (∅ ● ● ● ○ ○ ○ ○ ●) = just (SBC , indexed-indirect)
parse-opcode (∅ ● ● ● ○ ○ ● ○ ○) = just (CPX , zero-page)
parse-opcode (∅ ● ● ● ○ ○ ● ○ ●) = just (SBC , zero-page)
parse-opcode (∅ ● ● ● ○ ○ ● ● ○) = just (INC , zero-page)
parse-opcode (∅ ● ● ● ○ ● ○ ○ ○) = just (INX , implied)
parse-opcode (∅ ● ● ● ○ ● ○ ○ ●) = just (SBC , immediate)
parse-opcode (∅ ● ● ● ○ ● ○ ● ○) = just (NOP , implied)
parse-opcode (∅ ● ● ● ○ ● ● ○ ○) = just (CPX , absolute)
parse-opcode (∅ ● ● ● ○ ● ● ○ ●) = just (SBC , absolute)
parse-opcode (∅ ● ● ● ○ ● ● ● ○) = just (INC , absolute)
parse-opcode (∅ ● ● ● ● ○ ○ ○ ○) = just (BEQ , relative)
parse-opcode (∅ ● ● ● ● ○ ○ ○ ●) = just (SBC , indirect-indexed)
parse-opcode (∅ ● ● ● ● ○ ● ○ ●) = just (SBC , zero-page-X)
parse-opcode (∅ ● ● ● ● ○ ● ● ○) = just (INC , zero-page-X)
parse-opcode (∅ ● ● ● ● ● ○ ○ ○) = just (SED , implied)
parse-opcode (∅ ● ● ● ● ● ○ ○ ●) = just (SBC , absolute-Y)
parse-opcode (∅ ● ● ● ● ● ● ○ ●) = just (SBC , absolute-X)
parse-opcode (∅ ● ● ● ● ● ● ● ○) = just (INC , absolute-X)
parse-opcode _ = nothing

--------------------------------------------------------------------------------

{-
The first argument should be true if this operation only *reads* memory, and does not write it.
This is necessary because some addressing modes behave differently in that case.

Terminology (taken from Appendix A of http://archive.6502.org/books/mcs6500_family_hardware_manual.pdf)
  BAL, BAH = base address (for indirect operations)
  ADL, ADH = address
-}
effective-address : Bool → addressing-mode → State → CyclesBuilder (Word 16)
effective-address _ immediate s continuation =
  continuation $ increment (+ 1) $ State.program-counter s
effective-address _ absolute s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL → just $ 
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ ADH → just $ 
  continuation $ concat (ADL , ADH)
effective-address _ zero-page s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL → just $ 
  continuation $ concat (ADL , op₀ false)
effective-address _ indirect s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ IAL → just $ 
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ IAH → just $
  suc $ read (concat (IAL , IAH)) $ λ ADL → just $ 
  suc $ read (concat (increment (+ 1) IAL , IAH)) $ λ ADH → just $
  continuation $ concat (ADL , ADH)
effective-address read-only absolute-X s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL → just $
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ BAH →
  let (ADL , carry) = add-with-carry false BAL $ State.register-X s in
  flip Maybe.map (bool-from-bit carry) $ λ carry →
  Bool.if carry Bool.∨ Bool.not read-only then (
    suc $ read (concat (ADL , BAH)) $ λ _ → just $
    continuation $ concat (ADL , (Bool.if carry then increment (+ 1) BAH else BAH))
  ) else (
    continuation $ concat (ADL , BAH)
  )
effective-address read-only absolute-Y s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL → just $
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ BAH →
  let (ADL , carry) = add-with-carry false BAL $ State.register-Y s in
  flip Maybe.map (bool-from-bit carry) $ λ carry →
  Bool.if carry Bool.∨ Bool.not read-only then (
    suc $ read (concat (ADL , BAH)) $ λ _ → just $
    continuation $ concat (ADL , (Bool.if carry then increment (+ 1) BAH else BAH))
  ) else (
    continuation $ concat (ADL , BAH)
  )
effective-address _ zero-page-X s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL → just $
  suc $ read (concat (BAL , op₀ false)) $ λ _ → just $
  let BAL+X = add BAL $ State.register-X s in
  continuation $ concat (BAL+X , op₀ false)
effective-address _ zero-page-Y s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL → just $
  suc $ read (concat (BAL , op₀ false)) $ λ _ → just $
  let BAL+Y = add BAL $ State.register-Y s in
  continuation $ concat (BAL+Y , op₀ false)
effective-address _ indexed-indirect s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL → just $
  suc $ read (concat (BAL , op₀ false)) $ λ _ → just $
  let BAL+X = add BAL $ State.register-X s in
  suc $ read (concat (BAL+X , op₀ false)) $ λ ADL → just $
  suc $ read (concat (increment (+ 1) BAL+X , op₀ false)) $ λ ADH → just $
  continuation $ concat (ADL , ADH)
effective-address read-only indirect-indexed s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ IAL → just $
  suc $ read (concat (IAL , op₀ false)) $ λ BAL → just $
  suc $ read (concat (increment (+ 1) IAL , op₀ false)) $ λ BAH →
  let (ADL , carry) = add-with-carry false BAL $ State.register-Y s in
  flip Maybe.map (bool-from-bit carry) $ λ carry →
  Bool.if carry Bool.∨ Bool.not read-only then (
    suc $ read (concat (ADL , BAH)) $ λ _ → just $
    continuation $ concat (ADL , (Bool.if carry then increment (+ 1) BAH else BAH))
  ) else (
    continuation $ concat (ADL , BAH)
  )

-- These modes don't really produce addresses, so I'll error out.
effective-address _ accumulator s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) (λ _ → nothing)
effective-address _ implied s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) (λ _ → nothing)
-- I handle this case separately, so I'll error here too.
effective-address _ relative s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) (λ _ → nothing)


--------------------------------------------------------------------------------

mode-length : addressing-mode → ℕ
mode-length accumulator = 1
mode-length immediate = 2
mode-length implied = 1
mode-length relative = 2
mode-length absolute = 3
mode-length zero-page = 2
mode-length indirect = 3
mode-length absolute-X = 3
mode-length absolute-Y = 3
mode-length zero-page-X = 2
mode-length zero-page-Y = 2
mode-length indexed-indirect = 2
mode-length indirect-indexed = 2

inc-pc : addressing-mode → State → State
inc-pc mode s = record s {program-counter = increment (+ mode-length mode) $ State.program-counter s}

execute-read-op : (State × Word 8 → Maybe State) → addressing-mode → State → Cycles State
execute-read-op f mode s =
  effective-address Bool.true mode s $ λ addr →
  suc $ read addr $ λ w →
  Maybe.map zero $ f (inc-pc mode s , w)

execute-write-op : (State → State × Word 8) → addressing-mode → State → Cycles State
execute-write-op f mode s =
  effective-address Bool.false mode s $ λ addr →
  let (s , w) = f (inc-pc mode s) in
  suc $ write addr w $
  zero $ s

execute-modify-op : (State × Word 8 → State × Word 8) → addressing-mode → State → Cycles State
execute-modify-op f accumulator s =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ w → just $
  let (s , w) = f (inc-pc accumulator s , w) in
  zero $ record s {register-A = w}
execute-modify-op f mode s =
  effective-address Bool.false mode s $ λ addr →
  suc $ read addr $ λ w → just $
  suc $ write addr w $
  let (s , w) = f (inc-pc mode s , w) in
  suc $ write addr w $
  zero $ s

execute-non-memory-op : (State → State) → addressing-mode → State → Cycles State
execute-non-memory-op f mode s =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $
  zero $ f (inc-pc mode s)

execute-branch : (State → Bit) → State → Cycles State
execute-branch cond s =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ offset →
  bool-from-bit (cond s) Maybe.>>= λ cond →
  Bool.if cond
  then (
    let
      (PCL , PCH) = split (increment (+ 2) $ State.program-counter s)
      (ADL , carry) = add-with-carry false PCL offset
    in
    bool-from-bit carry Maybe.>>= λ carry →
    bool-from-bit (bit offset 7) Maybe.>>= λ backwards →
    let
      page-change = Data.Integer._-_ (Bool.if carry then + 1 else + 0) (Bool.if backwards then + 1 else + 0)
      next-instruction = concat (ADL , increment page-change PCH)
    in just $
    suc $ read (increment (+ 2) $ State.program-counter s) $ λ _ → just $
    Bool.if (does $ Data.Integer._≟_ page-change (+ 0))
    then (
      zero $ record s { program-counter = next-instruction }
    ) else (
      suc $ read (concat (ADL , PCH)) $ λ _ → just $
      zero $ record s { program-counter = next-instruction }
    )
  ) else just (
    zero $ record s { program-counter = increment (+ 2) $ State.program-counter s }
  )

--------------------------------------------------------------------------------

set-flags : (Flags → Flags) → State → State
set-flags f s =
  record s {
    flags = f (State.flags s)
  }

setZN : Word 8 → State → State
setZN w = set-flags $ λ flags →
    record flags {
      Z = w ≡ᵇ op₀ false;
      N = bit w 7
    }

run_instruction : instruction → addressing-mode → State → Cycles State
run ADC instruction = execute-read-op $ λ (s , num₁) →
  let
    num₀ = State.register-A s
    (binary-sum , binary-carry) = add-with-carry (Flags.C $ State.flags s) num₀ num₁
  in
  bool-from-bit (Flags.D $ State.flags s) Maybe.>>= λ decimal-mode →
  Bool.if decimal-mode
  then (
    -- This code is intended to simulate the 6502's behavior,
    -- even in cases where the operands aren't valid BCD numbers.
    -- I hope I did this right; someone familiar with the 6502's internals should check this.
    let
      (lo₀ , hi₀) = split {4} num₀
      (lo₁ , hi₁) = split {4} num₁

      (lo , carry-mid) = add-with-carry (Flags.C $ State.flags s) lo₀ lo₁
      (lo-minus-10 , no-decimal-carry) = sub-with-inverted-borrow true lo (∅ ● ○ ● ○)
    in bool-from-bit no-decimal-carry Maybe.>>= λ no-decimal-carry → let
      (lo , carry-mid) = Bool.if no-decimal-carry then (lo , carry-mid) else (lo-minus-10 , true)

      (hi , carry-out) = add-with-carry carry-mid hi₀ hi₁
      (hi-minus-10 , no-decimal-carry) = sub-with-inverted-borrow true hi (∅ ● ○ ● ○)
    in bool-from-bit no-decimal-carry Maybe.>>= λ no-decimal-carry → let
      (hi , carry-out) = Bool.if no-decimal-carry then (hi , carry-out) else (hi-minus-10 , true)
    in just $ record s {
      register-A = concat (lo , hi);
      flags = record (State.flags s) {
        C = carry-out;
        Z = binary-sum ≡ᵇ op₀ false;
        N = bit hi 3;
        V = (bit hi₀ 3 ∧ bit hi₁ 3 ∧ not (bit hi 3)) ∨ (not (bit hi₀ 3) ∧ not (bit hi₁ 3) ∧ bit hi 3)
      }
    }
  ) else (
    just $ record s {
      register-A = binary-sum;
      flags = record (State.flags s) {
        C = binary-carry;
        Z = binary-sum ≡ᵇ op₀ false;
        N = bit binary-sum 7;
        V = (bit num₀ 7 ∧ bit num₁ 7 ∧ not (bit binary-sum 7))
          ∨ (not (bit num₀ 7) ∧ not (bit num₁ 7) ∧ bit binary-sum 7)
      }
    }
  )
run AND instruction = execute-read-op $ \(s , w) → just $
  let w = op₂ _∧_ w (State.register-A s) in
  record (setZN w s) {register-A = w}
run ASL instruction = execute-modify-op $ λ (s , w) →
  let (w , carry) = pop-high (push-low (false , w)) in
  (set-flags (λ flags → record flags {C = carry}) (setZN w s) , w)
run BCC instruction = λ _ → execute-branch $ λ s → not (Flags.C (State.flags s))
run BCS instruction = λ _ → execute-branch $ λ s → Flags.C (State.flags s)
run BEQ instruction = λ _ → execute-branch $ λ s → Flags.Z (State.flags s)
run BIT instruction = execute-read-op $ \(s , w) → just $
  record s {
    flags = record (State.flags s) {
      N = bit w 7;
      V = bit w 6;
      Z = op₂ _∧_ w (State.register-A s) ≡ᵇ op₀ false
    }
  }
run BMI instruction = λ _ → execute-branch $ λ s → Flags.N (State.flags s)
run BNE instruction = λ _ → execute-branch $ λ s → not (Flags.Z (State.flags s))
run BPL instruction = λ _ → execute-branch $ λ s → Flags.N (State.flags s)
run BRK instruction = λ _ s →
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $
  let (PCL , PCH) = split $ increment (+ 2) $ State.program-counter s in
  suc $ write (concat (                   State.stack-pointer s  , op₀ false ●)) PCH $
  suc $ write (concat (increment (- + 1) (State.stack-pointer s) , op₀ false ●)) PCL $
  suc $ write (concat (increment (- + 2) (State.stack-pointer s) , op₀ false ●)) (byte-from-flags $ State.flags s) $
  suc $ read (op₀ true ○) $ λ ADL → just $
  suc $ read (op₀ true ●) $ λ ADH → just $
  zero $ record s {
    stack-pointer = increment (- + 3) $ State.stack-pointer s;
    program-counter = concat (ADL , ADH);
    flags = record (State.flags s) {I = true}
  }
run BVC instruction = λ _ → execute-branch $ λ s → not (Flags.V (State.flags s))
run BVS instruction = λ _ → execute-branch $ λ s → Flags.V (State.flags s)
run CLC instruction = execute-non-memory-op $ set-flags $ λ flags → record flags {C = false}
run CLD instruction = execute-non-memory-op $ set-flags $ λ flags → record flags {D = false}
run CLI instruction = execute-non-memory-op $ set-flags $ λ flags → record flags {I = false}
run CLV instruction = execute-non-memory-op $ set-flags $ λ flags → record flags {V = false}
run CMP instruction = execute-read-op $ \(s , w) → just $
  let (w , inv-borrow) = sub-with-inverted-borrow true (State.register-A s) w in
  set-flags (λ flags → record flags {C = inv-borrow}) (setZN w s)
run CPX instruction = execute-read-op $ \(s , w) → just $
  let (w , inv-borrow) = sub-with-inverted-borrow true (State.register-X s) w in
  set-flags (λ flags → record flags {C = inv-borrow}) (setZN w s)
run CPY instruction = execute-read-op $ \(s , w) → just $
  let (w , inv-borrow) = sub-with-inverted-borrow true (State.register-Y s) w in
  set-flags (λ flags → record flags {C = inv-borrow}) (setZN w s)
run DEC instruction = execute-modify-op $ λ (s , w) → let w = increment (- + 1) w in (setZN w s , w)
run DEX instruction = execute-non-memory-op $ λ s →
  let w = increment (- + 1) $ State.register-X s in record (setZN w s) {register-X = w}
run DEY instruction = execute-non-memory-op $ λ s →
  let w = increment (- + 1) $ State.register-Y s in record (setZN w s) {register-Y = w}
run EOR instruction = execute-read-op $ \(s , w) → just $
  let w = op₂ _xor_ w (State.register-A s) in
  record (setZN w s) {register-A = w}
run INC instruction = execute-modify-op $ λ (s , w) → let w = increment (+ 1) w in (setZN w s , w)
run INX instruction = execute-non-memory-op $ λ s →
  let w = increment (+ 1) $ State.register-X s in record (setZN w s) {register-X = w}
run INY instruction = execute-non-memory-op $ λ s →
  let w = increment (+ 1) $ State.register-Y s in record (setZN w s) {register-Y = w}
run JMP instruction = λ mode s →
  effective-address Bool.true mode s $ λ addr →
  zero $ record s {program-counter = addr}
run JSR instruction = λ mode s →
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL → just $
  suc $ read (concat (State.stack-pointer s , op₀ false ●)) $ λ _ → just $
  let (PCL , PCH) = split $ increment (+ 2) $ State.program-counter s in
  suc $ write (concat (State.stack-pointer s , op₀ false ●)) PCH $
  suc $ write (concat (increment (- + 1) (State.stack-pointer s) , op₀ false ●)) PCL $
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ ADH → just $
  zero $ record s {
    stack-pointer = increment (- + 2) $ State.stack-pointer s;
    program-counter = concat (ADL , ADH)
  }
run LDA instruction = execute-read-op $ \(s , w) → just $ record (setZN w s) {register-A = w}
run LDX instruction = execute-read-op $ \(s , w) → just $ record (setZN w s) {register-X = w}
run LDY instruction = execute-read-op $ \(s , w) → just $ record (setZN w s) {register-Y = w}
run LSR instruction = execute-modify-op $ λ (s , w) →
  let (carry , w) = pop-low (push-high (w , false)) in
  (set-flags (λ flags → record flags {C = carry}) (setZN w s) , w)
run NOP instruction = execute-non-memory-op $ λ s → s
run ORA instruction = execute-read-op $ \(s , w) → just $
  let w = op₂ _∨_ w (State.register-A s) in
  record (setZN w s) {register-A = w}
run PHA instruction = λ _ s →
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $
  suc $ write (concat (State.stack-pointer s , op₀ false ●))
    (State.register-A s) $
  zero $ record s {
    stack-pointer = increment (- + 1) $ State.stack-pointer s;
    program-counter = increment (+ 1) $ State.program-counter s
  }
run PHP instruction = λ _ s →
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $
  suc $ write (concat (State.stack-pointer s , op₀ false ●))
    (byte-from-flags $ State.flags s) $
  zero $ record s {
    stack-pointer = increment (- + 1) $ State.stack-pointer s;
    program-counter = increment (+ 1) $ State.program-counter s
  }
run PLA instruction = λ _ s →
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $
  suc $ read (concat (                 State.stack-pointer s  , op₀ false ●)) $ λ _ → just $
  suc $ read (concat (increment (+ 1) (State.stack-pointer s) , op₀ false ●)) $ λ w → just $
  zero $ record (setZN w s) {
    stack-pointer = increment (+ 1) $ State.stack-pointer s;
    register-A = w;
    program-counter = increment (+ 1) $ State.program-counter s
  }
run PLP instruction = λ _ s →
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $
  suc $ read (concat (                 State.stack-pointer s  , op₀ false ●)) $ λ _ → just $
  suc $ read (concat (increment (+ 1) (State.stack-pointer s) , op₀ false ●)) $ λ w → just $
  zero $ record s {
    stack-pointer = increment (+ 1) $ State.stack-pointer s;
    flags = flags-from-byte w;
    program-counter = increment (+ 1) $ State.program-counter s
  }
run ROL instruction = execute-modify-op $ λ (s , w) →
  let (w , carry) = pop-high (push-low (Flags.C (State.flags s) , w)) in
  (set-flags (λ flags → record flags {C = carry}) (setZN w s) , w)
run ROR instruction = execute-modify-op $ λ (s , w) →
  let (carry , w) = pop-low (push-high (w , Flags.C (State.flags s))) in
  (set-flags (λ flags → record flags {C = carry}) (setZN w s) , w)
run RTI instruction = λ _ s →
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $
  suc $ read (concat (                 State.stack-pointer s  , op₀ false ●)) $ λ _ → just $
  suc $ read (concat (increment (+ 1) (State.stack-pointer s) , op₀ false ●)) $ λ P → just $
  suc $ read (concat (increment (+ 2) (State.stack-pointer s) , op₀ false ●)) $ λ PCL → just $
  suc $ read (concat (increment (+ 3) (State.stack-pointer s) , op₀ false ●)) $ λ PCH → just $
  zero $ record s {
    stack-pointer = increment (+ 3) $ State.stack-pointer s;
    flags = flags-from-byte P;
    program-counter = concat (PCL , PCH)
  }
run RTS instruction = λ _ s →
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $
  suc $ read (concat (                 State.stack-pointer s  , op₀ false ●)) $ λ _ → just $
  suc $ read (concat (increment (+ 1) (State.stack-pointer s) , op₀ false ●)) $ λ PCL → just $
  suc $ read (concat (increment (+ 2) (State.stack-pointer s) , op₀ false ●)) $ λ PCH → just $
  suc $ read (concat (PCL , PCH)) $ λ _ → just $
  zero $ record s {
    stack-pointer = increment (+ 2) $ State.stack-pointer s;
    program-counter = increment (+ 1) $ concat (PCL , PCH)
  }
run SBC instruction = execute-read-op $ λ (s , num₁) →
  let
    num₀ = State.register-A s
    (binary-difference , binary-inv-borrow) = sub-with-inverted-borrow (Flags.C $ State.flags s) num₀ num₁
    flags =
      record (State.flags s) {
        C = binary-inv-borrow;
        Z = binary-difference ≡ᵇ op₀ false;
        N = bit binary-difference 7;
        V = (bit num₀ 7 ∧ not (bit num₁ 7) ∧ not (bit binary-difference 7))
          ∨ (not (bit num₀ 7) ∧ bit num₁ 7 ∧ bit binary-difference 7)
      }
  in
  bool-from-bit (Flags.D $ State.flags s) Maybe.>>= λ decimal-mode →
  Bool.if decimal-mode
  then (
    -- This code is intended to simulate the 6502's behavior,
    -- even in cases where the operands aren't valid BCD numbers.
    -- I hope I did this right; someone familiar with the 6502's internals should check this.
    let
      (lo₀ , hi₀) = split {4} num₀
      (lo₁ , hi₁) = split {4} num₁

      (lo , inv-borrow-mid) = sub-with-inverted-borrow (Flags.C $ State.flags s) lo₀ lo₁
      (hi , inv-borrow-out) = sub-with-inverted-borrow inv-borrow-mid hi₀ hi₁
    in
    bool-from-bit inv-borrow-mid Maybe.>>= λ inv-borrow-mid →
    bool-from-bit inv-borrow-out Maybe.>>= λ inv-borrow-out →
    let
      lo = Bool.if inv-borrow-mid then lo else add lo (∅ ● ○ ● ○)

      hi = Bool.if inv-borrow-out then hi else add hi (∅ ● ○ ● ○)
    in just $ record s {
      register-A = concat (lo , hi);
      flags = flags
    }
  ) else (
    just $ record s {
      register-A = binary-difference;
      flags = flags
    }
  )
run SEC instruction = execute-non-memory-op $ set-flags $ λ flags → record flags {C = false}
run SED instruction = execute-non-memory-op $ set-flags $ λ flags → record flags {D = false}
run SEI instruction = execute-non-memory-op $ set-flags $ λ flags → record flags {I = false}
run STA instruction = execute-write-op $ \s → (s , State.register-A s)
run STX instruction = execute-write-op $ \s → (s , State.register-X s)
run STY instruction = execute-write-op $ \s → (s , State.register-Y s)
run TAX instruction = execute-non-memory-op $ λ s → record (setZN (State.register-A s) s) {register-X = State.register-A s}
run TAY instruction = execute-non-memory-op $ λ s → record (setZN (State.register-A s) s) {register-Y = State.register-A s}
run TSX instruction = execute-non-memory-op $ λ s → record (setZN (State.stack-pointer s) s) {register-X = State.stack-pointer s}
run TXA instruction = execute-non-memory-op $ λ s → record (setZN (State.register-X s) s) {register-A = State.register-X s}
run TXS instruction = execute-non-memory-op $ λ s → record s {stack-pointer = State.register-X s}
run TYA instruction = execute-non-memory-op $ λ s → record (setZN (State.register-Y s) s) {register-A = State.register-Y s}

--------------------------------------------------------------------------------

-- Given a state, run one instruction.
-- If the final cycle fetches the next instruction, return one step early.
step : State -> Cycle (Cycles State)
step s = read (State.program-counter s) $
  Maybe.map (λ (instr , mode) → run_instruction instr mode s) ∘′ parse-opcode

--------------------------------------------------------------------------------

full-state : Set
full-state = Cycles State

-- One cycle at a time.
cycle : full-state -> Cycle full-state
cycle (zero x) = step x
cycle (suc x) = x