Changeset 1541 for src/ASM


Ignore:
Timestamp:
Nov 23, 2011, 4:31:01 PM (8 years ago)
Author:
mulligan
Message:

interpret.ma now compiles

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1540 r1541  
    766766      ].
    767767    try assumption
    768     try (
    769       normalize
    770       repeat (@ (le_S_S))
    771       @ (le_O_n)
    772     )
    773     try (
    774       @ (execute_1_technical … (subaddressing_modein …))
    775       @ I
    776     )
    777     try (
    778       normalize
    779       @ I
    780     )
    781       ]. (*5s*)
    782     try assumption (*12s*)
    783768    [1,2: >set_program_counter_ignores_clock normalize nodelta
    784769      >write_at_stack_pointer_ignores_clock
     
    824809    | Mov dptr ident ⇒
    825810      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    826       let preamble ≝ \fst (code_memory ? s) in
    827       let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
     811      let the_preamble ≝ \fst (code_memory ? s) in
     812      let data_labels ≝ construct_datalabels the_preamble in
    828813        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
    829814    ]
  • src/ASM/Status.ma

    r1526 r1541  
    13031303    address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
    13041304
    1305 definition construct_datalabels
    1306   λpreamble.
    1307     \fst (foldl ((identifier_map ASMTag Word) × nat) ? (
     1305definition construct_datalabels: preamble → ?
     1306  λthe_preamble: preamble.
     1307    \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
    13081308    λt. λpreamble.
    13091309      let 〈datalabels, addr〉 ≝ t in
    13101310      let 〈name, size〉 ≝ preamble in
    1311       let addr_16 ≝ bitvector_of_nat 16 addr in
    1312         〈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.