Changeset 337 for Deliverables


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.

Location:
Deliverables/D4.1/Matita
Files:
3 edited

Legend:

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

    r330 r337  
    2929(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3030
    31 ndefinition get_index
     31ndefinition get_index_bv
    3232  λn: Nat.
    3333  λb: BitVector n.
     
    3838interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
    3939   
    40 ndefinition set_index
     40ndefinition set_index_bv
    4141  λn: Nat.
    4242  λb: BitVector n.
     
    120120  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
    121121   
    122 ndefinition negation
     122ndefinition negation_bv
    123123  λn: Nat.
    124124  λb: BitVector n.
     
    131131(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    132132
    133 ndefinition rotate_left
    134   λm, n: Nat.
     133ndefinition rotate_left_bv
     134  λn, m: Nat.
    135135  λb: BitVector n.
    136136    rotate_left Bool n m b.
    137137
    138 ndefinition rotate_right
    139   λm, n: Nat.
     138ndefinition rotate_right_bv
     139  λn, m: Nat.
    140140  λb: BitVector n.
    141141    rotate_right Bool n m b.
    142142   
    143 ndefinition shift_left
    144   λm, n: Nat.
     143ndefinition shift_left_bv
     144  λn, m: Nat.
    145145  λb: BitVector n.
    146146  λc: Bool.
    147147    shift_left Bool n m b c.
    148148   
    149 ndefinition shift_right
    150   λm, n: Nat.
     149ndefinition shift_right_bv
     150  λn, m: Nat.
    151151  λb: BitVector n.
    152152  λc: Bool.
  • 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    
  • Deliverables/D4.1/Matita/Status.ma

    r331 r337  
    658658  λs: Status.
    659659  λr: BitVector three.
    660     let b ≝ get_index ? r Z ? in
    661     let c ≝ get_index ? r one ? in
    662     let d ≝ get_index ? r two ? in
     660    let b ≝ get_index_bv ? r Z ? in
     661    let c ≝ get_index_bv ? r one ? in
     662    let d ≝ get_index_bv ? r two ? in
    663663    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    664     let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
     664    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_bv four un two ?) (get_index_bv four un three ?) in
    665665    let offset ≝
    666666      if conjunction (negation r1) (negation r0) then
Note: See TracChangeset for help on using the changeset viewer.