Changeset 470


Ignore:
Timestamp:
Jan 21, 2011, 10:18:27 AM (7 years ago)
Author:
mulligan
Message:

Finished moving development over to standard library.

File:
1 edited

Legend:

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

    r466 r470  
    333333              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    334334                [ RELATIVE r ⇒ λrel: True.
    335                   if negation (get_cy_flag s) then
     335                  if ¬(get_cy_flag s) then
    336336                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    337337                      set_program_counter s new_pc
     
    353353              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    354354                [ RELATIVE r ⇒ λrel: True.
    355                   if negation (get_arg_1 s addr1 false) then
     355                  if ¬(get_arg_1 s addr1 false) then
    356356                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    357357                      set_program_counter s new_pc
     
    384384              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    385385                [ RELATIVE r ⇒ λrel: True.
    386                     if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
     386                    if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
    387387                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    388388                        set_program_counter s new_pc
     
    397397                    [ inl l ⇒
    398398                        let 〈addr1, addr2〉 ≝ l in
    399                         let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
     399                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
    400400                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
    401                           if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
     401                          if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
    402402                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    403403                            let s ≝ set_program_counter s new_pc in
     
    407407                    | inr r' ⇒
    408408                        let 〈addr1, addr2〉 ≝ r' in
    409                         let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
     409                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
    410410                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
    411                           if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
     411                          if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
    412412                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    413413                            let s ≝ set_program_counter s new_pc in
     
    423423                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
    424424                    let s ≝ set_arg_8 s addr1 result in
    425                       if negation (eq_bv ? result (zero 8)) then
     425                      if ¬(eq_bv ? result (zero 8)) then
    426426                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    427427                          set_program_counter s new_pc
Note: See TracChangeset for help on using the changeset viewer.