Changeset 2014


Ignore:
Timestamp:
Jun 2, 2012, 10:39:35 PM (5 years ago)
Author:
mulligan
Message:

Fixed problem in James' email message.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1971 r2014  
    13391339qed.
    13401340
     1341include alias "arithmetics/nat.ma".
     1342include alias "ASM/BitVectorTrie.ma".
     1343include alias "ASM/Vector.ma".
     1344
    13411345definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
    13421346  Σs': Status cm.
     
    13501354    let s ≝ set_program_counter … s0 pc in
    13511355      match instr return λx. x = instr → Σs:?.? with
    1352       [ RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] …
    1353         (addr_of_relative … cm) instr' s
    1354       | MOVC addr1 addr2 ⇒ λinstr_refl.
     1356      [ MOVC addr1 addr2 ⇒ λinstr_refl.
    13551357          let s ≝ set_clock ?? s (ticks + clock … s) in
    13561358          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':?. ? with
     
    14061408            | _ ⇒ λother: False. ⊥
    14071409            ] (subaddressing_modein … addr)
    1408         | LCALL addr ⇒ λinstr_refl.
     1410      | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s
     1411      | LCALL addr ⇒ λinstr_refl.
    14091412          let s ≝ set_clock ?? s (ticks + clock … s) in
    14101413          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
Note: See TracChangeset for help on using the changeset viewer.