Changeset 1541 for src/ASM

Timestamp:

Nov 23, 2011, 4:31:01 PM (10 years ago)

Author:

mulligan

Message:

interpret.ma now compiles

Location:

src/ASM

Files:

• Interpret.ma (modified) (2 diffs)
• Status.ma (modified) (1 diff)

src/ASM/Interpret.ma

@@ -766 +766 @@
       ].
     try assumption
-    try (
-      normalize
-      repeat (@ (le_S_S))
-      @ (le_O_n)
-    )
-    try (
-      @ (execute_1_technical … (subaddressing_modein …))
-      @ I
-    ) 
-    try (
-      normalize
-      @ I
-    )
-      ]. (*5s*)
-    try assumption (*12s*)
     [1,2: >set_program_counter_ignores_clock normalize nodelta
       >write_at_stack_pointer_ignores_clock
@@ -824 +809 @@
     | Mov dptr ident ⇒
       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
-      let preamble ≝ \fst (code_memory ? s) in
-      let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
+      let the_preamble ≝ \fst (code_memory ? s) in
+      let data_labels ≝ construct_datalabels the_preamble in
         set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
     ]

src/ASM/Status.ma

@@ -1303 +1303 @@
     address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
 
-definition construct_datalabels ≝
-  λpreamble.
-    \fst (foldl ((identifier_map ASMTag Word) × nat) ? (
+definition construct_datalabels: preamble → ? ≝
+  λthe_preamble: preamble.
+    \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
     λt. λpreamble.
       let 〈datalabels, addr〉 ≝ t in
       let 〈name, size〉 ≝ preamble in
-      let addr_16 ≝ bitvector_of_nat 16 addr in
-        〈add ? ? datalabels name addr_16, addr + size〉)
-          〈empty_map …, 0〉 preamble).
+      let 〈carry, sum〉 ≝ half_add … addr size in
+        〈add ? ? datalabels name addr, sum〉)
+          〈empty_map …, zero 16〉 (\snd the_preamble)).