Last change
on this file since 330 was
329,
checked in by mulligan, 10 years ago
|
Commit to restore deleted file.
|
File size:
1.8 KB
|
Rev | Line | |
---|
[329] | 1 | include "Status.ma". |
---|
| 2 | include "Fetch.ma". |
---|
| 3 | include "Cartesian.ma". |
---|
| 4 | include "Arithmetic.ma". |
---|
| 5 | include "List.ma". |
---|
| 6 | |
---|
| 7 | ndefinition execute_1: Status → Status ≝ |
---|
| 8 | λs. |
---|
| 9 | let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in |
---|
| 10 | let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in |
---|
| 11 | let s ≝ set_clock s (clock s + ticks) in |
---|
| 12 | let s ≝ set_program_counter s pc in |
---|
| 13 | let s ≝ |
---|
| 14 | match instr with |
---|
| 15 | [ ADD addr1 addr2 ⇒ |
---|
| 16 | match addr1 return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with |
---|
| 17 | [ ACC_A ⇒ λacc_a: True. |
---|
| 18 | match addr2 return λx. bool_to_Prop (is_in … [[ register; |
---|
| 19 | direct; |
---|
| 20 | indirect; |
---|
| 21 | data ]] x) → ? with |
---|
| 22 | [ REGISTER r ⇒ λregister: True. |
---|
| 23 | let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A) |
---|
| 24 | (get_arg_8 s false (REGISTER r)) false in |
---|
| 25 | let cy_flag ≝ get_index ? flags Z in |
---|
| 26 | let ac_flag ≝ get_index ? flags one in |
---|
| 27 | let ov_flag ≝ get_index ? flags two in |
---|
| 28 | let s ≝ set_arg_8 s ACC_A result in |
---|
| 29 | set_flags s cy_flag (Just? ac_flag) ov_flag |
---|
| 30 | | DIRECT d ⇒ λdirect: True. ? |
---|
| 31 | | INDIRECT i ⇒ λindirect: True. ? |
---|
| 32 | | DATA d ⇒ λdata: True. ? |
---|
| 33 | | _ ⇒ λother: False. ? |
---|
| 34 | ] (subaddressing_modein … addr2) |
---|
| 35 | | _ ⇒ λother: False. ? |
---|
| 36 | ] (subaddressing_modein … addr1) |
---|
| 37 | | _ ⇒ s |
---|
| 38 | ] |
---|
| 39 | in |
---|
| 40 | s. |
---|
| 41 | |
---|
| 42 | |
---|
Note: See
TracBrowser
for help on using the repository browser.