finegeometer/agda-emulator - Change BJQSZC43ZA4A6T4NSQOWQ5OQE2QK7JWWXLAWITMIKJTGUHP2RRRAC

Support partially-unknown values.

Created by finegeometer on May 3, 2022

BJQSZC43ZA4A6T4NSQOWQ5OQE2QK7JWWXLAWITMIKJTGUHP2RRRAC

Dependencies

In channels

main

Change contents

Insertion in memory.agda at line 5 [3.36]

[3.163]

open import Data.Maybe as Maybe using (Maybe; just; nothing)

Replacement in memory.agda at line 7 [3.36]

B:BD[3.164] → [3.164:226]

open import Word.Base using (Word; ∅; push-low; _○; _●)

[3.164]

[3.226]

open import Word.Base using (Word; ∅; push-low; _○; _●; _◍)

Replacement in memory.agda at line 14 [3.36]

B:BD[3.374] → [3.374:534]

read : {n : ℕ} {A : Set} → memory n A → (Word n → A)
read ram ∅ = ram
read ram (w ○) = proj₁ (read ram w)
read ram (w ●) = proj₂ (read ram w)

[3.374]

[3.534]

read : {n : ℕ} {A : Set} → memory n A → (Word n → Maybe A)
read ram ∅ = just ram
read ram (w ○) = Maybe.map proj₁ (read ram w)
read ram (w ●) = Maybe.map proj₂ (read ram w)
read ram (w ◍) = nothing

Replacement in memory.agda at line 20 [3.36]

B:BD[3.535] → [3.535:638]

modify : {n : ℕ} {A : Set} → Word n → (A → A) → (memory n A → memory n A)
modify ∅ f = f

[3.535]

[3.638]

modify : {n : ℕ} {A : Set} → Word n → (A → A) → memory n A → Maybe (memory n A)
modify ∅ f x = just (f x)

Insertion in memory.agda at line 24 [3.36]
[3.742]
[3.742]
```
modify (w ◍) f _ = nothing
```

Replacement in memory.agda at line 26 [3.36]

B:BD[3.743] → [3.743:820]

write : {n : ℕ} {A : Set} → Word n → A → (memory n A → memory n A)

[3.743]

[3.820]

write : {n : ℕ} {A : Set} → Word n → A → memory n A → Maybe (memory n A)

Replacement in Word/Base.agda at line 4 [2.162]

B:BD[2.241] → [2.241:312]

open import Data.Bool as Bool using (Bool; true; false; if_then_else_)

[2.241]

[2.312]

import Data.Bool as Bool

Insertion in Word/Base.agda at line 7 [2.162]
[2.407]
[2.407]
```
open import Data.Maybe using (Maybe; just; nothing)
```

Insertion in Word/Base.agda at line 12 [2.162]

[2.565]

open import Bit using (Bit; true; false; unknown; not; _∧_; _xor_)

Replacement in Word/Base.agda at line 18 [2.162]

B:BD[2.692] → [2.692:751]

  push-low : {n : ℕ} → Bool × Word n → Word (suc n)

[2.692]

[2.751]

  push-low : {n : ℕ} → Bit × Word n → Word (suc n)

Insertion in Word/Base.agda at line 22 [2.162]
[2.827]
[2.827]
```
pattern _◍ w = push-low (unknown , w)
```

Replacement in Word/Base.agda at line 26 [2.162]

B:BD[2.910] → [2.910:966]

pop-low : {n : ℕ} → Word (suc n) → Bool × Word n

[2.910]

[2.966]

pop-low : {n : ℕ} → Word (suc n) → Bit × Word n

Replacement in Word/Base.agda at line 29 [2.162]

B:BD[2.992] → [2.992:1050]

push-high : {n : ℕ} → Word n × Bool → Word (suc n)

[2.992]

[2.1050]

push-high : {n : ℕ} → Word n × Bit → Word (suc n)

