Changeset 827 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 24, 2011, 1:26:43 PM (10 years ago)
Author:
sacerdot
Message:

The preamble is now part of the PseudoStatus?.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r825 r827  
    675675  λps: PseudoStatus.
    676676  λid: Identifier.
    677     address_of_word_labels_code_mem (code_memory ? ps) id.
     677    address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
    678678
    679679definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝
    680680  λticks_of.
    681681  λs.
    682   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (code_memory ? s) (program_counter ? s) in
     682  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
    683683  let ticks ≝ ticks_of (program_counter ? s) in
    684684  let s ≝ set_clock ? s (clock ? s + ticks) in
Note: See TracChangeset for help on using the changeset viewer.