Changeset 928 for src

Timestamp:

Jun 9, 2011, 6:07:29 PM (9 years ago)

Author:

sacerdot

Message:

Technical splitting.

File:

• src/ASM/Interpret.ma (modified) (2 diffs)

src/ASM/Interpret.ma

@@ -513 +513 @@
 qed.
 
-definition execute_1: Status → Status ≝
-  λs: Status.
-    let 〈instr_pc, ticks〉 ≝ fetch (code_memory ? s) (program_counter ? s) in
+definition execute_1_0: Status → instruction × Word × nat → Status ≝
+  λs,instr_pc_ticks.
+    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
     let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
     let s ≝ set_clock ? s (clock ? s + ticks) in
@@ -625 +625 @@
 qed.
 
+definition execute_1: Status → Status ≝
+  λs: Status.
+    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
+     execute_1_0 s instr_pc_ticks.
+
 let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
   match l with