Replacement in Word/Base.agda at line 33 [2.162]

B:BD[2.1172] → [2.1172:1229]

pop-high : {n : ℕ} → Word (suc n) → Word n × Bool

[2.1172]

[2.1229]

pop-high : {n : ℕ} → Word (suc n) → Word n × Bit

Replacement in Word/Base.agda at line 39 [2.162]

B:BD[2.1459] → [2.1459:1535]

bit : {n : ℕ} → Word n → (i : ℕ) → {{Bool.T (i <ᵇ n)}} → Bool

[2.1459]

[2.1535]

bit : {n : ℕ} → Word n → (i : ℕ) → {{Bool.T (i <ᵇ n)}} → Bit

Replacement in Word/Base.agda at line 45 [2.162]

B:BD[2.1705] → [2.1705:1757]

_≡ᵇ_ : {n : ℕ} → Word n → Word n → Bool

[2.1705]

[2.1757]

_≡ᵇ_ : {n : ℕ} → Word n → Word n → Bit

Replacement in Word/Base.agda at line 47 [2.162]

B:BD[2.1779] → [2.1779:1893]

push-low (b₀ , w₀) ≡ᵇ push-low (b₁ , w₁) = (does (Bool._≟_ b₀ b₁) ) Bool.∧ (w₀ ≡ᵇ w₁)

[2.1779]

[2.1893]

push-low (b₀ , w₀) ≡ᵇ push-low (b₁ , w₁) = not (b₀ xor b₁) ∧ (w₀ ≡ᵇ w₁)

Replacement in Word/Base.agda at line 51 [2.162]

B:BD[2.1976] → [2.1976:2158]

op₀ : {n : ℕ} → Bool → Word n
op₁ : {n : ℕ} → (Bool → Bool) → (Word n → Word n)
op₂ : {n : ℕ} → (Bool → Bool → Bool) → (Word n → Word n → Word n)

[2.1976]

[2.2158]

op₀ : {n : ℕ} → Bit → Word n
op₁ : {n : ℕ} → (Bit → Bit) → (Word n → Word n)
op₂ : {n : ℕ} → (Bit → Bit → Bit) → (Word n → Word n → Word n)

Replacement in Word/Base.agda at line 78 [2.162]

B:BD[2.3015] → [2.3015:3114]

word-from-int {suc n} x = push-low ((Data.Nat._≟_ (x %ℕ 2) 0).does , word-from-int (x /ℕ 2))

[2.3015]

[2.3114]

word-from-int {suc n} x = push-low (Bit.bit-from-bool (x %ℕ 2 Data.Nat.≡ᵇ 0) , word-from-int (x /ℕ 2))

Replacement in Word/Base.agda at line 80 [2.162]

B:BD[2.3115] → [2.3115:3260]

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

[2.3115]

[2.3260]

nat-from-word : {n : ℕ} → Word n → Maybe ℕ
nat-from-word ∅ = Maybe.just 0
nat-from-word (push-low (b , w)) with Bit.bool-from-bit b | nat-from-word w
... | just b | just w = just ((Bool.if b then 1 else 0) + 2 * w)
... | _ | _ = nothing

Replacement in Word/Base.agda at line 88 [2.162]

B:BD[2.3343] → [2.3343:3850]

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

[2.3343]

[2.3850]

add-with-carry : {n : ℕ} → Bit → Word n → Word n → Word n × Bit

Replacement in Word/Base.agda at line 92 [2.162]

B:BD[2.3977] → [2.3977:4028]

    (b₂ , carry) = full-adder carry-in b₀ b₁

[2.3977]

[2.4028]

    b₂ = carry-in xor b₀ xor b₁
    carry = Bit.majority carry-in b₀ b₁

Replacement in Word/Base.agda at line 97 [2.162]

B:BD[2.4127] → [2.4127:4325]

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₁)

[2.4127]

[2.4325]

