Changeset 267


Ignore:
Timestamp:
Nov 23, 2010, 5:42:20 PM (9 years ago)
Author:
mulligan
Message:

Renamed Interpret to Status.

File:
1 moved

Legend:

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

    r266 r267  
    8585}.
    8686
    87 ncheck special_function_registers_8051.
    88 
    8987naxiom sfr8051_index_nineteen:
    9088  ∀i: SFR8051.
     
    218216                old_special_function_registers_8052.
    219217               
     218naxiom less_than_or_equal_monotone:
     219  ∀m, n: Nat.
     220    m ≤ n → S m ≤ S n.
     221   
     222alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
     223               
    220224ndefinition get_cy_flag ≝
    221225  λs: Status.
    222226    let sfr ≝ special_function_registers_8051 s in
    223     let psw ≝ get_index … (sfr_8051_index SFR_PSW) s ? in
    224       get_index … Z psw ?.
     227    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     228      get_index Bool eight psw Z ?.
     229    nnormalize.
     230    napply (less_than_or_equal_monotone ? ?).
     231    napply (less_than_or_equal_zero).
     232    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     233    napply (less_than_or_equal_zero).
     234nqed.
     235
     236ndefinition get_ac_flag ≝
     237  λs: Status.
     238    let sfr ≝ special_function_registers_8051 s in
     239    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     240      get_index Bool eight psw (S Z) ?.
     241    nnormalize.
     242    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     243    napply (less_than_or_equal_zero).
     244    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     245    napply (less_than_or_equal_zero).
     246nqed.
     247
     248ndefinition get_fo_flag ≝
     249  λs: Status.
     250    let sfr ≝ special_function_registers_8051 s in
     251    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     252      get_index Bool eight psw two ?.
     253    nnormalize.
     254    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     255    napply (less_than_or_equal_zero).
     256    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     257    napply (less_than_or_equal_zero).
     258nqed.
     259
     260ndefinition get_rs1_flag ≝
     261  λs: Status.
     262    let sfr ≝ special_function_registers_8051 s in
     263    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     264      get_index Bool eight psw three ?.
     265    nnormalize.
     266    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     267    napply (less_than_or_equal_zero).
     268    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     269    napply (less_than_or_equal_zero).
     270nqed.
     271
     272ndefinition get_rs0_flag ≝
     273  λs: Status.
     274    let sfr ≝ special_function_registers_8051 s in
     275    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     276      get_index Bool eight psw four ?.
     277    nnormalize.
     278    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     279    napply (less_than_or_equal_zero).
     280    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     281    napply (less_than_or_equal_zero).
     282nqed.
     283
     284ndefinition get_ov_flag ≝
     285  λs: Status.
     286    let sfr ≝ special_function_registers_8051 s in
     287    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     288      get_index Bool eight psw five ?.
     289    nnormalize.
     290    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     291    napply (less_than_or_equal_zero).
     292    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     293    napply (less_than_or_equal_zero).
     294nqed.
     295
     296ndefinition get_ud_flag ≝
     297  λs: Status.
     298    let sfr ≝ special_function_registers_8051 s in
     299    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     300      get_index Bool eight psw six ?.
     301    nnormalize.
     302    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     303    napply (less_than_or_equal_zero).
     304    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     305    napply (less_than_or_equal_zero).
     306nqed.
     307
     308ndefinition get_p_flag ≝
     309  λs: Status.
     310    let sfr ≝ special_function_registers_8051 s in
     311    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     312      get_index Bool eight psw seven ?.
     313    nnormalize.
     314    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     315    napply (less_than_or_equal_zero).
     316    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     317    napply (less_than_or_equal_zero).
     318nqed.
    225319               
    226320ndefinition set_high_internal_ram ≝
Note: See TracChangeset for help on using the changeset viewer.