Changeset 1527 for src/ASM


Ignore:
Timestamp:
Nov 22, 2011, 11:50:15 AM (8 years ago)
Author:
sacerdot
Message:

More on Russell.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1526 r1527  
    130130#M #s #f1 #f2 cases (set_arg_8 M s f1 f2)
    131131#a #E >E //
    132 qed.
     132qed.
     133
     134lemma tech_clocks_le:
     135 ∀M,s.∀t:Σs'. clock M s ≤ clock M s'. clock … s ≤ clock … t.
     136 #M #s * //
     137qed.
    133138
    134139definition execute_1_preinstruction:
     
    533538           let s ≝ add_ticks2 s in
    534539            s
    535         ]. (*67s*)
    536     try assumption (*180s*)
    537     try % (*41s*)
     540        ]. (*14s*)
     541    try assumption (*20s*)
     542    try % (*6s*)
    538543    try (
    539544      @ (execute_1_technical … (subaddressing_modein …))
    540545      @ I
    541     ) (*132s*)
    542  [(*1:/by/,2,3: /by/*)
    543  |4:
    544  |6,7,8,10,11,12,13,14,15: /by/ (*56s*)
    545  |16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*73s*)
    546  |33,35,39,41,43,54,55,56: /by/ (*48s*)
    547  |
     546    ) (*34s*)
     547 [1,2,3: /by/ (*41s*)
     548 |4,6,7,8,10,11,12,13,14,15: /by/ (*6s*)
     549 |16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*9s*)
     550 |33,35,39,41,43,54,55,56: /by/ (*6s*)
     551 |57: <set_args_8_ignores_clock /by/ (*0.5s ??*)
    548552 (* 31,32,34,36,44,48 facili *)
    549  (* 4,5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *)
    550 qed.
    551 
    552 include "ASM/JMCoercions.ma".
     553 (* 5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *)
     554 |*:cases daemon]
     555qed.
    553556
    554557definition execute_1_0: ∀s: Status. instruction × Word × nat → Σs': Status. clock … s ≤ clock … s' ≝
    555   λs,instr_pc_ticks.
     558  λs0,instr_pc_ticks.
    556559    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    557560    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    558     let s ≝ set_program_counter ? s pc in
    559     let s ≝
    560       match instr with
     561    let s ≝ set_program_counter ? s0 pc in
     562      match instr return λ_.Σs': Status. clock … s0 ≤ clock … s' with
    561563      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
    562564        (λx. λs.
     
    565567        | _ ⇒ λabsd. ⊥
    566568        ] (subaddressing_modein … x)) instr s
    567       | _ ⇒ ?
    568       ] in s.
    569       | ACALL addr ⇒
     569     | ACALL addr ⇒ ?(*
    570570          let s ≝ set_clock ? s (ticks + clock ? s) in
    571571          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     
    586586                set_program_counter ? s new_addr
    587587            | _ ⇒ λother: False. ⊥
    588             ] (subaddressing_modein … addr)
     588            ] (subaddressing_modein … addr)*)
    589589        | LCALL addr ⇒
    590590          let s ≝ set_clock ? s (ticks + clock ? s) in
     
    660660            | _ ⇒ λother: False. ⊥
    661661            ] (subaddressing_modein … addr)
    662       ]
    663     in
    664       s.
     662      ].
    665663    try assumption
    666664    try (
Note: See TracChangeset for help on using the changeset viewer.