sub-with-inverted-borrow : {n : ℕ} → Bit → Word n → Word n → Word n × Bit
sub-with-inverted-borrow inverted-borrow w₀ w₁ = add-with-carry inverted-borrow w₀ (op₁ not w₁)

Replacement in 6502-Processor.agda at line 3 [2.4734]

B:BD[2.4764] → [2.4764:4898]

open import Data.Bool using (Bool; true; false; if_then_else_; _∧_; _∨_; not)
open import Data.Maybe using (Maybe; just; nothing)

[2.4764]

[2.4898]

open import Data.Bool as Bool using (Bool)
open import Data.Maybe as Maybe using (Maybe; just; nothing)

Replacement in 6502-Processor.agda at line 10 [2.4734]
B:BD[2.5058] → [2.5058:5101]
```
open import Function using (_∘′_; _$_)
```
[2.5058]
[2.5101]
```
open import Function using (_∘′_; _$_; flip)
```
Insertion in 6502-Processor.agda at line 13 [2.4734]
[2.5144]
[2.5144]
```
open import Bit
```

Replacement in 6502-Processor.agda at line 26 [2.4734]

B:BD[2.5528] → [2.5528:5599]

    continuation : if r/w then (Word 8 → Maybe s) else (Word 8 × s)

[2.5528]

[2.5599]

    continuation : Bool.if r/w then (Word 8 → Maybe s) else (Word 8 × s)

Replacement in 6502-Processor.agda at line 28 [2.4734]

B:BD[2.5600] → [2.5600:5660]

read : {s : Set} → Word 16 → (Word 8 → s) → Cycle s

[2.5600]

[2.5660]

read : {s : Set} → Word 16 → (Word 8 → Maybe s) → Cycle s

Replacement in 6502-Processor.agda at line 32 [2.4734]

B:BD[2.5713] → [2.5713:5773]

    r/w = true;
    continuation = just ∘′ continuation

[2.5713]

[2.5773]

    r/w = Bool.true;
    continuation = continuation

Replacement in 6502-Processor.agda at line 40 [2.4734]
B:BD[2.5893] → [2.5893:5910]
```
    r/w = false;
```
[2.5893]
[2.5910]
```
    r/w = Bool.false;
```

Replacement in 6502-Processor.agda at line 55 [2.4734]

B:BD[2.7127] → [2.7127:7205]

    N : Bool
    V : Bool
    D : Bool
    I : Bool
    Z : Bool
    C : Bool

[2.7127]

[2.7205]

    N : Bit
    V : Bit
    D : Bit
    I : Bit
    Z : Bit
    C : Bit

Deletion in 6502-Processor.agda at line 318 [2.4734]

B:BD[2.21454] → [2.21454:21679]


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
  })

Replacement in 6502-Processor.agda at line 331 [2.4734]

B:BD[2.22276] → [2.22276:22416]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL →
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ ADH →

[2.22276]

[2.22416]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL → just $ 
  suc $ read (increment (+ 2) $ State.program-counter s) $ λ ADH → just $

Replacement in 6502-Processor.agda at line 335 [2.4734]

B:BD[2.22499] → [2.22499:22569]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL →

[2.22499]

[2.22569]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL → just $

Replacement in 6502-Processor.agda at line 338 [2.4734]

B:BD[2.22659] → [2.22659:22909]

  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 →

[2.22659]

[2.22909]

  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 $

Replacement in 6502-Processor.agda at line 344 [2.4734]

B:BD[2.23001] → [2.23001:23071]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL →

[2.23001]

[2.23071]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL → just $

Replacement in 6502-Processor.agda at line 347 [2.4734]

B:BD[2.23212] → [2.23212:23374]

  if carry ∨ not read-only then (
    suc $ read (concat (ADL , BAH)) $ λ _ →
    continuation $ concat (ADL , (if carry then increment (+ 1) BAH else BAH))

[2.23212]

[2.23374]

  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))

