Changeset 843 for src/ASM/Status.ma


Ignore:
Timestamp:
May 25, 2011, 3:57:42 PM (9 years ago)
Author:
sacerdot
Message:

Function moved from Interpret to Status.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r827 r843  
    10771077 λstatus.
    10781078   set_code_memory ? status (load_code_memory l).
     1079
     1080definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
     1081  λcode_mem.
     1082  λpc: Word.
     1083    let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in
     1084    let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in
     1085      〈instr, new_pc〉.
     1086    cases not_implemented.
     1087qed.
Note: See TracChangeset for help on using the changeset viewer.