Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (9 years ago)
Author:
mulligan
Message:

Moved over to standard library.

File:
1 edited

Legend:

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

    r439 r465  
    5353
    5454nlemma execute_1_technical:
    55   ∀n,m: Nat.
     55  ∀n,m: nat.
    5656  ∀v: Vector addressing_mode_tag (S n).
    5757  ∀q: Vector addressing_mode_tag (S m).
     
    9494            let ov_flag ≝ get_index' ? two ? flags in
    9595            let s ≝ set_arg_8 s ACC_A result in
    96               set_flags s cy_flag (Just Bit ac_flag) ov_flag
     96              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    9797        | ADDC addr1 addr2 ⇒
    9898            let old_cy_flag ≝ get_cy_flag s in
     
    103103            let ov_flag ≝ get_index' ? two ? flags in
    104104            let s ≝ set_arg_8 s ACC_A result in
    105               set_flags s cy_flag (Just Bit ac_flag) ov_flag
     105              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    106106        | SUBB addr1 addr2 ⇒
    107107            let old_cy_flag ≝ get_cy_flag s in
     
    112112            let ov_flag ≝ get_index' ? two ? flags in
    113113            let s ≝ set_arg_8 s ACC_A result in
    114               set_flags s cy_flag (Just Bit ac_flag) ov_flag
     114              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    115115        | ANL addr ⇒
    116116          match addr with
    117             [ Left l ⇒
     117            [ inl l ⇒
    118118              match l with
    119                 [ Left l' ⇒
     119                [ inl l' ⇒
    120120                  let 〈addr1, addr2〉 ≝ l' in
    121121                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    122122                    set_arg_8 s addr1 and_val
    123                 | Right r ⇒
     123                | right r ⇒
    124124                  let 〈addr1, addr2〉 ≝ r in
    125125                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    126126                    set_arg_8 s addr1 and_val
    127127                ]
    128             | Right r ⇒
     128            | right r ⇒
    129129              let 〈addr1, addr2〉 ≝ r in
    130130              let and_val ≝ conjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
    131                 set_flags s and_val (Nothing ?) (get_ov_flag s)
     131                set_flags s and_val (None ?) (get_ov_flag s)
    132132            ]
    133133        | ORL addr ⇒
    134134          match addr with
    135             [ Left l ⇒
     135            [ inl l ⇒
    136136              match l with
    137                 [ Left l' ⇒
     137                [ inl l' ⇒
    138138                  let 〈addr1, addr2〉 ≝ l' in
    139139                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    140140                    set_arg_8 s addr1 or_val
    141                 | Right r ⇒
     141                | right r ⇒
    142142                  let 〈addr1, addr2〉 ≝ r in
    143143                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    144144                    set_arg_8 s addr1 or_val
    145145                ]
    146             | Right r ⇒
     146            | right r ⇒
    147147              let 〈addr1, addr2〉 ≝ r in
    148148              let or_val ≝ inclusive_disjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
    149                 set_flags s or_val (Nothing ?) (get_ov_flag s)
     149                set_flags s or_val (None ?) (get_ov_flag s)
    150150            ]
    151151        | XRL addr ⇒
    152152          match addr with
    153             [ Left l' ⇒
     153            [ inl l' ⇒
    154154              let 〈addr1, addr2〉 ≝ l' in
    155155              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    156156                set_arg_8 s addr1 xor_val
    157             | Right r ⇒
     157            | right r ⇒
    158158              let 〈addr1, addr2〉 ≝ r in
    159159              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
     
    201201           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
    202202             match acc_b_nat with
    203                [ Z ⇒ set_flags s false (Nothing Bit) true
     203               [ Z ⇒ set_flags s false (None Bit) true
    204204               | S o ⇒
    205205                 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
     
    207207                 let s ≝ set_8051_sfr s SFR_ACC_A q in
    208208                 let s ≝ set_8051_sfr s SFR_ACC_B r in
    209                    set_flags s false (Nothing Bit) false
     209                   set_flags s false (None Bit) false
    210210               ]
    211211        | DA addr ⇒
     
    219219                    let new_acc ≝ nu @@ acc_nl' in
    220220                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
    221                       set_flags s cy_flag (Just ? (get_ac_flag s)) (get_ov_flag s)
     221                      set_flags s cy_flag (Some ? (get_ac_flag s)) (get_ov_flag s)
    222222                  else
    223223                    s
     
    395395                [ RELATIVE r ⇒ λrelative: True.
    396396                  match addr1 with
    397                     [ Left l ⇒
     397                    [ inl l ⇒
    398398                        let 〈addr1, addr2〉 ≝ l in
    399399                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
     
    402402                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    403403                            let s ≝ set_program_counter s new_pc in
    404                               set_flags s new_cy (Nothing ?) (get_ov_flag s)
     404                              set_flags s new_cy (None ?) (get_ov_flag s)
    405405                          else
    406                             (set_flags s new_cy (Nothing ?) (get_ov_flag s))
    407                     | Right r' ⇒
     406                            (set_flags s new_cy (None ?) (get_ov_flag s))
     407                    | right r' ⇒
    408408                        let 〈addr1, addr2〉 ≝ r' in
    409409                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
     
    412412                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    413413                            let s ≝ set_program_counter s new_pc in
    414                               set_flags s new_cy (Nothing ?) (get_ov_flag s)
     414                              set_flags s new_cy (None ?) (get_ov_flag s)
    415415                          else
    416                             (set_flags s new_cy (Nothing ?) (get_ov_flag s))
     416                            (set_flags s new_cy (None ?) (get_ov_flag s))
    417417                    ]
    418418                | _ ⇒ λother: False. ⊥
     
    484484          (* DPM: only copies --- doesn't affect I/O *)
    485485          match addr with
    486             [ Left l ⇒
     486            [ inl l ⇒
    487487              let 〈addr1, addr2〉 ≝ l in
    488488                set_arg_8 s addr1 (get_arg_8 s false addr2)
    489             | Right r ⇒
     489            | right r ⇒
    490490              let 〈addr1, addr2〉 ≝ r in
    491491                set_arg_8 s addr1 (get_arg_8 s false addr2)
     
    493493        | MOV addr ⇒
    494494          match addr with
    495             [ Left l ⇒
     495            [ inl l ⇒
    496496              match l with
    497                 [ Left l' ⇒
     497                [ inl l' ⇒
    498498                  match l' with
    499                     [ Left l'' ⇒
     499                    [ inl l'' ⇒
    500500                      match l'' with
    501                         [ Left l''' ⇒
     501                        [ inl l''' ⇒
    502502                          match l''' with
    503                             [ Left l'''' ⇒
     503                            [ inl l'''' ⇒
    504504                              let 〈addr1, addr2〉 ≝ l'''' in
    505505                                set_arg_8 s addr1 (get_arg_8 s false addr2)
    506                             | Right r'''' ⇒
     506                            | right r'''' ⇒
    507507                              let 〈addr1, addr2〉 ≝ r'''' in
    508508                                set_arg_8 s addr1 (get_arg_8 s false addr2)
    509509                            ]
    510                         | Right r''' ⇒
     510                        | right r''' ⇒
    511511                          let 〈addr1, addr2〉 ≝ r''' in
    512512                            set_arg_8 s addr1 (get_arg_8 s false addr2)
    513513                        ]
    514                     | Right r'' ⇒
     514                    | right r'' ⇒
    515515                      let 〈addr1, addr2〉 ≝ r'' in
    516516                        set_arg_16 s (get_arg_16 s addr2) addr1
    517517                    ]
    518                 | Right r ⇒
     518                | right r ⇒
    519519                  let 〈addr1, addr2〉 ≝ r in
    520520                    set_arg_1 s addr1 (get_arg_1 s addr2 false)
    521521                ]
    522             | Right r ⇒
     522            | right r ⇒
    523523              let 〈addr1, addr2〉 ≝ r in
    524524                set_arg_1 s addr1 (get_arg_1 s addr2 false)
     
    573573nqed.
    574574
    575 nlet rec execute (n: Nat) (s: Status) on n: Status ≝
     575nlet rec execute (n: nat) (s: Status) on n: Status ≝
    576576  match n with
    577577    [ Z ⇒ s
Note: See TracChangeset for help on using the changeset viewer.