Ignore:
Timestamp:
Nov 30, 2010, 12:26:45 PM (9 years ago)
Author:
mulligan
Message:

Changes to execute_1 file. Changes to get everything type checking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Interpret.ma

    r334 r337  
    107107              else
    108108                s
    109 (*
    110         | ANL addr1 addr2 ⇒
    111           match addr1 return λx. bool_to_Prop (is_in … [[ acc_a;
    112                                                           direct;
    113                                                           carry ]] x) → ? with
    114             [ ACC_A ⇒ λacc_a: True. ?
    115             | DIRECT d ⇒ λdirect: True. ?
    116             | CARRY ⇒ λcarry: True. ?
     109        | CLR addr ⇒
     110          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
     111            [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero eight)
     112            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
     113            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
    117114            | _ ⇒ λother: False. ?
    118             ] (subaddressing_modein … addr1) *)
     115            ] (subaddressing_modein … addr)
     116        | CPL addr ⇒
     117          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
     118            [ ACC_A ⇒ λacc_a: True.
     119                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     120                let new_acc ≝ negation_bv ? old_acc in
     121                  set_8051_sfr s SFR_ACC_A new_acc
     122            | CARRY ⇒ λcarry: True.
     123                let old_cy_flag ≝ get_arg_1 s CARRY true in
     124                let new_cy_flag ≝ negation old_cy_flag in
     125                  set_arg_1 s CARRY new_cy_flag
     126            | BIT_ADDR b ⇒ λbit_addr: True.
     127                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
     128                let new_bit ≝ negation old_bit in
     129                  set_arg_1 s (BIT_ADDR b) new_bit
     130            | _ ⇒ λother: False. ?
     131            ] (subaddressing_modein … addr)
     132        | SETB b ⇒ set_arg_1 s b false
     133        | RL _ ⇒ (* DPM: always ACC_A *)
     134            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     135            let new_acc ≝ rotate_left_bv ? one old_acc in
     136              set_8051_sfr s SFR_ACC_A new_acc
     137        | RR _ ⇒ (* DPM: always ACC_A *)
     138            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     139            let new_acc ≝ rotate_right_bv ? one old_acc in
     140              set_8051_sfr s SFR_ACC_A new_acc
     141        | RLC _ ⇒ (* DPM: always ACC_A *)
     142            let old_cy_flag ≝ get_cy_flag s in
     143            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     144            let new_cy_flag ≝ get_index_bv ? old_acc Z ? in
     145            let new_acc ≝ shift_left_bv eight one old_acc old_cy_flag in
     146            let s ≝ set_arg_1 s CARRY new_cy_flag in
     147              set_8051_sfr s SFR_ACC_A new_acc
     148        | RRC _ ⇒ (* DPM: always ACC_A *)
     149            let old_cy_flag ≝ get_cy_flag s in
     150            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     151            let new_cy_flag ≝ get_index_bv ? old_acc seven ? in
     152            let new_acc ≝ shift_right_bv eight one old_acc old_cy_flag in
     153            let s ≝ set_arg_1 s CARRY new_cy_flag in
     154              set_8051_sfr s SFR_ACC_A new_acc
     155        | SWAP _ ⇒ (* DPM: always ACC_A *)
     156            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     157            let 〈nu,nl〉 ≝ split ? four four old_acc in
     158            let new_acc ≝ nl @@ nu in
     159              set_8051_sfr s SFR_ACC_A new_acc
     160        | PUSH addr ⇒
     161            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
     162              [ DIRECT d ⇒ λdirect: True.
     163                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
     164                let s ≝ set_8051_sfr s SFR_SP new_sp in
     165                  write_at_stack_pointer s d
     166              | _ ⇒ λother: False. ?
     167              ] (subaddressing_modein … addr)
     168        | POP addr ⇒
     169            let contents ≝ read_at_stack_pointer s in
     170            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
     171            let s ≝ set_8051_sfr s SFR_SP new_sp in
     172              set_arg_8 s addr contents
     173        | XCH addr1 addr2 ⇒
     174            let old_addr ≝ get_arg_8 s false addr2 in
     175            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
     176            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
     177              set_arg_8 s addr2 old_acc
     178        | NOP ⇒ s
    119179        | _ ⇒ s
    120180        ]
    121181    in
    122182      s.
    123    
    124    
Note: See TracChangeset for help on using the changeset viewer.