Changeset 333


Ignore:
Timestamp:
Nov 29, 2010, 4:12:58 PM (9 years ago)
Author:
mulligan
Message:

Work on execute_1 function.

File:
1 edited

Legend:

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

    r331 r333  
    1414      match instr with
    1515        [ ADD addr1 addr2 ⇒
    16             match addr1 return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with
    17               [ ACC_A ⇒ λacc_a: True.
    18                 match addr2 return λx. bool_to_Prop (is_in … [[ register;
    19                                                                 direct;
    20                                                                 indirect;
    21                                                                 data ]] x) → ? with
    22                   [ REGISTER r ⇒ λregister: True.
    23                     let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
    24                                                            (get_arg_8 s false (REGISTER r)) false in
    25                     let cy_flag ≝ get_index … flags Z ? in
    26                     let ac_flag ≝ get_index … flags one ? in
    27                     let ov_flag ≝ get_index … flags two ? in
    28                     let s ≝ set_arg_8 s ACC_A result in
    29                       set_flags s cy_flag (Just Bit ac_flag) ov_flag
    30                   | DIRECT d ⇒ λdirect: True.
    31                     let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
    32                                                            (get_arg_8 s false (DIRECT d)) false in
    33                     let cy_flag ≝ get_index … flags Z ? in
    34                     let ac_flag ≝ get_index … flags one ? in
    35                     let ov_flag ≝ get_index … flags two ? in
    36                     let s ≝ set_arg_8 s ACC_A result in
    37                       set_flags s cy_flag (Just Bit ac_flag) ov_flag
    38                   | INDIRECT i ⇒ λindirect: True.
    39                     let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
    40                                                            (get_arg_8 s false (INDIRECT i)) false in
    41                     let cy_flag ≝ get_index … flags Z ? in
    42                     let ac_flag ≝ get_index … flags one ? in
    43                     let ov_flag ≝ get_index … flags two ? in
    44                     let s ≝ set_arg_8 s ACC_A result in
    45                       set_flags s cy_flag (Just Bit ac_flag) ov_flag
    46                   | DATA d ⇒ λdata: True.
    47                     let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
    48                                                            (get_arg_8 s false (DATA d)) false in
    49                     let cy_flag ≝ get_index … flags Z ? in
    50                     let ac_flag ≝ get_index … flags one ? in
    51                     let ov_flag ≝ get_index … flags two ? in
    52                     let s ≝ set_arg_8 s ACC_A result in
    53                       set_flags s cy_flag (Just Bit ac_flag) ov_flag
    54                   | _ ⇒ λother: False. ?
    55                   ] (subaddressing_modein … addr2)
    56             | _ ⇒ λother: False. ?
    57             ] (subaddressing_modein … addr1)
     16            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
     17                                                   (get_arg_8 s false addr2) false in
     18            let cy_flag ≝ get_index … flags Z ? in
     19            let ac_flag ≝ get_index … flags one ? in
     20            let ov_flag ≝ get_index … flags two ? in
     21            let s ≝ set_arg_8 s ACC_A result in
     22              set_flags s cy_flag (Just Bit ac_flag) ov_flag
    5823        | ADDC addr1 addr2 ⇒
    5924            let old_cy_flag ≝ get_cy_flag s in
    60             match addr1 return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with
     25            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
     26                                                   (get_arg_8 s false addr2) old_cy_flag in
     27            let cy_flag ≝ get_index … flags Z ? in
     28            let ac_flag ≝ get_index … flags one ? in
     29            let ov_flag ≝ get_index … flags two ? in
     30            let s ≝ set_arg_8 s ACC_A result in
     31              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     32        | SUBB addr1 addr2 ⇒
     33            let old_cy_flag ≝ get_cy_flag s in
     34            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
     35                                                   (get_arg_8 s false addr2) old_cy_flag in
     36            let cy_flag ≝ get_index … flags Z ? in
     37            let ac_flag ≝ get_index … flags one ? in
     38            let ov_flag ≝ get_index … flags two ? in
     39            let s ≝ set_arg_8 s ACC_A result in
     40              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     41        | INC addr ⇒
     42            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
     43                                                           register;
     44                                                           direct;
     45                                                           indirect;
     46                                                           dptr ]] x) → ? with
    6147              [ ACC_A ⇒ λacc_a: True.
    62                 match addr2 return λx. bool_to_Prop (is_in … [[ register;
    63                                                                 direct;
    64                                                                 indirect;
    65                                                                 data ]] x) → ? with
    66                   [ REGISTER r ⇒ λregister: True.
    67                     let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
    68                                                            (get_arg_8 s false (REGISTER r)) old_cy_flag in
    69                     let cy_flag ≝ get_index … flags Z ? in
    70                     let ac_flag ≝ get_index … flags one ? in
    71                     let ov_flag ≝ get_index … flags two ? in
    72                     let s ≝ set_arg_8 s ACC_A result in
    73                       set_flags s cy_flag (Just Bit ac_flag) ov_flag
    74                   | DIRECT d ⇒ λdirect: True.
    75                     let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
    76                                                            (get_arg_8 s false (DIRECT d)) old_cy_flag in
    77                     let cy_flag ≝ get_index … flags Z ? in
    78                     let ac_flag ≝ get_index … flags one ? in
    79                     let ov_flag ≝ get_index … flags two ? in
    80                     let s ≝ set_arg_8 s ACC_A result in
    81                       set_flags s cy_flag (Just Bit ac_flag) ov_flag
    82                   | INDIRECT i ⇒ λindirect: True.
    83                     let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
    84                                                            (get_arg_8 s false (INDIRECT i)) old_cy_flag in
    85                     let cy_flag ≝ get_index … flags Z ? in
    86                     let ac_flag ≝ get_index … flags one ? in
    87                     let ov_flag ≝ get_index … flags two ? in
    88                     let s ≝ set_arg_8 s ACC_A result in
    89                       set_flags s cy_flag (Just Bit ac_flag) ov_flag
    90                   | DATA d ⇒ λdata: True.
    91                     let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
    92                                                            (get_arg_8 s false (DATA d)) old_cy_flag in
    93                     let cy_flag ≝ get_index … flags Z ? in
    94                     let ac_flag ≝ get_index … flags one ? in
    95                     let ov_flag ≝ get_index … flags two ? in
    96                     let s ≝ set_arg_8 s ACC_A result in
    97                       set_flags s cy_flag (Just Bit ac_flag) ov_flag
    98                   | _ ⇒ λother: False. ?
    99                   ] (subaddressing_modein … addr2)
    100             | _ ⇒ λother: False. ?
    101             ] (subaddressing_modein … addr1)
     48                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in
     49                  set_arg_8 s ACC_A result
     50              | REGISTER r ⇒ λregister: True.
     51                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in
     52                  set_arg_8 s (REGISTER r) result
     53              | DIRECT d ⇒ λdirect: True.
     54                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in
     55                  set_arg_8 s (DIRECT d) result
     56              | INDIRECT i ⇒ λindirect: True.
     57                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in
     58                  set_arg_8 s (INDIRECT i) result
     59              | DPTR ⇒ λdptr: True.
     60                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in
     61                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in
     62                let s ≝ set_8051_sfr s SFR_DPL bl in
     63                  set_8051_sfr s SFR_DPH bu
     64              | _ ⇒ λother: False. ?
     65              ] (subaddressing_modein … addr)
     66       | DEC addr ⇒
     67           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in
     68             set_arg_8 s addr result
     69        | MUL addr1 addr2 ⇒
     70           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
     71           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
     72           let product ≝ acc_a_nat * acc_b_nat in
     73           let ov_flag ≝ product ≥ two_hundred_and_fifty_six in
     74           let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in
     75           let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in
     76           let s ≝ set_8051_sfr s SFR_ACC_A low in
     77             set_8051_sfr s SFR_ACC_B high
     78        | DIV addr1 addr2 ⇒
     79           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
     80           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
     81             match acc_b_nat with
     82               [ Z ⇒ set_flags s false (Nothing Bit) true
     83               | S o ⇒
     84                 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
     85                 let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in
     86                 let s ≝ set_8051_sfr s SFR_ACC_A q in
     87                 let s ≝ set_8051_sfr s SFR_ACC_B r in
     88                   set_flags s false (Nothing Bit) false
     89               ]
     90(*
     91         DA addr ⇒
     92            match addr return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with
     93              [ ACC_A ⇒ λacc_a: True.
     94                let 〈 acc_nu, acc_nl 〉 ≝
     95              | _ ⇒ λother: False. ?
     96              ] (subaddressing_modein … addr) *)
    10297        | _ ⇒ s
    10398        ]
Note: See TracChangeset for help on using the changeset viewer.