Changeset 1476 for src/ASM


Ignore:
Timestamp:
Nov 1, 2011, 5:04:14 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r1475 r1476  
    1717 λp. ticks_of … (mk_policy p).
    1818
    19 axiom execute_1_pseudo_instruction:
    20  (Word → nat × nat) → PseudoStatus → IO io_out io_in (trace × PseudoStatus).
     19definition execute_1_pseudo_instruction_trace:
     20 (Word → nat × nat) → PseudoStatus → IO io_out io_in (trace × PseudoStatus) ≝
     21λticks_of,s.
     22 let 〈instr,pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory … s)) (program_counter … s) in
     23 let s ≝ execute_1_pseudo_instruction ticks_of s in
     24 match instr with
     25 [ Cost cst ⇒ ret … 〈Echarge (an_identifier … cst), s〉
     26 | _ ⇒ ret ? 〈E0, s〉 ].
    2127
    2228axiom pseudo_is_final: (Word → nat × nat) → PseudoStatus → option int.
    2329
    2430definition pseudo_exec: trans_system io_out io_in ≝
    25  mk_trans_system … pseudo_is_final execute_1_pseudo_instruction.
     31 mk_trans_system … pseudo_is_final execute_1_pseudo_instruction_trace.
    2632
    2733definition pseudo_ASM_fullexec: fullexec io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.