Changeset 843


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

Function moved from Interpret to Status.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r827 r843  
    632632qed.
    633633
    634 definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
    635   λcode_mem.
    636   λpc: Word.
    637     let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in
    638     let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in
    639       〈instr, new_pc〉.
    640     cases not_implemented.
    641 qed.
    642 
    643634let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
    644635  match l with
  • 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.