You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on May 19, 2025. It is now read-only.
(* val exec : registers * instruction -> registers *)
159
181
funexec (regs, insn) =
160
182
case insn of
161
-
ADC x => letval v1 = value (regs, x) val v2 = v1 + #A regs in regs # {A = v2, P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0), C = (Word8.andb (v1, 0wx80) = 0wx80)}} end
183
+
ADC x => letval v1 = value (regs, x) val v2 = v1 + #A regs + b2w (#C (#P regs)) in regs # {A = v2, P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), V = checkV (#A regs, v1, v2) ,Z = (v2=0w0), C = (v2 < #A regs)}} end
162
184
| AND x => letval v1 = value (regs, x) val v2 = Word8.andb (#A regs, v1) in regs # {A = v2, P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0)}} end
185
+
| ASL (Address Accumulator) => letval v1 = (#A regs) val v2 = v1 * 0w2 in regs # {A = v2 ,P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0), C = (Word8.andb (v1, 0wx80) = 0wx80)}} end
163
186
| ASL (Address x) => letval v1 = value (regs, Address x) val v2 = v1 * 0w2 in (write (address (regs, x), v2); regs # {P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0), C = (Word8.andb (v1, 0wx80) = 0wx80)}}) end
164
187
| BCC x => (ifnot (#C (#P regs)) then regs # {PC = address (regs, x)} else regs)
165
188
| BCS x => (if #C (#P regs) then regs # {PC = address (regs, x)} else regs)
@@ -172,48 +195,52 @@ fun exec (regs, insn) =
172
195
| BVC x => (ifnot (#V (#P regs)) then regs # {PC = address (regs, x)} else regs)
173
196
| BVS x => (if #V (#P regs) then regs # {PC = address (regs, x)} else regs)
174
197
| CLC x => (regs # {P = (#P regs) # {C=false}})
175
-
| CLD x => regs
176
-
| CLI x => regs
177
-
| CLV x => regs
178
-
| CMP x => regs
179
-
| CPX x => regs
180
-
| CPY x => regs
181
-
| DEC x => regs
182
-
| DEX x => regs
183
-
| DEY x => regs
184
-
| EOR x => regs
185
-
| INC x => regs
186
-
| INX x => regs
187
-
| INY x => regs
198
+
| CLD x => (regs # {P = (#P regs) # {D=false}})
199
+
| CLI x => (regs # {P = (#P regs) # {I=false}})
200
+
| CLV x => (regs # {P = (#P regs) # {V=false}})
201
+
| CMP x => letval v1 = value (regs, x) val v2 = #A regs - v1 in regs # {P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0), C = not (v2 > #A regs)}} end
202
+
| CPX x => letval v1 = value (regs, x) val v2 = #X regs - v1 in regs # {P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0), C = not (v2 > #X regs)}} end
203
+
| CPY x => letval v1 = value (regs, x) val v2 = #Y regs - v1 in regs # {P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0), C = not (v2 > #Y regs)}} end
204
+
| DEC (Address x) => letval v1 = value (regs, Address x) val v2 = v1 - 0w1 in (write (address (regs, x), v2); regs # {P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0)}}) end
205
+
| DEX x => letval v = #X regs - 0w1 in regs # {X = v, P = (#P regs) # {N = (Word8.andb (v, 0wx80) = 0wx80), Z = (v=0w0)}} end
206
+
| DEY x => letval v = #Y regs - 0w1 in regs # {Y = v, P = (#P regs) # {N = (Word8.andb (v, 0wx80) = 0wx80), Z = (v=0w0)}} end
207
+
| EOR x => letval v1 = value (regs, x) val v2 = Word8.xorb (#A regs, v1) in regs # {A = v2, P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0)}} end
208
+
| INC (Address x) => letval v1 = value (regs, Address x) val v2 = v1 + 0w1 in (write (address (regs, x), v2); regs # {P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0)}}) end
209
+
| INX x => letval v = #X regs + 0w1 in regs # {X = v, P = (#P regs) # {N = (Word8.andb (v, 0wx80) = 0wx80), Z = (v=0w0)}} end
210
+
| INY x => letval v = #Y regs + 0w1 in regs # {Y = v, P = (#P regs) # {N = (Word8.andb (v, 0wx80) = 0wx80), Z = (v=0w0)}} end
| LDA x => letval v = value (regs, x) in regs # {A = v, P = (#P regs) # {N = (Word8.andb (v, 0wx80) = 0wx80), Z = (v=0w0)}} end
191
214
| LDX x => letval v = value (regs, x) in regs # {X = v, P = (#P regs) # {N = (Word8.andb (v, 0wx80) = 0wx80), Z = (v=0w0)}} end
192
-
| LDY x => regs
193
-
| LSR x => regs
215
+
| LDY x => letval v = value (regs, x) in regs # {Y = v, P = (#P regs) # {N = (Word8.andb (v, 0wx80) = 0wx80), Z = (v=0w0)}} end
216
+
| LSR (Address Accumulator) => letval v1 = (#A regs) val v2 = v1 div 0w2 in regs # {A = v2 ,P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0), C = (Word8.andb (v1, 0w1) = 0w1)}} end
217
+
| LSR (Address x) => letval v1 = value (regs, Address x) val v2 = v1 div 0w2 in (write (address (regs, x), v2); regs # {P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0), C = (Word8.andb (v1, 0w1) = 0w1)}}) end
194
218
| NOP x => regs
195
-
| ORA x => regs
196
-
| PHA x => regs
197
-
| PHP x => regs
198
-
| PLA x => regs
199
-
| PLP x => regs
200
-
| ROL x => regs
201
-
| ROR x => regs
202
-
| RTI x => regs
219
+
| ORA x => letval v1 = value (regs, x) val v2 = Word8.orb (#A regs, v1) in regs # {A = v2, P = (#P regs) # {N = (Word8.andb (v2, 0wx80) = 0wx80), Z = (v2=0w0)}} end
0 commit comments