Changeset 286


Ignore:
Timestamp:
Nov 25, 2010, 11:18:27 AM (9 years ago)
Author:
mulligan
Message:

Added bit address lookup for registers.

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

Legend:

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

    r281 r286  
    2727ndefinition eighteen ≝ nine + nine.
    2828ndefinition nineteen ≝ ten + nine.
     29ndefinition twenty_four ≝ sixteen + eight.
    2930ndefinition one_hundred ≝ ten * ten.
    3031ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
  • Deliverables/D4.1/Matita/Status.ma

    r285 r286  
    567567      ncases not_implemented.
    568568nqed.
     569
     570ndefinition bit_address_of_register ≝
     571  λs: Status.
     572  λb, c, d: Bit.
     573    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
     574    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
     575    let offset ≝
     576      if conjunction (negation r1) (negation r0) then
     577        Z
     578      else if conjunction (negation r1) r0 then
     579        eight
     580      else if conjunction r1 r0 then
     581        twenty_four
     582      else
     583        sixteen
     584    in
     585      bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
     586    nnormalize.
     587    nrepeat (napply less_than_or_equal_monotone).
     588    napply less_than_or_equal_zero.
     589    nrepeat (napply less_than_or_equal_monotone).
     590    napply less_than_or_equal_zero.
     591nqed.
Note: See TracChangeset for help on using the changeset viewer.