Replacement in 6502-Processor.agda at line 355 [2.4734]

B:BD[2.23483] → [2.23483:23553]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL →

[2.23483]

[2.23553]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL → just $

Replacement in 6502-Processor.agda at line 358 [2.4734]

B:BD[2.23694] → [2.23694:23856]

  if carry ∨ not read-only then (
    suc $ read (concat (ADL , BAH)) $ λ _ →
    continuation $ concat (ADL , (if carry then increment (+ 1) BAH else BAH))

[2.23694]

[2.23856]

  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))

Replacement in 6502-Processor.agda at line 366 [2.4734]

B:BD[2.23958] → [2.23958:24081]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL →
  suc $ read (concat (BAL , op₀ false)) $ λ _ →

[2.23958]

[2.24081]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL → just $
  suc $ read (concat (BAL , op₀ false)) $ λ _ → just $

Replacement in 6502-Processor.agda at line 371 [2.4734]

B:BD[2.24222] → [2.24222:24345]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL →
  suc $ read (concat (BAL , op₀ false)) $ λ _ →

[2.24222]

[2.24345]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL → just $
  suc $ read (concat (BAL , op₀ false)) $ λ _ → just $

Replacement in 6502-Processor.agda at line 376 [2.4734]

B:BD[2.24491] → [2.24491:24614]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL →
  suc $ read (concat (BAL , op₀ false)) $ λ _ →

[2.24491]

[2.24614]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ BAL → just $
  suc $ read (concat (BAL , op₀ false)) $ λ _ → just $

Replacement in 6502-Processor.agda at line 379 [2.4734]

B:BD[2.24660] → [2.24660:24790]

  suc $ read (concat (BAL+X , op₀ false)) $ λ ADL →
  suc $ read (concat (increment (+ 1) BAL+X , op₀ false)) $ λ ADH →

[2.24660]

[2.24790]

  suc $ read (concat (BAL+X , op₀ false)) $ λ ADL → just $
  suc $ read (concat (increment (+ 1) BAL+X , op₀ false)) $ λ ADH → just $

Replacement in 6502-Processor.agda at line 383 [2.4734]

B:BD[2.24888] → [2.24888:25013]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ IAL →
  suc $ read (concat (IAL , op₀ false)) $ λ BAL →

[2.24888]

[2.25013]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ IAL → just $
  suc $ read (concat (IAL , op₀ false)) $ λ BAL → just $

Replacement in 6502-Processor.agda at line 387 [2.4734]

B:BD[2.25155] → [2.25155:25317]

  if carry ∨ not read-only then (
    suc $ read (concat (ADL , BAH)) $ λ _ →
    continuation $ concat (ADL , (if carry then increment (+ 1) BAH else BAH))

[2.25155]

[2.25317]

  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))

Replacement in 6502-Processor.agda at line 397 [2.4734]

B:BD[2.25486] → [2.25486:25597]

  suc (record {addr = increment (+ 1) $ State.program-counter s; r/w = true; continuation = λ _ → nothing})

[2.25486]

[2.25597]

  suc $ read (increment (+ 1) $ State.program-counter s) (λ _ → nothing)

Replacement in 6502-Processor.agda at line 399 [2.4734]

B:BD[2.25642] → [2.25642:25753]

  suc (record {addr = increment (+ 1) $ State.program-counter s; r/w = true; continuation = λ _ → nothing})

[2.25642]

[2.25753]

  suc $ read (increment (+ 1) $ State.program-counter s) (λ _ → nothing)

Replacement in 6502-Processor.agda at line 402 [2.4734]

B:BD[2.25857] → [2.25857:25968]

  suc (record {addr = increment (+ 1) $ State.program-counter s; r/w = true; continuation = λ _ → nothing})

[2.25857]

[2.25968]

  suc $ read (increment (+ 1) $ State.program-counter s) (λ _ → nothing)

Replacement in 6502-Processor.agda at line 425 [2.4734]

