Changeset 1541 for src/ASM/Interpret.ma

Timestamp:

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

Author:

mulligan

Message:

interpret.ma now compiles

File:

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

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
     ]