Changeset 1969 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 18, 2012, 6:14:01 PM (8 years ago)
Author:
sacerdot
Message:

Some more progress, but now we must prove something on a Russell function
without using Russell: too painful.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1964 r1969  
    882882      program_counter.
    883883
     884definition addr_of_relative ≝
     885 λM,cm. λx:[[relative]]. λs: PreStatus M cm.
     886  match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
     887   [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
     888   | _ ⇒ λabsd. ⊥
     889   ] (subaddressing_modein … x).
     890 @absd
     891qed.
     892
    884893definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
    885894  Σs': Status cm.
     
    894903      match instr return λx. x = instr → Σs:?.? with
    895904      [ RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] …
    896         (λx. λs.
    897         match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    898         [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
    899         | _ ⇒ λabsd. ⊥
    900         ] (subaddressing_modein … x)) instr' s
     905        (addr_of_relative … cm) instr' s
    901906      | MOVC addr1 addr2 ⇒ λinstr_refl.
    902907          let s ≝ set_clock ?? s (ticks + clock … s) in
     
    971976  [1,2,3,4,5,6,7,8:
    972977    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
    973     try // (*CSC: Veeery slow*)
     978    try //
    974979    -s destruct(INSTR_PC) <instr_refl whd
    975980    try (#absurd normalize in absurd; try destruct(absurd) try %) %
Note: See TracChangeset for help on using the changeset viewer.