B:BD[2.26594] → [2.26594:26687]

execute-read-op : (State × Word 8 → State) → addressing-mode → State → Cycles State

[2.26594]

[2.26687]

execute-read-op : (State × Word 8 → Maybe State) → addressing-mode → State → Cycles State

Replacement in 6502-Processor.agda at line 427 [2.4734]
B:BD[2.26714] → [2.26714:26760]
```
  effective-address true mode s $ λ addr →
```
[2.26714]
[2.26760]
```
  effective-address Bool.true mode s $ λ addr →
```
Replacement in 6502-Processor.agda at line 429 [2.4734]
B:BD[2.26789] → [2.26789:26820]
```
  zero $ f (inc-pc mode s , w)
```
[2.26789]
[2.26820]
```
  Maybe.map zero $ f (inc-pc mode s , w)
```
Replacement in 6502-Processor.agda at line 433 [2.4734]
B:BD[2.26943] → [2.26943:26990]
```
  effective-address false mode s $ λ addr →
```
[2.26943]
[2.26990]
```
  effective-address Bool.false mode s $ λ addr →
```

Replacement in 6502-Processor.agda at line 440 [2.4734]

B:BD[2.27203] → [2.27203:27271]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ w →

[2.27203]

[2.27271]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ w → just $

Replacement in 6502-Processor.agda at line 444 [2.4734]

B:BD[2.27383] → [2.27383:27459]

  effective-address false mode s $ λ addr →
  suc $ read addr $ λ w →

[2.27383]

[2.27459]

  effective-address Bool.false mode s $ λ addr →
  suc $ read addr $ λ w → just $

Replacement in 6502-Processor.agda at line 453 [2.4734]

B:BD[2.27680] → [2.27680:27748]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ →

[2.27680]

[2.27748]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $

Replacement in 6502-Processor.agda at line 456 [2.4734]

B:BD[2.27776] → [2.27776:27837]

execute-branch : (State → Bool) → State → Cycles State

[2.27776]

[2.27837]

execute-branch : (State → Bit) → State → Cycles State

Replacement in 6502-Processor.agda at line 459 [2.4734]
B:BD[2.27934] → [2.27934:27946]
```
  if cond s
```
[2.27934]
[2.27946]
```
  bool-from-bit (cond s) Maybe.>>= λ cond →
  Bool.if cond
```
Deletion in 6502-Processor.agda at line 462 [2.4734]
B:BD[2.27955] → [2.27955:28025]
```
    suc $ read (increment (+ 2) $ State.program-counter s) $ λ _ →
```

Replacement in 6502-Processor.agda at line 465 [2.4734]

B:BD[2.28157] → [2.28157:28259]

      page-change = Data.Integer._-_ (if carry then + 1 else + 0) (if bit offset 7 then + 1 else + 0)

[2.28157]

[2.28259]

    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)

Replacement in 6502-Processor.agda at line 471 [2.4734]

B:BD[2.28325] → [2.28325:28381]

    in if (does $ Data.Integer._≟_ page-change (+ 0))

[2.28325]

[2.28381]

    in just $
    suc $ read (increment (+ 2) $ State.program-counter s) $ λ _ → just $
    Bool.if (does $ Data.Integer._≟_ page-change (+ 0))

Replacement in 6502-Processor.agda at line 477 [2.4734]

B:BD[2.28466] → [2.28466:28515]

      suc $ read (concat (ADL , PCH)) $ λ _ →

[2.28466]

[2.28515]

      suc $ read (concat (ADL , PCH)) $ λ _ → just $

Replacement in 6502-Processor.agda at line 480 [2.4734]

B:BD[2.28582] → [2.28582:28679]

  ) else (zero $ record s {
    program-counter = increment (+ 2) $ State.program-counter s
  })

[2.28582]

[2.28679]

  ) else just (
    zero $ record s { program-counter = increment (+ 2) $ State.program-counter s }
  )

