Changeset 2062 for src/ASM/Interpret.ma
- Timestamp:
- Jun 13, 2012, 5:00:35 PM (9 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.