- Timestamp:
- Nov 23, 2011, 4:31:01 PM (8 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret.ma
r1540 r1541 766 766 ]. 767 767 try assumption 768 try (769 normalize770 repeat (@ (le_S_S))771 @ (le_O_n)772 )773 try (774 @ (execute_1_technical … (subaddressing_modein …))775 @ I776 )777 try (778 normalize779 @ I780 )781 ]. (*5s*)782 try assumption (*12s*)783 768 [1,2: >set_program_counter_ignores_clock normalize nodelta 784 769 >write_at_stack_pointer_ignores_clock … … 824 809 | Mov dptr ident ⇒ 825 810 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 826 let preamble ≝ \fst (code_memory ? s) in827 let data_labels ≝ construct_datalabels (map … (fst …) preamble)in811 let the_preamble ≝ \fst (code_memory ? s) in 812 let data_labels ≝ construct_datalabels the_preamble in 828 813 set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr 829 814 ] -
src/ASM/Status.ma
r1526 r1541 1303 1303 address_of_word_labels_code_mem (\snd (code_memory ? ps)) id. 1304 1304 1305 definition construct_datalabels ≝1306 λ preamble.1307 \fst (foldl ((identifier_map ASMTag Word) × nat) ? (1305 definition construct_datalabels: preamble → ? ≝ 1306 λthe_preamble: preamble. 1307 \fst (foldl ((identifier_map ASMTag Word) × Word) ? ( 1308 1308 λt. λpreamble. 1309 1309 let 〈datalabels, addr〉 ≝ t in 1310 1310 let 〈name, size〉 ≝ preamble in 1311 let addr_16 ≝ bitvector_of_nat 16 addrin1312 〈add ? ? datalabels name addr _16, addr + size〉)1313 〈empty_map …, 0〉 preamble).1311 let 〈carry, sum〉 ≝ half_add … addr size in 1312 〈add ? ? datalabels name addr, sum〉) 1313 〈empty_map …, zero 16〉 (\snd the_preamble)).
Note: See TracChangeset
for help on using the changeset viewer.