source: Deliverables/D4.1/Matita/Interpret.ma @ 329

Last change on this file since 329 was 329, checked in by mulligan, 9 years ago

Commit to restore deleted file.

File size: 1.8 KB
Line 
1include "Status.ma".
2include "Fetch.ma".
3include "Cartesian.ma".
4include "Arithmetic.ma".
5include "List.ma".
6
7ndefinition 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.