module Word where
open import Word.Base public
-- TODO: Word.Properties

module Word.Base where
open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Bool as Bool using (Bool; true; false; if_then_else_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Unit using (⊤)
open import Data.Nat using (ℕ; zero; suc; _<ᵇ_; _+_; _*_)
open import Data.Integer using (ℤ; _%ℕ_; _/ℕ_)
open import Relation.Nullary using (does)
--------------------------------------------------------------------------------
data Word : ℕ → Set where
  ∅ : Word 0
  push-low : {n : ℕ} → Bool × Word n → Word (suc n)
pattern _● w = push-low (true , w)
pattern _○ w = push-low (false , w)
--------------------------------------------------------------------------------
pop-low : {n : ℕ} → Word (suc n) → Bool × Word n
pop-low (push-low x) = x
push-high : {n : ℕ} → Word n × Bool → Word (suc n)
push-high (∅ , b) = push-low (b , ∅)
push-high (push-low (b₁ , w) , b₂) = push-low (b₁ , push-high (w , b₂))
pop-high : {n : ℕ} → Word (suc n) → Word n × Bool
pop-high {0} (push-low (b , ∅)) = (∅ , b)
pop-high {suc n} (push-low (b₁ , w)) = let (w , b₂) = pop-high w in (push-low (b₁ , w) , b₂)
--------------------------------------------------------------------------------
bit : {n : ℕ} → Word n → (i : ℕ) → {{Bool.T (i <ᵇ n)}} → Bool
bit (push-low (b , w)) zero = b
bit (push-low (b , w)) (suc i) {{pf}} = bit w i {{pf}}
--------------------------------------------------------------------------------
_≡ᵇ_ : {n : ℕ} → Word n → Word n → Bool
∅ ≡ᵇ ∅ = true
push-low (b₀ , w₀) ≡ᵇ push-low (b₁ , w₁) = (does (Bool._≟_ b₀ b₁) ) Bool.∧ (w₀ ≡ᵇ w₁)
--------------------------------------------------------------------------------
op₀ : {n : ℕ} → Bool → Word n
op₁ : {n : ℕ} → (Bool → Bool) → (Word n → Word n)
op₂ : {n : ℕ} → (Bool → Bool → Bool) → (Word n → Word n → Word n)
op₀ {zero} f = ∅
op₀ {suc n} f = push-low (f , op₀ f)
op₁ f ∅ = ∅
op₁ f (push-low (b₀ , w₀)) = push-low (f b₀ , op₁ f w₀)
op₂ f ∅ ∅ = ∅
op₂ f (push-low (b₀ , w₀)) (push-low (b₁ , w₁)) = push-low (f b₀ b₁ , op₂ f w₀ w₁)
--------------------------------------------------------------------------------
concat : {m n : ℕ} → Word m × Word n → Word (m + n)
concat (∅ , w₁) = w₁
concat (push-low (b , w₀) , w₁) = push-low (b , concat (w₀ , w₁))
split : {m n : ℕ} → Word (m + n) → Word m × Word n
split {zero} w = (∅ , w)
split {suc m} (push-low (b , w)) = let (w₀ , w₁) = split w in (push-low (b , w₀) , w₁)
--------------------------------------------------------------------------------
word-from-int : {n : ℕ} → ℤ → Word n
word-from-int {zero} _ = ∅
word-from-int {suc n} x = push-low ((Data.Nat._≟_ (x %ℕ 2) 0).does , word-from-int (x /ℕ 2))
nat-from-word : {n : ℕ} → Word n → ℕ
nat-from-word ∅ = 0
nat-from-word (push-low (b , w)) = (if b then 1 else 0) + 2 * nat-from-word w
--------------------------------------------------------------------------------
full-adder : Bool → Bool → Bool → Bool × Bool
full-adder false false false = (false , false)
full-adder false false  true = ( true , false)
full-adder false  true false = ( true , false)
full-adder false  true  true = (false ,  true)
full-adder  true false false = ( true , false)
full-adder  true false  true = (false ,  true)
full-adder  true  true false = (false ,  true)
full-adder  true  true  true = ( true ,  true)
add-with-carry : {n : ℕ} → Bool → Word n → Word n → Word n × Bool
add-with-carry carry ∅ ∅ = (∅ , carry)
add-with-carry carry-in (push-low (b₀ , w₀)) (push-low (b₁ , w₁)) =
  let
    (b₂ , carry) = full-adder carry-in b₀ b₁
    (w₂ , carry-out) = add-with-carry carry w₀ w₁
  in (push-low (b₂ , w₂) , carry-out)
sub-with-inverted-borrow : {n : ℕ} → Bool → Word n → Word n → Word n × Bool
sub-with-inverted-borrow inverted-borrow w₀ w₁ = add-with-carry inverted-borrow w₀ (op₁ Bool.not w₁)
--------------------------------------------------------------------------------
add : {n : ℕ} → Word n → Word n → Word n
add w₀ w₁ = proj₁ (add-with-carry false w₀ w₁)
increment : {n : ℕ} → ℤ → Word n → Word n
increment n w = add (word-from-int n) w
--------------------------------------------------------------------------------

module 6502-Processor where
open import Data.Bool using (Bool; true; false; if_then_else_; _∧_; _∨_; not)
open import Data.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 (_∘′_; _$_)
open import Relation.Nullary using (does)
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 : if r/w then (Word 8 → Maybe s) else (Word 8 × s)
read : {s : Set} → Word 16 → (Word 8 → s) → Cycle s
read addr continuation =
  record {
    addr = addr;
    r/w = true;
    continuation = just ∘′ continuation
  }
write : {s : Set} → Word 16 → Word 8 → s → Cycle s
write addr w continuation =
  record {
    addr = addr;
    r/w = false;
    continuation = (w , 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)
-}
data Cycles : Set → Set where
  zero : {s : Set} → s → Cycles s
  suc : {s : Set} → Cycle (Cycles s) → Cycles s
{-
_>>=_ : {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)
-}
CyclesBuilder : Set → Set₁
CyclesBuilder a = {b : Set} → (a → Cycles b) → Cycles b
--------------------------------------------------------------------------------
record Flags : Set where
  field
    N : Bool
    V : Bool
    D : Bool
    I : Bool
    Z : Bool
    C : Bool
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
--------------------------------------------------------------------------------
fetch-opcode : Word 16 → CyclesBuilder (instruction × addressing-mode)
fetch-opcode pc continuation =
  suc (record {
    addr = pc;
    r/w = true;
    continuation = Data.Maybe.map continuation ∘′ parse-opcode
  })
{-
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 →
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ ADH →
  continuation $ concat (ADL , ADH)
effective-address _ zero-page s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL →
  continuation $ concat (ADL , op₀ false)
effective-address _ indirect s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ IAL →
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ IAH →
  suc $ read (concat (IAL , IAH)) $ λ ADL →
  suc $ read (concat (increment (+ 1) IAL , IAH)) $ λ ADH →
  continuation $ concat (ADL , ADH)
effective-address read-only absolute-X s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL →
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ BAH →
  let (ADL , carry) = add-with-carry false BAL $ State.register-X s in
  if carry ∨ not read-only then (
    suc $ read (concat (ADL , BAH)) $ λ _ →
    continuation $ concat (ADL , (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 →
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ BAH →
  let (ADL , carry) = add-with-carry false BAL $ State.register-Y s in
  if carry ∨ not read-only then (
    suc $ read (concat (ADL , BAH)) $ λ _ →
    continuation $ concat (ADL , (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 →
  suc $ read (concat (BAL , op₀ false)) $ λ _ →
  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 →
  suc $ read (concat (BAL , op₀ false)) $ λ _ →
  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 →
  suc $ read (concat (BAL , op₀ false)) $ λ _ →
  let BAL+X = add BAL $ State.register-X s in
  suc $ read (concat (BAL+X , op₀ false)) $ λ ADL →
  suc $ read (concat (increment (+ 1) BAL+X , op₀ false)) $ λ ADH →
  continuation $ concat (ADL , ADH)
effective-address read-only indirect-indexed s continuation =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ IAL →
  suc $ read (concat (IAL , op₀ false)) $ λ BAL →
  suc $ read (concat (increment (+ 1) IAL , op₀ false)) $ λ BAH →
  let (ADL , carry) = add-with-carry false BAL $ State.register-Y s in
  if carry ∨ not read-only then (
    suc $ read (concat (ADL , BAH)) $ λ _ →
    continuation $ concat (ADL , (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 (record {addr = increment (+ 1) $ State.program-counter s; r/w = true; continuation = λ _ → nothing})
effective-address _ implied s continuation =
  suc (record {addr = increment (+ 1) $ State.program-counter s; r/w = true; continuation = λ _ → nothing})
-- I handle this case separately, so I'll error here too.
effective-address _ relative s continuation =
  suc (record {addr = increment (+ 1) $ State.program-counter s; r/w = true; continuation = λ _ → 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 → State) → addressing-mode → State → Cycles State
execute-read-op f mode s =
  effective-address true mode s $ λ addr →
  suc $ read addr $ λ w →
  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 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 →
  let (s , w) = f (inc-pc accumulator s , w) in
  zero $ record s {register-A = w}
execute-modify-op f mode s =
  effective-address false mode s $ λ addr →
  suc $ read addr $ λ w →
  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) $ λ _ →
  zero $ f (inc-pc mode s)
execute-branch : (State → Bool) → State → Cycles State
execute-branch cond s =
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ offset →
  if cond s
  then (
    suc $ read (increment (+ 2) $ State.program-counter s) $ λ _ →
    let
      (PCL , PCH) = split (increment (+ 2) $ State.program-counter s)
      (ADL , carry) = add-with-carry false PCL offset
      page-change = Data.Integer._-_ (if carry then + 1 else + 0) (if bit offset 7 then + 1 else + 0)
      next-instruction = concat (ADL , increment page-change PCH)
    in if (does $ Data.Integer._≟_ page-change (+ 0))
    then (
      zero $ record s { program-counter = next-instruction }
    ) else (
      suc $ read (concat (ADL , PCH)) $ λ _ →
      zero $ record s { program-counter = next-instruction }
    )
  ) else (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 if Flags.D $ State.flags s
  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 (∅ ● ○ ● ○)
      (lo , carry-mid) = 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 (∅ ● ○ ● ○)
      (hi , carry-out) = if no-decimal-carry then (hi , carry-out) else (hi-minus-10 , true)
    in 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 (
    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) →
  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) →
  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) $ λ _ →
  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 →
  suc $ read (op₀ true ●) $ λ ADH →
  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) →
  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) →
  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) →
  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) →
  let w = op₂ Data.Bool._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 true mode s $ λ addr →
  zero $ record s {program-counter = addr}
run JSR instruction = λ mode s →
  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL →
  suc $ read (concat (State.stack-pointer s , op₀ false ●)) $ λ _ →
  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 →
  zero $ record s {
    stack-pointer = increment (- + 2) $ State.stack-pointer s;
    program-counter = concat (ADL , ADH)
  }
run LDA instruction = execute-read-op $ \(s , w) → record (setZN w s) {register-A = w}
run LDX instruction = execute-read-op $ \(s , w) → record (setZN w s) {register-X = w}
run LDY instruction = execute-read-op $ \(s , w) → 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) →
  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) $ λ _ →
  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) $ λ _ →
  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) $ λ _ →
  suc $ read (concat (                 State.stack-pointer s  , op₀ false ●)) $ λ _ →
  suc $ read (concat (increment (+ 1) (State.stack-pointer s) , op₀ false ●)) $ λ w →
  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) $ λ _ →
  suc $ read (concat (                 State.stack-pointer s  , op₀ false ●)) $ λ _ →
  suc $ read (concat (increment (+ 1) (State.stack-pointer s) , op₀ false ●)) $ λ w →
  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) $ λ _ →
  suc $ read (concat (                 State.stack-pointer s  , op₀ false ●)) $ λ _ →
  suc $ read (concat (increment (+ 1) (State.stack-pointer s) , op₀ false ●)) $ λ P →
  suc $ read (concat (increment (+ 2) (State.stack-pointer s) , op₀ false ●)) $ λ PCL →
  suc $ read (concat (increment (+ 3) (State.stack-pointer s) , op₀ false ●)) $ λ PCH →
  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) $ λ _ →
  suc $ read (concat (                 State.stack-pointer s  , op₀ false ●)) $ λ _ →
  suc $ read (concat (increment (+ 1) (State.stack-pointer s) , op₀ false ●)) $ λ PCL →
  suc $ read (concat (increment (+ 2) (State.stack-pointer s) , op₀ false ●)) $ λ PCH →
  suc $ read (concat (PCL , PCH)) $ λ _ →
  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 if Flags.D $ State.flags s
  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₁
      lo = if inv-borrow-mid then lo else add lo (∅ ● ○ ● ○)
      (hi , inv-borrow-out) = sub-with-inverted-borrow inv-borrow-mid hi₀ hi₁
      hi = if inv-borrow-out then hi else add hi (∅ ● ○ ● ○)
    in record s {
      register-A = concat (lo , hi);
      flags = flags
    }
  ) else (
    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 =
  record {
    addr = State.program-counter s;
    r/w = true;
    continuation = Data.Maybe.map (λ (instr , mode) → run_instruction instr mode s) ∘′ parse-opcode
  }
--------------------------------------------------------------------------------
-- One cycle at a time.
cycle : Cycles State -> Cycle (Cycles State)
cycle (zero x) = step x
cycle (suc x) = x

.git
.DS_Store
*.agdai