Changeset 1037 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jun 23, 2011, 2:56:20 AM (8 years ago)
Author:
sacerdot
Message:

Main theorem: comments are working again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r985 r1037  
    651651     execute_1_0 s instr_pc_ticks.
    652652
    653 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
    654   λticks_of.
    655   λs.
    656   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
    657   let ticks ≝ ticks_of (program_counter ? s) in
     653definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
     654  λticks,s,instr,pc.
    658655  let s ≝ set_program_counter ? s pc in
    659656  let s ≝
     
    690687qed.
    691688
     689definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
     690  λticks_of,s.
     691  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
     692  let ticks ≝ ticks_of (program_counter ? s) in
     693   execute_1_pseudo_instruction0 ticks s instr pc.
     694
    692695let rec execute (n: nat) (s: Status) on n: Status ≝
    693696  match n with
Note: See TracChangeset for help on using the changeset viewer.