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

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

More changes to get everything to typecheck.

File size: 6.2 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 Bit ac_flag) ov_flag
30                  | DIRECT d ⇒ λdirect: True.
31                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
32                                                           (get_arg_8 s false (DIRECT d)) false in
33                    let cy_flag ≝ get_index … flags Z ? in
34                    let ac_flag ≝ get_index … flags one ? in
35                    let ov_flag ≝ get_index … flags two ? in
36                    let s ≝ set_arg_8 s ACC_A result in
37                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
38                  | INDIRECT i ⇒ λindirect: True.
39                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
40                                                           (get_arg_8 s false (INDIRECT i)) false in
41                    let cy_flag ≝ get_index … flags Z ? in
42                    let ac_flag ≝ get_index … flags one ? in
43                    let ov_flag ≝ get_index … flags two ? in
44                    let s ≝ set_arg_8 s ACC_A result in
45                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
46                  | DATA d ⇒ λdata: True.
47                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
48                                                           (get_arg_8 s false (DATA d)) false in
49                    let cy_flag ≝ get_index … flags Z ? in
50                    let ac_flag ≝ get_index … flags one ? in
51                    let ov_flag ≝ get_index … flags two ? in
52                    let s ≝ set_arg_8 s ACC_A result in
53                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
54                  | _ ⇒ λother: False. ?
55                  ] (subaddressing_modein … addr2)
56            | _ ⇒ λother: False. ?
57            ] (subaddressing_modein … addr1)
58        | ADDC addr1 addr2 ⇒
59            let old_cy_flag ≝ get_cy_flag s in
60            match addr1 return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with
61              [ ACC_A ⇒ λacc_a: True.
62                match addr2 return λx. bool_to_Prop (is_in … [[ register;
63                                                                direct;
64                                                                indirect;
65                                                                data ]] x) → ? with
66                  [ REGISTER r ⇒ λregister: True.
67                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
68                                                           (get_arg_8 s false (REGISTER r)) old_cy_flag in
69                    let cy_flag ≝ get_index … flags Z ? in
70                    let ac_flag ≝ get_index … flags one ? in
71                    let ov_flag ≝ get_index … flags two ? in
72                    let s ≝ set_arg_8 s ACC_A result in
73                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
74                  | DIRECT d ⇒ λdirect: True.
75                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
76                                                           (get_arg_8 s false (DIRECT d)) old_cy_flag in
77                    let cy_flag ≝ get_index … flags Z ? in
78                    let ac_flag ≝ get_index … flags one ? in
79                    let ov_flag ≝ get_index … flags two ? in
80                    let s ≝ set_arg_8 s ACC_A result in
81                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
82                  | INDIRECT i ⇒ λindirect: True.
83                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
84                                                           (get_arg_8 s false (INDIRECT i)) old_cy_flag in
85                    let cy_flag ≝ get_index … flags Z ? in
86                    let ac_flag ≝ get_index … flags one ? in
87                    let ov_flag ≝ get_index … flags two ? in
88                    let s ≝ set_arg_8 s ACC_A result in
89                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
90                  | DATA d ⇒ λdata: True.
91                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
92                                                           (get_arg_8 s false (DATA d)) old_cy_flag in
93                    let cy_flag ≝ get_index … flags Z ? in
94                    let ac_flag ≝ get_index … flags one ? in
95                    let ov_flag ≝ get_index … flags two ? in
96                    let s ≝ set_arg_8 s ACC_A result in
97                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
98                  | _ ⇒ λother: False. ?
99                  ] (subaddressing_modein … addr2)
100            | _ ⇒ λother: False. ?
101            ] (subaddressing_modein … addr1)
102        | _ ⇒ s
103        ]
104    in
105      s.
106   
107   
Note: See TracBrowser for help on using the repository browser.