Changeset 757 for src/ASM/Interpret.ma

Timestamp:

Apr 18, 2011, 12:30:53 PM (9 years ago)

Author:

mulligan

Message:

Lots more fixing to get both front and backends using same conventions and types.

File:

• src/ASM/Interpret.ma (modified) (5 diffs)

src/ASM/Interpret.ma

@@ -156 +156 @@
 
 include alias "arithmetics/nat.ma".
+include alias "ASM/BitVectorTrie.ma".
 
 definition execute_1: Status → Status ≝
@@ -172 +173 @@
             let ov_flag ≝ get_index' ? 2 ? flags in
             let s ≝ set_arg_8 s ACC_A result in
-              set_flags s cy_flag (Some Bit ac_flag) ov_flag    
+              set_flags s cy_flag (Some Bit ac_flag) ov_flag
         | ADDC addr1 addr2 ⇒
             let old_cy_flag ≝ get_cy_flag s in
@@ -240 +241 @@
         | INC addr ⇒
             match addr return λx. bool_to_Prop (is_in … [[ acc_a;
-                                                           register;
+                                                           registr;
                                                            direct;
                                                            indirect;
@@ -427 +428 @@
             | _ ⇒ λother: False. ⊥
             ] (subaddressing_modein … addr)
-        | MOVC addr1 addr2 ⇒
-          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
-            [ ACC_DPTR ⇒ λacc_dptr: True.
-              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
-              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
-              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
-              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
-                set_8051_sfr s SFR_ACC_A result
-            | ACC_PC ⇒ λacc_pc: True.
-              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
-              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
-              (* DPM: Under specified: does the carry from PC incrementation affect the *)
-              (*      addition of the PC with the DPTR? At the moment, no.              *)
-              let s ≝ set_program_counter s inc_pc in
-              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
-              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
-                set_8051_sfr s SFR_ACC_A result
-            | _ ⇒ λother: False. ⊥
-            ] (subaddressing_modein … addr2)
         | MOVX addr ⇒
           (* DPM: only copies --- doesn't affect I/O *)
@@ -631 +613 @@
                 ] (subaddressing_modein … addr2)
             ]
+        | MOVC addr1 addr2 ⇒
+          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
+            [ ACC_DPTR ⇒ λacc_dptr: True.
+              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
+              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
+              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
+              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
+                set_8051_sfr s SFR_ACC_A result
+            | ACC_PC ⇒ λacc_pc: True.
+              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
+              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
+              (* DPM: Under specified: does the carry from PC incrementation affect the *)
+              (*      addition of the PC with the DPTR? At the moment, no.              *)
+              let s ≝ set_program_counter s inc_pc in
+              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
+              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
+                set_8051_sfr s SFR_ACC_A result
+            | _ ⇒ λother: False. ⊥
+            ] (subaddressing_modein … addr2)
         | NOP ⇒ s
         ]