Changeset 825 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 23, 2011, 6:12:51 PM (9 years ago)
Author:
mulligan
Message:

lots of refactoring, finally got something to prove

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r822 r825  
    632632qed.
    633633
    634 definition fetch_pseudo_instruction: PseudoStatus → Word → (Word → nat) → ((pseudo_instruction × Word) × nat) ≝
    635   λps: PseudoStatus.
     634definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
     635  λcode_mem.
    636636  λpc: Word.
    637   λticks_of: Word → nat.
    638     let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … (code_memory ? ps) ? in
     637    let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in
    639638    let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in
    640       〈〈instr, new_pc〉, ticks_of pc〉.
     639      〈instr, new_pc〉.
    641640    cases not_implemented.
    642641qed.
     
    668667    ].
    669668
     669definition address_of_word_labels_code_mem ≝
     670  λcode_mem.
     671  λid: Identifier.
     672    bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) code_mem).
     673
    670674definition address_of_word_labels ≝
    671675  λps: PseudoStatus.
    672676  λid: Identifier.
    673     bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) (code_memory ? ps)).
     677    address_of_word_labels_code_mem (code_memory ? ps) id.
    674678
    675679definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝
    676680  λticks_of.
    677681  λs.
    678   let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction s (program_counter ? s) ticks_of in
    679   let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
     682  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (code_memory ? s) (program_counter ? s) in
     683  let ticks ≝ ticks_of (program_counter ? s) in
    680684  let s ≝ set_clock ? s (clock ? s + ticks) in
    681685  let s ≝ set_program_counter ? s pc in
Note: See TracChangeset for help on using the changeset viewer.