Changeset 1541 for src/ASM/Status.ma


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

interpret.ma now compiles

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.