Changeset 334 for Deliverables


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

More added.

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

Legend:

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

    r281 r334  
    2929    | false ⇒ c
    3030    ].
     31   
     32ncheck inclusive_disjunction.
    3133
    3234nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝
  • 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        ]
  • Deliverables/D4.1/Matita/depends

    r332 r334  
     1Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
     2Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    13Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    3 Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
    44BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    55Cartesian.ma Universes.ma
     6Universes.ma
    67Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    78Either.ma Bool.ma Maybe.ma Universes.ma
    8 Universes.ma
    99ASM.ma BitVectorTrie.ma Either.ma String.ma
    10 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1110Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1211Char.ma Universes.ma
     12Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1313Connectives.ma Plogic/equality.ma
    1414Bool.ma Universes.ma
    1515Assembly.ma ASM.ma
    1616List.ma Bool.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
     17Interpret.ma Arithmetic.ma Cartesian.ma List.ma Status.ma
    1718Util.ma Nat.ma
    18 Interpret.ma Arithmetic.ma Cartesian.ma Fetch.ma List.ma Status.ma
     19Compare.ma Universes.ma
    1920BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    20 Compare.ma Universes.ma
    2121String.ma Char.ma List.ma
    2222Plogic/equality.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.