Changeset 3064 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Apr 2, 2013, 1:02:59 PM (7 years ago)
Author:
sacerdot
Message:

Efficiency of the semantics of assembly improved by avoiding the recomputation
of address_of_word_labels maps at every step.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r3062 r3064  
    11981198  let s ≝
    11991199    match instr with
    1200     [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (code cm) x) instr s
     1200    [ Instruction instr ⇒
     1201       execute_1_preinstruction ticks …
     1202        (λx, y. addr_of_label x) instr s
    12011203    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
    12021204    | Cost cst ⇒ s
Note: See TracChangeset for help on using the changeset viewer.