Changeset 2062 for src/ASM/Interpret.ma
 Timestamp:
 Jun 13, 2012, 5:00:35 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r2056 r2062 1222 1222 1223 1223 definition execute_1_pseudo_instruction: 1224 (Word → nat × nat) → ∀cm.∀s:PseudoStatus cm.1224 ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < \snd cm → nat × nat) → ∀s:PseudoStatus cm. 1225 1225 nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <\snd cm → 1226 1226 PseudoStatus cm 1227 1227 ≝ 1228 λ ticks_of,cm,s,pc_ok.1228 λcm,ticks_of,s,pc_ok. 1229 1229 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in 1230 let ticks ≝ ticks_of (program_counter … s) in1230 let ticks ≝ ticks_of (program_counter … s) pc_ok in 1231 1231 execute_1_pseudo_instruction0 ticks cm s instr pc. 1232 1232
Note: See TracChangeset
for help on using the changeset viewer.