Ignore:
Timestamp:
Nov 29, 2010, 5:34:18 PM (9 years ago)
Author:
mulligan
Message:

More added.

File:
1 edited

Legend:

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

    r333 r334  
    1 include "Status.ma".
    2 include "Fetch.ma".
     1include "Status.ma". 
     2(* include "Fetch.ma". *)
    33include "Cartesian.ma".
    44include "Arithmetic.ma".
    55include "List.ma".
     6
     7naxiom fetch: BitVectorTrie Byte sixteen → Word → (preinstruction [[relative]]) × Word × Nat.
     8
     9alias id "inclusive_disjunction" = "cic:/matita/ng/Bool/inclusive_disjunction.fix(0,0,1)".
    610
    711ndefinition execute_1: Status → Status ≝
     
    8892                   set_flags s false (Nothing Bit) false
    8993               ]
     94        | DA addr ⇒
     95            let 〈 acc_nu, acc_nl 〉 ≝ split ? four four (get_8051_sfr s SFR_ACC_A) in
     96              if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
     97                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
     98                let cy_flag ≝ get_index ? flags Z ? in
     99                let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
     100                  if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
     101                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat four six) in
     102                    let new_acc ≝ nu @@ acc_nl' in
     103                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
     104                      set_flags s cy_flag (Just ? (get_ac_flag s)) (get_ov_flag s)
     105                  else
     106                    s
     107              else
     108                s
    90109(*
    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) *)
     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. ?
     117            | _ ⇒ λother: False. ?
     118            ] (subaddressing_modein … addr1) *)
    97119        | _ ⇒ s
    98120        ]
Note: See TracChangeset for help on using the changeset viewer.