Replacement in 6502-Processor.agda at line 504 [2.4734]

B:BD[2.29286] → [2.29286:29318]

  in if Flags.D $ State.flags s

[2.29286]

[2.29318]

  in
  bool-from-bit (Flags.D $ State.flags s) Maybe.>>= λ decimal-mode →
  Bool.if decimal-mode

Replacement in 6502-Processor.agda at line 517 [2.4734]

B:BD[2.29814] → [2.29814:29907]

      (lo , carry-mid) = if no-decimal-carry then (lo , carry-mid) else (lo-minus-10 , true)

[2.29814]

[2.29907]

    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)

Replacement in 6502-Processor.agda at line 522 [2.4734]

B:BD[2.30066] → [2.30066:30177]

      (hi , carry-out) = if no-decimal-carry then (hi , carry-out) else (hi-minus-10 , true)
    in record s {

[2.30066]

[2.30177]

    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 {

Replacement in 6502-Processor.agda at line 534 [2.4734]
B:BD[2.30486] → [2.30486:30501]
```
    record s {
```
[2.30486]
[2.30501]
```
    just $ record s {
```

Replacement in 6502-Processor.agda at line 545 [2.4734]

B:BD[2.30838] → [2.30838:30891]

run AND instruction = execute-read-op $ \(s , w) →

[2.30838]

[2.30891]

run AND instruction = execute-read-op $ \(s , w) → just $

Replacement in 6502-Processor.agda at line 554 [2.4734]

B:BD[2.31408] → [2.31408:31461]

run BIT instruction = execute-read-op $ \(s , w) →

[2.31408]

[2.31461]

run BIT instruction = execute-read-op $ \(s , w) → just $

Replacement in 6502-Processor.agda at line 566 [2.4734]

B:BD[2.31905] → [2.31905:31973]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ →

[2.31905]

[2.31973]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $

Replacement in 6502-Processor.agda at line 571 [2.4734]

B:BD[2.32349] → [2.32349:32435]

  suc $ read (op₀ true ○) $ λ ADL →
  suc $ read (op₀ true ●) $ λ ADH →

[2.32349]

[2.32435]

  suc $ read (op₀ true ○) $ λ ADL → just $
  suc $ read (op₀ true ●) $ λ ADH → just $

Replacement in 6502-Processor.agda at line 584 [2.4734]

B:BD[2.33162] → [2.33162:33215]

run CMP instruction = execute-read-op $ \(s , w) →

[2.33162]

[2.33215]

run CMP instruction = execute-read-op $ \(s , w) → just $

Replacement in 6502-Processor.agda at line 587 [2.4734]

B:BD[2.33365] → [2.33365:33418]

run CPX instruction = execute-read-op $ \(s , w) →

[2.33365]

[2.33418]

run CPX instruction = execute-read-op $ \(s , w) → just $

Replacement in 6502-Processor.agda at line 590 [2.4734]

B:BD[2.33568] → [2.33568:33621]

run CPY instruction = execute-read-op $ \(s , w) →

[2.33568]

[2.33621]

run CPY instruction = execute-read-op $ \(s , w) → just $

Replacement in 6502-Processor.agda at line 598 [2.4734]

B:BD[2.34161] → [2.34161:34272]

run EOR instruction = execute-read-op $ \(s , w) →
  let w = op₂ Data.Bool._xor_ w (State.register-A s) in

[2.34161]

[2.34272]

run EOR instruction = execute-read-op $ \(s , w) → just $
  let w = op₂ _xor_ w (State.register-A s) in

Replacement in 6502-Processor.agda at line 607 [2.4734]
B:BD[2.34730] → [2.34730:34776]
```
  effective-address true mode s $ λ addr →
```
[2.34730]
[2.34776]
```
  effective-address Bool.true mode s $ λ addr →
```

Replacement in 6502-Processor.agda at line 610 [2.4734]

B:BD[2.34855] → [2.34855:35000]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL →
  suc $ read (concat (State.stack-pointer s , op₀ false ●)) $ λ _ →

[2.34855]

[2.35000]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ ADL → just $
  suc $ read (concat (State.stack-pointer s , op₀ false ●)) $ λ _ → just $

Replacement in 6502-Processor.agda at line 615 [2.4734]

B:BD[2.35235] → [2.35235:35305]

  suc $ read (increment (+ 2) $ State.program-counter s) $ λ ADH →

[2.35235]

[2.35305]

  suc $ read (increment (+ 2) $ State.program-counter s) $ λ ADH → just $

Replacement in 6502-Processor.agda at line 620 [2.4734]

B:BD[2.35433] → [2.35433:35700]

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}

[2.35433]

[2.35700]

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}

