Changeset 265


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

Test commit.

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

Legend:

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

    r259 r265  
    8585}.
    8686
    87 alias id "replicate" = "cic:/matita/Cerco/Vector/replicate.fix(0,1,1)".
     87ncheck special_function_registers_8051.
     88
     89naxiom sfr8051_index_nineteen:
     90  ∀i: SFR8051.
     91    sfr_8051_index i < nineteen.
     92   
     93naxiom sfr8052_index_five:
     94  ∀i: SFR8052.
     95    sfr_8052_index i < five.
     96
     97ndefinition get_8051_sfr ≝
     98  λs: Status.
     99  λi: SFR8051.
     100    let sfr ≝ special_function_registers_8051 s in
     101    let index ≝ sfr_8051_index i in
     102      get_index … sfr index ?.
     103    napply (sfr8051_index_nineteen i).
     104nqed.
     105
     106ndefinition get_8052_sfr ≝
     107  λs: Status.
     108  λi: SFR8052.
     109    let sfr ≝ special_function_registers_8052 s in
     110    let index ≝ sfr_8052_index i in
     111      get_index … sfr index ?.
     112    napply (sfr8052_index_five i).
     113nqed.
    88114
    89115ndefinition set_8051_sfr ≝
     
    91117  λi: SFR8051.
    92118  λb: Byte.
    93     let index ≝ sfr_8051_status i in
    94     let
     119    let index ≝ sfr_8051_index i in
     120    let old_code_memory ≝ code_memory s in
     121    let old_low_internal_ram ≝ low_internal_ram s in
     122    let old_high_internal_ram ≝ high_internal_ram s in
     123    let old_external_ram ≝ external_ram s in
     124    let old_program_counter ≝ program_counter s in
     125    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     126    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     127    let new_special_function_registers_8051 ≝
     128      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
     129      mk_Status old_code_memory
     130                old_low_internal_ram
     131                old_high_internal_ram
     132                old_external_ram
     133                old_program_counter
     134                new_special_function_registers_8051
     135                old_special_function_registers_8052.
     136    napply (sfr8051_index_nineteen i).
     137nqed.
     138
     139ndefinition set_8052_sfr ≝
     140  λs: Status.
     141  λi: SFR8052.
     142  λb: Byte.
     143    let index ≝ sfr_8052_index i in
     144    let old_code_memory ≝ code_memory s in
     145    let old_low_internal_ram ≝ low_internal_ram s in
     146    let old_high_internal_ram ≝ high_internal_ram s in
     147    let old_external_ram ≝ external_ram s in
     148    let old_program_counter ≝ program_counter s in
     149    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     150    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     151    let new_special_function_registers_8052 ≝
     152      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
     153      mk_Status old_code_memory
     154                old_low_internal_ram
     155                old_high_internal_ram
     156                old_external_ram
     157                old_program_counter
     158                old_special_function_registers_8051
     159                new_special_function_registers_8052.
     160    napply (sfr8052_index_five i).
     161nqed.
     162
     163ndefinition set_program_counter ≝
     164  λs: Status.
     165  λi: SFR8052.
     166  λw: Word.
     167    let index ≝ sfr_8052_index i in
     168    let old_code_memory ≝ code_memory s in
     169    let old_low_internal_ram ≝ low_internal_ram s in
     170    let old_high_internal_ram ≝ high_internal_ram s in
     171    let old_external_ram ≝ external_ram s in
     172    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     173    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     174      mk_Status old_code_memory
     175                old_low_internal_ram
     176                old_high_internal_ram
     177                old_external_ram
     178                w
     179                old_special_function_registers_8051
     180                old_special_function_registers_8052.
     181               
     182ndefinition set_code_memory ≝
     183  λs: Status.
     184  λi: SFR8052.
     185  λr: BitVectorTrie Byte sixteen.
     186    let index ≝ sfr_8052_index i in
     187    let old_low_internal_ram ≝ low_internal_ram s in
     188    let old_high_internal_ram ≝ high_internal_ram s in
     189    let old_external_ram ≝ external_ram s in
     190    let old_program_counter ≝ program_counter s in
     191    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     192    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     193      mk_Status r
     194                old_low_internal_ram
     195                old_high_internal_ram
     196                old_external_ram
     197                old_program_counter
     198                old_special_function_registers_8051
     199                old_special_function_registers_8052.
     200               
     201ndefinition set_low_internal_ram ≝
     202  λs: Status.
     203  λi: SFR8052.
     204  λr: BitVectorTrie Byte seven.
     205    let index ≝ sfr_8052_index i in
     206    let old_code_memory ≝ code_memory s in
     207    let old_high_internal_ram ≝ high_internal_ram s in
     208    let old_external_ram ≝ external_ram s in
     209    let old_program_counter ≝ program_counter s in
     210    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     211    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     212      mk_Status old_code_memory
     213                r
     214                old_high_internal_ram
     215                old_external_ram
     216                old_program_counter
     217                old_special_function_registers_8051
     218                old_special_function_registers_8052.
     219               
     220ndefinition get_cy_flag ≝
     221  λs: Status.
     222    let sfr ≝ special_function_registers_8051 s in
     223    let psw ≝ get_index … (get_8051_index SFR_PSW) s ? in
     224      get_index … Z psw ?.
     225               
     226ndefinition set_high_internal_ram ≝
     227  λs: Status.
     228  λi: SFR8052.
     229  λr: BitVectorTrie Byte seven.
     230    let index ≝ sfr_8052_index i in
     231    let old_code_memory ≝ code_memory s in
     232    let old_low_internal_ram ≝ low_internal_ram s in
     233    let old_high_internal_ram ≝ high_internal_ram s in
     234    let old_external_ram ≝ external_ram s in
     235    let old_program_counter ≝ program_counter s in
     236    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     237    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     238      mk_Status old_code_memory
     239                old_low_internal_ram
     240                r
     241                old_external_ram
     242                old_program_counter
     243                old_special_function_registers_8051
     244                old_special_function_registers_8052.
    95245
    96246ndefinition initialise_status ≝
  • Deliverables/D4.1/Matita/Nat.ma

    r261 r265  
    5757(* Add Boolean versions.                                                      *)
    5858ndefinition less_than_p ≝
    59   λm, n: Nat.
    60     m ≤ n ∧ ¬(m = n).
     59  λm: Nat.
     60  λn: Nat.
     61    less_than_or_equal_p (S m) n.
    6162   
    6263notation "hvbox(n break < m)"
  • Deliverables/D4.1/Matita/Vector.ma

    r262 r265  
    4040naxiom succ_less_than_injective:
    4141  ∀m, n: Nat.
    42     S m < S n → m < n.
     42    less_than_p (S m) (S n) → m < n.
    4343   
    4444naxiom nothing_less_than_Z:
Note: See TracChangeset for help on using the changeset viewer.