Changeset 2212 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jul 18, 2012, 5:30:26 PM (7 years ago)
Author:
mulligan
Message:

More work on the INC case

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2160 r2212  
    159159            ]
    160160        | INC addr ⇒ λinstr_refl.
    161             match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with
     161            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → ? with
    162162              [ ACC_A ⇒ λacc_a: True.
    163163                let s' ≝ add_ticks1 s in
     
    231231                s
    232232        | CLR addr ⇒ λinstr_refl.
    233           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
     233          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    234234            [ ACC_A ⇒ λacc_a: True.
    235235              let s ≝ add_ticks1 s in
     
    244244            ] (subaddressing_modein … addr)
    245245        | CPL addr ⇒ λinstr_refl.
    246           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
     246          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    247247            [ ACC_A ⇒ λacc_a: True.
    248248                let s ≝ add_ticks1 s in
     
    298298              set_8051_sfr … s SFR_ACC_A new_acc
    299299        | PUSH addr ⇒ λinstr_refl.
    300             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
     300            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
    301301              [ DIRECT d ⇒ λdirect: True.
    302302                let s ≝ add_ticks1 s in
Note: See TracChangeset for help on using the changeset viewer.