Replacement in 6502-Processor.agda at line 627 [2.4734]

B:BD[2.35939] → [2.35939:35992]

run ORA instruction = execute-read-op $ \(s , w) →

[2.35939]

[2.35992]

run ORA instruction = execute-read-op $ \(s , w) → just $

Replacement in 6502-Processor.agda at line 631 [2.4734]

B:BD[2.36111] → [2.36111:36179]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ →

[2.36111]

[2.36179]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $

Replacement in 6502-Processor.agda at line 639 [2.4734]

B:BD[2.36455] → [2.36455:36523]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ →

[2.36455]

[2.36523]

  suc $ read (increment (+ 1) $ State.program-counter s) $ λ _ → just $

Replacement in 6502-Processor.agda at line 647 [2.4734]

B:BD[2.36812] → [2.36812:37066]

  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 →

[2.36812]

[2.37066]

  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 $

Replacement in 6502-Processor.agda at line 656 [2.4734]

B:BD[2.37278] → [2.37278:37532]

  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 →

[2.37278]

[2.37532]

  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 $

Replacement in 6502-Processor.agda at line 671 [2.4734]

B:BD[2.38145] → [2.38145:38589]

  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 →

[2.38145]

[2.38589]

  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 $

Replacement in 6502-Processor.agda at line 682 [2.4734]

B:BD[2.38779] → [2.38779:39175]

  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)) $ λ _ →

[2.38779]

[2.39175]

  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 $

Replacement in 6502-Processor.agda at line 703 [2.4734]

B:BD[2.39861] → [2.39861:39893]

  in if Flags.D $ State.flags s

[2.39861]

[2.39893]

  in
  bool-from-bit (Flags.D $ State.flags s) Maybe.>>= λ decimal-mode →
  Bool.if decimal-mode

Replacement in 6502-Processor.agda at line 715 [2.4734]

B:BD[2.40308] → [2.40308:40379]

      lo = if inv-borrow-mid then lo else add lo (∅ ● ○ ● ○)

[2.40308]

[2.40379]

      (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 (∅ ● ○ ● ○)

Replacement in 6502-Processor.agda at line 722 [2.4734]

B:BD[2.40380] → [2.40380:40551]

      (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 {

[2.40380]

[2.40551]

      hi = Bool.if inv-borrow-out then hi else add hi (∅ ● ○ ● ○)
    in just $ record s {

Replacement in 6502-Processor.agda at line 728 [2.4734]
B:BD[2.40625] → [2.40625:40640]
```
    record s {
```
[2.40625]
[2.40640]
```
    just $ record s {
```

Replacement in 6502-Processor.agda at line 751 [2.4734]

B:BD[2.42191] → [2.42191:42374]

step s =
  record {
    addr = State.program-counter s;
    r/w = true;
    continuation = Data.Maybe.map (λ (instr , mode) → run_instruction instr mode s) ∘′ parse-opcode
  }

[2.42191]

[2.42374]

step s = read (State.program-counter s) $
  Maybe.map (λ (instr , mode) → run_instruction instr mode s) ∘′ parse-opcode