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